awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact one_right x hx
-- 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
x_1 y_1 : M
hx_1 : Membership.mem (γ := Submonoid M) (closure s) x_1
hy : Membership.mem (γ := Submonoid M) (closure s) y_1
h₁ : motive x x_1 hx hx_1
h₂ : motive x y_1 hx hy
⊢ motive x (x_1 * y_1) hx ⋯

Tactic:
mul_right _ _ _ _ _ hx 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
x_1 y_1 : M
hx_1 : Membership.mem (γ := Submonoid M) (closure s) x_1
hy : Membership.mem (γ := Submonoid M) (closure s) y_1
h₁ : motive x x_1 hx hx_1
h₂ : motive x y_1 hx hy
⊢ motive x (x_1 * y_1) hx ⋯

Tactic:
exact mul_right _ _ _ _ _ hx 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
hy : Membership.mem (γ := Submonoid M) (closure s) y
mem₁ : ∀ (z : M) (hz : z ∈ s), motive x z hx ⋯
one : motive x 1 hx ⋯
mul :
  ∀ (x_1 y : M) (hx_1 : Membership.mem (γ := Submonoid M) (closure s) x_1)
    (hy : Membership.mem (γ := Submonoid M) (closure s) y) (h₁ : motive x x_1 hx hx_1) (h₂ : motive x y hx hy),
    motive x (x_1 * y) hx ⋯
⊢ motive x y hx hy

Tactic:
induction hy using closure_induction with
  | mem z hz => 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₂
  | one => exact one_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ hx h₁ h₂

Premises used: Submonoid.mul, Submonoid.one
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
motive : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x x_1 : M
h : x_1 ∈ s
⊢ motive x_1

Tactic:
mem _ h
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
motive : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x x_1 : M
h : x_1 ∈ s
⊢ motive x_1

Tactic:
exact mem _ h
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
motive : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
⊢ motive 1

Tactic:
one
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
motive : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
⊢ motive 1

Tactic:
exact one
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
motive : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x x_1 y : M
hx : Membership.mem (γ := Submonoid M) (Submonoid.closure s) x_1
hy : Membership.mem (γ := Submonoid M) (Submonoid.closure s) y
h₁ : motive x_1
h₂ : motive y
⊢ motive (x_1 * y)

Tactic:
mul _ _ h₁ h₂
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
motive : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x x_1 y : M
hx : Membership.mem (γ := Submonoid M) (Submonoid.closure s) x_1
hy : Membership.mem (γ := Submonoid M) (Submonoid.closure s) y
h₁ : motive x_1
h₂ : motive y
⊢ motive (x_1 * y)

Tactic:
exact mul _ _ h₁ h₂
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
motive : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
⊢ Membership.mem (γ := Submonoid M) (Submonoid.closure s) x

Tactic:
induction closure.symm ▸ mem_top x using closure_induction with
  | mem _ h => exact mem _ h
  | one => exact one
  | mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂
-- 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
p : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
⊢ Eq (α := Submonoid M) (Submonoid.closure s) ⊤

Tactic:
closure
-- 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
p : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
⊢ Eq (α := Submonoid M) (Submonoid.closure s) ⊤

Tactic:
exact closure
-- 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
p : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
hx : x ∈ s
⊢ p x

Tactic:
mem x hx
-- 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
p : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
hx : x ∈ s
⊢ p x

Tactic:
exact mem x hx
-- 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
p : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
⊢ p 1

Tactic:
one
-- 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
p : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
⊢ p 1

Tactic:
exact one
-- 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
p : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
x y : M
h₁ : p x
h₂ : p y
⊢ p (x * y)

Tactic:
mul _ _ h₁ h₂
-- 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
p : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
x y : M
h₁ : p x
h₂ : p y
⊢ p (x * y)

Tactic:
exact mul _ _ h₁ h₂
-- 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
p : M → Prop
s : Set M
closure : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
closure₁ : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
mem₁ : ∀ (x : M) (hx : x ∈ s), p x
one₁ : p 1
mul₁ : ∀ (x y : M) (h₁ : p x) (h₂ : p y), p (x * y)
⊢ p x

Tactic:
induction x using dense_induction s with
  | closure => exact closure
  | mem x hx => exact mem x hx
  | one => exact one
  | mul _ _ h₁ h₂ => exact mul _ _ h₁ h₂
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
a : (↑(closure s) : Set M) ≤ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
a₁ : {1} ∪ (↑(Subsemigroup.closure s) : Set M) ≤ (↑(closure s) : Set M)
⊢ (↑(closure s) : Set M) = {1} ∪ (↑(Subsemigroup.closure s) : Set M)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x_1 x : M
hx : x ∈ s
⊢ x ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)

