awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
A : Type u_2
inst : AddGroup A
x : A
symm :
  (↑(Subgroup.zpowers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Subgroup (Multiplicative A)) :
      Set (Multiplicative A)) =
    (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) '' (↑(AddSubgroup.zmultiples x) : Set A)
⊢ (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) '' (↑(AddSubgroup.zmultiples x) : Set A) =
    (↑(Subgroup.zpowers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Subgroup (Multiplicative A)) :
      Set (Multiplicative A))

Tactic:
symm
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
A : Type u_2
inst : AddGroup A
x : A
rw :
  (⇑(Equiv.symm Multiplicative.ofAdd) : (a : Multiplicative A) → A) ''
      (↑(Subgroup.zpowers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Subgroup (Multiplicative A)) :
        Set (Multiplicative A)) =
    (↑(AddSubgroup.zmultiples x) : Set A)
⊢ (↑(Subgroup.zpowers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Subgroup (Multiplicative A)) :
      Set (Multiplicative A)) =
    (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) '' (↑(AddSubgroup.zmultiples x) : Set A)

Tactic:
rw [Equiv.eq_image_iff_symm_image_eq]

Premises used: Equiv.eq_image_iff_symm_image_eq
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
A : Type u_2
inst : AddGroup A
x : A
⊢ (⇑(Equiv.symm Multiplicative.ofAdd) : (a : Multiplicative A) → A) ''
      (↑(Subgroup.zpowers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Subgroup (Multiplicative A)) :
        Set (Multiplicative A)) =
    (↑(AddSubgroup.zmultiples x) : Set A)

Tactic:
ofMul_image_zpowers_eq_zmultiples_ofMul

Premises used: Additive, ofMul_image_zpowers_eq_zmultiples_ofMul, Multiplicative
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
A : Type u_2
inst : AddGroup A
x : A
⊢ (⇑(Equiv.symm Multiplicative.ofAdd) : (a : Multiplicative A) → A) ''
      (↑(Subgroup.zpowers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Subgroup (Multiplicative A)) :
        Set (Multiplicative A)) =
    (↑(AddSubgroup.zmultiples x) : Set A)

Tactic:
exact ofMul_image_zpowers_eq_zmultiples_ofMul

Premises used: ofMul_image_zpowers_eq_zmultiples_ofMul
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
N : Type u_3
inst_2 : Group N
s : Set G
g_1 g : G
x x_1 : ↥(zpowers g)
val : G
w : ℤ
h₁ : (fun (x : ℤ) ↦ g ^ x) w = val
val_1 : G
w_1 : ℤ
h₂ : (fun (x : ℤ) ↦ g ^ x) w_1 = val_1
⊢ HMul.hMul (α := ↥(zpowers g)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) val ⋯)
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) val_1 ⋯) =
    HMul.hMul (α := ↥(zpowers g))
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) val_1 ⋯)
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) val ⋯)

Tactic:
simp [← h₁, ← h₂, zpow_mul_comm]

Premises used: zpow_mul_comm
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
g : G
H : Subgroup G
rw : closure {g} ≤ H ↔ g ∈ H
rw₁ : {g} ⊆ (↑H : Set G) ↔ g ∈ H
rw₂ : g ∈ (↑H : Set G) ↔ g ∈ H
rw₃ rw₄ : g ∈ H ↔ g ∈ H
⊢ zpowers g ≤ H ↔ g ∈ H

Tactic:
rw [zpowers_eq_closure, closure_le, Set.singleton_subset_iff, SetLike.mem_coe]

Premises used: Set.singleton_subset_iff, Subgroup.closure_le, SetLike.mem_coe, Subgroup.zpowers_eq_closure
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
g : G
rw : LE.le (α := Subgroup G) (zpowers g) ⊥ ↔ g = 1
rw₁ : Membership.mem (γ := Subgroup G) ⊥ g ↔ g = 1
rw₂ rw₃ : g = 1 ↔ g = 1
⊢ Eq (α := Subgroup G) (zpowers g) ⊥ ↔ g = 1

Tactic:
rw [eq_bot_iff, zpowers_le, mem_bot]

