awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
s : Finset α
t : Finset β
inst_2 : Nonempty α
inst_3 : Nonempty β
⊢ s ×ˢ t = univ ↔ s = univ ∧ t = univ

Tactic:
simp [eq_univ_iff_forall, forall_and]

Premises used: Finset.eq_univ_iff_forall, forall_and
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_4
β : Type u_5
inst : Fintype α
inst_1 : Fintype β
⊢ card (α × β) = card α * card β

Tactic:
card_product _ _

Premises used: Finset.univ, Finset.card_product, Fintype.card
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
β : Type u_2
⊢ Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β

Tactic:
⟨fun H => ?_, fun H =>
      H.elim (and_imp.2 <| @Prod.infinite_of_left α β) (and_imp.2 <| @Prod.infinite_of_right α β)⟩

Premises used: Iff.mpr, and_imp, Prod.infinite_of_left, Prod.infinite_of_right, Iff.intro, Or.elim
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
β : Type u_2
H : ∀ (H : Infinite (α × β)), Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
⊢ Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β

Tactic:
refine
    ⟨fun H => ?_, fun H =>
      H.elim (and_imp.2 <| @Prod.infinite_of_left α β) (and_imp.2 <| @Prod.infinite_of_right α β)⟩
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
β : Type u_2
H : Infinite (α × β)
rw : Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β
⊢ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β

Tactic:
rw [and_comm]

Premises used: and_comm
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
β : Type u_2
H : Infinite (α × β)
rcases : ∀ (a : α) (b : β), Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β
⊢ Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β

Tactic:
rcases Infinite.nonempty (α × β) with ⟨a, b⟩

Premises used: Infinite.nonempty, Prod
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
β : Type u_2
H : Infinite (α × β)
a : α
b : β
contrapose! : ∀ (H : (∀ (_ : Nonempty β), Finite α) ∧ ∀ (_ : Nonempty α), Finite β), Finite (α × β)
⊢ Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β

Tactic:
contrapose! H
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
H : (∀ (_ : Nonempty β), Finite α) ∧ ∀ (_ : Nonempty α), Finite β
⊢ Finite α

Tactic:
haveI := H.1 ⟨b⟩
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
H : (∀ (_ : Nonempty β), Finite α) ∧ ∀ (_ : Nonempty α), Finite β
this : Finite α
⊢ Finite β

Tactic:
haveI := H.2 ⟨a⟩
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
H : (∀ (_ : Nonempty β), Finite α) ∧ ∀ (_ : Nonempty α), Finite β
this_1 : Finite α
this : Finite β
⊢ Finite (α × β)

Tactic:
infer_instance
-- Module: Mathlib.Data.Fintype.Prod
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)
⊢ Infinite ((i : ι) → π i)

Tactic:
choose m n hm using fun i => exists_pair_ne (π i)

Premises used: exists_pair_ne
-- Module: Mathlib.Data.Fintype.Prod
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 ι
m n : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ n i
⊢ Infinite ((i : ι) → π i)

Tactic:
Infinite.of_injective (fun i => update m i (n i)) fun x y h => of_not_not fun hne => ?_

Premises used: Infinite.of_injective, Function.update, of_not_not
-- Module: Mathlib.Data.Fintype.Prod
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 ι
m n : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ n i
refine :
  ∀ (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)

Tactic:
refine Infinite.of_injective (fun i => update m i (n i)) fun x y h => of_not_not fun hne => ?_

Premises used: Infinite.of_injective, Function.update, of_not_not
-- Module: Mathlib.Data.Fintype.Prod
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 ι
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
⊢ n x = m x ∧ ∀ (x_1 : ι), x_1 ≠ x → m x_1 = update (β := π) m y (n y) x_1

Tactic:
simp_rw [update_eq_iff, update_of_ne hne] at h

Premises used: Function.update_eq_iff, Function.update_of_ne
-- Module: Mathlib.Data.Fintype.Prod
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 ι
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:
(hm x h.1.symm).elim

Premises used: False.elim, And.left, Eq.symm
-- Module: Mathlib.Data.Fintype.Prod
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 ι
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:
exact (hm x h.1.symm).elim

Premises used: False.elim, And.left, Eq.symm
-- Module: Mathlib.Data.Fintype.Prod
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
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
⊢ Infinite ((i : ι) → π i)

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

Premises used: Function.update_eq_iff, exists_pair_ne
-- Module: Mathlib.Data.Fintype.Prod
Goal:
ι : Sort u_4
π : ι → Sort u_5
i : ι
inst : Infinite.{u_5} (π i)
inst_1 : ∀ (i : ι), Nonempty.{u_5} (π i)
let : ∀ (m : (a : ι) → π a), Infinite ((i : ι) → π i)
⊢ Infinite ((i : ι) → π i)

