case mp
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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

case mpr
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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
constructor
case mp
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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
case mp
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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
intro h
case mp.left
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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

case mp.right
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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
case mp
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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
constructor
case mp.left.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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
case mp.left
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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
rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
no goals
case mp.left.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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
exact (h hy1).1
case mp.right.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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
case mp.right
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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
rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
no goals
case mp.right.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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
exact (h hy1).2
case mpr.intro.mk
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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
case mpr
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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
rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h
no goals
case mpr.intro.mk
M : Type u_1
N : Type u_2
P : Type ?u.58318
σ : Type ?u.58321
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
exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