awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fintype.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type u_5
inst : ∀ (i : ι), Nontrivial.{u_5} (π i)
inst_1 : Infinite ι
choose : ∀ (m n : (i : ι) → π i) (hm : ∀ (i : ι), m i ≠ n i), Infinite ((i : ι) → π i)
choose₁ :
  ∀ (m n : (i : ι) → π i) (hm : ∀ (i : ι), m i ≠ n i) (x y : ι)
    (h :
      Eq (α := (i : ι) → π i) ((fun (i : ι) ↦ update (β := π) m i (n i)) x)
        ((fun (i : ι) ↦ update (β := π) m i (n i)) y))
    (hne : ¬x = y), False
⊢ Infinite ((i : ι) → π i)
have choose₂ : ∀ (m n : (i : ι) → π i) (hm : ∀ (i : ι), m i ≠ n i) (x y : ι) (hne : ¬x = y)
  (h : n x = m x ∧ ∀ (x_1 : ι), x_1 ≠ x → m x_1 = update (β := π) m y (n y) x_1), False
Tactic: classical
  choose m n hm using fun i => exists_pair_ne (π i)
  refine Infinite.of_injective (fun i => update m i (n i)) fun x y h => of_not_not fun hne => ?_
  simp_rw [update_eq_iff, update_of_ne hne] at h
  exact (hm x h.1.symm).elim
-- Lean 4 proof step from Mathlib.Data.Fintype.Prod (goal)
Goal:
ι : Sort u_4
π : ι → Sort u_5
i : ι
inst : Infinite.{u_5} (π i)
inst_1 : ∀ (i : ι), Nonempty.{u_5} (π i)
⊢ Infinite ((i : ι) → π i)
have let : ∀ (m : (a : ι) → π a), Infinite ((i : ι) → π i)
Tactic: let ⟨m⟩ := @Pi.instNonempty ι π _
-- Lean 4 proof step from Mathlib.Data.Fintype.Prod (goal)
Goal:
ι : Sort u_4
π : ι → Sort u_5
i : ι
inst : Infinite.{u_5} (π i)
inst_1 : ∀ (i : ι), Nonempty.{u_5} (π i)
⊢ Infinite ((i : ι) → π i)
have let : ∀ (m : (a : ι) → π a), Infinite ((i : ι) → π i)
Tactic: classical
  let ⟨m⟩ := @Pi.instNonempty ι π _
  exact Infinite.of_injective _ (update_injective m i)
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
l_1 : List ι
i : ι
l : List ι
a : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ Eq (α := Quotient (α := (i_1 : ι) → i_1 ∈ i :: l → α i_1) (piSetoid (α := fun (i_1 : ι) ↦ i_1 ∈ i :: l → α i_1)))
    (listChoice (α := α) fun (x1 : ι) (x2 : x1 ∈ i :: l) ↦ ⟦a x1 x2⟧) ⟦a⟧
have unfold : Eq (α := Quotient (α := (i_1 : ι) → i_1 ∈ i :: l → α i_1) (piSetoid (α := fun (i_1 : ι) ↦ i_1 ∈ i :: l → α i_1)))
  (Quotient.liftOn₂
    (List.Pi.head.{u_1, u_2} (α := fun (j : ι) ↦ Quotient (S j)) (l := l) fun (x1 : ι) (x2 : x1 ∈ i :: l) ↦ ⟦a x1 x2⟧)
    (listChoice (α := α) fun (j : ι) (hj : j ∈ l) ↦ (fun (x1 : ι) (x2 : x1 ∈ i :: l) ↦ ⟦a x1 x2⟧) j sorry)
    (fun (x1 : α i) (x2 : (i : ι) → i ∈ l → α i) ↦ ⟦List.Pi.cons (α := α) i l x1 x2⟧) sorry)
  ⟦a⟧
