awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ Eq.{u_1 + 1} (α := M) 1 (Finsupp.prod 0 fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x_1 x y : M
hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) x
hy : Membership.mem (γ := Submonoid M) (closure (Set.range f)) y
hx' : ∃ (a : ι →₀ ℕ), x = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2
hy' : ∃ (a : ι →₀ ℕ), y = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2
mul :
  ∀ (v : ι →₀ ℕ)
    (hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2))
    (hx' :
      ∃ (a : ι →₀ ℕ),
        Eq.{u_1 + 1} (α := M) (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2))
    (w : ι →₀ ℕ)
    (hy : Membership.mem (γ := Submonoid M) (closure (Set.range f)) (w.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2))
    (hy' :
      ∃ (a : ι →₀ ℕ),
        Eq.{u_1 + 1} (α := M) (w.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)),
    ∃ (a : ι →₀ ℕ),
      HMul.hMul (α := M) (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (w.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) =
        a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2
⊢ ∃ (a : ι →₀ ℕ), x * y = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2

Tactic:
obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'

Premises used: And.intro, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
hx' :
  ∃ (a : ι →₀ ℕ),
    Eq.{u_1 + 1} (α := M) (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
w : ι →₀ ℕ
hy : Membership.mem (γ := Submonoid M) (closure (Set.range f)) (w.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
hy' :
  ∃ (a : ι →₀ ℕ),
    Eq.{u_1 + 1} (α := M) (w.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
h :
  HMul.hMul (α := M) (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (w.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) =
    (v + w).prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2
⊢ ∃ (a : ι →₀ ℕ),
    HMul.hMul (α := M) (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (w.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) =
      a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2

Tactic:
use v + w
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
hx' :
  ∃ (a : ι →₀ ℕ),
    Eq.{u_1 + 1} (α := M) (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
w : ι →₀ ℕ
hy : Membership.mem (γ := Submonoid M) (closure (Set.range f)) (w.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
hy' :
  ∃ (a : ι →₀ ℕ),
    Eq.{u_1 + 1} (α := M) (w.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
h : ∀ a ∈ v.support ∪ w.support, HPow.hPow (β := ℕ) (f a) 0 = 1
h₁ : ∀ a ∈ v.support ∪ w.support, ∀ (b₁ b₂ : ℕ), f a ^ (b₁ + b₂) = f a ^ b₁ * f a ^ b₂
⊢ HMul.hMul (α := M) (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (w.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) =
    (v + w).prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2

Tactic:
rw [Finsupp.prod_add_index]

Premises used: Finsupp.prod_add_index
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
hx' :
  ∃ (a : ι →₀ ℕ),
    Eq.{u_1 + 1} (α := M) (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
w : ι →₀ ℕ
hy : Membership.mem (γ := Submonoid M) (closure (Set.range f)) (w.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
hy' :
  ∃ (a : ι →₀ ℕ),
    Eq.{u_1 + 1} (α := M) (w.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
⊢ ∀ a ∈ v.support ∪ w.support, HPow.hPow (β := ℕ) (f a) 0 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
hx' :
  ∃ (a : ι →₀ ℕ),
    Eq.{u_1 + 1} (α := M) (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
w : ι →₀ ℕ
hy : Membership.mem (γ := Submonoid M) (closure (Set.range f)) (w.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
hy' :
  ∃ (a : ι →₀ ℕ),
    Eq.{u_1 + 1} (α := M) (w.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
⊢ ∀ a ∈ v.support ∪ w.support, ∀ (b₁ b₂ : ℕ), f a ^ (b₁ + b₂) = f a ^ b₁ * f a ^ b₂

Tactic:
simp [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) x
mem : ∀ (x : M) (h : x ∈ Set.range f), ∃ (a : ι →₀ ℕ), x = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2
one : ∃ (a : ι →₀ ℕ), Eq.{u_1 + 1} (α := M) 1 (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) x)
    (hy : Membership.mem (γ := Submonoid M) (closure (Set.range f)) y)
    (hx' : ∃ (a : ι →₀ ℕ), x = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
    (hy' : ∃ (a : ι →₀ ℕ), y = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2),
    ∃ (a : ι →₀ ℕ), x * y = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2
⊢ ∃ (a : ι →₀ ℕ), x = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2

Tactic:
induction hx using closure_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; exact ⟨Finsupp.single i 1, by simp⟩
  | one => use 0; simp
  | mul x y hx hy hx' hy' =>
    obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'
    use v + w
    rw [Finsupp.prod_add_index]
    · simp
    · simp [pow_add]

Premises used: Submonoid.mul, Finsupp.prod_add_index, pow_add, Submonoid.one, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) x
mem : ∀ (x : M) (h : x ∈ Set.range f), ∃ (a : ι →₀ ℕ), x = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2
one : ∃ (a : ι →₀ ℕ), Eq.{u_1 + 1} (α := M) 1 (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) x)
    (hy : Membership.mem (γ := Submonoid M) (closure (Set.range f)) y)
    (hx' : ∃ (a : ι →₀ ℕ), x = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
    (hy' : ∃ (a : ι →₀ ℕ), y = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2),
    ∃ (a : ι →₀ ℕ), x * y = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2
⊢ ∃ (a : ι →₀ ℕ), x = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2

Tactic:
classical
  induction hx using closure_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; exact ⟨Finsupp.single i 1, by simp⟩
  | one => use 0; simp
  | mul x y hx hy hx' hy' =>
    obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'
    use v + w
    rw [Finsupp.prod_add_index]
    · simp
    · simp [pow_add]

Premises used: Submonoid.mul, Finsupp.prod_add_index, pow_add, Submonoid.one, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst_1 : Fintype ι
hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) x
obtain :
  ∀ (a : ι →₀ ℕ)
    (hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)),
    ∃ (a_1 : ι → ℕ), Eq.{u_1 + 1} (α := M) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (∏ i : ι, f i ^ a_1 i)
⊢ ∃ (a : ι → ℕ), x = ∏ i : ι, f i ^ a i

Tactic:
obtain ⟨a, rfl⟩ := exists_finsupp_of_mem_closure_range f x hx

Premises used: Submonoid.exists_finsupp_of_mem_closure_range, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
inst_1 : Fintype ι
a : ι →₀ ℕ
hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
⊢ Eq.{u_1 + 1} (α := M) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
    (∏ i : ι, HPow.hPow (β := ℕ) (f i) ((a : (a : ι) → ℕ) i : ℕ))

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
inst_1 : Fintype ι
a : ι →₀ ℕ
hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)
⊢ ∃ (a_1 : ι → ℕ), Eq.{u_1 + 1} (α := M) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) (∏ i : ι, f i ^ a_1 i)

Tactic:
exact ⟨a, by simp⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ Membership.mem (γ := Submonoid M) (closure (Set.range f)) x ↔
    ∃ (a : ι →₀ ℕ), x = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2

Tactic:
⟨exists_finsupp_of_mem_closure_range f x, ?_⟩

Premises used: Submonoid.exists_finsupp_of_mem_closure_range, Iff.intro
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
refine :
  (∃ (a : ι →₀ ℕ), x = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) →
    Membership.mem (γ := Submonoid M) (closure (Set.range f)) x
⊢ Membership.mem (γ := Submonoid M) (closure (Set.range f)) x ↔
    ∃ (a : ι →₀ ℕ), x = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2

Tactic:
refine ⟨exists_finsupp_of_mem_closure_range f x, ?_⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
a : ι →₀ ℕ
⊢ Membership.mem (γ := Submonoid M) (closure (Set.range f)) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)

Tactic:
prod_mem _ fun i hi ↦ pow_mem (subset_closure (Set.mem_range_self i)) _

Premises used: Set.mem_range_self, Submonoid.prod_mem, Set.Mem, pow_mem, Submonoid.subset_closure, DFunLike.coe, Finsupp.prod
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
a : ι →₀ ℕ
⊢ Membership.mem (γ := Submonoid M) (closure (Set.range f)) (a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2)

Tactic:
exact prod_mem _ fun i hi ↦ pow_mem (subset_closure (Set.mem_range_self i)) _

Premises used: Set.mem_range_self, Submonoid.prod_mem, pow_mem, Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst_1 : Fintype ι
rw :
  (∃ (a : ι →₀ ℕ), x = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) ↔
    ∃ (b : ι →₀ ℕ),
      x =
        ∏ i : ι,
          HPow.hPow (β := ℕ) (f i) ((Equiv.symm (Equiv.symm Finsupp.equivFunOnFinite) : (a : ι →₀ ℕ) → ι → ℕ) b i)
⊢ Membership.mem (γ := Submonoid M) (closure (Set.range f)) x ↔ ∃ (a : ι → ℕ), x = ∏ i : ι, f i ^ a i

Tactic:
rw [Finsupp.equivFunOnFinite.symm.exists_congr_left, mem_closure_range_iff]

Premises used: Equiv.exists_congr_left, Finsupp.equivFunOnFinite, Submonoid.mem_closure_range_iff, Equiv.symm
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst_1 : Fintype ι
⊢ (∃ (a : ι →₀ ℕ), x = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2) ↔
    ∃ (b : ι →₀ ℕ),
      x =
        ∏ i : ι,
          HPow.hPow (β := ℕ) (f i) ((Equiv.symm (Equiv.symm Finsupp.equivFunOnFinite) : (a : ι →₀ ℕ) → ι → ℕ) b i)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
inst_1 : Fintype (↑s : Type u_1)
rw :
  Membership.mem (γ := Submonoid M)
    (closure (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) x
| Membership.mem (γ := Submonoid M) (closure s) x

Tactic:
rw [← Subtype.range_coe (s := s)]

Premises used: Subtype.range_coe
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
inst_1 : Fintype (↑s : Type u_1)
conv_lhs :
  Membership.mem (γ := Submonoid M)
      (closure (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) x ↔
    ∃ (a : (↑s : Type u_1) → ℕ), x = ∏ i : (↑s : Type u_1), (↑i : M) ^ a i
⊢ Membership.mem (γ := Submonoid M) (closure s) x ↔
    ∃ (a : (↑s : Type u_1) → ℕ), x = ∏ i : (↑s : Type u_1), (↑i : M) ^ a i

Tactic:
conv_lhs => rw [← Subtype.range_coe (s := s)]

Premises used: Subtype.range_coe
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
inst_1 : Fintype (↑s : Type u_1)
⊢ Membership.mem (γ := Submonoid M)
      (closure (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) x ↔
    ∃ (a : (↑s : Type u_1) → ℕ), x = ∏ i : (↑s : Type u_1), (↑i : M) ^ a i

Tactic:
mem_closure_range_iff_of_fintype

Premises used: Submonoid.mem_closure_range_iff_of_fintype
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
inst_1 : Fintype (↑s : Type u_1)
⊢ Membership.mem (γ := Submonoid M)
      (closure (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) x ↔
    ∃ (a : (↑s : Type u_1) → ℕ), x = ∏ i : (↑s : Type u_1), (↑i : M) ^ a i

Tactic:
exact mem_closure_range_iff_of_fintype

Premises used: Submonoid.mem_closure_range_iff_of_fintype
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Finset M
⊢ Membership.mem (γ := Submonoid M) (closure (↑s : Set M)) x ↔ ∃ (a : ↥s → ℕ), x = ∏ i : ↥s, (↑i : M) ^ a i

Tactic:
mem_closure_iff_of_fintype

Premises used: Submonoid.mem_closure_iff_of_fintype
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x : M
⊢ Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i

Tactic:
⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Premises used: iSup, Membership.mem, le_iSup, Iff.intro, _private.0.Submonoid.mem_iSup_of_directed.match_1
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x : M
refine : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
⊢ Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x : M
this : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x → ∃ (i : ι), x ∈ S i
⊢ Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i

Tactic:
simpa only [closure_iUnion, closure_eq (S _)] using this

Premises used: Submonoid.closure_eq, Submonoid.closure_iUnion
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x : M
suffices : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x → ∃ (i : ι), x ∈ S i
⊢ Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i

Tactic:
suffices x ∈ closure (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
    simpa only [closure_iUnion, closure_eq (S _)] using this
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x : M
hx : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
⊢ ∀ (x : M) (h : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x), ∃ (i : ι), x ∈ S i

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x : M
hx : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
⊢ ∃ (i : ι), 1 ∈ S i

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x : M
refine :
  ∀ (hx : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x) (x y : M)
    (hx : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x)
    (hy : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) y),
    (∃ (i : ι), x ∈ S i) → (∃ (i : ι), y ∈ S i) → ∃ (i : ι), x * y ∈ S i
⊢ Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x → ∃ (i : ι), x ∈ S i

Tactic:
refine fun hx ↦ closure_induction (by simp) (by simp) ?_ hx
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x_1 : M
hx : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x_1
x y : M
hx_1 : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
hy : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) y
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
obtain : ∀ (k : ι) (hik : S i ≤ S k) (hjk : S j ≤ S k), ∃ (i : ι), x * y ∈ S i
⊢ ∃ (i : ι), x * y ∈ S i

Tactic:
obtain ⟨k, hik, hjk⟩ := hS i j
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x_1 : M
hx : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x_1
x y : M
hx_1 : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
hy : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) y
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ ∃ (i : ι), x * y ∈ S i

Tactic:
⟨k, mul_mem (hik hi) (hjk hj)⟩

Premises used: Exists.intro, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x_1 : M
hx : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x_1
x y : M
hx_1 : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
hy : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) y
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ ∃ (i : ι), x * y ∈ S i

Tactic:
exact ⟨k, mul_mem (hik hi) (hjk hj)⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : ∃ (i : ι), p i
S : ι → Submonoid M
hS : DirectedOn ((fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
rw :
  ∀ (hp : Nonempty.{max 1 (u_4 + 1)} (Subtype p)) {S : ι → Submonoid M}
    (hS : DirectedOn ((fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) on S) {i : ι | p i}) {x : M},
    Membership.mem (γ := Submonoid M) (⨆ (i : ι), ⨆ (_ : p i), S i) x ↔ ∃ (i : ι), p i ∧ x ∈ S i
⊢ Membership.mem (γ := Submonoid M) (⨆ (i : ι), ⨆ (_ : p i), S i) x ↔ ∃ (i : ι), p i ∧ x ∈ S i

Tactic:
rw [← nonempty_subtype] at hp

Premises used: nonempty_subtype
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty.{max 1 (u_4 + 1)} (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
rw : (∃ (i : Subtype p), x ∈ S (↑i : ι)) ↔ ∃ (i : ι), p i ∧ x ∈ S i
hS₁ : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) fun (x : Subtype p) ↦ S (↑x : ι)
⊢ Membership.mem (γ := Submonoid M) (⨆ (i : ι), ⨆ (_ : p i), S i) x ↔ ∃ (i : ι), p i ∧ x ∈ S i

Tactic:
rw [iSup_subtype', mem_iSup_of_directed]

Premises used: iSup_subtype', Submonoid.mem_iSup_of_directed
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty.{max 1 (u_4 + 1)} (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
⊢ (∃ (i : Subtype p), x ∈ S (↑i : ι)) ↔ ∃ (i : ι), p i ∧ x ∈ S i

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty.{max 1 (u_4 + 1)} (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
hS₁ : Directed (ι := Subtype p) (S ⁻¹'o fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) (Subtype.val (p := p))
⊢ Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) fun (x : Subtype p) ↦ S (↑x : ι)

Tactic:
rw [← Function.comp_def, directed_comp]

Premises used: Function.comp_def, directed_comp
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty.{max 1 (u_4 + 1)} (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
⊢ Directed (ι := Subtype p) (S ⁻¹'o fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) (Subtype.val (p := p))

Tactic:
hS.directed_val

Premises used: Set.Mem, setOf, DirectedOn.directed_val, Order.Preimage
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty.{max 1 (u_4 + 1)} (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
⊢ Directed (ι := Subtype p) (S ⁻¹'o fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) (Subtype.val (p := p))

Tactic:
exact hS.directed_val

Premises used: DirectedOn.directed_val
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
pos : ∀ (h : p), Membership.mem (γ := Submonoid M) (⨆ (h : p), S h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ S h
neg : ∀ (h : ¬p), Membership.mem (γ := Submonoid M) (⨆ (h : p), S h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ S h
⊢ Membership.mem (γ := Submonoid M) (⨆ (h : p), S h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ S h

Tactic:
by_cases h : p
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
h : p
⊢ Membership.mem (γ := Submonoid M) (⨆ (h : p), S h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ S h

Tactic:
simp +contextual [h]
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
h : ¬p
⊢ Membership.mem (γ := Submonoid M) (⨆ (h : p), S h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ S h

Tactic:
simp +contextual [h]
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x : M
⊢ x ∈ (↑(⨆ (i : ι), S i) : Set M) ↔ Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x

Tactic:
simp [mem_iSup_of_directed hS]

Premises used: Submonoid.mem_iSup_of_directed
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
S : Set (Submonoid M)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x : M
⊢ Nonempty.{u_1 + 1} (↑S : Type u_1)

Tactic:
haveI : Nonempty S := Sne.to_subtype
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
S : Set (Submonoid M)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x : M
this : Nonempty.{u_1 + 1} (↑S : Type u_1)
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val]

Premises used: DirectedOn.directed_val, Submonoid.mem_iSup_of_directed, sSup_eq_iSup'
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : MulOneClass M
S : Set (Submonoid M)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x : M
⊢ x ∈ (↑(sSup S) : Set M) ↔ Membership.mem (γ := Set M) (⋃ s ∈ S, (↑s : Set M)) x

Tactic:
simp [mem_sSup_of_directedOn Sne hS]

Premises used: Submonoid.mem_sSup_of_directedOn