-- 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
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
⊢ 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 ∧
      ∃ (a_1 : (i : Fin n) → (↑(s i.succ) : Type u_1)),
        x * List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(a_1 i) : α)) = 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]