case a
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ H₁ ⊓ H₂
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ = 1
apply hdis.le_bot
case a.left
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₁.toSubmonoid

case a.right
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₂.toSubmonoid
case a
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ H₁ ⊓ H₂
constructor
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y * x⁻¹ * y⁻¹ = 1
⊢ x * y = y * x
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y * x⁻¹ * y⁻¹ = 1
⊢ _root_.Commute x y
show x * y = y * x
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y = (x⁻¹ * y⁻¹)⁻¹
⊢ x * y = y * x
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y * x⁻¹ * y⁻¹ = 1
⊢ x * y = y * x
rw [mul_assoc, mul_eq_one_iff_eq_inv] at this
no goals
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y = (x⁻¹ * y⁻¹)⁻¹
⊢ x * y = y * x
simp only [this, mul_inv_rev, inv_inv]
case a.left
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * (y * x⁻¹ * y⁻¹) ∈ H₁
case a.left
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₁.toSubmonoid
suffices x * (y * x⁻¹ * y⁻¹) ∈ H₁ by simpa [mul_assoc]
no goals
case a.left
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * (y * x⁻¹ * y⁻¹) ∈ H₁
exact H₁.mul_mem hx (hH₁.conj_mem _ (H₁.inv_mem hx) _)
no goals
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * (y * x⁻¹ * y⁻¹) ∈ H₁
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₁.toSubmonoid
simpa [mul_assoc]
case a.right
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ H₂
case a.right
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₂.toSubmonoid
show x * y * x⁻¹ * y⁻¹ ∈ H₂
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ ∈ H₂
case a.right
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ H₂
apply H₂.mul_mem _ (H₂.inv_mem hy)
no goals
G : Type u_1
G' : Type ?u.717622
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.717631
inst✝¹ : AddGroup A
N : Type ?u.717637
inst✝ : Group N
H₁ H₂ : Subgroup G
hH₁ : Normal H₁
hH₂ : Normal H₂
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ ∈ H₂
apply hH₂.conj_mem _ hy