-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
t : Finset ι
f : ι → Set α
a : α
empty :
  ∀ (a : α),
    Membership.mem (γ := Set α) (∏ i ∈ ∅, f i) a ↔
      ∃ (g : ι → α) (_ : ∀ {i : ι}, Membership.mem (γ := Finset ι) ∅ i → g i ∈ f i), ∏ i ∈ ∅, g i = a
insert insert₁ :
  ∀ (i : ι) (is : Finset ι) (hi : i ∉ is)
    (ih :
      ∀ (a : α),
        Membership.mem (γ := Set α) (∏ i ∈ is, f i) a ↔
          ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a)
    (a : α),
    Membership.mem (γ := Set α) (∏ i ∈ Insert.insert i is, f i) a ↔
      ∃ (g : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ Insert.insert i is → g i_1 ∈ f i_1), ∏ i ∈ Insert.insert i is, g i = a
insert₂ :
  ∀ (i : ι) (is : Finset ι) (hi : i ∉ is)
    (ih :
      ∀ (a : α),
        Membership.mem (γ := Set α) (∏ i ∈ is, f i) a ↔
          ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a)
    (a : α),
    (∃ x ∈ f i, ∃ (y : α), Membership.mem (γ := Set α) (∏ x ∈ is, f x) y ∧ x * y = a) ↔
      ∃ (g : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ Insert.insert i is → g i_1 ∈ f i_1), ∏ i ∈ Insert.insert i is, g i = a
insert₃ :
  ∀ (i : ι) (is : Finset ι) (hi : i ∉ is)
    (ih :
      ∀ (a : α),
        Membership.mem (γ := Set α) (∏ i ∈ is, f i) a ↔
          ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a)
    (a : α),
    (∃ x ∈ f i, ∃ (y : α), Membership.mem (γ := Set α) (∏ x ∈ is, f x) y ∧ x * y = a) ↔
      ∃ (g : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ Insert.insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a
insert₄ :
  ∀ (i : ι) (is : Finset ι) (hi : i ∉ is)
    (ih :
      ∀ (a : α),
        Membership.mem (γ := Set α) (∏ i ∈ is, f i) a ↔
          ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a)
    (a : α),
    (∃ x ∈ f i, ∃ (y : α), (∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a) ↔
      ∃ (g : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ Insert.insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a
⊢ Membership.mem (γ := Set α) (∏ i ∈ t, f i) a ↔ ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ t → g i ∈ f i), ∏ i ∈ t, g i = a
have insert₅ : ∀ (i : ι) (is : Finset ι) (hi : i ∉ is)
  (ih :
    ∀ (a : α),
      Membership.mem (γ := Set α) (∏ i ∈ is, f i) a ↔
        ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a)
  (a : α),
  (∃ x ∈ f i, ∃ (y : α), (∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a) →
    ∃ (g : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ Insert.insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a
Tactic: classical
    induction t using Finset.induction_on generalizing a with
    | empty =>
      simp_rw [Finset.prod_empty, Set.mem_one]
      exact ⟨fun h ↦ ⟨fun _ ↦ a, fun hi ↦ False.elim (Finset.notMem_empty _ hi), h.symm⟩,
        fun ⟨_, _, hf⟩ ↦ hf.symm⟩
    | insert i is hi ih => ?_
    rw [Finset.prod_insert hi, Set.mem_mul]
    simp_rw [Finset.prod_insert hi]
    simp_rw [ih]
    constructor
    · rintro ⟨x, y, hx, ⟨g, hg, rfl⟩, rfl⟩
      refine ⟨Function.update g i x, ?_, ?_⟩
      · intro j hj
        obtain rfl | hj := Finset.mem_insert.mp hj
        · rwa [Function.update_self]
        · rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
          exact hg hj
      · rw [Finset.prod_update_of_notMem hi, Function.update_self]
    · rintro ⟨g, hg, rfl⟩
      exact ⟨g i, hg (is.mem_insert_self _), is.prod g,
        ⟨⟨g, fun hi ↦ hg (Finset.mem_insert_of_mem hi), rfl⟩, rfl⟩⟩
Cleared hypotheses: t, a