awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
⊢ ∀ (k : ℕ),
    Fintype.card G ≤ k →
      Fintype.card.{u_5} (↑(S ^ k) : Type u_5) = Fintype.card.{u_5} (↑(S ^ Fintype.card G) : Type u_5)
have inr : ∀ (x n : ℕ) (h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)),
  ∀ b ∈ S ^ (n + 2), b * a⁻¹ ∈ S ^ (n + 1)
Tactic: refine fun _ ↦ Nat.stabilises_of_monotone mono (fun n ↦ set_fintype_card_le_univ (S ^ n))
    fun n h ↦ le_antisymm (mono (n + 1).le_succ) (key a⁻¹ (S ^ (n + 2)) (S ^ (n + 1)) ?_)
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
⊢ S ^ n * {a} = S ^ (n + 1)
have have : ∀ (this : Fintype (↑(S ^ n * Set.singleton a) : Type u_5)), S ^ n * {a} = S ^ (n + 1)
Tactic: have : Fintype (S ^ n * Set.singleton a) := by
      classical
      apply fintypeMul
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
this : Fintype (↑(S ^ n * Set.singleton a) : Type u_5)
⊢ S ^ n * {a} = S ^ (n + 1)
have refine_1 : S ^ n * {a} ⊆ S ^ (n + 1)
Tactic: refine Set.eq_of_subset_of_card_le ?_ (le_trans (ge_of_eq h) ?_)
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
this : Fintype (↑(S ^ n * Set.singleton a) : Type u_5)
refine_1 : S ^ n * {a} ⊆ S ^ (n + 1)
⊢ S ^ n * {a} = S ^ (n + 1)
have refine_2 : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) ≤ Fintype.card.{u_5} (↑(S ^ n * {a}) : Type u_5)
Tactic: refine Set.eq_of_subset_of_card_le ?_ (le_trans (ge_of_eq h) ?_)
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (hypothesis)
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
⊢ ∀ b ∈ S ^ (n + 2), b * a⁻¹ ∈ S ^ (n + 1)
have h₂ : S ^ n * {a} = S ^ (n + 1)
Tactic: replace h₂ : S ^ n * {a} = S ^ (n + 1) := by
    have : Fintype (S ^ n * Set.singleton a) := by
      classical
      apply fintypeMul
    refine Set.eq_of_subset_of_card_le ?_ (le_trans (ge_of_eq h) ?_)
    · exact mul_subset_mul Set.Subset.rfl (Set.singleton_subset_iff.mpr ha)
    · convert! key a (S ^ n) (S ^ n * { a }) fun b hb ↦ Set.mul_mem_mul hb (Set.mem_singleton a)
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
h₂ : S ^ n * {a} = S ^ (n + 1)
⊢ ∀ b ∈ S ^ (n + 2), b * a⁻¹ ∈ S ^ (n + 1)
have inr : ∀ ⦃x : G⦄, x ∈ S ^ (n + 1) → x * a * a⁻¹ ∈ S ^ (n + 1)
Tactic: rw [pow_succ', ← h₂, ← mul_assoc, ← pow_succ', h₂, mul_singleton, forall_mem_image]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Lattice (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
a : α
S : Set (Set β)
⊢ a • ⋃₀ S = ⋃ s ∈ S, a • s
have rw : HSMul.hSMul (β := Set β) a (⋃ i ∈ S, i) = ⋃ s ∈ S, a • s
Tactic: rw [sUnion_eq_biUnion, smul_set_iUnion₂]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Lattice (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
a : α
S : Set (Set β)
rw : HSMul.hSMul (β := Set β) a (⋃ i ∈ S, i) = ⋃ s ∈ S, a • s
⊢ a • ⋃₀ S = ⋃ s ∈ S, a • s
have rw₁ : Eq.{u_3 + 1} (α := Set β) (⋃ i ∈ S, a • i) (⋃ s ∈ S, a • s)
Tactic: rw [sUnion_eq_biUnion, smul_set_iUnion₂]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (↑(f i) : α)) = a
have zero : Membership.mem (γ := Set α) (List.prod []) a ↔ ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), List.prod [] = a
Tactic: simp_rw [List.ofFn_zero, List.prod_nil, Fin.exists_fin_zero_pi, eq_comm, Set.mem_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
zero : Membership.mem (γ := Set α) (List.prod []) a ↔ ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), List.prod [] = a
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (↑(f i) : α)) = a
have zero₁ : Membership.mem (γ := Set α) 1 a ↔ ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), 1 = a
Tactic: simp_rw [List.ofFn_zero, List.prod_nil, Fin.exists_fin_zero_pi, eq_comm, Set.mem_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
zero : Membership.mem (γ := Set α) (List.prod []) a ↔ ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), List.prod [] = a
zero₁ : Membership.mem (γ := Set α) 1 a ↔ ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), 1 = a
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (↑(f i) : α)) = a
have zero₂ : Membership.mem (γ := Set α) 1 a ↔ 1 = a
Tactic: simp_rw [List.ofFn_zero, List.prod_nil, Fin.exists_fin_zero_pi, eq_comm, Set.mem_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
zero : Membership.mem (γ := Set α) (List.prod []) a ↔ ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), List.prod [] = a
zero₁ : Membership.mem (γ := Set α) 1 a ↔ ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), 1 = a
zero₂ : Membership.mem (γ := Set α) 1 a ↔ 1 = a
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (↑(f i) : α)) = a
have zero₃ : Membership.mem (γ := Set α) 1 a ↔ a = 1
Tactic: simp_rw [List.ofFn_zero, List.prod_nil, Fin.exists_fin_zero_pi, eq_comm, Set.mem_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
n_1 n : ℕ
ih :
  ∀ {a : α} {s : Fin n → Set α},
    a ∈ (List.ofFn s).prod ↔
      ∃ (f : (i : Fin n) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a
a : α
s : Fin (n + 1) → Set α
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (↑(f i) : α)) = a
have succ : a ∈ (s 0 :: List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ).prod ↔
  ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
    ((↑(f 0) : α) :: List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i.succ) : α)).prod = a