Tactic: unfold listChoice List.Pi.tail
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
l_1 : List ι
i : ι
l : List ι
a : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ Eq (α := Quotient (α := (i_1 : ι) → i_1 ∈ i :: l → α i_1) (piSetoid (α := fun (i_1 : ι) ↦ i_1 ∈ i :: l → α i_1)))
    (Quotient.liftOn₂
      (List.Pi.head.{u_1, u_2} (α := fun (j : ι) ↦ Quotient (S j)) (l := l) fun (x1 : ι) (x2 : x1 ∈ i :: l) ↦ ⟦a x1 x2⟧)
      (listChoice (α := α) fun (j : ι) (hj : j ∈ l) ↦ (fun (x1 : ι) (x2 : x1 ∈ i :: l) ↦ ⟦a x1 x2⟧) j ⋯)
      (fun (x1 : α i) (x2 : (i : ι) → i ∈ l → α i) ↦ ⟦List.Pi.cons (α := α) i l x1 x2⟧) ⋯)
    ⟦a⟧
have rw : Eq (α := Quotient (α := (i_1 : ι) → i_1 ∈ i :: l → α i_1) (piSetoid (α := fun (i_1 : ι) ↦ i_1 ∈ i :: l → α i_1)))
  (Quotient.liftOn₂
    (List.Pi.head.{u_1, u_2} (α := fun (j : ι) ↦ Quotient (S j)) (l := l) fun (x1 : ι) (x2 : x1 ∈ i :: l) ↦ ⟦a x1 x2⟧)
    ⟦fun (j : ι) (hj : j ∈ l) ↦ a j sorry⟧ (fun (x1 : α i) (x2 : (i : ι) → i ∈ l → α i) ↦ ⟦List.Pi.cons (α := α) i l x1 x2⟧)
    sorry)
  ⟦a⟧
Tactic: rw [listChoice_mk]
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
l_1 : List ι
i : ι
l : List ι
C : ((i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)) → Prop
f : ∀ (a : (i_1 : ι) → i_1 ∈ i :: l → α i_1), C fun (x1 : ι) (x2 : x1 ∈ i :: l) ↦ ⟦a x1 x2⟧
q : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
⊢ C q
have rw : C
  (List.Pi.cons (α := fun (j : ι) ↦ Quotient (S j)) i l
    (List.Pi.head.{u_1, u_2} (α := fun (j : ι) ↦ Quotient (S j)) (l := l) q)
    (List.Pi.tail (α := fun (j : ι) ↦ Quotient (S j)) q))
Tactic: rw [← List.Pi.cons_eta q]
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
l_1 : List ι
i : ι
l : List ι
C : ((i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)) → Prop
f : ∀ (a : (i_1 : ι) → i_1 ∈ i :: l → α i_1), C fun (x1 : ι) (x2 : x1 ∈ i :: l) ↦ ⟦a x1 x2⟧
q : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
⊢ C
    (List.Pi.cons (α := fun (j : ι) ↦ Quotient (S j)) i l
      (List.Pi.head.{u_1, u_2} (α := fun (j : ι) ↦ Quotient (S j)) (l := l) q)
      (List.Pi.tail (α := fun (j : ι) ↦ Quotient (S j)) q))
have a : ∀ (a : α i),
  C (List.Pi.cons (α := fun (j : ι) ↦ Quotient (S j)) i l ⟦a⟧ (List.Pi.tail (α := fun (j : ι) ↦ Quotient (S j)) q))