Tactic:
let ⟨m⟩ := @Pi.instNonempty ι π _
-- Module: Mathlib.Data.Fintype.Prod
Goal:
ι : Sort u_4
π : ι → Sort u_5
i : ι
inst : Infinite.{u_5} (π i)
inst_1 : ∀ (i : ι), Nonempty.{u_5} (π i)
m : (a : ι) → π a
⊢ Infinite ((i : ι) → π i)

Tactic:
Infinite.of_injective _ (update_injective m i)

Premises used: Infinite.of_injective, Function.update_injective
-- Module: Mathlib.Data.Fintype.Prod
Goal:
ι : Sort u_4
π : ι → Sort u_5
i : ι
inst : Infinite.{u_5} (π i)
inst_1 : ∀ (i : ι), Nonempty.{u_5} (π i)
m : (a : ι) → π a
⊢ Infinite ((i : ι) → π i)

Tactic:
exact Infinite.of_injective _ (update_injective m i)

Premises used: Infinite.of_injective, Function.update_injective
-- Module: Mathlib.Data.Fintype.Prod
Goal:
ι : Sort u_4
π : ι → Sort u_5
i : ι
inst : Infinite.{u_5} (π i)
inst_1 : ∀ (i : ι), Nonempty.{u_5} (π i)
let let₁ let₂ : ∀ (m : (a : ι) → π a), Infinite ((i : ι) → π i)
⊢ Infinite ((i : ι) → π i)

Tactic:
classical
  let ⟨m⟩ := @Pi.instNonempty ι π _
  exact Infinite.of_injective _ (update_injective m i)
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type u_5
inst : ∀ (i : ι), Infinite.{u_5 + 1} (π i)
inst_1 : Nonempty ι
⊢ Infinite ((i : ι) → π i)

Tactic:
Pi.infinite_of_exists_right (Classical.arbitrary ι)

Premises used: Pi.infinite_of_exists_right, Classical.arbitrary
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : Type u_5
inst : Nontrivial π
inst_1 : Infinite ι
⊢ Infinite (ι → π)

Tactic:
Pi.infinite_of_left

Premises used: Pi.infinite_of_left
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : Type u_5
inst : Infinite π
inst_1 : Nonempty ι
⊢ Infinite (ι → π)

Tactic:
Pi.infinite_of_right

Premises used: Pi.infinite_of_right
-- Module: Mathlib.Data.Fintype.Quotient
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
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 ⋯)
      (fun (x1 : α i) (x2 : (i : ι) → i ∈ l → α i) ↦ ⟦List.Pi.cons (α := α) i l x1 x2⟧) ⋯)
    ⟦a⟧
⊢ 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⟧

Tactic:
unfold listChoice List.Pi.tail

Premises used: List.Pi.tail, Quotient.listChoice
-- Module: Mathlib.Data.Fintype.Quotient
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
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 ⋯⟧
      (fun (x1 : α i) (x2 : (i : ι) → i ∈ l → α i) ↦ ⟦List.Pi.cons (α := α) i l x1 x2⟧) ⋯)
    ⟦a⟧
⊢ 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⟧

Tactic:
rw [listChoice_mk]
-- Module: Mathlib.Data.Fintype.Quotient
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⟧)
      ⟦fun (j : ι) (hj : j ∈ l) ↦ a j ⋯⟧
      (fun (x1 : α i) (x2 : (i : ι) → i ∈ l → α i) ↦ ⟦List.Pi.cons (α := α) i l x1 x2⟧) ⋯)
    ⟦a⟧

Tactic:
congrArg (⟦·⟧) (List.Pi.cons_eta a)

Premises used: List.Pi.cons_eta, congrArg, Quotient.mk
-- Module: Mathlib.Data.Fintype.Quotient
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⟧)
      ⟦fun (j : ι) (hj : j ∈ l) ↦ a j ⋯⟧
      (fun (x1 : α i) (x2 : (i : ι) → i ∈ l → α i) ↦ ⟦List.Pi.cons (α := α) i l x1 x2⟧) ⋯)
    ⟦a⟧

Tactic:
exact congrArg (⟦·⟧) (List.Pi.cons_eta a)

Premises used: List.Pi.cons_eta, congrArg, Quotient.mk
-- Module: Mathlib.Data.Fintype.Quotient
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)
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))
⊢ C q