Premises used: Subgroup.zpowers_le, eq_bot_iff, Subgroup.mem_bot
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
g : G
⊢ Ne (α := Subgroup G) (zpowers g) ⊥ ↔ g ≠ 1

Tactic:
zpowers_eq_bot.not

Premises used: Iff.not, Subgroup.zpowers_eq_bot
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
⊢ Eq.{u_1 + 1} (α := Subgroup G) (zpowers 1) ⊥

Tactic:
Subgroup.zpowers_eq_bot.mpr rfl

Premises used: Iff.mpr, Subgroup.zpowers_eq_bot, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
g : G
x : Subgroup G
⊢ zpowers g⁻¹ ≤ x ↔ zpowers g ≤ x

Tactic:
simp only [zpowers_le, inv_mem_iff]

Premises used: Subgroup.zpowers_le, inv_mem_iff
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
a : ℤ
⊢ Eq (α := AddSubgroup ℤ) (AddSubgroup.zmultiples (↑a.natAbs : ℤ)) (AddSubgroup.zmultiples a)

Tactic:
simp [le_antisymm_iff, Int.mem_zmultiples_iff, Int.dvd_natAbs, Int.natAbs_dvd]

Premises used: Int.dvd_natAbs, Int.mem_zmultiples_iff, le_antisymm_iff, Int.natAbs_dvd
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
h : ∀ (x : ℤ), Membership.mem (γ := AddSubgroup ℤ) (AddSubgroup.closure {1}) x ↔ Membership.mem (γ := AddSubgroup ℤ) ⊤ x
⊢ Eq (α := AddSubgroup ℤ) (AddSubgroup.closure {1}) ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
x : ℤ
⊢ Membership.mem (γ := AddSubgroup ℤ) (AddSubgroup.closure {1}) x ↔ Membership.mem (γ := AddSubgroup ℤ) ⊤ x

Tactic:
simp [AddSubgroup.mem_closure_singleton]

Premises used: AddSubgroup.mem_closure_singleton
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Goal:
G : Type u_1
inst : Group G
g : G
⊢ Eq (α := Subgroup G) (MonoidHom.range (G := Multiplicative ℤ) ((zpowersHom G : (a : G) → Multiplicative ℤ →* G) g))
    (zpowers g)

Tactic:
rfl

Premises used: MonoidHom.range, Subgroup.copy, Multiplicative, Subgroup.zpowers, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
N : Type u_3
inst_2 : Group N
a : G
⊢ Countable.{u_1 + 1} ↥(zpowers a)

Tactic:
Set.rangeFactorization_surjective.countable

Premises used: Function.Surjective.countable, Set.Mem, setOf, Set.rangeFactorization_surjective, Set.range
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Goal:
A : Type u_2
inst : AddGroup A
a : A
⊢ Eq (α := AddSubgroup A) (AddMonoidHom.range (G := ℤ) ((zmultiplesHom A : (a : A) → ℤ →+ A) a)) (zmultiples a)

Tactic:
rfl

Premises used: AddMonoidHom.range, AddSubgroup.copy, AddSubgroup.zmultiples, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Goal:
R : Type u_4
inst : Ring R
r : R
k : ℤ
⊢ Membership.mem (γ := AddSubgroup R) (zmultiples r) ((↑k : R) * r)

Tactic:
simpa only [← zsmul_eq_mul] using zsmul_mem_zmultiples r k