Tactic: induction List.Pi.head q using Quotient.ind with | _ a
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
l_1 : List ι
i : ι
l : List ι
C : ((i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)) → Prop
f : ∀ (a : (i_1 : ι) → i_1 ∈ i :: l → α i_1), C fun (x1 : ι) (x2 : x1 ∈ i :: l) ↦ ⟦a x1 x2⟧
q : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a : α i
⊢ C (List.Pi.cons (α := fun (j : ι) ↦ Quotient (S j)) i l ⟦a⟧ (List.Pi.tail (α := fun (j : ι) ↦ Quotient (S j)) q))
have a₁ : ∀ (a_1 : (i : ι) → i ∈ l → α i),
  (fun (q : (i : ι) → i ∈ l → Quotient (S i)) ↦ C (List.Pi.cons (α := fun (i : ι) ↦ Quotient (S i)) i l ⟦a⟧ q))
    fun (x1 : ι) (x2 : x1 ∈ l) ↦ ⟦a_1 x1 x2⟧
Tactic: refine @list_ind _ (fun q ↦ C (List.Pi.cons _ _ ⟦a⟧ q)) ?_ (List.Pi.tail q)
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
l_1 : List ι
i : ι
l : List ι
C : ((i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)) → Prop
f : ∀ (a : (i_1 : ι) → i_1 ∈ i :: l → α i_1), C fun (x1 : ι) (x2 : x1 ∈ i :: l) ↦ ⟦a x1 x2⟧
q : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a : α i
as : (i : ι) → i ∈ l → α i
⊢ C (List.Pi.cons (α := fun (i : ι) ↦ Quotient (S i)) i l ⟦a⟧ fun (x1 : ι) (x2 : x1 ∈ l) ↦ ⟦as x1 x2⟧)
have a₁ : C fun (j : ι) (hj : j ∈ i :: l) ↦ ⟦List.Pi.cons (α := α) i l a as j hj⟧
Tactic: rw [List.Pi.cons_map a as (fun i ↦ Quotient.mk (S i))]
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
C_1 : ((i : ι) → Quotient (S i)) → Prop
f : ∀ (a : (i : ι) → α i), C_1 fun (x : ι) ↦ ⟦a x⟧
q : (i : ι) → Quotient (S i)
m : Multiset ι
C : ((i : ι) → i ∈ m → Quotient (S i)) → Prop
⊢ (∀ (a : (i : ι) → i ∈ m → α i), C fun (x1 : ι) (x2 : x1 ∈ m) ↦ ⟦a x1 x2⟧) →
    ∀ (q : (i : ι) → i ∈ m → Quotient (S i)), C q
have a : ∀ (a : List ι) (C : ((i : ι) → i ∈ ⟦a⟧ → Quotient (S i)) → Prop),
  (∀ (a_1 : (i : ι) → i ∈ ⟦a⟧ → α i), C fun (x1 : ι) (x2 : x1 ∈ ⟦a⟧) ↦ ⟦a_1 x1 x2⟧) →
    ∀ (q : (i : ι) → i ∈ ⟦a⟧ → Quotient (S i)), C q
Tactic: induction m using Quotient.ind
Cleared hypotheses: m, C
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
C : ((i : ι) → Quotient (S i)) → Prop
f : ∀ (a : (i : ι) → α i), C fun (x : ι) ↦ ⟦a x⟧
q : (i : ι) → Quotient (S i)
⊢ C q
have have : ∀
  (this :
    ∀ {m : Multiset ι} (C : ((i : ι) → i ∈ m → Quotient (S i)) → Prop),
      (∀ (a : (i : ι) → i ∈ m → α i), C fun (x1 : ι) (x2 : x1 ∈ m) ↦ ⟦a x1 x2⟧) →
        ∀ (q : (i : ι) → i ∈ m → Quotient (S i)), C q),
  C q
