[GOAL]
M✝ : Type u_1
N : Type u_2
A✝ : Type u_3
inst✝⁴ : MulOneClass M✝
s : Set M✝
inst✝³ : AddZeroClass A✝
t : Set A✝
M : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ x ^ 0 ∈ S
[PROOFSTEP]
rw [pow_zero]
[GOAL]
M✝ : Type u_1
N : Type u_2
A✝ : Type u_3
inst✝⁴ : MulOneClass M✝
s : Set M✝
inst✝³ : AddZeroClass A✝
t : Set A✝
M : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ 1 ∈ S
[PROOFSTEP]
exact OneMemClass.one_mem S
[GOAL]
M✝ : Type u_1
N : Type u_2
A✝ : Type u_3
inst✝⁴ : MulOneClass M✝
s : Set M✝
inst✝³ : AddZeroClass A✝
t : Set A✝
M : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ x ^ (n + 1) ∈ S
[PROOFSTEP]
rw [pow_succ]
[GOAL]
M✝ : Type u_1
N : Type u_2
A✝ : Type u_3
inst✝⁴ : MulOneClass M✝
s : Set M✝
inst✝³ : AddZeroClass A✝
t : Set A✝
M : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ x * x ^ n ∈ S
[PROOFSTEP]
exact mul_mem hx (pow_mem hx n)
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
p q : Submonoid M
h : (fun s => s.carrier) p = (fun s => s.carrier) q
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
q : Submonoid M
toSubsemigroup✝ : Subsemigroup M
one_mem'✝ : 1 ∈ toSubsemigroup✝.carrier
h : (fun s => s.carrier) { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ } = (fun s => s.carrier) q
⊢ { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
toSubsemigroup✝¹ : Subsemigroup M
one_mem'✝¹ : 1 ∈ toSubsemigroup✝¹.carrier
toSubsemigroup✝ : Subsemigroup M
one_mem'✝ : 1 ∈ toSubsemigroup✝.carrier
h :
  (fun s => s.carrier) { toSubsemigroup := toSubsemigroup✝¹, one_mem' := one_mem'✝¹ } =
    (fun s => s.carrier) { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }
⊢ { toSubsemigroup := toSubsemigroup✝¹, one_mem' := one_mem'✝¹ } =
    { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toSubsemigroup
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
toSubsemigroup✝¹ : Subsemigroup M
one_mem'✝¹ : 1 ∈ toSubsemigroup✝¹.carrier
toSubsemigroup✝ : Subsemigroup M
one_mem'✝ : 1 ∈ toSubsemigroup✝.carrier
h :
  (fun s => s.carrier) { toSubsemigroup := toSubsemigroup✝¹, one_mem' := one_mem'✝¹ } =
    (fun s => s.carrier) { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }
⊢ toSubsemigroup✝¹ = toSubsemigroup✝
[PROOFSTEP]
exact SetLike.coe_injective' h
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
a✝ b✝ : M
ha : a✝ ∈ {1}
hb : b✝ ∈ {1}
⊢ a✝ * b✝ ∈ {1}
[PROOFSTEP]
simp only [Set.mem_singleton_iff] at *
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
a✝ b✝ : M
ha : a✝ = 1
hb : b✝ = 1
⊢ a✝ * b✝ = 1
[PROOFSTEP]
rw [ha, hb, mul_one]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
s : Set (Submonoid M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ (t : Submonoid M) (_ : t ∈ s), ↑t
hy : b✝ ∈ ⋂ (t : Submonoid M) (_ : t ∈ s), ↑t
i : Submonoid M
h : i ∈ s
⊢ a✝ ∈ i
[PROOFSTEP]
apply Set.mem_iInter₂.1 hx i h
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
s : Set (Submonoid M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ (t : Submonoid M) (_ : t ∈ s), ↑t
hy : b✝ ∈ ⋂ (t : Submonoid M) (_ : t ∈ s), ↑t
i : Submonoid M
h : i ∈ s
⊢ b✝ ∈ i
[PROOFSTEP]
apply Set.mem_iInter₂.1 hy i h
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S✝ : Submonoid M
ι : Sort u_4
S : ι → Submonoid M
x : M
⊢ x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i
[PROOFSTEP]
simp only [iInf, mem_sInf, Set.forall_range_iff]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S✝ : Submonoid M
ι : Sort u_4
S : ι → Submonoid M
⊢ ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
[PROOFSTEP]
simp only [iInf, coe_sInf, Set.biInter_range]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
h : Subsingleton M
x y : Submonoid M
i : M
⊢ 1 ∈ x ↔ 1 ∈ y
[PROOFSTEP]
simp [Submonoid.one_mem]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
s : Set M
p : (x : M) → x ∈ closure s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H1 : p 1 (_ : 1 ∈ closure s)
Hmul : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
x : M
hx : x ∈ closure s
⊢ p x hx
[PROOFSTEP]
refine' Exists.elim _ fun (hx : x ∈ closure s) (hc : p x hx) => hc
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
s : Set M
p : (x : M) → x ∈ closure s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H1 : p 1 (_ : 1 ∈ closure s)
Hmul : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
x : M
hx : x ∈ closure s
⊢ ∃ x_1, p x x_1
[PROOFSTEP]
exact closure_induction hx (fun x hx => ⟨_, Hs x hx⟩) ⟨_, H1⟩ fun x y ⟨hx', hx⟩ ⟨hy', hy⟩ => ⟨_, Hmul _ _ _ _ hx hy⟩
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
p : M → Prop
x : M
s : Set M
hs : closure s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
H1 : p 1
Hmul : ∀ (x y : M), p x → p y → p (x * y)
⊢ p x
[PROOFSTEP]
have : ∀ x ∈ closure s, p x := fun x hx => closure_induction hx Hs H1 Hmul
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
p : M → Prop
x : M
s : Set M
hs : closure s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
H1 : p 1
Hmul : ∀ (x y : M), p x → p y → p (x * y)
this : ∀ (x : M), x ∈ closure s → p x
⊢ p x
[PROOFSTEP]
simpa [hs] using this x
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
m : M
p : Submonoid M
⊢ closure {m} ≤ p ↔ m ∈ p
[PROOFSTEP]
rw [closure_le, singleton_subset_iff, SetLike.mem_coe]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
ι : Sort u_4
p : ι → Submonoid M
m : M
⊢ m ∈ ⨆ (i : ι), p i ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N
[PROOFSTEP]
rw [← closure_singleton_le_iff_mem, le_iSup_iff]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid 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
[PROOFSTEP]
simp only [closure_singleton_le_iff_mem]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
ι : Sort u_4
p : ι → Submonoid M
⊢ ⨆ (i : ι), p i = closure (⋃ (i : ι), ↑(p i))
[PROOFSTEP]
simp_rw [Submonoid.closure_iUnion, Submonoid.closure_eq]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S p₁ p₂ : Submonoid M
⊢ Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
[PROOFSTEP]
simp_rw [disjoint_iff_inf_le, SetLike.le_def, mem_inf, and_imp, mem_bot]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝² : MulOneClass M
s : Set M
inst✝¹ : AddZeroClass A
t : Set A
inst✝ : MulOneClass N
f g : M →* N
a✝ b✝ : M
hx : ↑f a✝ = ↑g a✝
hy : ↑f b✝ = ↑g b✝
⊢ a✝ * b✝ ∈ {x | ↑f x = ↑g x}
[PROOFSTEP]
simp [*]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝² : MulOneClass M
s : Set M
inst✝¹ : AddZeroClass A
t : Set A
inst✝ : MulOneClass N
f g : M →* N
⊢ 1 ∈
    { carrier := {x | ↑f x = ↑g x},
        mul_mem' := (_ : ∀ {a b : M}, ↑f a = ↑g a → ↑f b = ↑g b → ↑f (a * b) = ↑g (a * b)) }.carrier
[PROOFSTEP]
rw [Set.mem_setOf_eq, f.map_one, g.map_one]
[GOAL]
M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
⊢ ∀ {a b : M}, a ∈ setOf IsUnit → b ∈ setOf IsUnit → a * b ∈ setOf IsUnit
[PROOFSTEP]
intro a b ha hb
[GOAL]
M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
a b : M
ha : a ∈ setOf IsUnit
hb : b ∈ setOf IsUnit
⊢ a * b ∈ setOf IsUnit
[PROOFSTEP]
rw [Set.mem_setOf_eq] at *
[GOAL]
M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
a b : M
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b)
[PROOFSTEP]
exact IsUnit.mul ha hb
[GOAL]
M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
⊢ 1 ∈
    { carrier := setOf IsUnit,
        mul_mem' := (_ : ∀ {a b : M}, a ∈ setOf IsUnit → b ∈ setOf IsUnit → a * b ∈ setOf IsUnit) }.carrier
[PROOFSTEP]
simp only [isUnit_one, Set.mem_setOf_eq]
[GOAL]
M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
a : M
⊢ a ∈ submonoid M ↔ IsUnit a
[PROOFSTEP]
change a ∈ setOf IsUnit ↔ IsUnit a
[GOAL]
M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
a : M
⊢ a ∈ setOf IsUnit ↔ IsUnit a
[PROOFSTEP]
rw [Set.mem_setOf_eq]
[GOAL]
M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.38168
N : Type ?u.38171
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ (x : M), x ∈ s → ∀ (y : M), f (x * y) = f x * f y
x y : M
⊢ f (1 * y) = f 1 * f y
[PROOFSTEP]
rw [one_mul, h1, one_mul]
[GOAL]
M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.38168
N : Type ?u.38171
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ (x : M), x ∈ s → ∀ (y : M), f (x * y) = f x * f y
x a b : M
ha : ∀ (y : M), f (a * y) = f a * f y
hb : ∀ (y : M), f (b * y) = f b * f y
y : M
⊢ f (a * b * y) = f (a * b) * f y
[PROOFSTEP]
rw [mul_assoc, ha, ha, hb, mul_assoc]
[GOAL]
M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.40855
N : Type ?u.40858
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x y : M
⊢ ∀ (x : M),
    OneHom.toFun { toFun := f, map_one' := h1 } (x * 1) =
      OneHom.toFun { toFun := f, map_one' := h1 } x * OneHom.toFun { toFun := f, map_one' := h1 } 1
[PROOFSTEP]
simp [h1]
[GOAL]
M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.40855
N : Type ?u.40858
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x✝ y y₁ y₂ : M
h₁ : ∀ (x : M), f (x * y₁) = f x * f y₁
h₂ : ∀ (x : M), f (x * y₂) = f x * f y₂
x : M
⊢ OneHom.toFun { toFun := f, map_one' := h1 } (x * (y₁ * y₂)) =
    OneHom.toFun { toFun := f, map_one' := h1 } x * OneHom.toFun { toFun := f, map_one' := h1 } (y₁ * y₂)
[PROOFSTEP]
simp [← mul_assoc, h₁, h₂]