Tactic: simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ,
      mem_mul, @ih, exists_exists_eq_and, SetCoe.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
n_1 n : ℕ
ih :
  ∀ {a : α} {s : Fin n → Set α},
    a ∈ (List.ofFn s).prod ↔
      ∃ (f : (i : Fin n) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a
a : α
s : Fin (n + 1) → Set α
succ :
  a ∈ (s 0 :: List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ).prod ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      ((↑(f 0) : α) :: List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i.succ) : α)).prod = a
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (↑(f i) : α)) = a
have succ₁ : a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
  ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
    (↑(f 0) : α) * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i.succ) : α)) = a
Tactic: simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ,
      mem_mul, @ih, exists_exists_eq_and, SetCoe.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
n_1 n : ℕ
ih :
  ∀ {a : α} {s : Fin n → Set α},
    a ∈ (List.ofFn s).prod ↔
      ∃ (f : (i : Fin n) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a
a : α
s : Fin (n + 1) → Set α
succ :
  a ∈ (s 0 :: List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ).prod ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      ((↑(f 0) : α) :: List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i.succ) : α)).prod = a
succ₁ :
  a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      (↑(f 0) : α) * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i.succ) : α)) = a
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (↑(f i) : α)) = a
have succ₂ : a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
  ∃ (a_1 : (↑(s 0) : Type u_1)),
    ∃ (v : (i : Fin n) → (↑(s i.succ) : Type u_1)),
      HMul.hMul (α := α) (↑(Fin.cons (α := fun (i : Fin (n + 1)) ↦ (↑(s i) : Type u_1)) a_1 v 0) : α)
          (List.prod
            (List.ofFn (n := n) fun (i : Fin n) ↦
              (↑(Fin.cons (α := fun (i : Fin (n + 1)) ↦ (↑(s i) : Type u_1)) a_1 v i.succ) : α))) =
        a
Tactic: simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ,
      mem_mul, @ih, exists_exists_eq_and, SetCoe.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
n_1 n : ℕ
ih :
  ∀ {a : α} {s : Fin n → Set α},
    a ∈ (List.ofFn s).prod ↔
      ∃ (f : (i : Fin n) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a
a : α
s : Fin (n + 1) → Set α
succ :
  a ∈ (s 0 :: List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ).prod ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      ((↑(f 0) : α) :: List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i.succ) : α)).prod = a
succ₁ :
  a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      (↑(f 0) : α) * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i.succ) : α)) = a
succ₂ :
  a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
    ∃ (a_1 : (↑(s 0) : Type u_1)),
      ∃ (v : (i : Fin n) → (↑(s i.succ) : Type u_1)),
        HMul.hMul (α := α) (↑(Fin.cons (α := fun (i : Fin (n + 1)) ↦ (↑(s i) : Type u_1)) a_1 v 0) : α)
            (List.prod
              (List.ofFn (n := n) fun (i : Fin n) ↦
                (↑(Fin.cons (α := fun (i : Fin (n + 1)) ↦ (↑(s i) : Type u_1)) a_1 v i.succ) : α))) =
          a
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (↑(f i) : α)) = a
have succ₃ : a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
  ∃ (a_1 : (↑(s 0) : Type u_1)),
    ∃ (v : (i : Fin n) → (↑(s i.succ) : Type u_1)),
      (↑a_1 : α) *
          List.prod
            (List.ofFn (n := n) fun (i : Fin n) ↦
              (↑(Fin.cons (α := fun (i : Fin (n + 1)) ↦ (↑(s i) : Type u_1)) a_1 v i.succ) : α)) =
        a
