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

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