Premises used: zsmul_eq_mul, AddSubgroup.zsmul_mem_zmultiples
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Goal:
R : Type u_4
inst : Ring R
k : ℤ
⊢ Eq.{u_4 + 1} (α := R) ((fun (x : ℤ) ↦ HSMul.hSMul (β := R) x 1) k) (↑k : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Goal:
A : Type u_4
inst : AddGroupWithOne A
h :
  ∀ (a : A),
    Membership.mem (γ := AddSubgroup A) (AddMonoidHom.range (castAddHom A)) a ↔
      Membership.mem (γ := AddSubgroup A) (zmultiples 1) a
⊢ Eq.{u_4 + 1} (α := AddSubgroup A) (AddMonoidHom.range (castAddHom A)) (zmultiples 1)

Tactic:
ext a
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Goal:
A : Type u_4
inst : AddGroupWithOne A
a : A
h : (∃ (x : ℤ), (castAddHom A : (a : ℤ) → A) x = a) ↔ Membership.mem (γ := AddSubgroup A) (zmultiples 1) a
h₁ : (∃ (x : ℤ), (↑x : A) = a) ↔ Membership.mem (γ := AddSubgroup A) (zmultiples 1) a
h₂ : (∃ (x : ℤ), (↑x : A) = a) ↔ ∃ (k : ℤ), HSMul.hSMul (β := A) k 1 = a
⊢ Membership.mem (γ := AddSubgroup A) (AddMonoidHom.range (castAddHom A)) a ↔
    Membership.mem (γ := AddSubgroup A) (zmultiples 1) a

Tactic:
simp_rw [AddMonoidHom.mem_range, Int.coe_castAddHom, AddSubgroup.mem_zmultiples_iff, zsmul_one]

Premises used: Int.coe_castAddHom, AddSubgroup.mem_zmultiples_iff, zsmul_one, AddMonoidHom.mem_range
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Goal:
n : ℕ
h :
  ∀ (m : ℤ),
    Membership.mem (γ := AddSubgroup ℤ) (AddMonoidHom.range (nsmulAddMonoidHom n)) m ↔
      Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑n : ℤ)) m
⊢ Eq (α := AddSubgroup ℤ) (AddMonoidHom.range (nsmulAddMonoidHom n)) (zmultiples (↑n : ℤ))

Tactic:
ext m : 1
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Goal:
n : ℕ
m : ℤ
h : (∃ (x : ℤ), (↑n : ℤ) * x = m) ↔ ∃ (c : ℤ), m = (↑n : ℤ) * c
⊢ Membership.mem (γ := AddSubgroup ℤ) (AddMonoidHom.range (nsmulAddMonoidHom n)) m ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑n : ℤ)) m

Tactic:
simp [mem_zmultiples_iff, dvd_def]

Premises used: dvd_def, Int.mem_zmultiples_iff
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Goal:
n : ℕ
m : ℤ
⊢ (∃ (x : ℤ), (↑n : ℤ) * x = m) ↔ ∃ (c : ℤ), m = (↑n : ℤ) * c

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Goal:
a b : ℤ
a₁ : LE.le (α := AddSubgroup ℤ) (closure {a, b}) (zmultiples (↑(a.gcd b) : ℤ))
a₂ : LE.le (α := AddSubgroup ℤ) (zmultiples (↑(a.gcd b) : ℤ)) (closure {a, b})
⊢ Eq (α := AddSubgroup ℤ) (closure {a, b}) (zmultiples (↑(a.gcd b) : ℤ))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Goal:
a b : ℤ
⊢ LE.le (α := AddSubgroup ℤ) (closure {a, b}) (zmultiples (↑(a.gcd b) : ℤ))

Tactic:
grind [closure_le, mem_zmultiples_iff, SetLike.mem_coe, gcd_dvd_left, gcd_dvd_right]

Premises used: Int.mem_zmultiples_iff, Int.gcd_dvd_left, SetLike.mem_coe, Int.gcd_dvd_right, AddSubgroup.closure_le
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Goal:
a b : ℤ
⊢ LE.le (α := AddSubgroup ℤ) (zmultiples (↑(a.gcd b) : ℤ)) (closure {a, b})

Tactic:
simp [zmultiples_le, mem_closure_pair, gcd_eq_gcd_ab, mul_comm]

Premises used: AddSubgroup.zmultiples_le, mul_comm, Int.gcd_eq_gcd_ab, AddSubgroup.mem_closure_pair
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
N : Type u_2
A : Type u_3
inst : MulOneClass M
s_1 : Set M
inst_1 : AddZeroClass A
t : Set A
S : Submonoid M
s : Set (Submonoid M)
a b : M
hx : Membership.mem (γ := Set M) (⋂ t ∈ s, (↑t : Set M)) a
hy : Membership.mem (γ := Set M) (⋂ t ∈ s, (↑t : Set M)) b
i : Submonoid M
h : i ∈ s
⊢ a ∈ i