Tactic: simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ,
      mem_mul, @ih, exists_exists_eq_and, SetCoe.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
n_1 n : ℕ
ih :
  ∀ {a : α} {s : Fin n → Set α},
    a ∈ (List.ofFn s).prod ↔
      ∃ (f : (i : Fin n) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a
a : α
s : Fin (n + 1) → Set α
succ :
  a ∈ (s 0 :: List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ).prod ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      ((↑(f 0) : α) :: List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i.succ) : α)).prod = a
succ₁ :
  a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      (↑(f 0) : α) * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i.succ) : α)) = a
succ₂ :
  a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
    ∃ (a_1 : (↑(s 0) : Type u_1)),
      ∃ (v : (i : Fin n) → (↑(s i.succ) : Type u_1)),
        HMul.hMul (α := α) (↑(Fin.cons (α := fun (i : Fin (n + 1)) ↦ (↑(s i) : Type u_1)) a_1 v 0) : α)
            (List.prod
              (List.ofFn (n := n) fun (i : Fin n) ↦
                (↑(Fin.cons (α := fun (i : Fin (n + 1)) ↦ (↑(s i) : Type u_1)) a_1 v i.succ) : α))) =
          a
succ₃ :
  a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
    ∃ (a_1 : (↑(s 0) : Type u_1)),
      ∃ (v : (i : Fin n) → (↑(s i.succ) : Type u_1)),
        (↑a_1 : α) *
            List.prod
              (List.ofFn (n := n) fun (i : Fin n) ↦
                (↑(Fin.cons (α := fun (i : Fin (n + 1)) ↦ (↑(s i) : Type u_1)) a_1 v i.succ) : α)) =
          a
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (↑(f i) : α)) = a
have succ₄ : a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
  ∃ (a_1 : (↑(s 0) : Type u_1)),
    ∃ (v : (i : Fin n) → (↑(s i.succ) : Type u_1)),
      (↑a_1 : α) * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(v i) : α)) = a
Tactic: simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ,
      mem_mul, @ih, exists_exists_eq_and, SetCoe.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
n_1 n : ℕ
ih :
  ∀ {a : α} {s : Fin n → Set α},
    a ∈ (List.ofFn s).prod ↔
      ∃ (f : (i : Fin n) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a
a : α
s : Fin (n + 1) → Set α
succ :
  a ∈ (s 0 :: List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ).prod ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      ((↑(f 0) : α) :: List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i.succ) : α)).prod = a
succ₁ :
  a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      (↑(f 0) : α) * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i.succ) : α)) = a
succ₂ :
  a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
    ∃ (a_1 : (↑(s 0) : Type u_1)),
      ∃ (v : (i : Fin n) → (↑(s i.succ) : Type u_1)),
        HMul.hMul (α := α) (↑(Fin.cons (α := fun (i : Fin (n + 1)) ↦ (↑(s i) : Type u_1)) a_1 v 0) : α)
            (List.prod
              (List.ofFn (n := n) fun (i : Fin n) ↦
                (↑(Fin.cons (α := fun (i : Fin (n + 1)) ↦ (↑(s i) : Type u_1)) a_1 v i.succ) : α))) =
          a
succ₃ :
  a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
    ∃ (a_1 : (↑(s 0) : Type u_1)),
      ∃ (v : (i : Fin n) → (↑(s i.succ) : Type u_1)),
        (↑a_1 : α) *
            List.prod
              (List.ofFn (n := n) fun (i : Fin n) ↦
                (↑(Fin.cons (α := fun (i : Fin (n + 1)) ↦ (↑(s i) : Type u_1)) a_1 v i.succ) : α)) =
          a
succ₄ :
  a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
    ∃ (a_1 : (↑(s 0) : Type u_1)),
      ∃ (v : (i : Fin n) → (↑(s i.succ) : Type u_1)),
        (↑a_1 : α) * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(v i) : α)) = a
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (↑(f i) : α)) = a
have succ₅ : (∃ (x : α),
    x ∈ s 0 ∧
      ∃ (y : α),
        Membership.mem (γ := Set α) (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ)) y ∧ x * y = a) ↔
  ∃ (a_1 : (↑(s 0) : Type u_1)),
    ∃ (v : (i : Fin n) → (↑(s i.succ) : Type u_1)),
      (↑a_1 : α) * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(v i) : α)) = a
