awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
a : β
ha : a ∈ s
b : β
hb : b ∈ t
obtain :
  ∀ (a : α) (ha : Membership.mem (α := β) s ((m : (a : α) → β) a : β)),
    Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
      ((fun (x1 x2 : β) ↦ x1 / x2) ((m : (a : α) → β) a) b)
⊢ Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)) ((fun (x1 x2 : β) ↦ x1 / x2) a b)

Tactic:
obtain ⟨a, rfl⟩ := hs ha

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
b : β
hb : b ∈ t
a : α
ha : Membership.mem (α := β) s ((m : (a : α) → β) a : β)
obtain :
  ∀ (b : α) (hb : Membership.mem (α := β) t ((m : (a : α) → β) b : β)),
    Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
      ((fun (x1 x2 : β) ↦ x1 / x2) ((m : (a : α) → β) a) ((m : (a : α) → β) b))
⊢ Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
    ((fun (x1 x2 : β) ↦ x1 / x2) ((m : (a : α) → β) a) b)

Tactic:
obtain ⟨b, rfl⟩ := ht hb

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
a : α
ha : Membership.mem (α := β) s ((m : (a : α) → β) a : β)
b : α
hb : Membership.mem (α := β) t ((m : (a : α) → β) b : β)
⊢ Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
    ((fun (x1 x2 : β) ↦ x1 / x2) ((m : (a : α) → β) a) ((m : (a : α) → β) b))

Tactic:
⟨a / b, map_div ..⟩

Premises used: Set.Mem, setOf, HDiv.hDiv, Exists.intro, Set.range, map_div
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
a : α
ha : Membership.mem (α := β) s ((m : (a : α) → β) a : β)
b : α
hb : Membership.mem (α := β) t ((m : (a : α) → β) b : β)
⊢ Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
    ((fun (x1 x2 : β) ↦ x1 / x2) ((m : (a : α) → β) a) ((m : (a : α) → β) b))

Tactic:
exact ⟨a / b, map_div ..⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
s t : Set β
w : α
left : Membership.mem (γ := Set α) ((⇑m : (a : α) → β) ⁻¹' s) w
w_1 : α
left_1 : Membership.mem (γ := Set α) ((⇑m : (a : α) → β) ⁻¹' t) w_1
⊢ Membership.mem (γ := Set α) ((⇑m : (a : α) → β) ⁻¹' (s / t)) ((fun (x1 x2 : α) ↦ x1 / x2) w w_1)

Tactic:
⟨_, ‹_›, _, ‹_›, (map_div m ..).symm⟩

Premises used: Set.Mem, setOf, Set.preimage, Set.image2, And.intro, Exists.intro, Eq.symm, map_div
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
s t : Set β
w : α
left : Membership.mem (γ := Set α) ((⇑m : (a : α) → β) ⁻¹' s) w
w_1 : α
left_1 : Membership.mem (γ := Set α) ((⇑m : (a : α) → β) ⁻¹' t) w_1
⊢ Membership.mem (γ := Set α) ((⇑m : (a : α) → β) ⁻¹' (s / t)) ((fun (x1 x2 : α) ↦ x1 / x2) w w_1)

Tactic:
exact ⟨_, ‹_›, _, ‹_›, (map_div m ..).symm⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
hm : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑m : (a : α) → β)
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
rw :
  image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)) =
    HDiv.hDiv (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' s))
      (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t))
rw₁ :
  image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)) =
    s / image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t)
rw₂ : image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)) = s / t
rw₃ rw₄ : s / t = s / t
⊢ Eq.{u_3 + 1} (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)))
    ((⇑m : (a : α) → β) '' HDiv.hDiv (α := Set α) ((⇑m : (a : α) → β) ⁻¹' s) ((⇑m : (a : α) → β) ⁻¹' t))

Tactic:
rw [image_div, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (div_subset_range m hs ht)]

Premises used: Iff.mpr, Set.div_subset_range, Set.image_div, Set.image_preimage_eq_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → Inv (α i)
s : Set ι
t : (i : ι) → Set (α i)
h :
  ∀ (x : (i : ι) → α i),
    x ∈ (s.pi (α := α) t)⁻¹ ↔ Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ (t i)⁻¹) x
⊢ (s.pi (α := α) t)⁻¹ = s.pi (α := α) fun (i : ι) ↦ (t i)⁻¹

Tactic:
ext x
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → Inv (α i)
s : Set ι
t : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ x ∈ (s.pi (α := α) t)⁻¹ ↔ Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ (t i)⁻¹) x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Mul β
A : Set α
B₁ B₂ : Set β
f₁ f₂ : α → β
h₁ : MapsTo f₁ A B₁
h₂ : MapsTo f₂ A B₂
⊢ MapsTo (f₁ * f₂) A (B₁ * B₂)

Tactic:
fun _ h => mul_mem_mul (h₁ h) (h₂ h)

Premises used: Set.Mem, Set.MapsTo, Set.mul_mem_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : InvolutiveInv β
A : Set α
B : Set β
f : α → β
h : MapsTo f A B
⊢ MapsTo f⁻¹ A B⁻¹