Tactic:
Or.inr <| Subsemigroup.subset_closure hx

Premises used: Set.union, Set.Mem, setOf, Subsemigroup.subset_closure, Or.inr
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x_1 x : M
hx : x ∈ s
⊢ x ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)

Tactic:
exact Or.inr <| Subsemigroup.subset_closure hx

Premises used: Subsemigroup.subset_closure, Or.inr
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x : M
⊢ Membership.mem (γ := Set M) {1} 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x : M
⊢ 1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)

Tactic:
exact Or.inl <| by simp

Premises used: Or.inl
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x_1 x hx_1 : M
y : Membership.mem (γ := Submonoid M) (closure s) x
hy_1 : Membership.mem (γ := Submonoid M) (closure s) hx_1
hx : x ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
hy : hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
⊢ x = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x

Tactic:
push _ ∈ _ at hx hy
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x_1 x hx_1 : M
y : Membership.mem (γ := Submonoid M) (closure s) x
hy_1 : Membership.mem (γ := Submonoid M) (closure s) hx_1
hx : x ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
hy : hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
hx₁ : x = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x
⊢ hx_1 = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1

Tactic:
push _ ∈ _ at hx hy
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x_1 x hx_1 : M
y : Membership.mem (γ := Submonoid M) (closure s) x
hy_1 : Membership.mem (γ := Submonoid M) (closure s) hx_1
hx : x = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x
hy : hx_1 = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1
a :
  ∀ (y : Membership.mem (γ := Submonoid M) (closure s) 1)
    (hx : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1)
    (hy : Membership.mem (γ := Submonoid M) (closure s) 1)
    (hy : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1),
    HMul.hMul (α := M) 1 1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
a₁ :
  ∀ (y : Membership.mem (γ := Submonoid M) (closure s) 1)
    (hx : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1)
    (hy : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1),
    1 * hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
a₂ :
  ∀ (hx : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) 1)
    (hy : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1),
    x * 1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
a₃ :
  ∀ (hx : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1),
    x * hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
⊢ x * hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)

Tactic:
obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy

Premises used: And.intro, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x : M
y : Membership.mem (γ := Submonoid M) (closure s) 1
hx : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1
hy_1 : Membership.mem (γ := Submonoid M) (closure s) 1
hy : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1
⊢ HMul.hMul (α := M) 1 1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)

Tactic:
simp_all [mul_mem]

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x hx_1 : M
hy_1 : Membership.mem (γ := Submonoid M) (closure s) hx_1
hy_2 : hx_1 = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1
y : Membership.mem (γ := Submonoid M) (closure s) 1
hx : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1
hy : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1
⊢ 1 * hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)

Tactic:
simp_all [mul_mem]

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x_1 x : M
y : Membership.mem (γ := Submonoid M) (closure s) x
hx_1 : x = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x
hx : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x
hy_1 : Membership.mem (γ := Submonoid M) (closure s) 1
hy : Eq.{u_1 + 1} (α := M) 1 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) 1
⊢ x * 1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)

Tactic:
simp_all [mul_mem]

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x_1 x hx_1 : M
y : Membership.mem (γ := Submonoid M) (closure s) x
hy_1 : Membership.mem (γ := Submonoid M) (closure s) hx_1
hx_2 : x = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x
hy_2 : hx_1 = 1 ∨ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1
hx : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x
hy : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) hx_1
⊢ x * hx_1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)

Tactic:
simp_all [mul_mem]

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x : M
hx : x ∈ (↑(closure s) : Set M)
a : ∀ (x : M) (hx : x ∈ s), x ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
a₁ : 1 ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
a₂ :
  ∀ (x hx : M) (y : Membership.mem (γ := Submonoid M) (closure s) x)
    (hy : Membership.mem (γ := Submonoid M) (closure s) hx) (hx_1 : x ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M))
    (hy : hx ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)), x * hx ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)
⊢ x ∈ {1} ∪ (↑(Subsemigroup.closure s) : Set M)

Tactic:
induction hx using closure_induction with
    | mem x hx => exact Or.inr <| Subsemigroup.subset_closure hx
    | one => exact Or.inl <| by simp
    | mul x hx y hy hx hy =>
      push _ ∈ _ at hx hy
      obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
      all_goals simp_all [mul_mem]

Premises used: Submonoid.mul, Subsemigroup.subset_closure, Submonoid.one, Or.inl, Or.inr, rfl, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x : M
hx : Membership.mem (γ := Set M) {1} x
⊢ x = 1

