refactor(data/fintype/basic): move fin_choice to a new file (#18337)

There is a refactor in the works for these definitions; it will be easier to review and port the refactor if we move this all to a new file first and just forward-port the deletion.

src/data/fintype/basic.lean

@@ -793,73 +793,6 @@ lemma mem_image_univ_iff_mem_range
   b ∈ univ.image f ↔ b ∈ set.range f :=
 by simp
 
-/-- An auxiliary function for `quotient.fin_choice`.  Given a
-collection of setoids indexed by a type `ι`, a (finite) list `l` of
-indices, and a function that for each `i ∈ l` gives a term of the
-corresponding quotient type, then there is a corresponding term in the
-quotient of the product of the setoids indexed by `l`. -/
-def quotient.fin_choice_aux {ι : Type*} [decidable_eq ι]
-  {α : ι → Type*} [S : ∀ i, setoid (α i)] :
-  Π (l : list ι), (Π i ∈ l, quotient (S i)) → @quotient (Π i ∈ l, α i) (by apply_instance)
-| []       f := ⟦λ i, false.elim⟧
-| (i :: l) f := begin
-  refine quotient.lift_on₂ (f i (list.mem_cons_self _ _))
-    (quotient.fin_choice_aux l (λ j h, f j (list.mem_cons_of_mem _ h)))
-    _ _,
-  exact λ a l, ⟦λ j h,
-    if e : j = i then by rw e; exact a else
-    l _ (h.resolve_left e)⟧,
-  refine λ a₁ l₁ a₂ l₂ h₁ h₂, quotient.sound (λ j h, _),
-  by_cases e : j = i; simp [e],
-  { subst j, exact h₁ },
-  { exact h₂ _ _ }
-end
-
-theorem quotient.fin_choice_aux_eq {ι : Type*} [decidable_eq ι]
-  {α : ι → Type*} [S : ∀ i, setoid (α i)] :
-  ∀ (l : list ι) (f : Π i ∈ l, α i), quotient.fin_choice_aux l (λ i h, ⟦f i h⟧) = ⟦f⟧
-| []       f := quotient.sound (λ i h, h.elim)
-| (i :: l) f := begin
-  simp [quotient.fin_choice_aux, quotient.fin_choice_aux_eq l],
-  refine quotient.sound (λ j h, _),
-  by_cases e : j = i; simp [e],
-  subst j, refl
-end
-
-/-- Given a collection of setoids indexed by a fintype `ι` and a
-function that for each `i : ι` gives a term of the corresponding
-quotient type, then there is corresponding term in the quotient of the
-product of the setoids. -/
-def quotient.fin_choice {ι : Type*} [decidable_eq ι] [fintype ι]
-  {α : ι → Type*} [S : ∀ i, setoid (α i)]
-  (f : Π i, quotient (S i)) : @quotient (Π i, α i) (by apply_instance) :=
-quotient.lift_on (@quotient.rec_on _ _ (λ l : multiset ι,
-    @quotient (Π i ∈ l, α i) (by apply_instance))
-    finset.univ.1
-    (λ l, quotient.fin_choice_aux l (λ i _, f i))
-    (λ a b h, begin
-      have := λ a, quotient.fin_choice_aux_eq a (λ i h, quotient.out (f i)),
-      simp [quotient.out_eq] at this,
-      simp [this],
-      let g := λ a:multiset ι, ⟦λ (i : ι) (h : i ∈ a), quotient.out (f i)⟧,
-      refine eq_of_heq ((eq_rec_heq _ _).trans (_ : g a == g b)),
-      congr' 1, exact quotient.sound h,
-    end))
-  (λ f, ⟦λ i, f i (finset.mem_univ _)⟧)
-  (λ a b h, quotient.sound $ λ i, h _ _)
-
-theorem quotient.fin_choice_eq {ι : Type*} [decidable_eq ι] [fintype ι]
-  {α : ι → Type*} [∀ i, setoid (α i)]
-  (f : Π i, α i) : quotient.fin_choice (λ i, ⟦f i⟧) = ⟦f⟧ :=
-begin
-  let q, swap, change quotient.lift_on q _ _ = _,
-  have : q = ⟦λ i h, f i⟧,
-  { dsimp only [q],
-    exact quotient.induction_on
-      (@finset.univ ι _).1 (λ l, quotient.fin_choice_aux_eq _ _) },
-  simp [this], exact setoid.refl _
-end
-
 namespace fintype
 
 section choose

src/data/fintype/quotient.lean

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2018 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import data.fintype.basic
+
+/-!
+# Quotients of families indexed by a finite type
+
+This file provides `quotient.fin_choice`, a mechanism to go from a finite family of quotients
+to a quotient of finite families.
+
+## Main definitions
+
+* `quotient.fin_choice`
+
+-/
+
+/-- An auxiliary function for `quotient.fin_choice`.  Given a
+collection of setoids indexed by a type `ι`, a (finite) list `l` of
+indices, and a function that for each `i ∈ l` gives a term of the
+corresponding quotient type, then there is a corresponding term in the
+quotient of the product of the setoids indexed by `l`. -/
+def quotient.fin_choice_aux {ι : Type*} [decidable_eq ι]
+  {α : ι → Type*} [S : ∀ i, setoid (α i)] :
+  Π (l : list ι), (Π i ∈ l, quotient (S i)) → @quotient (Π i ∈ l, α i) (by apply_instance)
+| []       f := ⟦λ i, false.elim⟧
+| (i :: l) f := begin
+  refine quotient.lift_on₂ (f i (list.mem_cons_self _ _))
+    (quotient.fin_choice_aux l (λ j h, f j (list.mem_cons_of_mem _ h)))
+    _ _,
+  exact λ a l, ⟦λ j h,
+    if e : j = i then by rw e; exact a else
+    l _ (h.resolve_left e)⟧,
+  refine λ a₁ l₁ a₂ l₂ h₁ h₂, quotient.sound (λ j h, _),
+  by_cases e : j = i; simp [e],
+  { subst j, exact h₁ },
+  { exact h₂ _ _ }
+end
+
+theorem quotient.fin_choice_aux_eq {ι : Type*} [decidable_eq ι]
+  {α : ι → Type*} [S : ∀ i, setoid (α i)] :
+  ∀ (l : list ι) (f : Π i ∈ l, α i), quotient.fin_choice_aux l (λ i h, ⟦f i h⟧) = ⟦f⟧
+| []       f := quotient.sound (λ i h, h.elim)
+| (i :: l) f := begin
+  simp [quotient.fin_choice_aux, quotient.fin_choice_aux_eq l],
+  refine quotient.sound (λ j h, _),
+  by_cases e : j = i; simp [e],
+  subst j, refl
+end
+
+/-- Given a collection of setoids indexed by a fintype `ι` and a
+function that for each `i : ι` gives a term of the corresponding
+quotient type, then there is corresponding term in the quotient of the
+product of the setoids. -/
+def quotient.fin_choice {ι : Type*} [decidable_eq ι] [fintype ι]
+  {α : ι → Type*} [S : ∀ i, setoid (α i)]
+  (f : Π i, quotient (S i)) : @quotient (Π i, α i) (by apply_instance) :=
+quotient.lift_on (@quotient.rec_on _ _ (λ l : multiset ι,
+    @quotient (Π i ∈ l, α i) (by apply_instance))
+    finset.univ.1
+    (λ l, quotient.fin_choice_aux l (λ i _, f i))
+    (λ a b h, begin
+      have := λ a, quotient.fin_choice_aux_eq a (λ i h, quotient.out (f i)),
+      simp [quotient.out_eq] at this,
+      simp [this],
+      let g := λ a:multiset ι, ⟦λ (i : ι) (h : i ∈ a), quotient.out (f i)⟧,
+      refine eq_of_heq ((eq_rec_heq _ _).trans (_ : g a == g b)),
+      congr' 1, exact quotient.sound h,
+    end))
+  (λ f, ⟦λ i, f i (finset.mem_univ _)⟧)
+  (λ a b h, quotient.sound $ λ i, h _ _)
+
+theorem quotient.fin_choice_eq {ι : Type*} [decidable_eq ι] [fintype ι]
+  {α : ι → Type*} [∀ i, setoid (α i)]
+  (f : Π i, α i) : quotient.fin_choice (λ i, ⟦f i⟧) = ⟦f⟧ :=
+begin
+  let q, swap, change quotient.lift_on q _ _ = _,
+  have : q = ⟦λ i h, f i⟧,
+  { dsimp only [q],
+    exact quotient.induction_on
+      (@finset.univ ι _).1 (λ l, quotient.fin_choice_aux_eq _ _) },
+  simp [this], exact setoid.refl _
+end

src/model_theory/quotients.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
-import data.fintype.basic
+import data.fintype.quotient
 import model_theory.semantics
 
 /-!