Tactic:
apply Set.mem_iInter₂.1 hx i h

Premises used: Set.mem_iInter₂, Iff.mp
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
N : Type u_2
A : Type u_3
inst : MulOneClass M
s_1 : Set M
inst_1 : AddZeroClass A
t : Set A
S : Submonoid M
s : Set (Submonoid M)
a b : M
hx : Membership.mem (γ := Set M) (⋂ t ∈ s, (↑t : Set M)) a
hy : Membership.mem (γ := Set M) (⋂ t ∈ s, (↑t : Set M)) b
i : Submonoid M
h : i ∈ s
⊢ b ∈ i

Tactic:
apply Set.mem_iInter₂.1 hy i h

Premises used: Set.mem_iInter₂, Iff.mp
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
S : Set (Submonoid M)
⊢ (↑(sInf S) : Set M) = ⋂ s ∈ S, (↑s : Set M)

Tactic:
rfl

Premises used: iInf, Set.iInter, setOf, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
S : Set (Submonoid M)
x : M
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
Set.mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.mem_iInter₂
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
x : M
⊢ Membership.mem (γ := Submonoid M) (⨅ (i : ι), S i) x ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Premises used: iInf, Set.forall_mem_range, Submonoid.mem_sInf
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
⊢ (↑(⨅ (i : ι), S i) : Set M) = ⋂ (i : ι), (↑(S i) : Set M)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Premises used: iInf, Set.biInter_range, Submonoid.coe_sInf
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x : M
⊢ Membership.mem (γ := Submonoid M) (closure s) x ↔ ∀ (S : Submonoid M), s ⊆ (↑S : Set M) → x ∈ S

Tactic:
mem_sInf

Premises used: Set.Mem, setOf, Submonoid.mem_sInf
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
⊢ s ⊆ (↑(closure s) : Set M)

Tactic:
fun _ hx => mem_closure.2 fun _ hS => hS hx

Premises used: Iff.mpr, Submonoid.mem_closure, Set.Subset
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x : M
hx : x ∈ s
⊢ Membership.mem (γ := Submonoid M) (closure s) x

Tactic:
subset_closure hx

Premises used: Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
P : M
hP : P ∉ closure s
⊢ P ∉ s

Tactic:
fun h =>
  hP (subset_closure h)

Premises used: Submonoid.subset_closure, Not
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
S : Submonoid M
⊢ closure s ≤ S ↔ s ⊆ (↑S : Set M)

Tactic:
⟨Subset.trans subset_closure, fun h => sInf_le h⟩

Premises used: Set.Subset.trans, sInf_le, Iff.intro, Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s t : Set M
h : s ⊆ t
⊢ LE.le (α := Submonoid M) (closure s) (closure t)

Tactic:
closure_le.2 <| Subset.trans h subset_closure

Premises used: Iff.mpr, Set.Subset.trans, Submonoid.subset_closure, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
S : Submonoid M
h₁ : s ⊆ (↑S : Set M)
h₂ : S ≤ closure s
⊢ closure s = S

Tactic:
le_antisymm (closure_le.2 h₁) h₂

Premises used: Iff.mpr, le_antisymm, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
motive : (x : M) → Membership.mem (γ := Submonoid M) (closure s) x → Prop
mem : ∀ (x : M) (h : x ∈ s), motive x ⋯
one : motive 1 ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y), motive x hx → motive y hy → motive (x * y) ⋯
x : M
hx : Membership.mem (γ := Submonoid M) (closure s) x
⊢ motive x hx

Tactic:
let S : Submonoid M :=
    { carrier := { x | ∃ hx, motive x hx }
      one_mem' := ⟨_, one⟩
      mul_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, mul _ _ _ _ hpx hpy⟩ }
  closure_le (S := S) |>.mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Premises used: Iff.mpr, HMul.hMul, Subsemigroup.mk, setOf, Membership.mem, Exists, id, _private.0.Submonoid.closure_induction.match_1, Submonoid.closure, Exists.intro, Submonoid.mk, OneMemClass.one_mem, Submonoid.subset_closure, Submonoid.closure_le, Exists.elim, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