Tactic:
fun _ ha => inv_mem_inv.2 (h ha)

Premises used: Iff.mpr, Set.Mem, Set.inv_mem_inv, Set.MapsTo
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Div β
A : Set α
B₁ B₂ : Set β
f₁ f₂ : α → β
h₁ : MapsTo f₁ A B₁
h₂ : MapsTo f₂ A B₂
⊢ MapsTo (f₁ / f₂) A (B₁ / B₂)

Tactic:
fun _ ha => div_mem_div (h₁ ha) (h₂ ha)

Premises used: Set.Mem, Set.div_mem_div, Set.MapsTo
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
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))
rw₄ 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))
⊢ Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (a :: as).prod)
    (List.prod (List.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) (a :: as)))

Tactic:
rw [List.map_cons, List.prod_cons, List.prod_cons, image_mul, image_list_prod _ _]

Premises used: List.map_cons, Set.image_mul, List.prod_cons
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : FunLike F α β
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : MonoidHomClass F α β
f : F
⊢ ∀ (a : List (Set α)),
    Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' Multiset.prod ⟦a⟧)
      (Multiset.prod (Multiset.map (fun (s : Set α) ↦ (⇑f : (a : α) → β) '' s) ⟦a⟧))

Tactic:
simpa only [Multiset.quot_mk_to_coe, Multiset.prod_coe, Multiset.map_coe] using
      image_list_prod f

Premises used: Multiset.quot_mk_to_coe, Set.image_list_prod, Multiset.map_coe, Multiset.prod_coe
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst : FunLike F α β
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : MonoidHomClass F α β
f : F
m : Finset ι
s : ι → Set α
⊢ Eq.{u_3 + 1} (α := Set β) (image.{u_2, u_3} (α := α) (⇑f : (a : α) → β) (∏ i ∈ m, s i))
    (∏ i ∈ m, (⇑f : (a : α) → β) '' s i)

Tactic:
(image_multiset_prod f _).trans <| congr_arg Multiset.prod <| Multiset.map_map _ _ _

Premises used: Multiset.prod, Set.image_multiset_prod, Finset.prod, congr_arg, Multiset.map_map, Eq.trans
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
a : α
empty : a = 1 ↔ ∃ (g : ι → α) (_ : ∀ {i : ι}, Membership.mem (γ := Finset ι) ∅ i → g i ∈ f i), 1 = a
⊢ Membership.mem (γ := Set α) (∏ i ∈ ∅, f i) a ↔
    ∃ (g : ι → α) (_ : ∀ {i : ι}, Membership.mem (γ := Finset ι) ∅ i → g i ∈ f i), ∏ i ∈ ∅, g i = a

Tactic:
simp_rw [Finset.prod_empty, Set.mem_one]

Premises used: Finset.prod_empty, Set.mem_one
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
a : α
⊢ a = 1 ↔ ∃ (g : ι → α) (_ : ∀ {i : ι}, Membership.mem (γ := Finset ι) ∅ i → g i ∈ f i), 1 = a

Tactic:
⟨fun h ↦ ⟨fun _ ↦ a, fun hi ↦ False.elim (Finset.notMem_empty _ hi), h.symm⟩,
        fun ⟨_, _, hf⟩ ↦ hf.symm⟩

Premises used: False.elim, _private.0.Set.mem_finsetProd.match_1, Finset.notMem_empty, Iff.intro, Exists.intro, OfNat.ofNat, Eq.symm, Eq
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
a : α
⊢ a = 1 ↔ ∃ (g : ι → α) (_ : ∀ {i : ι}, Membership.mem (γ := Finset ι) ∅ i → g i ∈ f i), 1 = a

Tactic:
exact ⟨fun h ↦ ⟨fun _ ↦ a, fun hi ↦ False.elim (Finset.notMem_empty _ hi), h.symm⟩,
        fun ⟨_, _, hf⟩ ↦ hf.symm⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
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

Tactic:
?_
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
t : Finset ι
f : ι → Set α
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 : α),
    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

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 => ?_

Premises used: Finset.prod_empty, Set.mem_one, Insert.insert
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
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 : α), 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 ∈ 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

Tactic:
rw [Finset.prod_insert hi, Set.mem_mul]