Tactic:
simpa using hx
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x : M
hx : Membership.mem (γ := Set M) {1} x
⊢ x ∈ (↑(closure s) : Set M)

Tactic:
exact (show x = 1 by simpa using hx) ▸ one_mem (closure s)
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x : M
hx : x ∈ (↑(Subsemigroup.closure s) : Set M)
⊢ x ∈ (↑(closure s) : Set M)

Tactic:
Subsemigroup.closure_le.mpr subset_closure hx

Premises used: Iff.mpr, Set.Mem, Subsemigroup.closure_le, Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
x : M
hx : x ∈ (↑(Subsemigroup.closure s) : Set M)
⊢ x ∈ (↑(closure s) : Set M)

Tactic:
exact Subsemigroup.closure_le.mpr subset_closure hx

Premises used: Iff.mpr, Subsemigroup.closure_le, Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
S : Submonoid M
⊢ closure (↑S : Set M) = S

Tactic:
(Submonoid.gi M).l_u_eq S

Premises used: Submonoid.gi, GaloisInsertion.l_u_eq
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
⊢ Eq.{u_1 + 1} (α := Submonoid M) (closure ∅) ⊥

Tactic:
(Submonoid.gi M).gc.l_bot

Premises used: GaloisConnection.l_bot, Submonoid.gi, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
⊢ Eq.{u_1 + 1} (α := Submonoid M) (closure univ) ⊤

Tactic:
@coe_top M _ ▸ closure_eq ⊤

Premises used: Eq.rec, Submonoid.closure_eq, Submonoid.coe_top, Top.top
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s t : Set M
⊢ Eq (α := Submonoid M) (closure (s ∪ t)) (closure s ⊔ closure t)

Tactic:
(Submonoid.gi M).gc.l_sup

Premises used: Submonoid.gi, GaloisConnection.l_sup, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
N N' : Submonoid M
simp_rw : N ⊔ N' = closure (↑N : Set M) ⊔ closure (↑N' : Set M)
⊢ N ⊔ N' = closure ((↑N : Set M) ∪ (↑N' : Set M))

Tactic:
simp_rw [closure_union, closure_eq]

Premises used: Submonoid.closure_eq, Submonoid.closure_union
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
s : ι → Set M
⊢ Eq.{u_1 + 1} (α := Submonoid M) (closure (⋃ (i : ι), s i)) (⨆ (i : ι), closure (s i))

Tactic:
(Submonoid.gi M).gc.l_iSup

Premises used: GaloisConnection.l_iSup, Submonoid.gi, Set.iUnion, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
m : M
p : Submonoid M
rw : {m} ⊆ (↑p : Set M) ↔ m ∈ p
rw₁ : m ∈ (↑p : Set M) ↔ m ∈ p
rw₂ rw₃ : m ∈ p ↔ m ∈ p
⊢ closure {m} ≤ p ↔ m ∈ p

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

Premises used: Set.singleton_subset_iff, SetLike.mem_coe, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
rw : Membership.mem (γ := Submonoid M) (closure s) 1
⊢ Eq (α := Submonoid M) (closure (insert 1 s)) (closure s)

Tactic:
rw [insert_eq, closure_union, sup_eq_right, closure_singleton_le_iff_mem]

Premises used: Submonoid.closure_singleton_le_iff_mem, Set.insert_eq, sup_eq_right, Submonoid.closure_union
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
⊢ Membership.mem (γ := Submonoid M) (closure s) 1

Tactic:
apply one_mem

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
m : M
rw : (∀ (b : Submonoid M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N
⊢ Membership.mem (γ := Submonoid M) (⨆ (i : ι), p i) m ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
rw [← closure_singleton_le_iff_mem, le_iSup_iff]

Premises used: Submonoid.closure_singleton_le_iff_mem, le_iSup_iff
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
m : M
⊢ (∀ (b : Submonoid M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
simp only [closure_singleton_le_iff_mem]

Premises used: Submonoid.closure_singleton_le_iff_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
simp_rw : Eq.{u_1 + 1} (α := Submonoid M) (⨆ (i : ι), p i) (⨆ (i : ι), closure (↑(p i) : Set M))
⊢ Eq.{u_1 + 1} (α := Submonoid M) (⨆ (i : ι), p i) (closure (⋃ (i : ι), (↑(p i) : Set M)))

Tactic:
simp_rw [Submonoid.closure_iUnion, Submonoid.closure_eq]

Premises used: Submonoid.closure_eq, Submonoid.closure_iUnion