Tactic:
rw [← List.Pi.cons_eta q]

Premises used: List.Pi.cons_eta
-- Module: Mathlib.Data.Fintype.Quotient
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 :
  ∀ (a : α i),
    C (List.Pi.cons (α := fun (j : ι) ↦ Quotient (S j)) i l ⟦a⟧ (List.Pi.tail (α := fun (j : ι) ↦ Quotient (S j)) q))
⊢ 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:
induction List.Pi.head q using Quotient.ind with | _ a

Premises used: List.Pi.head, Quotient.ind
-- Module: Mathlib.Data.Fintype.Quotient
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))

Tactic:
@list_ind _ (fun q ↦ C (List.Pi.cons _ _ ⟦a⟧ q)) ?_ (List.Pi.tail q)

Premises used: List.Pi.tail
-- Module: Mathlib.Data.Fintype.Quotient
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
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⟧
⊢ C (List.Pi.cons (α := fun (j : ι) ↦ Quotient (S j)) i l ⟦a⟧ (List.Pi.tail (α := fun (j : ι) ↦ Quotient (S j)) q))

Tactic:
refine @list_ind _ (fun q ↦ C (List.Pi.cons _ _ ⟦a⟧ q)) ?_ (List.Pi.tail q)

Premises used: List.Pi.tail
-- Module: Mathlib.Data.Fintype.Quotient
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
a₁ : C fun (j : ι) (hj : j ∈ i :: l) ↦ ⟦List.Pi.cons (α := α) i l a as j hj⟧
⊢ C (List.Pi.cons (α := fun (i : ι) ↦ Quotient (S i)) i l ⟦a⟧ fun (x1 : ι) (x2 : x1 ∈ l) ↦ ⟦as x1 x2⟧)

Tactic:
rw [List.Pi.cons_map a as (fun i ↦ Quotient.mk (S i))]

Premises used: List.Pi.cons_map, Quotient.mk
-- Module: Mathlib.Data.Fintype.Quotient
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 fun (j : ι) (hj : j ∈ i :: l) ↦ ⟦List.Pi.cons (α := α) i l a as j hj⟧

Tactic:
f _
-- Module: Mathlib.Data.Fintype.Quotient
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 fun (j : ι) (hj : j ∈ i :: l) ↦ ⟦List.Pi.cons (α := α) i l a as j hj⟧

Tactic:
exact f _
-- Module: Mathlib.Data.Fintype.Quotient
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 :
  ∀ (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
⊢ (∀ (a : (i : ι) → i ∈ m → α i), C fun (x1 : ι) (x2 : x1 ∈ m) ↦ ⟦a x1 x2⟧) →
    ∀ (q : (i : ι) → i ∈ m → Quotient (S i)), C q

Tactic:
induction m using Quotient.ind

Premises used: Quotient.ind
-- Module: Mathlib.Data.Fintype.Quotient
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)
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:
list_ind

Premises used: Quotient.list_ind, Multiset.Mem
-- Module: Mathlib.Data.Fintype.Quotient
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)
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:
exact list_ind
-- Module: Mathlib.Data.Fintype.Quotient
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)
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
⊢ 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
-- Module: Mathlib.Data.Fintype.Quotient
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)
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:
this (fun q ↦ C (q · (Finset.mem_univ _))) (fun _ ↦ f _) (fun i _ ↦ q i)

Premises used: Finset.mem_univ
-- Module: Mathlib.Data.Fintype.Quotient
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)
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:
exact this (fun q ↦ C (q · (Finset.mem_univ _))) (fun _ ↦ f _) (fun i _ ↦ q i)

Premises used: Finset.mem_univ
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
C : ((i : ι) → Quotient (S i)) → Prop
q : (i : ι) → Quotient (S i)
f : ∀ (a : (i : ι) → α i), C fun (x : ι) ↦ ⟦a x⟧
⊢ C q

Tactic:
ind_fintype_pi f q

Premises used: Quotient.ind_fintype_pi
-- Module: Mathlib.Data.Fintype.Quotient
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)
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 ⋯) ⋯
                (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)
⊢ Quotient (α := (i : ι) → α i) (piSetoid (α := α))

Tactic:
refine e.liftOn
    (fun l ↦ (listChoice fun i _ ↦ q i).map (fun a i ↦ a i (l.2 i)) ?_) ?_

Premises used: Quotient.map, Quotient.listChoice, Quotient.liftOn
-- Module: Mathlib.Data.Fintype.Quotient
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) ⋯)
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)

Tactic:
fun _ _ h i ↦ h i _

Premises used: Subtype.property