Theorem: Submonoid.snd_prodProperty (Kaplanski4/Absorbing.lean)

State before:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
⊢ Subsemigroup.ProdProperty (prod s t).toSubsemigroup → Subsemigroup.ProdProperty t.toSubsemigroup
Tactic:
rintro h x y hxy
State after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
h : Subsemigroup.ProdProperty (prod s t).toSubsemigroup
x y : N
hxy : x * y ∈ t.toSubsemigroup
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z

State before:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
h : Subsemigroup.ProdProperty (prod s t).toSubsemigroup
x y : N
hxy : x * y ∈ t.toSubsemigroup
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z
Tactic:
specialize h (1, x) (1, y)
State after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : N
hxy : x * y ∈ t.toSubsemigroup
h :
  (1, x) * (1, y) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (1, x) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (1, y) z
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z

State before:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : N
hxy : x * y ∈ t.toSubsemigroup
h :
  (1, x) * (1, y) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (1, x) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (1, y) z
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z
Tactic:
rw [Prod.one_mk_mul_one_mk] at h
State after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : N
hxy : x * y ∈ t.toSubsemigroup
h :
  (1, x * y) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (1, x) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (1, y) z
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z

State before:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : N
hxy : x * y ∈ t.toSubsemigroup
h :
  (1, x * y) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (1, x) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (1, y) z
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z
Tactic:
obtain ⟨⟨a, ha, ha₂⟩, b, hb, hb₂⟩ := h (Submonoid.mem_prod.2 ⟨s.one_mem, hxy⟩)
State after:
case intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : N
hxy : x * y ∈ t.toSubsemigroup
h :
  (1, x * y) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (1, x) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (1, y) z
a : M × N
ha : a ∈ (prod s t).toSubsemigroup
ha₂ : Associated (1, x) a
b : M × N
hb : b ∈ (prod s t).toSubsemigroup
hb₂ : Associated (1, y) b
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z

State before:
case intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : N
hxy : x * y ∈ t.toSubsemigroup
h :
  (1, x * y) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (1, x) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (1, y) z
a : M × N
ha : a ∈ (prod s t).toSubsemigroup
ha₂ : Associated (1, x) a
b : M × N
hb : b ∈ (prod s t).toSubsemigroup
hb₂ : Associated (1, y) b
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z
Tactic:
exact ⟨⟨a.2, (Submonoid.mem_prod.1 ha).2, (Subsemigroup.Prod.associated_iff.1 ha₂).2⟩, b.2,
  (Submonoid.mem_prod.1 hb).2, (Subsemigroup.Prod.associated_iff.1 hb₂).2⟩
State after:
no goals