Premises used: Finset.prod_insert, Set.mem_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
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 : α), 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
⊢ (∃ 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:
simp_rw [Finset.prod_insert hi]

Premises used: Finset.prod_insert
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
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 : α), 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:
simp_rw [ih]
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
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
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
⊢ (∃ 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:
constructor
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
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

Tactic:
⟨Function.update g i x, ?_, ?_⟩

Premises used: Function.update, Exists.intro
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
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
insert₁ :
  update (β := fun (a : ι) ↦ α) g i x i * ∏ i_1 ∈ is, update (β := fun (a : ι) ↦ α) g i x i_1 = x * ∏ i ∈ is, g i
⊢ ∃ (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

Tactic:
refine ⟨Function.update g i x, ?_, ?_⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
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
insert₁ : ∀ (hj : j ∈ is), update (β := fun (a : ι) ↦ α) g i x j ∈ f j
⊢ update (β := fun (a : ι) ↦ α) g i x j ∈ f j

Tactic:
obtain rfl | hj := Finset.mem_insert.mp hj

Premises used: Finset.mem_insert, Iff.mp, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
is : Finset ι
ih :
  ∀ (a : α),
    Membership.mem (γ := Set α) (∏ i ∈ is, f i) a ↔ ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hi : j ∉ is
y : x ∈ f j
hj : j ∈ Insert.insert j is
insert insert₁ insert₂ insert₃ : x ∈ f j
⊢ update (β := fun (a : ι) ↦ α) g j x j ∈ f j

Tactic:
rwa [Function.update_self]

Premises used: Function.update_self
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
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.insert i is
hj : j ∈ is
insert : g j ∈ f j
⊢ update (β := fun (a : ι) ↦ α) g i x j ∈ f j

Tactic:
rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]

Premises used: ne_of_mem_of_not_mem, Function.update_of_ne
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
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
⊢ g j ∈ f j

Tactic:
hg hj
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
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
⊢ g j ∈ f j

Tactic:
exact hg hj
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
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
insert₁ insert₂ : x * ∏ 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

Tactic:
rw [Finset.prod_update_of_notMem hi, Function.update_self]

Premises used: Finset.prod_update_of_notMem, Function.update_self
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
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
g : ι → α
hg : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1
⊢ ∃ x ∈ f i,
    ∃ (y : α), (∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = g i * ∏ i ∈ is, g i

Tactic:
⟨g i, hg (is.mem_insert_self _), is.prod g,
        ⟨⟨g, fun hi ↦ hg (Finset.mem_insert_of_mem hi), rfl⟩, rfl⟩⟩

Premises used: Finset.mem_insert_self, Finset.prod, Finset.mem_insert_of_mem, And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
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
g : ι → α
hg : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1
⊢ ∃ x ∈ f i,
    ∃ (y : α), (∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = g i * ∏ i ∈ is, g i

Tactic:
exact ⟨g i, hg (is.mem_insert_self _), is.prod g,
        ⟨⟨g, fun hi ↦ hg (Finset.mem_insert_of_mem hi), rfl⟩, rfl⟩⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
α : Type u_2
inst : CommMonoid α
n : ℕ
s : Set α
a : α
⊢ a ∈ s ^ n ↔ ∃ (f : Fin n → α), (∀ (i : Fin n), f i ∈ s) ∧ ∏ i : Fin n, f i = a

Tactic:
simpa using mem_finsetProd (t := .univ) (f := fun _ : Fin n ↦ s) _

Premises used: Finset.univ, Set.mem_finsetProd
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Fintype ι
f : ι → Set α
a : α
rw :
  (∃ (g : ι → α) (_ : ∀ {i : ι}, Membership.mem (γ := Finset ι) Finset.univ i → g i ∈ f i), ∏ i : ι, g i = a) ↔
    ∃ (g : ι → α) (_ : ∀ (i : ι), g i ∈ f i), ∏ i : ι, g i = a
⊢ Membership.mem (γ := Set α) (∏ i : ι, f i) a ↔ ∃ (g : ι → α) (_ : ∀ (i : ι), g i ∈ f i), ∏ i : ι, g i = a

Tactic:
rw [mem_finsetProd]

Premises used: Set.mem_finsetProd
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Fintype ι
f : ι → Set α
a : α
⊢ (∃ (g : ι → α) (_ : ∀ {i : ι}, Membership.mem (γ := Finset ι) Finset.univ i → g i ∈ f i), ∏ i : ι, g i = a) ↔
    ∃ (g : ι → α) (_ : ∀ (i : ι), g i ∈ f i), ∏ i : ι, g i = a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
g : ι → α
hg : ∀ (i : ι), Membership.mem (γ := List ι) [] i → g i ∈ f i
nil : Membership.mem (γ := Set α) (List.prod []) (List.prod [])
nil₁ : Membership.mem (γ := Set α) 1 1
⊢ (List.map g []).prod ∈ (List.map f []).prod

Tactic:
simp_rw [List.map_nil, List.prod_nil, Set.mem_one]

Premises used: Set.mem_one, List.prod_nil, List.map_nil
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
g : ι → α
h : ι
tl : List ι
ih : ∀ (hg : ∀ i ∈ tl, g i ∈ f i), (List.map g tl).prod ∈ (List.map f tl).prod
hg : ∀ i ∈ h :: tl, g i ∈ f i
cons : g h * (List.map g tl).prod ∈ f h * (List.map f tl).prod
⊢ (List.map g (h :: tl)).prod ∈ (List.map f (h :: tl)).prod

Tactic:
simp_rw [List.map_cons, List.prod_cons]

Premises used: List.map_cons, List.prod_cons