feat: quotient lift on a finite family (#5576)

In the future it may be used to prove that `ZFSet` is a model of ZF set theory without using `Classical.choice`. Specifically, it will be used to prove that all first-order formulas of `ZFSet` are definable.

Comparing to `(finChoice q).liftOn f`, `finLiftOn q f` asks users to provide a proof of `(∀ i, a i ≈ b i) → f a = f b` instead of `a ≈ b → f a = f b`, which is more readable and easier to rewrite. It also makes it easier for users to discover and use relevant APIs.



Co-authored-by: negiizhao <egresf@gmail.com>

Author: astrainfinita

Mathlib/Data/Fintype/Quotient.lean

@@ -1,90 +1,239 @@
 /-
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
+Authors: Mario Carneiro, Yuyang Zhao
 -/
+import Mathlib.Data.List.Pi
 import Mathlib.Data.Fintype.Basic
 
 /-!
 # Quotients of families indexed by a finite type
 
-This file provides `Quotient.finChoice`, a mechanism to go from a finite family of quotients
-to a quotient of finite families.
+This file proves some basic facts and defines lifting and recursion principle for quotients indexed
+by a finite type.
 
 ## Main definitions
 
-* `Quotient.finChoice`
+* `Quotient.finChoice`: Given a function `f : Π i, Quotient (S i)` on a fintype `ι`, returns the
+  class of functions `Π i, α i` sending each `i` to an element of the class `f i`.
+* `Quotient.finChoiceEquiv`: A finite family of quotients is equivalent to a quotient of
+  finite families.
+* `Quotient.finLiftOn`: Given a fintype `ι`. A function on `Π i, α i` which respects
+  setoid `S i` for each `i` can be lifted to a function on `Π i, Quotient (S i)`.
+* `Quotient.finRecOn`: Recursion principle for quotients indexed by a finite type. It is the
+  dependent version of `Quotient.finLiftOn`.
 
 -/
 
 
-/-- An auxiliary function for `Quotient.finChoice`.  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.finChoiceAux {ι : Type*} [DecidableEq ι] {α : ι → Type*} [S : ∀ i, Setoid (α i)] :
-    ∀ l : List ι, (∀ i ∈ l, Quotient (S i)) → @Quotient (∀ i ∈ l, α i) (by infer_instance)
-  | [], _ => ⟦fun _ h => nomatch List.not_mem_nil _ h⟧
-  | i :: l, f => by
-    refine Quotient.liftOn₂ (f i (List.mem_cons_self _ _))
-        (Quotient.finChoiceAux l fun j h => f j (List.mem_cons_of_mem _ h)) ?_ ?_
-    · exact fun a l => ⟦fun j h =>
-        if e : j = i then by rw [e]; exact a else l _ ((List.mem_cons.1 h).resolve_left e)⟧
-    refine fun a₁ l₁ a₂ l₂ h₁ h₂ => Quotient.sound fun j h => ?_
-    by_cases e : j = i
-    · simp [e]; subst j
-      exact h₁
-    · simpa [e] using h₂ _ _
-
-theorem Quotient.finChoiceAux_eq {ι : Type*} [DecidableEq ι] {α : ι → Type*}
-    [S : ∀ i, Setoid (α i)] :
-    ∀ (l : List ι) (f : ∀ i ∈ l, α i), (Quotient.finChoiceAux l fun i h => ⟦f i h⟧) = ⟦f⟧
-  | [], _ => Quotient.sound fun _ h => nomatch List.not_mem_nil _ h
-  | i :: l, f => by
-    simp only [finChoiceAux, Quotient.finChoiceAux_eq l, eq_mpr_eq_cast, lift_mk]
-    refine Quotient.sound fun j h => ?_
-    by_cases e : j = i <;> simp [e] <;> try exact Setoid.refl _
-    subst j; exact Setoid.refl _
-
-/-- 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.finChoice {ι : Type*} [DecidableEq ι] [Fintype ι] {α : ι → Type*}
-    [S : ∀ i, Setoid (α i)] (f : ∀ i, Quotient (S i)) : @Quotient (∀ i, α i) (by infer_instance) :=
-  Quotient.liftOn
-    (@Quotient.recOn _ _ (fun l : Multiset ι => @Quotient (∀ i ∈ l, α i) (by infer_instance))
-      Finset.univ.1 (fun l => Quotient.finChoiceAux l fun i _ => f i) (fun a b h => by
-      have := fun a => Quotient.finChoiceAux_eq a fun i _ => Quotient.out (f i)
-      simp? [Quotient.out_eq] at this says simp only [out_eq] at this
-      simp only [Multiset.quot_mk_to_coe, this]
-      let g := fun a : Multiset ι =>
-        (⟦fun (i : ι) (_ : i ∈ a) => Quotient.out (f i)⟧ : Quotient (by infer_instance))
-      apply eq_of_heq
-      trans (g a)
-      · exact eqRec_heq (φ := fun l : Multiset ι => @Quotient (∀ i ∈ l, α i) (by infer_instance))
-          (Quotient.sound h) (g a)
-      · change HEq (g a) (g b); congr 1; exact Quotient.sound h))
-    (fun f => ⟦fun i => f i (Finset.mem_univ _)⟧) (fun _ _ h => Quotient.sound fun i => by apply h)
-
-theorem Quotient.finChoice_eq {ι : Type*} [DecidableEq ι] [Fintype ι] {α : ι → Type*}
-    [∀ i, Setoid (α i)] (f : ∀ i, α i) : (Quotient.finChoice fun i => ⟦f i⟧) = ⟦f⟧ := by
-  dsimp only [Quotient.finChoice]
-  conv_lhs =>
-    enter [1]
-    tactic =>
-      change _ = ⟦fun i _ => f i⟧
-      exact Quotient.inductionOn (@Finset.univ ι _).1 fun l => Quotient.finChoiceAux_eq _ _
+namespace Quotient
+
+section List
+variable {ι : Type*} [DecidableEq ι] {α : ι → Sort*} {S : ∀ i, Setoid (α i)} {β : Sort*}
+
+/-- Given a collection of setoids indexed by a type `ι`, a 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 listChoice {l : List ι} (q : ∀ i ∈ l, Quotient (S i)) : @Quotient (∀ i ∈ l, α i) piSetoid :=
+  match l with
+  |     [] => ⟦nofun⟧
+  | i :: _ => Quotient.liftOn₂ (List.Pi.head (i := i) q)
+    (listChoice (List.Pi.tail q))
+    (⟦List.Pi.cons _ _ · ·⟧)
+    (fun _ _ _ _ ha hl ↦ Quotient.sound (List.Pi.forall_rel_cons_ext ha hl))
+
+theorem listChoice_mk {l : List ι} (a : ∀ i ∈ l, α i) : listChoice (S := S) (⟦a · ·⟧) = ⟦a⟧ :=
+  match l with
+  |     [] => Quotient.sound nofun
+  | i :: l => by
+    unfold listChoice List.Pi.tail
+    rw [listChoice_mk]
+    exact congrArg (⟦·⟧) (List.Pi.cons_eta a)
+
+/-- Choice-free induction principle for quotients indexed by a `List`. -/
+@[elab_as_elim]
+lemma list_ind {l : List ι} {C : (∀ i ∈ l, Quotient (S i)) → Prop}
+    (f : ∀ a : ∀ i ∈ l, α i, C (⟦a · ·⟧)) (q : ∀ i ∈ l, Quotient (S i)) : C q :=
+  match l with
+  |     [] => cast (congr_arg _ (funext₂ nofun)) (f nofun)
+  | i :: l => by
+    rw [← List.Pi.cons_eta q]
+    induction' List.Pi.head q using Quotient.ind with a
+    refine @list_ind _ (fun q ↦ C (List.Pi.cons _ _ ⟦a⟧ q)) ?_ (List.Pi.tail q)
+    intro as
+    rw [List.Pi.cons_map a as (fun i ↦ Quotient.mk (S i))]
+    exact f _
+
+end List
+
+section Fintype
+variable {ι : Type*} [Fintype ι] [DecidableEq ι] {α : ι → Sort*} {S : ∀ i, Setoid (α i)} {β : Sort*}
+
+/-- Choice-free induction principle for quotients indexed by a finite type.
+  See `Quotient.induction_on_pi` for the general version assuming `Classical.choice`. -/
+@[elab_as_elim]
+lemma ind_fintype_pi {C : (∀ i, Quotient (S i)) → Prop}
+    (f : ∀ a : ∀ i, α i, C (⟦a ·⟧)) (q : ∀ i, Quotient (S i)) : C q := by
+  have {m : Multiset ι} (C : (∀ i ∈ m, Quotient (S i)) → Prop) :
+      ∀ (_ : ∀ a : ∀ i ∈ m, α i, C (⟦a · ·⟧)) (q : ∀ i ∈ m, Quotient (S i)), C q := by
+    induction m using Quotient.ind
+    exact list_ind
+  exact this (fun q ↦ C (q · (Finset.mem_univ _))) (fun _ ↦ f _) (fun i _ ↦ q i)
+
+/-- Choice-free induction principle for quotients indexed by a finite type.
+  See `Quotient.induction_on_pi` for the general version assuming `Classical.choice`. -/
+@[elab_as_elim]
+lemma induction_on_fintype_pi {C : (∀ i, Quotient (S i)) → Prop}
+    (q : ∀ i, Quotient (S i)) (f : ∀ a : ∀ i, α i, C (⟦a ·⟧)) : C q :=
+  ind_fintype_pi f q
+
+/-- 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.
+  See `Quotient.choice` for the noncomputable general version. -/
+def finChoice (q : ∀ i, Quotient (S i)) :
+    @Quotient (∀ i, α i) piSetoid := by
+  let e := Equiv.subtypeQuotientEquivQuotientSubtype (fun l : List ι ↦ ∀ i, i ∈ l)
+    (fun s : Multiset ι ↦ ∀ i, i ∈ s) (fun i ↦ Iff.rfl) (fun _ _ ↦ Iff.rfl) ⟨_, Finset.mem_univ⟩
+  refine e.liftOn
+    (fun l ↦ (listChoice fun i _ ↦ q i).map (fun a i ↦ a i (l.2 i)) ?_) ?_
+  · exact fun _ _ h i ↦ h i _
+  intro _ _ _
+  refine ind_fintype_pi (fun a ↦ ?_) q
+  simp_rw [listChoice_mk, Quotient.map_mk]
+
+theorem finChoice_eq (a : ∀ i, α i) :
+    finChoice (S := S) (⟦a ·⟧) = ⟦a⟧ := by
+  dsimp [finChoice]
+  obtain ⟨l, hl⟩ := (Finset.univ.val : Multiset ι).exists_rep
+  simp_rw [← hl, Equiv.subtypeQuotientEquivQuotientSubtype, listChoice_mk]
+  rfl
+
+lemma eval_finChoice (f : ∀ i, Quotient (S i)) :
+    eval (finChoice f) = f :=
+  induction_on_fintype_pi f (fun a ↦ by rw [finChoice_eq]; rfl)
+
+/-- Lift a function on `∀ i, α i` to a function on `∀ i, Quotient (S i)`. -/
+def finLiftOn (q : ∀ i, Quotient (S i)) (f : (∀ i, α i) → β)
+    (h : ∀ (a b : ∀ i, α i), (∀ i, a i ≈ b i) → f a = f b) : β :=
+  (finChoice q).liftOn f h
+
+@[simp]
+lemma finLiftOn_empty [e : IsEmpty ι] (q : ∀ i, Quotient (S i)) :
+    finLiftOn (β := β) q = fun f _ ↦ f e.elim := by
+  ext f h
+  dsimp [finLiftOn]
+  induction finChoice q using Quotient.ind
+  exact h _ _ e.elim
+
+@[simp]
+lemma finLiftOn_mk (a : ∀ i, α i) :
+    finLiftOn (S := S) (β := β) (⟦a ·⟧) = fun f _ ↦ f a := by
+  ext f h
+  dsimp [finLiftOn]
+  rw [finChoice_eq]
   rfl
 
+/-- `Quotient.finChoice` as an equivalence. -/
+@[simps]
+def finChoiceEquiv :
+    (∀ i, Quotient (S i)) ≃ @Quotient (∀ i, α i) piSetoid where
+  toFun := finChoice
+  invFun := eval
+  left_inv q := by
+    refine induction_on_fintype_pi q (fun a ↦ ?_)
+    rw [finChoice_eq]
+    rfl
+  right_inv q := by
+    induction q using Quotient.ind
+    exact finChoice_eq _
+
+/-- Recursion principle for quotients indexed by a finite type. -/
+@[elab_as_elim]
+def finHRecOn {C : (∀ i, Quotient (S i)) → Sort*}
+    (q : ∀ i, Quotient (S i))
+    (f : ∀ a : ∀ i, α i, C (⟦a ·⟧))
+    (h : ∀ (a b : ∀ i, α i), (∀ i, a i ≈ b i) → HEq (f a) (f b)) :
+    C q :=
+  eval_finChoice q ▸ (finChoice q).hrecOn f h
+
+/-- Recursion principle for quotients indexed by a finite type. -/
+@[elab_as_elim]
+def finRecOn {C : (∀ i, Quotient (S i)) → Sort*}
+    (q : ∀ i, Quotient (S i))
+    (f : ∀ a : ∀ i, α i, C (⟦a ·⟧))
+    (h : ∀ (a b : ∀ i, α i) (h : ∀ i, a i ≈ b i),
+      Eq.ndrec (f a) (funext fun i ↦ Quotient.sound (h i)) = f b) :
+    C q :=
+  finHRecOn q f (rec_heq_iff_heq.mp <| heq_of_eq <| h · · ·)
+
+@[simp]
+lemma finHRecOn_mk {C : (∀ i, Quotient (S i)) → Sort*}
+    (a : ∀ i, α i) :
+    finHRecOn (C := C) (⟦a ·⟧) = fun f _ ↦ f a := by
+  ext f h
+  refine eq_of_heq ((eqRec_heq _ _).trans ?_)
+  rw [finChoice_eq]
+  rfl
+
+@[simp]
+lemma finRecOn_mk {C : (∀ i, Quotient (S i)) → Sort*}
+    (a : ∀ i, α i) :
+    finRecOn (C := C) (⟦a ·⟧) = fun f _ ↦ f a := by
+  unfold finRecOn
+  simp
+
+end Fintype
+
+end Quotient
+
+namespace Trunc
+variable {ι : Type*} [DecidableEq ι] [Fintype ι] {α : ι → Sort*} {β : Sort*}
+
 /-- Given a function that for each `i : ι` gives a term of the corresponding
 truncation type, then there is corresponding term in the truncation of the product. -/
-def Trunc.finChoice {ι : Type*} [DecidableEq ι] [Fintype ι] {α : ι → Type*}
-    (f : ∀ i, Trunc (α i)) : Trunc (∀ i, α i) :=
-  Quotient.map' id (fun _ _ _ => trivial)
-    (Quotient.finChoice f (S := fun _ => trueSetoid))
+def finChoice (q : ∀ i, Trunc (α i)) : Trunc (∀ i, α i) :=
+  Quotient.map' id (fun _ _ _ => trivial) (Quotient.finChoice q)
 
-theorem Trunc.finChoice_eq {ι : Type*} [DecidableEq ι] [Fintype ι] {α : ι → Type*}
-    (f : ∀ i, α i) : (Trunc.finChoice fun i => Trunc.mk (f i)) = Trunc.mk f :=
+theorem finChoice_eq (f : ∀ i, α i) : (Trunc.finChoice fun i => Trunc.mk (f i)) = Trunc.mk f :=
   Subsingleton.elim _ _
+
+/-- Lift a function on `∀ i, α i` to a function on `∀ i, Trunc (α i)`. -/
+def finLiftOn (q : ∀ i, Trunc (α i)) (f : (∀ i, α i) → β) (h : ∀ (a b : ∀ i, α i), f a = f b) : β :=
+  Quotient.finLiftOn q f (fun _ _ _ ↦ h _ _)
+
+@[simp]
+lemma finLiftOn_empty [e : IsEmpty ι] (q : ∀ i, Trunc (α i)) :
+    finLiftOn (β := β) q = fun f _ ↦ f e.elim :=
+  funext₂ fun _ _ ↦ congrFun₂ (Quotient.finLiftOn_empty q) _ _
+
+@[simp]
+lemma finLiftOn_mk (a : ∀ i, α i) :
+    finLiftOn (β := β) (⟦a ·⟧) = fun f _ ↦ f a :=
+  funext₂ fun _ _ ↦ congrFun₂ (Quotient.finLiftOn_mk a) _ _
+
+/-- `Trunc.finChoice` as an equivalence. -/
+@[simps]
+def finChoiceEquiv : (∀ i, Trunc (α i)) ≃ Trunc (∀ i, α i) where
+  toFun := finChoice
+  invFun q i := q.map (· i)
+  left_inv _ := Subsingleton.elim _ _
+  right_inv _ := Subsingleton.elim _ _
+
+/-- Recursion principle for `Trunc`s indexed by a finite type. -/
+@[elab_as_elim]
+def finRecOn {C : (∀ i, Trunc (α i)) → Sort*}
+    (q : ∀ i, Trunc (α i))
+    (f : ∀ a : ∀ i, α i, C (mk <| a ·))
+    (h : ∀ (a b : ∀ i, α i), (Eq.ndrec (f a) (funext fun _ ↦ Trunc.eq _ _)) = f b) :
+    C q :=
+  Quotient.finRecOn q (f ·) (fun _ _ _ ↦ h _ _)
+
+@[simp]
+lemma finRecOn_mk {C : (∀ i, Trunc (α i)) → Sort*}
+    (a : ∀ i, α i) :
+    finRecOn (C := C) (⟦a ·⟧) = fun f _ ↦ f a := by
+  unfold finRecOn
+  simp
+
+end Trunc

Mathlib/Data/Quot.lean

@@ -387,6 +387,17 @@ instance piSetoid {ι : Sort*} {α : ι → Sort*} [∀ i, Setoid (α i)] : Seto
             fun h _ ↦ Setoid.symm (h _),
             fun h₁ h₂ _ ↦ Setoid.trans (h₁ _) (h₂ _)⟩
 
+/-- Given a class of functions `q : @Quotient (∀ i, α i) _`, returns the class of `i`-th projection
+`Quotient (S i)`. -/
+def Quotient.eval {ι : Type*} {α : ι → Sort*} {S : ∀ i, Setoid (α i)}
+    (q : @Quotient (∀ i, α i) (by infer_instance)) (i : ι) : Quotient (S i) :=
+  q.map (· i) fun _ _ h ↦ by exact h i
+
+@[simp]
+theorem Quotient.eval_mk {ι : Type*} {α : ι → Type*} {S : ∀ i, Setoid (α i)} (f : ∀ i, α i) :
+    Quotient.eval (S := S) ⟦f⟧ = fun i ↦ ⟦f i⟧ :=
+  rfl
+
 /-- Given a function `f : Π i, Quotient (S i)`, returns the class of functions `Π i, α i` sending
 each `i` to an element of the class `f i`. -/
 noncomputable def Quotient.choice {ι : Type*} {α : ι → Type*} {S : ∀ i, Setoid (α i)}