[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
p q : Subsemigroup M
h : p.carrier = q.carrier
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
q : Subsemigroup M
carrier✝ : Set M
mul_mem'✝ : ∀ {a b : M}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
h : { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier = q.carrier
⊢ { carrier := carrier✝, mul_mem' := mul_mem'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
carrier✝¹ : Set M
mul_mem'✝¹ : ∀ {a b : M}, a ∈ carrier✝¹ → b ∈ carrier✝¹ → a * b ∈ carrier✝¹
carrier✝ : Set M
mul_mem'✝ : ∀ {a b : M}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
h : { carrier := carrier✝¹, mul_mem' := mul_mem'✝¹ }.carrier = { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier
⊢ { carrier := carrier✝¹, mul_mem' := mul_mem'✝¹ } = { carrier := carrier✝, mul_mem' := mul_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s✝ : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
s : Set (Subsemigroup M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ (t : Subsemigroup M) (_ : t ∈ s), ↑t
hy : b✝ ∈ ⋂ (t : Subsemigroup M) (_ : t ∈ s), ↑t
i : Subsemigroup 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✝¹ : Mul M
s✝ : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
s : Set (Subsemigroup M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ (t : Subsemigroup M) (_ : t ∈ s), ↑t
hy : b✝ ∈ ⋂ (t : Subsemigroup M) (_ : t ∈ s), ↑t
i : Subsemigroup 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✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S✝ : Subsemigroup M
ι : Sort u_4
S : ι → Subsemigroup 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✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S✝ : Subsemigroup M
ι : Sort u_4
S : ι → Subsemigroup 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✝² : Mul M
s : Set M
inst✝¹ : Add A
t : Set A
S : Subsemigroup M
inst✝ : Subsingleton (Subsemigroup M)
⊢ Subsingleton M
[PROOFSTEP]
constructor
[GOAL]
case allEq
M : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Mul M
s : Set M
inst✝¹ : Add A
t : Set A
S : Subsemigroup M
inst✝ : Subsingleton (Subsemigroup M)
⊢ ∀ (a b : M), a = b
[PROOFSTEP]
intro x y
[GOAL]
case allEq
M : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Mul M
s : Set M
inst✝¹ : Add A
t : Set A
S : Subsemigroup M
inst✝ : Subsingleton (Subsemigroup M)
x y : M
⊢ x = y
[PROOFSTEP]
have : ∀ a : M, a ∈ (⊥ : Subsemigroup M) := by simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Mul M
s : Set M
inst✝¹ : Add A
t : Set A
S : Subsemigroup M
inst✝ : Subsingleton (Subsemigroup M)
x y : M
⊢ ∀ (a : M), a ∈ ⊥
[PROOFSTEP]
simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]
[GOAL]
case allEq
M : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Mul M
s : Set M
inst✝¹ : Add A
t : Set A
S : Subsemigroup M
inst✝ : Subsingleton (Subsemigroup M)
x y : M
this : ∀ (a : M), a ∈ ⊥
⊢ x = y
[PROOFSTEP]
exact absurd (this x) not_mem_bot
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
hn : Nonempty M
h : ⊥ = ⊤
⊢ False
[PROOFSTEP]
obtain ⟨x⟩ := id hn
[GOAL]
case intro
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
hn : Nonempty M
h : ⊥ = ⊤
x : M
⊢ False
[PROOFSTEP]
refine' absurd (_ : x ∈ ⊥) not_mem_bot
[GOAL]
case intro
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
hn : Nonempty M
h : ⊥ = ⊤
x : M
⊢ x ∈ ⊥
[PROOFSTEP]
simp [h]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s✝ : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
s : Set M
p : (x : M) → x ∈ closure s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(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✝¹ : Mul M
s✝ : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
s : Set M
p : (x : M) → x ∈ closure s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(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⟩) fun x y ⟨hx', hx⟩ ⟨hy', hy⟩ => ⟨_, Hmul _ _ _ _ hx hy⟩
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s✝ : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
p : M → Prop
x : M
s : Set M
hs : closure s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
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 Hmul
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s✝ : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
p : M → Prop
x : M
s : Set M
hs : closure s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
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✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
m : M
p : Subsemigroup 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✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
ι : Sort u_4
p : ι → Subsemigroup M
m : M
⊢ m ∈ ⨆ (i : ι), p i ↔ ∀ (N : Subsemigroup 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✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
ι : Sort u_4
p : ι → Subsemigroup M
m : M
⊢ (∀ (b : Subsemigroup M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔
    ∀ (N : Subsemigroup 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✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
ι : Sort u_4
p : ι → Subsemigroup M
⊢ ⨆ (i : ι), p i = closure (⋃ (i : ι), ↑(p i))
[PROOFSTEP]
simp_rw [Subsemigroup.closure_iUnion, Subsemigroup.closure_eq]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Mul M
s : Set M
inst✝¹ : Add A
t : Set A
inst✝ : Mul 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
M : Type ?u.26668
N : Type ?u.26671
inst✝¹ : Semigroup M
inst✝ : Semigroup N
s : Set M
f : M → N
hs : closure s = ⊤
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
⊢ f (x * (y₁ * y₂)) = f x * f (y₁ * y₂)
[PROOFSTEP]
simp only [← mul_assoc, h₁, h₂]
