Theorem: Subsemigroup.prod_of_prodProperty (Kaplanski4/Absorbing.lean)

State before:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Subsemigroup M
t : Subsemigroup N
⊢ ProdProperty s ∧ ProdProperty t → ProdProperty (prod s t)
Tactic:
rintro ⟨hs, ht⟩ x y hxy
State after:
case intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Subsemigroup M
t : Subsemigroup N
hs : ProdProperty s
ht : ProdProperty t
x y : M × N
hxy : x * y ∈ prod s t
⊢ (∃ z ∈ prod s t, Associated x z) ∧ ∃ z ∈ prod s t, Associated y z

State before:
case intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Subsemigroup M
t : Subsemigroup N
hs : ProdProperty s
ht : ProdProperty t
x y : M × N
hxy : x * y ∈ prod s t
⊢ (∃ z ∈ prod s t, Associated x z) ∧ ∃ z ∈ prod s t, Associated y z
Tactic:
obtain ⟨⟨z, hz, hz₂⟩, z', hz', hz'₂⟩ := hs x.1 y.1 hxy.1
State after:
case intro.intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Subsemigroup M
t : Subsemigroup N
hs : ProdProperty s
ht : ProdProperty t
x y : M × N
hxy : x * y ∈ prod s t
z : M
hz : z ∈ s
hz₂ : Associated x.1 z
z' : M
hz' : z' ∈ s
hz'₂ : Associated y.1 z'
⊢ (∃ z ∈ prod s t, Associated x z) ∧ ∃ z ∈ prod s t, Associated y z

State before:
case intro.intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Subsemigroup M
t : Subsemigroup N
hs : ProdProperty s
ht : ProdProperty t
x y : M × N
hxy : x * y ∈ prod s t
z : M
hz : z ∈ s
hz₂ : Associated x.1 z
z' : M
hz' : z' ∈ s
hz'₂ : Associated y.1 z'
⊢ (∃ z ∈ prod s t, Associated x z) ∧ ∃ z ∈ prod s t, Associated y z
Tactic:
obtain ⟨⟨w, hw, hw₂⟩, w', hw', hw'₂⟩ := ht x.2 y.2 hxy.2
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Subsemigroup M
t : Subsemigroup N
hs : ProdProperty s
ht : ProdProperty t
x y : M × N
hxy : x * y ∈ prod s t
z : M
hz : z ∈ s
hz₂ : Associated x.1 z
z' : M
hz' : z' ∈ s
hz'₂ : Associated y.1 z'
w : N
hw : w ∈ t
hw₂ : Associated x.2 w
w' : N
hw' : w' ∈ t
hw'₂ : Associated y.2 w'
⊢ (∃ z ∈ prod s t, Associated x z) ∧ ∃ z ∈ prod s t, Associated y z

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Subsemigroup M
t : Subsemigroup N
hs : ProdProperty s
ht : ProdProperty t
x y : M × N
hxy : x * y ∈ prod s t
z : M
hz : z ∈ s
hz₂ : Associated x.1 z
z' : M
hz' : z' ∈ s
hz'₂ : Associated y.1 z'
w : N
hw : w ∈ t
hw₂ : Associated x.2 w
w' : N
hw' : w' ∈ t
hw'₂ : Associated y.2 w'
⊢ (∃ z ∈ prod s t, Associated x z) ∧ ∃ z ∈ prod s t, Associated y z
Tactic:
exact ⟨⟨(z, w), Subsemigroup.mem_prod.2 ⟨hz, hw⟩, Prod.associated_iff.2 ⟨hz₂, hw₂⟩⟩,
(z', w'), Subsemigroup.mem_prod.2 ⟨hz', hw'⟩, Prod.associated_iff.2 ⟨hz'₂, hw'₂⟩⟩
State after:
no goals