[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a✝ b✝ : M
ha : a✝ ∈ ↑f ⁻¹' ↑S
hb : b✝ ∈ ↑f ⁻¹' ↑S
⊢ ↑f (a✝ * b✝) ∈ S
[PROOFSTEP]
rw [map_mul]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a✝ b✝ : M
ha : a✝ ∈ ↑f ⁻¹' ↑S
hb : b✝ ∈ ↑f ⁻¹' ↑S
⊢ ↑f a✝ * ↑f b✝ ∈ S
[PROOFSTEP]
exact mul_mem ha hb
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
S : Subsemigroup P
⊢ ∀ (x : P), x ∈ comap (MulHom.id P) S ↔ x ∈ S
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
⊢ ∀ {a b : N}, a ∈ ↑f '' ↑S → b ∈ ↑f '' ↑S → a * b ∈ ↑f '' ↑S
[PROOFSTEP]
rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
[GOAL]
case intro.intro.intro.intro
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
x : M
hx : x ∈ ↑S
y : M
hy : y ∈ ↑S
⊢ ↑f x * ↑f y ∈ ↑f '' ↑S
[PROOFSTEP]
exact ⟨x * y, @mul_mem (Subsemigroup M) M _ _ _ _ _ _ hx hy, by rw [map_mul]⟩
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
x : M
hx : x ∈ ↑S
y : M
hy : y ∈ ↑S
⊢ ↑f (x * y) = ↑f x * ↑f y
[PROOFSTEP]
rw [map_mul]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
ι : Type u_5
f : M →ₙ* N
hf : Function.Injective ↑f
S : Subsemigroup M
x : M
⊢ x ∈ comap f (map f S) → x ∈ S
[PROOFSTEP]
simp [mem_comap, mem_map, hf.eq_iff]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
ι : Type u_5
f : M →ₙ* N
hf : Function.Surjective ↑f
S : Subsemigroup N
x : N
h : x ∈ S
y : M
hy : ↑f y = x
⊢ y ∈ comap f S ∧ ↑f y = x
[PROOFSTEP]
simp [hy, h]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
s : Set M
x✝¹ : { x // x ∈ closure s }
x : M
hx : x ∈ closure s
x✝ : { val := x, property := hx } ∈ ⊤
⊢ { val := x, property := hx } ∈ closure (Subtype.val ⁻¹' s)
[PROOFSTEP]
refine' closure_induction' _ (fun g hg => subset_closure hg) (fun g₁ g₂ hg₁ hg₂ => _) hx
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
s : Set M
x✝¹ : { x // x ∈ closure s }
x : M
hx : x ∈ closure s
x✝ : { val := x, property := hx } ∈ ⊤
g₁ : M
g₂ : g₁ ∈ closure s
hg₁ : M
hg₂ : hg₁ ∈ closure s
⊢ { val := g₁, property := g₂ } ∈ closure (Subtype.val ⁻¹' s) →
    { val := hg₁, property := hg₂ } ∈ closure (Subtype.val ⁻¹' s) →
      { val := g₁ * hg₁, property := (_ : g₁ * hg₁ ∈ closure s) } ∈ closure (Subtype.val ⁻¹' s)
[PROOFSTEP]
exact Subsemigroup.mul_mem _
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
x : M × N
⊢ x ∈ prod s ⊤ ↔ x ∈ comap (MulHom.fst M N) s
[PROOFSTEP]
simp [mem_prod, MulHom.coe_fst]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
s : Subsemigroup N
x : M × N
⊢ x ∈ prod ⊤ s ↔ x ∈ comap (MulHom.snd M N) s
[PROOFSTEP]
simp [mem_prod, MulHom.coe_snd]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
⊢ ↑(prod ⊥ ⊥) = ↑⊥
[PROOFSTEP]
simp [coe_prod, Prod.one_eq_mk]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ u ≤ prod s t ↔ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ u ≤ prod s t → map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
[PROOFSTEP]
intro h
[GOAL]
case mp
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ prod s t
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
[PROOFSTEP]
constructor
[GOAL]
case mp.left
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ prod s t
⊢ map (fst M N) u ≤ s
[PROOFSTEP]
rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
[GOAL]
case mp.left.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ prod s t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ ↑u
⊢ ↑(fst M N) (y1, y2) ∈ s
[PROOFSTEP]
exact (h hy1).1
[GOAL]
case mp.right
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ prod s t
⊢ map (snd M N) u ≤ t
[PROOFSTEP]
rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
[GOAL]
case mp.right.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ prod s t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ ↑u
⊢ ↑(snd M N) (y1, y2) ∈ t
[PROOFSTEP]
exact (h hy1).2
[GOAL]
case mpr
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t → u ≤ prod s t
[PROOFSTEP]
rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h
[GOAL]
case mpr.intro.mk
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
hH : map (fst M N) u ≤ s
hK : map (snd M N) u ≤ t
x1 : M
x2 : N
h : (x1, x2) ∈ u
⊢ (x1, x2) ∈ prod s t
[PROOFSTEP]
exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
g : N →ₙ* P
f : M →ₙ* N
⊢ map g (srange f) = srange (comp g f)
[PROOFSTEP]
simpa only [srange_eq_map] using (⊤ : Subsemigroup M).map_map g f
[GOAL]
M : Type u_1
N✝ : Type u_2
P : Type u_3
σ : Type u_4
inst✝³ : Mul M
inst✝² : Mul N✝
inst✝¹ : Mul P
S : Subsemigroup M
N : Type u_5
inst✝ : Mul N
f : M →ₙ* N
⊢ ↑(srange f) = ↑⊤ ↔ Set.range ↑f = Set.univ
[PROOFSTEP]
rw [coe_srange, coe_top]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
f : M →ₙ* N
M' : Subsemigroup M
⊢ Function.Surjective ↑(subsemigroupMap f M')
[PROOFSTEP]
rintro ⟨_, x, hx, rfl⟩
[GOAL]
case mk.intro.intro
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
f : M →ₙ* N
M' : Subsemigroup M
x : M
hx : x ∈ ↑M'
⊢ ∃ a, ↑(subsemigroupMap f M') a = { val := ↑f x, property := (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f x) }
[PROOFSTEP]
exact ⟨⟨x, hx⟩, rfl⟩
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
S : Subsemigroup M
inst✝¹ : Nonempty M
inst✝ : Nonempty N
s : Subsemigroup M
t : Subsemigroup N
⊢ prod s t = ⊤ ↔ s = ⊤ ∧ t = ⊤
[PROOFSTEP]
simp only [eq_top_iff, le_prod_iff, ← (gc_map_comap _).le_iff_le, ← srange_eq_map, srange_fst, srange_snd]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝¹ : Mul M
inst✝ : Mul N
S T : Subsemigroup M
f : M →ₙ* N
g : N → M
h : Function.LeftInverse g ↑f
src✝ : M →ₙ* { x // x ∈ MulHom.srange f } := MulHom.srangeRestrict f
x : { x // x ∈ MulHom.srange f }
x' : M
hx' : ↑f x' = ↑x
⊢ ↑f (g ↑x) = ↑x
[PROOFSTEP]
rw [← hx', h x']