motive :
  (x y : M) → Membership.mem (γ := Submonoid M) (closure s) x → Membership.mem (γ := Submonoid M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯
one_left : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive 1 x ⋯ hx
one_right : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯
x y z : M
hz : z ∈ s
x_1 : M
h : x_1 ∈ s
⊢ motive x_1 z ⋯ ⋯

Tactic:
mem _ _ h hz
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
motive :
  (x y : M) → Membership.mem (γ := Submonoid M) (closure s) x → Membership.mem (γ := Submonoid M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯
one_left : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive 1 x ⋯ hx
one_right : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯
x y z : M
hz : z ∈ s
x_1 : M
h : x_1 ∈ s
⊢ motive x_1 z ⋯ ⋯

Tactic:
exact mem _ _ h hz
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
motive :
  (x y : M) → Membership.mem (γ := Submonoid M) (closure s) x → Membership.mem (γ := Submonoid M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯
one_left : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive 1 x ⋯ hx
one_right : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯
x y z : M
hz : z ∈ s
⊢ motive 1 z ⋯ ⋯

Tactic:
one_left _ (subset_closure hz)

Premises used: Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
motive :
  (x y : M) → Membership.mem (γ := Submonoid M) (closure s) x → Membership.mem (γ := Submonoid M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯
one_left : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive 1 x ⋯ hx
one_right : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯
x y z : M
hz : z ∈ s
⊢ motive 1 z ⋯ ⋯

Tactic:
exact one_left _ (subset_closure hz)

Premises used: Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
motive :
  (x y : M) → Membership.mem (γ := Submonoid M) (closure s) x → Membership.mem (γ := Submonoid M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯
one_left : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive 1 x ⋯ hx
one_right : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯
x y z : M
hz : z ∈ s
x_1 y_1 : M
hx : Membership.mem (γ := Submonoid M) (closure s) x_1
hy : Membership.mem (γ := Submonoid M) (closure s) y_1
h₁ : motive x_1 z hx ⋯
h₂ : motive y_1 z hy ⋯
⊢ motive (x_1 * y_1) z ⋯ ⋯

Tactic:
mul_left _ _ _ _ _ _ h₁ h₂
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
motive :
  (x y : M) → Membership.mem (γ := Submonoid M) (closure s) x → Membership.mem (γ := Submonoid M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯
one_left : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive 1 x ⋯ hx
one_right : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯
x y z : M
hz : z ∈ s
x_1 y_1 : M
hx : Membership.mem (γ := Submonoid M) (closure s) x_1
hy : Membership.mem (γ := Submonoid M) (closure s) y_1
h₁ : motive x_1 z hx ⋯
h₂ : motive y_1 z hy ⋯
⊢ motive (x_1 * y_1) z ⋯ ⋯

Tactic:
exact mul_left _ _ _ _ _ _ h₁ h₂
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
motive :
  (x y : M) → Membership.mem (γ := Submonoid M) (closure s) x → Membership.mem (γ := Submonoid M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯
one_left : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive 1 x ⋯ hx
one_right : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯
x y : M
hx : Membership.mem (γ := Submonoid M) (closure s) x
z : M
hz : z ∈ s
mem₁ : ∀ (x : M) (h : x ∈ s), motive x z ⋯ ⋯
mem₂ : motive 1 z ⋯ ⋯
mem₃ :
  ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (h₁ : motive x z hx ⋯) (h₂ : motive y z hy ⋯),
    motive (x * y) z ⋯ ⋯
⊢ motive x z hx ⋯

Tactic:
induction hx using closure_induction with
    | mem _ h => exact mem _ _ h hz
    | one => exact one_left _ (subset_closure hz)
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂

Premises used: Submonoid.mul, Submonoid.one, Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
motive :
  (x y : M) → Membership.mem (γ := Submonoid M) (closure s) x → Membership.mem (γ := Submonoid M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯
one_left : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive 1 x ⋯ hx
one_right : ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x), motive x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (hz : Membership.mem (γ := Submonoid M) (closure s) z),
    motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯
x y : M
hx : Membership.mem (γ := Submonoid M) (closure s) x
⊢ motive x 1 hx ⋯

Tactic:
one_right x hx