Theorem: Submonoid.fst_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 s.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 : M
hxy : x * y ∈ s.toSubsemigroup
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.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 : M
hxy : x * y ∈ s.toSubsemigroup
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.toSubsemigroup, Associated y z
Tactic:
specialize h (x, 1) (y, 1)
State after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : M
hxy : x * y ∈ s.toSubsemigroup
h :
  (x, 1) * (y, 1) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (x, 1) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (y, 1) z
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.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 : M
hxy : x * y ∈ s.toSubsemigroup
h :
  (x, 1) * (y, 1) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (x, 1) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (y, 1) z
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.toSubsemigroup, Associated y z
Tactic:
rw [Prod.mk_one_mul_mk_one] 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 : M
hxy : x * y ∈ s.toSubsemigroup
h :
  (x * y, 1) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (x, 1) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (y, 1) z
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.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 : M
hxy : x * y ∈ s.toSubsemigroup
h :
  (x * y, 1) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (x, 1) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (y, 1) z
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.toSubsemigroup, Associated y z
Tactic:
obtain ⟨⟨a, ha, ha₂⟩, b, hb, hb₂⟩ := h (Submonoid.mem_prod.2 ⟨hxy, t.one_mem⟩)
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 : M
hxy : x * y ∈ s.toSubsemigroup
h :
  (x * y, 1) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (x, 1) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (y, 1) z
a : M × N
ha : a ∈ (prod s t).toSubsemigroup
ha₂ : Associated (x, 1) a
b : M × N
hb : b ∈ (prod s t).toSubsemigroup
hb₂ : Associated (y, 1) b
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.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 : M
hxy : x * y ∈ s.toSubsemigroup
h :
  (x * y, 1) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (x, 1) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (y, 1) z
a : M × N
ha : a ∈ (prod s t).toSubsemigroup
ha₂ : Associated (x, 1) a
b : M × N
hb : b ∈ (prod s t).toSubsemigroup
hb₂ : Associated (y, 1) b
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.toSubsemigroup, Associated y z
Tactic:
exact ⟨⟨a.1, (Submonoid.mem_prod.1 ha).1, (Subsemigroup.Prod.associated_iff.1 ha₂).1⟩, b.1,
  (Submonoid.mem_prod.1 hb).1, (Subsemigroup.Prod.associated_iff.1 hb₂).1⟩
State after:
no goals