case mp
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ prod s t ≤ u → map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u

case mpr
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u → prod s t ≤ u
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ prod s t ≤ u ↔ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u
constructor
case mp
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
⊢ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u
case mp
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ prod s t ≤ u → map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u
intro h
case mp.left
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
⊢ map (inl M N) s ≤ u

case mp.right
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
⊢ map (inr M N) t ≤ u
case mp
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
⊢ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u
constructor
case mp.left.intro.intro
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
x : M
hx : x ∈ ↑s
⊢ ↑(inl M N) x ∈ u
case mp.left
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
⊢ map (inl M N) s ≤ u
rintro _ ⟨x, hx, rfl⟩
case mp.left.intro.intro.a
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
x : M
hx : x ∈ ↑s
⊢ ↑(inl M N) x ∈ prod s t
case mp.left.intro.intro
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
x : M
hx : x ∈ ↑s
⊢ ↑(inl M N) x ∈ u
apply h
no goals
case mp.left.intro.intro.a
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
x : M
hx : x ∈ ↑s
⊢ ↑(inl M N) x ∈ prod s t
exact ⟨hx, Submonoid.one_mem _⟩
case mp.right.intro.intro
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
x : N
hx : x ∈ ↑t
⊢ ↑(inr M N) x ∈ u
case mp.right
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
⊢ map (inr M N) t ≤ u
rintro _ ⟨x, hx, rfl⟩
case mp.right.intro.intro.a
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
x : N
hx : x ∈ ↑t
⊢ ↑(inr M N) x ∈ prod s t
case mp.right.intro.intro
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
x : N
hx : x ∈ ↑t
⊢ ↑(inr M N) x ∈ u
apply h
no goals
case mp.right.intro.intro.a
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : prod s t ≤ u
x : N
hx : x ∈ ↑t
⊢ ↑(inr M N) x ∈ prod s t
exact ⟨Submonoid.one_mem _, hx⟩
case mpr.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
⊢ (x1, x2) ∈ u
case mpr
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u → prod s t ≤ u
rintro ⟨hH, hK⟩ ⟨x1, x2⟩ ⟨h1, h2⟩
case mpr.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
h1' : ↑(inl M N) x1 ∈ u
⊢ (x1, x2) ∈ u
case mpr.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
⊢ (x1, x2) ∈ u
have h1' : inl M N x1 ∈ u := by
  apply hH
  simpa using h1
case mpr.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
h1' : ↑(inl M N) x1 ∈ u
h2' : ↑(inr M N) x2 ∈ u
⊢ (x1, x2) ∈ u
case mpr.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
h1' : ↑(inl M N) x1 ∈ u
⊢ (x1, x2) ∈ u
have h2' : inr M N x2 ∈ u := by
  apply hK
  simpa using h2
no goals
case mpr.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
h1' : ↑(inl M N) x1 ∈ u
h2' : ↑(inr M N) x2 ∈ u
⊢ (x1, x2) ∈ u
simpa using Submonoid.mul_mem _ h1' h2'
case a
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
⊢ ↑(inl M N) x1 ∈ map (inl M N) s
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
⊢ ↑(inl M N) x1 ∈ u
apply hH
no goals
case a
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
⊢ ↑(inl M N) x1 ∈ map (inl M N) s
simpa using h1
case a
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
h1' : ↑(inl M N) x1 ∈ u
⊢ ↑(inr M N) x2 ∈ map (inr M N) t
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
h1' : ↑(inl M N) x1 ∈ u
⊢ ↑(inr M N) x2 ∈ u
apply hK
no goals
case a
M : Type u_1
N : Type u_2
P : Type ?u.111775
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.111796
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).fst ∈ ↑s
h2 : (x1, x2).snd ∈ ↑t
h1' : ↑(inl M N) x1 ∈ u
⊢ ↑(inr M N) x2 ∈ map (inr M N) t
simpa using h2