Tactic: 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
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
  (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
        (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
      (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
        Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
    (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯)
⊢ Quotient (α := (i : ι) → α i) (piSetoid (α := α))
have refine_1 : ∀ (l : { l : List ι // ∀ (i : ι), i ∈ l }) ⦃a b : (i : ι) → i ∈ (↑l : List ι) → α i⦄,
  a ≈ b →
    HasEquiv.Equiv (α := (i : ι) → α i) ((fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i sorry) a)
      ((fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i sorry) b)
Tactic: refine e.liftOn
    (fun l ↦ (listChoice fun i _ ↦ q i).map (fun a i ↦ a i (l.2 i)) ?_) ?_
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
  (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
        (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
      (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
        Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
    (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯)
refine_1 :
  ∀ (l : { l : List ι // ∀ (i : ι), i ∈ l }) ⦃a b : (i : ι) → i ∈ (↑l : List ι) → α i⦄,
    a ≈ b →
      HasEquiv.Equiv (α := (i : ι) → α i) ((fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) a)
        ((fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) b)
⊢ Quotient (α := (i : ι) → α i) (piSetoid (α := α))
have refine_2 : ∀ (a b : { l : List ι // ∀ (i : ι), i ∈ l }),
  a ≈ b →
    Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
      ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
          (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
              (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i sorry) sorry
              (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
            Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
        a)
      ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
          (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
              (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i sorry) sorry
              (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
            Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
        b)
Tactic: refine e.liftOn
    (fun l ↦ (listChoice fun i _ ↦ q i).map (fun a i ↦ a i (l.2 i)) ?_) ?_
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
  (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
        (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
      (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
        Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
    (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯)
a b : { l : List ι // ∀ (i : ι), i ∈ l }
h : a ≈ b
⊢ Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
            (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
            (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
          Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      a)
    ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
            (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
            (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
          Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      b)
have refine_2 : ∀ (a_1 : (i : ι) → α i),
  Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
            (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i sorry) sorry
            (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ (fun (x : ι) ↦ ⟦a_1 x⟧) i) :
          Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      a)
    ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
            (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i sorry) sorry
            (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ (fun (x : ι) ↦ ⟦a_1 x⟧) i) :
          Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      b)
Tactic: refine ind_fintype_pi (fun a ↦ ?_) q
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
  (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
        (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
      (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
        Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
    (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯)
a_1 b : { l : List ι // ∀ (i : ι), i ∈ l }
h : a_1 ≈ b
a : (i : ι) → α i
refine_2 refine_2₁ :
  Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑a_1 : List ι) → α i))
      (fun (a : (i : ι) → i ∈ (↑a_1 : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
      (listChoice (α := α) fun (i : ι) (x : i ∈ (↑a_1 : List ι)) ↦ ⟦a i⟧))
    (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑b : List ι) → α i))
      (fun (a : (i : ι) → i ∈ (↑b : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
      (listChoice (α := α) fun (i : ι) (x : i ∈ (↑b : List ι)) ↦ ⟦a i⟧))
⊢ Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
            (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
            (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ (fun (x : ι) ↦ ⟦a x⟧) i) :
          Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      a_1)
    ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
            (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
            (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ (fun (x : ι) ↦ ⟦a x⟧) i) :
          Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      b)
have refine_2₂ : Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
  (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑a_1 : List ι) → α i))
    (fun (a : (i : ι) → i ∈ (↑a_1 : List ι) → α i) (i : ι) ↦ a i sorry) sorry ⟦fun (x1 : ι) (x2 : x1 ∈ (↑a_1 : List ι)) ↦ a x1⟧)
  (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑b : List ι) → α i))
    (fun (a : (i : ι) → i ∈ (↑b : List ι) → α i) (i : ι) ↦ a i sorry) sorry ⟦fun (x1 : ι) (x2 : x1 ∈ (↑b : List ι)) ↦ a x1⟧)
Tactic: simp_rw [listChoice_mk, Quotient.map_mk]
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
a : (i : ι) → α i
⊢ Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α))) (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧) ⟦a⟧
have dsimp : Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
  (Quotient.liftOn
    ((Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
          (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) sorry sorry :
        (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
          Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
      (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) sorry))
    (fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
      Quotient.map (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i sorry) sorry
        (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ ⟦a i⟧))
    sorry)
  ⟦a⟧
Tactic: dsimp [finChoice]
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
a : (i : ι) → α i
⊢ Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    (Quotient.liftOn
      ((Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
            (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
          (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
            Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
        (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯))
      (fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        Quotient.map (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
          (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ ⟦a i⟧))
      ⋯)
    ⟦a⟧
have obtain : ∀ (l : List ι) (hl : ⟦l⟧ = Finset.val Finset.univ),
  Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    (Quotient.liftOn
      ((Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
            (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) sorry sorry :
          (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
            Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
        (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) sorry))
      (fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        Quotient.map (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i sorry) sorry
          (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ ⟦a i⟧))
      sorry)
    ⟦a⟧
Tactic: obtain ⟨l, hl⟩ := (Finset.univ.val : Multiset ι).exists_rep
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
a : (i : ι) → α i
l : List ι
hl : ⟦l⟧ = Finset.val Finset.univ
⊢ Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    (Quotient.liftOn
      ((Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
            (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
          (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
            Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
        (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯))
      (fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        Quotient.map (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
          (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ ⟦a i⟧))
      ⋯)
    ⟦a⟧
have simp_rw : Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
  (Quotient.liftOn (s := Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
    (({
          toFun := fun (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) ↦
            Quotient.hrecOn (motive := fun (x : Quotient (List.isSetoid ι)) ↦
              (∀ (i : ι), i ∈ x) →
                Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
                  (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
              (↑a : Quotient (List.isSetoid ι))
              (fun (a : List ι) (h : ∀ (i : ι), i ∈ ⟦a⟧) ↦ ⟦Subtype.mk (p := fun (l : List ι) ↦ ∀ (i : ι), i ∈ l) a sorry⟧)
              sorry sorry,
          invFun :=
            fun
              (a :
                Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
                  (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)) ↦
            a.liftOn
              (fun (a : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
                Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) ⟦(↑a : List ι)⟧ sorry)
              sorry,
          left_inv := sorry, right_inv := sorry } :
        (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
          Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
      (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) ⟦l⟧ sorry))
    (fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
      Quotient.map (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i sorry) sorry
        ⟦fun (x1 : ι) (x2 : x1 ∈ (↑l : List ι)) ↦ a x1⟧)
    sorry)
  ⟦a⟧
Tactic: simp_rw [← hl, Equiv.subtypeQuotientEquivQuotientSubtype, listChoice_mk]
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
f : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ Eq (α := (i : ι) → Quotient (S i)) (eval (α := α) (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧)) fun (x : ι) ↦ ⟦a x⟧
have rw : Eq (α := (i : ι) → Quotient (S i)) (eval (α := α) ⟦a⟧) fun (x : ι) ↦ ⟦a x⟧
Tactic: rw [finChoice_eq]
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Quotient (S i)
⊢ Eq (α := (f : ((i : ι) → α i) → β) → (h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b) → β)
    (finLiftOn (α := α) q)
    fun (f : ((i : ι) → α i) → β) (x : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b) ↦
    f fun (a : ι) ↦ e.elim (p := fun (x : ι) ↦ α x) a
have h : ∀ (f : ((i : ι) → α i) → β) (h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b),
  finLiftOn (α := α) q f h = f fun (a : ι) ↦ e.elim (p := fun (x : ι) ↦ α x) a
Tactic: ext f h
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Quotient (S i)
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
⊢ finLiftOn (α := α) q f h = f fun (a : ι) ↦ e.elim (p := fun (x : ι) ↦ α x) a
have h₁ : (finChoice (α := α) q).liftOn f h = f fun (a : ι) ↦ e.elim (p := fun (x : ι) ↦ α x) a
Tactic: dsimp [finLiftOn]
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
e : IsEmpty ι
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 = f fun (a : ι) ↦ e.elim (p := fun (x : ι) ↦ α x) a
have h₁ : ∀ (a : (i : ι) → α i),
  Quotient.liftOn (s := piSetoid (α := α)) ⟦a⟧ f h = f fun (a : ι) ↦ e.elim (p := fun (x : ι) ↦ α x) a
Tactic: induction finChoice q using Quotient.ind