awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → Inv (α i)
s : Set ι
t : (i : ι) → Set (α i)
⊢ (s.pi (α := α) t)⁻¹ = s.pi (α := α) fun (i : ι) ↦ (t i)⁻¹
have h : ∀ (x : (i : ι) → α i),
  x ∈ (s.pi (α := α) t)⁻¹ ↔ Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ (t i)⁻¹) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : FunLike F α β
inst_1 : Monoid α
inst_2 : Monoid β
inst_3 : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
⊢ Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (a :: as).prod)
    (List.prod (List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) (a :: as)))
have rw : Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (a :: as).prod)
  (List.prod ((⇑f : (a : α) → β) '' a :: List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as))
Tactic: rw [List.map_cons, List.prod_cons, List.prod_cons, image_mul, image_list_prod _ _]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : FunLike F α β
inst_1 : Monoid α
inst_2 : Monoid β
inst_3 : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
rw :
  Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (a :: as).prod)
    (List.prod ((⇑f : (a : α) → β) '' a :: List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as))
⊢ Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (a :: as).prod)
    (List.prod (List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) (a :: as)))
have rw₁ : Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (a * as.prod))
  (List.prod ((⇑f : (a : α) → β) '' a :: List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as))
Tactic: rw [List.map_cons, List.prod_cons, List.prod_cons, image_mul, image_list_prod _ _]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : FunLike F α β
inst_1 : Monoid α
inst_2 : Monoid β
inst_3 : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
rw :
  Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (a :: as).prod)
    (List.prod ((⇑f : (a : α) → β) '' a :: List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as))
rw₁ :
  Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (a * as.prod))
    (List.prod ((⇑f : (a : α) → β) '' a :: List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as))
⊢ Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (a :: as).prod)
    (List.prod (List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) (a :: as)))
have rw₂ : (⇑f : (a : α) → β) '' (a * as.prod) =
  HMul.hMul (α := Set β) ((⇑f : (a : α) → β) '' a) (List.prod (List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as))
Tactic: rw [List.map_cons, List.prod_cons, List.prod_cons, image_mul, image_list_prod _ _]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : FunLike F α β
inst_1 : Monoid α
inst_2 : Monoid β
inst_3 : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
rw :
  Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (a :: as).prod)
    (List.prod ((⇑f : (a : α) → β) '' a :: List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as))
rw₁ :
  Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (a * as.prod))
    (List.prod ((⇑f : (a : α) → β) '' a :: List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as))
rw₂ :
  (⇑f : (a : α) → β) '' (a * as.prod) =
    HMul.hMul (α := Set β) ((⇑f : (a : α) → β) '' a)
      (List.prod (List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as))
⊢ Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (a :: as).prod)
    (List.prod (List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) (a :: as)))
have rw₃ : HMul.hMul (α := Set β) ((⇑f : (a : α) → β) '' a) ((⇑f : (a : α) → β) '' as.prod) =
  HMul.hMul (α := Set β) ((⇑f : (a : α) → β) '' a) (List.prod (List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as))
Tactic: rw [List.map_cons, List.prod_cons, List.prod_cons, image_mul, image_list_prod _ _]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : FunLike F α β
inst_1 : Monoid α
inst_2 : Monoid β
inst_3 : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
rw :
  Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (a :: as).prod)
    (List.prod ((⇑f : (a : α) → β) '' a :: List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as))
rw₁ :
  Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (a * as.prod))
    (List.prod ((⇑f : (a : α) → β) '' a :: List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as))
rw₂ :
  (⇑f : (a : α) → β) '' (a * as.prod) =
    HMul.hMul (α := Set β) ((⇑f : (a : α) → β) '' a)
      (List.prod (List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as))
rw₃ :
  HMul.hMul (α := Set β) ((⇑f : (a : α) → β) '' a) ((⇑f : (a : α) → β) '' as.prod) =
    HMul.hMul (α := Set β) ((⇑f : (a : α) → β) '' a)
      (List.prod (List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as))
⊢ Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (a :: as).prod)
    (List.prod (List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) (a :: as)))
have rw₄ : HMul.hMul (α := Set β) ((⇑f : (a : α) → β) '' a) (List.prod (List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as)) =
  HMul.hMul (α := Set β) ((⇑f : (a : α) → β) '' a) (List.prod (List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) as))
Tactic: rw [List.map_cons, List.prod_cons, List.prod_cons, image_mul, image_list_prod _ _]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
a : α
⊢ Membership.mem (γ := Set α) (∏ i ∈ ∅, f i) a ↔
    ∃ (g : ι → α) (_ : ∀ {i : ι}, Membership.mem (γ := Finset ι) ∅ i → g i ∈ f i), ∏ i ∈ ∅, g i = a
have empty : a = 1 ↔ ∃ (g : ι → α) (_ : ∀ {i : ι}, Membership.mem (γ := Finset ι) ∅ i → g i ∈ f i), 1 = a
Tactic: simp_rw [Finset.prod_empty, Set.mem_one]
-- 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 : α
⊢ 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 : α),
  Membership.mem (γ := Set α) (∏ i ∈ insert i is, f i) a ↔
    ∃ (g : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), ∏ i ∈ insert i is, g i = a
