case h.h.a
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ Setoid.Rel (setoid ↑⊥ ↑H) a b ↔ Setoid.Rel (QuotientGroup.leftRel H) a b
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ Setoid.Rel (setoid ↑⊥ ↑H) = Setoid.Rel (QuotientGroup.leftRel H)
ext (a b)
case h.h.a
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ (∃ a_1, a_1 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_1 * a * b_1) ↔ a⁻¹ * b ∈ H
case h.h.a
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ Setoid.Rel (setoid ↑⊥ ↑H) a b ↔ Setoid.Rel (QuotientGroup.leftRel H) a b
rw [rel_iff, Setoid.Rel, QuotientGroup.leftRel_apply]
case h.h.a.mp
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ (∃ a_1, a_1 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_1 * a * b_1) → a⁻¹ * b ∈ H

case h.h.a.mpr
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ a⁻¹ * b ∈ H → ∃ a_2, a_2 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_2 * a * b_1
case h.h.a
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ (∃ a_1, a_1 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_1 * a * b_1) ↔ a⁻¹ * b ∈ H
constructor
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ a⁻¹ * (1 * a * b) ∈ H
case h.h.a.mp
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ (∃ a_1, a_1 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_1 * a * b_1) → a⁻¹ * b ∈ H
rintro ⟨a, rfl : a = 1, b, hb, rfl⟩
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ a⁻¹ * (1 * a * b) ∈ H
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ a⁻¹ * (1 * a * b) ∈ H
change a⁻¹ * (1 * a * b) ∈ H
no goals
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ a⁻¹ * (1 * a * b) ∈ H
rwa [one_mul, inv_mul_cancel_left]
case h.h.a.mpr
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
⊢ ∃ a_1, a_1 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_1 * a * b_1
case h.h.a.mpr
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ a⁻¹ * b ∈ H → ∃ a_2, a_2 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_2 * a * b_1
rintro (h : a⁻¹ * b ∈ H)
no goals
case h.h.a.mpr
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
⊢ ∃ a_1, a_1 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_1 * a * b_1
exact ⟨1, rfl, a⁻¹ * b, h, by rw [one_mul, mul_inv_cancel_left]⟩
no goals
G : Type u_1
inst✝¹ : Group G
α : Type ?u.15522
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
⊢ b = 1 * a * (a⁻¹ * b)
rw [one_mul, mul_inv_cancel_left]