Tactic: simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ,
      mem_mul, @ih, exists_exists_eq_and, SetCoe.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
n_1 n : ℕ
ih :
  ∀ {a : α} {s : Fin n → Set α},
    a ∈ (List.ofFn s).prod ↔
      ∃ (f : (i : Fin n) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a
a : α
s : Fin (n + 1) → Set α
succ :
  a ∈ (s 0 :: List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ).prod ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      ((↑(f 0) : α) :: List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i.succ) : α)).prod = a
succ₁ :
  a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      (↑(f 0) : α) * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i.succ) : α)) = a
succ₂ :
  a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
    ∃ (a_1 : (↑(s 0) : Type u_1)),
      ∃ (v : (i : Fin n) → (↑(s i.succ) : Type u_1)),
        HMul.hMul (α := α) (↑(Fin.cons (α := fun (i : Fin (n + 1)) ↦ (↑(s i) : Type u_1)) a_1 v 0) : α)
            (List.prod
              (List.ofFn (n := n) fun (i : Fin n) ↦
                (↑(Fin.cons (α := fun (i : Fin (n + 1)) ↦ (↑(s i) : Type u_1)) a_1 v i.succ) : α))) =
          a
succ₃ :
  a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
    ∃ (a_1 : (↑(s 0) : Type u_1)),
      ∃ (v : (i : Fin n) → (↑(s i.succ) : Type u_1)),
        (↑a_1 : α) *
            List.prod
              (List.ofFn (n := n) fun (i : Fin n) ↦
                (↑(Fin.cons (α := fun (i : Fin (n + 1)) ↦ (↑(s i) : Type u_1)) a_1 v i.succ) : α)) =
          a
succ₄ :
  a ∈ s 0 * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ) ↔
    ∃ (a_1 : (↑(s 0) : Type u_1)),
      ∃ (v : (i : Fin n) → (↑(s i.succ) : Type u_1)),
        (↑a_1 : α) * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(v i) : α)) = a
succ₅ :
  (∃ (x : α),
      x ∈ s 0 ∧
        ∃ (y : α),
          Membership.mem (γ := Set α) (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ s i.succ)) y ∧ x * y = a) ↔
    ∃ (a_1 : (↑(s 0) : Type u_1)),
      ∃ (v : (i : Fin n) → (↑(s i.succ) : Type u_1)),
        (↑a_1 : α) * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(v i) : α)) = a
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (↑(f i) : α)) = a
have succ₆ : (∃ (x : α),
    x ∈ s 0 ∧
      ∃ (y : α),
        (∃ (f : (i : Fin n) → (↑(s i.succ) : Type u_1)),
            List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = y) ∧
          x * y = a) ↔
  ∃ (a_1 : (↑(s 0) : Type u_1)),
    ∃ (v : (i : Fin n) → (↑(s i.succ) : Type u_1)),
      (↑a_1 : α) * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(v i) : α)) = a
Tactic: simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ,
      mem_mul, @ih, exists_exists_eq_and, SetCoe.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
n : ℕ
a : α
s : Fin n → Set α
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin n) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a
have zero : ∀ {a : α} {s : Fin 0 → Set α},
  a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (↑(f i) : α)) = a
Tactic: induction n generalizing a with
  | zero => simp_rw [List.ofFn_zero, List.prod_nil, Fin.exists_fin_zero_pi, eq_comm, Set.mem_one]
  | succ n ih =>
    simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ,
      mem_mul, @ih, exists_exists_eq_and, SetCoe.exists, exists_prop]
Cleared hypotheses: a, s
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
n : ℕ
a : α
s : Fin n → Set α
zero :
  ∀ {a : α} {s : Fin 0 → Set α},
    a ∈ (List.ofFn s).prod ↔
      ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (↑(f i) : α)) = a
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin n) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a
have succ : ∀ (n : ℕ)
  (ih :
    ∀ {a : α} {s : Fin n → Set α},
      a ∈ (List.ofFn s).prod ↔
        ∃ (f : (i : Fin n) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a)
  {a : α} {s : Fin (n + 1) → Set α},
  a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
      List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (↑(f i) : α)) = a
Tactic: induction n generalizing a with
  | zero => simp_rw [List.ofFn_zero, List.prod_nil, Fin.exists_fin_zero_pi, eq_comm, Set.mem_one]
  | succ n ih =>
    simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ,
      mem_mul, @ih, exists_exists_eq_and, SetCoe.exists, exists_prop]
Cleared hypotheses: a, s