Tactic: 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 => ?_
Cleared hypotheses: t, a
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
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 i is, f i) a ↔
    ∃ (g : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), ∏ i ∈ insert i is, g i = a
have insert : (∃ x ∈ f i, ∃ (y : α), Membership.mem (γ := Set α) (∏ x ∈ is, f x) y ∧ x * y = a) ↔
  ∃ (g : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), ∏ i ∈ insert i is, g i = a
Tactic: rw [Finset.prod_insert hi, Set.mem_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
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 i is → g i_1 ∈ f i_1), ∏ i ∈ insert i is, g i = a
have insert : (∃ x ∈ f i, ∃ (y : α), Membership.mem (γ := Set α) (∏ x ∈ is, f x) y ∧ x * y = a) ↔
  ∃ (g : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a
Tactic: simp_rw [Finset.prod_insert hi]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
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 i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a
have insert : (∃ 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 i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a
Tactic: simp_rw [ih]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
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 i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a
have insert : (∃ 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 i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
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 : α
insert :
  (∃ 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
⊢ (∃ 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
have insert₁ : (∃ (g : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ Insert.insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a) →
  ∃ x ∈ f i, ∃ (y : α), (∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
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
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ ∃ (g_1 : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g_1 i_1 ∈ f i_1), g_1 i * ∏ i ∈ is, g_1 i = x * ∏ i ∈ is, g i
have insert : ∀ {i_1 : ι}, i_1 ∈ insert i is → update (β := fun (a : ι) ↦ α) g i x i_1 ∈ f i_1
Tactic: refine ⟨Function.update g i x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
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
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
insert : ∀ {i_1 : ι}, i_1 ∈ Insert.insert i is → update (β := fun (a : ι) ↦ α) g i x i_1 ∈ f i_1
⊢ ∃ (g_1 : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ Insert.insert i is → g_1 i_1 ∈ f i_1),
    g_1 i * ∏ i ∈ is, g_1 i = x * ∏ i ∈ is, g i
have insert₁ : update (β := fun (a : ι) ↦ α) g i x i * ∏ i_1 ∈ is, update (β := fun (a : ι) ↦ α) g i x i_1 = x * ∏ i ∈ is, g i
Tactic: refine ⟨Function.update g i x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
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
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hj : j ∈ insert i is
⊢ update (β := fun (a : ι) ↦ α) g i x j ∈ f j
have insert : ∀ (hi : j ∉ is) (y : x ∈ f j) (hj : j ∈ insert j is), update (β := fun (a : ι) ↦ α) g j x j ∈ f j
Tactic: obtain rfl | hj := Finset.mem_insert.mp hj
Cleared hypotheses: i, hi, y, hj
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
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
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hj : j ∈ Insert.insert i is
insert : ∀ (hi : j ∉ is) (y : x ∈ f j) (hj : j ∈ Insert.insert j is), update (β := fun (a : ι) ↦ α) g j x j ∈ f j
⊢ update (β := fun (a : ι) ↦ α) g i x j ∈ f j
have insert₁ : ∀ (hj : j ∈ is), update (β := fun (a : ι) ↦ α) g i x j ∈ f j
Tactic: obtain rfl | hj := Finset.mem_insert.mp hj
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
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
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hj_1 : j ∈ insert i is
hj : j ∈ is
⊢ update (β := fun (a : ι) ↦ α) g i x j ∈ f j
have insert : g j ∈ f j
Tactic: rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
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
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ update (β := fun (a : ι) ↦ α) g i x i * ∏ i_1 ∈ is, update (β := fun (a : ι) ↦ α) g i x i_1 = x * ∏ i ∈ is, g i
have insert : update (β := fun (a : ι) ↦ α) g i x i * ∏ x ∈ is, g x = x * ∏ i ∈ is, g i
Tactic: rw [Finset.prod_update_of_notMem hi, Function.update_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
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
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
insert : update (β := fun (a : ι) ↦ α) g i x i * ∏ x ∈ is, g x = x * ∏ i ∈ is, g i
⊢ update (β := fun (a : ι) ↦ α) g i x i * ∏ i_1 ∈ is, update (β := fun (a : ι) ↦ α) g i x i_1 = x * ∏ i ∈ is, g i
have insert₁ : x * ∏ x ∈ is, g x = x * ∏ i ∈ is, g i
Tactic: rw [Finset.prod_update_of_notMem hi, Function.update_self]
-- 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 : α
⊢ Membership.mem (γ := Set α) (∏ i ∈ t, f i) a ↔ ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ t → g i ∈ f i), ∏ i ∈ t, g i = a
have empty : ∀ (a : α),
  Membership.mem (γ := Set α) (∏ i ∈ ∅, f i) a ↔
    ∃ (g : ι → α) (_ : ∀ {i : ι}, Membership.mem (γ := Finset ι) ∅ i → g i ∈ f i), ∏ i ∈ ∅, 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
-- 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
⊢ 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 : α),
  Membership.mem (γ := Set α) (∏ i ∈ insert i is, f i) a ↔
    ∃ (g : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), ∏ i ∈ insert 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
-- 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
⊢ 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 : α), 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
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
-- 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
⊢ 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 : α), 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
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