[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
a b c d : G
hab : Setoid.r a b
hcd : Setoid.r c d
⊢ Setoid.r (a * c) (b * d)
[PROOFSTEP]
rw [leftRel_eq] at hab hcd ⊢
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
a b c d : G
hab : a⁻¹ * b ∈ N
hcd : c⁻¹ * d ∈ N
⊢ (fun x y => x⁻¹ * y ∈ N) (a * c) (b * d)
[PROOFSTEP]
dsimp only
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
a b c d : G
hab : a⁻¹ * b ∈ N
hcd : c⁻¹ * d ∈ N
⊢ (a * c)⁻¹ * (b * d) ∈ N
[PROOFSTEP]
calc
  (a * c)⁻¹ * (b * d) = c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) := by
    simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
  _ ∈ N := N.mul_mem (nN.conj_mem _ hab _) hcd
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
a b c d : G
hab : a⁻¹ * b ∈ N
hcd : c⁻¹ * d ∈ N
⊢ (a * c)⁻¹ * (b * d) = c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d)
[PROOFSTEP]
simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
x y : G
⊢ x⁻¹ * y ∈ N ↔ ∃ z, z ∈ N ∧ x * z = y
[PROOFSTEP]
simp only [← _root_.eq_inv_mul_iff_mul_eq, exists_prop, exists_eq_right]
[GOAL]
G : Type u
inst✝¹ : Group G
N✝ : Subgroup G
nN✝ : Subgroup.Normal N✝
H : Type v
inst✝ : Group H
N : Subgroup G
nN : Subgroup.Normal N
x : G
⊢ ↑x = 1 ↔ x ∈ N
[PROOFSTEP]
refine' QuotientGroup.eq.trans _
[GOAL]
G : Type u
inst✝¹ : Group G
N✝ : Subgroup G
nN✝ : Subgroup.Normal N✝
H : Type v
inst✝ : Group H
N : Subgroup G
nN : Subgroup.Normal N
x : G
⊢ x⁻¹ * 1 ∈ N ↔ x ∈ N
[PROOFSTEP]
rw [mul_one, Subgroup.inv_mem_iff]
[GOAL]
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
I : Type w
inst✝¹ : Group I
f : G →* H
inst✝ : Subgroup.Normal (MonoidHom.range f)
g : H →* I
h : MonoidHom.comp (mk' (MonoidHom.range f)) (Subgroup.subtype (MonoidHom.ker g)) = 1
x : H
hx : x ∈ MonoidHom.ker g
⊢ ↑x = 1
[PROOFSTEP]
exact FunLike.congr_fun h ⟨x, hx⟩
[GOAL]
G : Type u
inst✝¹ : Group G
N✝ : Subgroup G
nN✝ : Subgroup.Normal N✝
H : Type v
inst✝ : Group H
N : Subgroup G
nN : Subgroup.Normal N
x y : G
⊢ ↑x = ↑y ↔ x / y ∈ N
[PROOFSTEP]
refine' eq_comm.trans (QuotientGroup.eq.trans _)
[GOAL]
G : Type u
inst✝¹ : Group G
N✝ : Subgroup G
nN✝ : Subgroup.Normal N✝
H : Type v
inst✝ : Group H
N : Subgroup G
nN : Subgroup.Normal N
x y : G
⊢ y⁻¹ * x ∈ N ↔ x / y ∈ N
[PROOFSTEP]
rw [nN.mem_comm_iff, div_eq_mul_inv]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
HN : ∀ (x : G), x ∈ N → ↑φ x = 1
x y : G
h : ↑(QuotientGroup.con N) x y
⊢ ↑(Con.ker φ) x y
[PROOFSTEP]
simp only [QuotientGroup.con, leftRel_apply, Con.rel_mk] at h 
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
HN : ∀ (x : G), x ∈ N → ↑φ x = 1
x y : G
h : x⁻¹ * y ∈ N
⊢ ↑(Con.ker φ) x y
[PROOFSTEP]
rw [Con.ker_rel]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
HN : ∀ (x : G), x ∈ N → ↑φ x = 1
x y : G
h : x⁻¹ * y ∈ N
⊢ ↑φ x = ↑φ y
[PROOFSTEP]
calc
  φ x = φ (y * (x⁻¹ * y)⁻¹) := by rw [mul_inv_rev, inv_inv, mul_inv_cancel_left]
  _ = φ y := by rw [φ.map_mul, HN _ (N.inv_mem h), mul_one]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
HN : ∀ (x : G), x ∈ N → ↑φ x = 1
x y : G
h : x⁻¹ * y ∈ N
⊢ ↑φ x = ↑φ (y * (x⁻¹ * y)⁻¹)
[PROOFSTEP]
rw [mul_inv_rev, inv_inv, mul_inv_cancel_left]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
HN : ∀ (x : G), x ∈ N → ↑φ x = 1
x y : G
h : x⁻¹ * y ∈ N
⊢ ↑φ (y * (x⁻¹ * y)⁻¹) = ↑φ y
[PROOFSTEP]
rw [φ.map_mul, HN _ (N.inv_mem h), mul_one]
[GOAL]
G : Type u
inst✝² : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝¹ : Group H
M : Subgroup H
inst✝ : Subgroup.Normal M
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ G ⧸ N →* H ⧸ M
[PROOFSTEP]
refine' QuotientGroup.lift N ((mk' M).comp f) _
[GOAL]
G : Type u
inst✝² : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝¹ : Group H
M : Subgroup H
inst✝ : Subgroup.Normal M
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ ∀ (x : G), x ∈ N → ↑(MonoidHom.comp (mk' M) f) x = 1
[PROOFSTEP]
intro x hx
[GOAL]
G : Type u
inst✝² : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝¹ : Group H
M : Subgroup H
inst✝ : Subgroup.Normal M
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
⊢ ↑(MonoidHom.comp (mk' M) f) x = 1
[PROOFSTEP]
refine' QuotientGroup.eq.2 _
[GOAL]
G : Type u
inst✝² : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝¹ : Group H
M : Subgroup H
inst✝ : Subgroup.Normal M
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
⊢ (↑f x)⁻¹ * 1 ∈ M
[PROOFSTEP]
rw [mul_one, Subgroup.inv_mem_iff]
[GOAL]
G : Type u
inst✝² : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝¹ : Group H
M : Subgroup H
inst✝ : Subgroup.Normal M
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
⊢ ↑f x ∈ M
[PROOFSTEP]
exact h hx
[GOAL]
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
I : Type u_1
inst✝² : Group I
M : Subgroup H
O : Subgroup I
inst✝¹ : Subgroup.Normal M
inst✝ : Subgroup.Normal O
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : optParam (N ≤ Subgroup.comap (MonoidHom.comp g f) O) (_ : N ≤ Subgroup.comap (MonoidHom.comp g f) O)
x : G ⧸ N
⊢ ↑(map M O g hg) (↑(map N M f hf) x) = ↑(map N O (MonoidHom.comp g f) hgf) x
[PROOFSTEP]
refine' induction_on' x fun x => _
[GOAL]
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
I : Type u_1
inst✝² : Group I
M : Subgroup H
O : Subgroup I
inst✝¹ : Subgroup.Normal M
inst✝ : Subgroup.Normal O
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : optParam (N ≤ Subgroup.comap (MonoidHom.comp g f) O) (_ : N ≤ Subgroup.comap (MonoidHom.comp g f) O)
x✝ : G ⧸ N
x : G
⊢ ↑(map M O g hg) (↑(map N M f hf) ↑x) = ↑(map N O (MonoidHom.comp g f) hgf) ↑x
[PROOFSTEP]
simp only [map_mk, MonoidHom.comp_apply]
[GOAL]
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
G' : Subgroup G
H' : Subgroup H
inst✝¹ : Subgroup.Normal G'
inst✝ : Subgroup.Normal H'
e : G ≃* H
he : Subgroup.map (↑e) G' = H'
src✝ : G ⧸ G' →* H ⧸ H' := map G' H' ↑e (_ : G' ≤ Subgroup.comap (↑e) H')
x : G ⧸ G'
⊢ ↑(map H' G' ↑(MulEquiv.symm e) (_ : H' ≤ Subgroup.comap (↑(MulEquiv.symm e)) G'))
      (↑(map G' H' ↑e (_ : G' ≤ Subgroup.comap (↑e) H')) x) =
    x
[PROOFSTEP]
rw [map_map G' H' G' e e.symm (he ▸ G'.le_comap_map (e : G →* H)) (he ▸ (G'.map_equiv_eq_comap_symm e).le)]
[GOAL]
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
G' : Subgroup G
H' : Subgroup H
inst✝¹ : Subgroup.Normal G'
inst✝ : Subgroup.Normal H'
e : G ≃* H
he : Subgroup.map (↑e) G' = H'
src✝ : G ⧸ G' →* H ⧸ H' := map G' H' ↑e (_ : G' ≤ Subgroup.comap (↑e) H')
x : G ⧸ G'
⊢ ↑(map G' G' (MonoidHom.comp ↑(MulEquiv.symm e) ↑e)
          (_ : G' ≤ Subgroup.comap (MonoidHom.comp ↑(MulEquiv.symm e) ↑e) G'))
      x =
    x
[PROOFSTEP]
simp only [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm, MulEquiv.coe_monoidHom_refl, map_id_apply]
[GOAL]
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
G' : Subgroup G
H' : Subgroup H
inst✝¹ : Subgroup.Normal G'
inst✝ : Subgroup.Normal H'
e : G ≃* H
he : Subgroup.map (↑e) G' = H'
src✝ : G ⧸ G' →* H ⧸ H' := map G' H' ↑e (_ : G' ≤ Subgroup.comap (↑e) H')
x : H ⧸ H'
⊢ ↑(map G' H' ↑e (_ : G' ≤ Subgroup.comap (↑e) H'))
      (↑(map H' G' ↑(MulEquiv.symm e) (_ : H' ≤ Subgroup.comap (↑(MulEquiv.symm e)) G')) x) =
    x
[PROOFSTEP]
rw [map_map H' G' H' e.symm e (he ▸ (G'.map_equiv_eq_comap_symm e).le) (he ▸ G'.le_comap_map (e : G →* H))]
[GOAL]
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
G' : Subgroup G
H' : Subgroup H
inst✝¹ : Subgroup.Normal G'
inst✝ : Subgroup.Normal H'
e : G ≃* H
he : Subgroup.map (↑e) G' = H'
src✝ : G ⧸ G' →* H ⧸ H' := map G' H' ↑e (_ : G' ≤ Subgroup.comap (↑e) H')
x : H ⧸ H'
⊢ ↑(map H' H' (MonoidHom.comp ↑e ↑(MulEquiv.symm e))
          (_ : H' ≤ Subgroup.comap (MonoidHom.comp ↑e ↑(MulEquiv.symm e)) H'))
      x =
    x
[PROOFSTEP]
simp only [← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self, MulEquiv.coe_monoidHom_refl, map_id_apply]
[GOAL]
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
G' : Subgroup G
H' : Subgroup H
inst✝¹ : Subgroup.Normal G'
inst✝ : Subgroup.Normal H'
he : optParam (Subgroup.map (↑(MulEquiv.refl G)) G' = G') (_ : Subgroup.map (MonoidHom.id G) G' = G')
⊢ congr G' G' (MulEquiv.refl G) he = MulEquiv.refl (G ⧸ G')
[PROOFSTEP]
ext ⟨x⟩
[GOAL]
case h.mk
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
G' : Subgroup G
H' : Subgroup H
inst✝¹ : Subgroup.Normal G'
inst✝ : Subgroup.Normal H'
he : optParam (Subgroup.map (↑(MulEquiv.refl G)) G' = G') (_ : Subgroup.map (MonoidHom.id G) G' = G')
x✝ : G ⧸ G'
x : G
⊢ ↑(congr G' G' (MulEquiv.refl G) he) (Quot.mk Setoid.r x) = ↑(MulEquiv.refl (G ⧸ G')) (Quot.mk Setoid.r x)
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ ker φ
a b : G
h : ↑φ a = ↑φ b
⊢ Setoid.r a b
[PROOFSTEP]
rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_self]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
g : G
hg : g ∈ ker φ
⊢ g ∈ ker (rangeRestrict φ)
[PROOFSTEP]
rwa [ker_rangeRestrict]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ ker φ
a b : G
h : ↑(rangeRestrict φ) a = ↑(rangeRestrict φ) b
⊢ Setoid.r a b
[PROOFSTEP]
rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h, φ.rangeRestrict.map_inv, inv_mul_self]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Surjective ↑(rangeKerLift φ)
[PROOFSTEP]
rintro ⟨_, g, rfl⟩
[GOAL]
case mk.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ ∃ a, ↑(rangeKerLift φ) a = { val := ↑φ g, property := (_ : ∃ y, ↑φ y = ↑φ g) }
[PROOFSTEP]
use mk g
[GOAL]
case h
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ ↑(rangeKerLift φ) ↑g = { val := ↑φ g, property := (_ : ∃ y, ↑φ y = ↑φ g) }
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
ψ : H → G
hφ : Function.RightInverse ψ ↑φ
src✝ : G ⧸ ker φ →* H := kerLift φ
x : G ⧸ ker φ
⊢ ↑(kerLift φ) ((mk ∘ ψ) (↑(kerLift φ) x)) = ↑(kerLift φ) x
[PROOFSTEP]
rw [Function.comp_apply, kerLift_mk', hφ]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
A' A B' B : Subgroup G
hAN : Subgroup.Normal (Subgroup.subgroupOf A' A)
hBN : Subgroup.Normal (Subgroup.subgroupOf B' B)
h' : A' = B'
h : A = B
⊢ MonoidHom.comp (quotientMapSubgroupOfOfLe (_ : B' ≤ A') (_ : B ≤ A))
      (quotientMapSubgroupOfOfLe (_ : A' ≤ B') (_ : A ≤ B)) =
    MonoidHom.id ({ x // x ∈ A } ⧸ Subgroup.subgroupOf A' A)
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case h.h.mk
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
A' A B' B : Subgroup G
hAN : Subgroup.Normal (Subgroup.subgroupOf A' A)
hBN : Subgroup.Normal (Subgroup.subgroupOf B' B)
h' : A' = B'
h : A = B
x : G
hx : x ∈ A
⊢ ↑(MonoidHom.comp
          (MonoidHom.comp (quotientMapSubgroupOfOfLe (_ : B' ≤ A') (_ : B ≤ A))
            (quotientMapSubgroupOfOfLe (_ : A' ≤ B') (_ : A ≤ B)))
          (mk' (Subgroup.subgroupOf A' A)))
      { val := x, property := hx } =
    ↑(MonoidHom.comp (MonoidHom.id ({ x // x ∈ A } ⧸ Subgroup.subgroupOf A' A)) (mk' (Subgroup.subgroupOf A' A)))
      { val := x, property := hx }
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
A' A B' B : Subgroup G
hAN : Subgroup.Normal (Subgroup.subgroupOf A' A)
hBN : Subgroup.Normal (Subgroup.subgroupOf B' B)
h' : A' = B'
h : A = B
⊢ MonoidHom.comp (quotientMapSubgroupOfOfLe (_ : A' ≤ B') (_ : A ≤ B))
      (quotientMapSubgroupOfOfLe (_ : B' ≤ A') (_ : B ≤ A)) =
    MonoidHom.id ({ x // x ∈ B } ⧸ Subgroup.subgroupOf B' B)
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case h.h.mk
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
A' A B' B : Subgroup G
hAN : Subgroup.Normal (Subgroup.subgroupOf A' A)
hBN : Subgroup.Normal (Subgroup.subgroupOf B' B)
h' : A' = B'
h : A = B
x : G
hx : x ∈ B
⊢ ↑(MonoidHom.comp
          (MonoidHom.comp (quotientMapSubgroupOfOfLe (_ : A' ≤ B') (_ : A ≤ B))
            (quotientMapSubgroupOfOfLe (_ : B' ≤ A') (_ : B ≤ A)))
          (mk' (Subgroup.subgroupOf B' B)))
      { val := x, property := hx } =
    ↑(MonoidHom.comp (MonoidHom.id ({ x // x ∈ B } ⧸ Subgroup.subgroupOf B' B)) (mk' (Subgroup.subgroupOf B' B)))
      { val := x, property := hx }
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g✝ : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
g : A
x✝ : g ∈ range (zpowGroupHom n)
h : A
hg : h ^ n = g
⊢ ↑(zpowGroupHom n) (↑f h) = ↑f g
[PROOFSTEP]
simp only [← hg, map_zpow, zpowGroupHom_apply]
[GOAL]
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
⊢ MulEquiv.refl (A ⧸ range (zpowGroupHom n)) = equivQuotientZPowOfEquiv (MulEquiv.refl A) n
[PROOFSTEP]
ext x
[GOAL]
case h
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
x : A ⧸ range (zpowGroupHom n)
⊢ ↑(MulEquiv.refl (A ⧸ range (zpowGroupHom n))) x = ↑(equivQuotientZPowOfEquiv (MulEquiv.refl A) n) x
[PROOFSTEP]
rw [← Quotient.out_eq' x]
[GOAL]
case h
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
x : A ⧸ range (zpowGroupHom n)
⊢ ↑(MulEquiv.refl (A ⧸ range (zpowGroupHom n))) (Quotient.mk'' (Quotient.out' x)) =
    ↑(equivQuotientZPowOfEquiv (MulEquiv.refl A) n) (Quotient.mk'' (Quotient.out' x))
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
⊢ MulEquiv.trans (equivQuotientZPowOfEquiv e n) (equivQuotientZPowOfEquiv d n) =
    equivQuotientZPowOfEquiv (MulEquiv.trans e d) n
[PROOFSTEP]
ext x
[GOAL]
case h
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
x : A ⧸ range (zpowGroupHom n)
⊢ ↑(MulEquiv.trans (equivQuotientZPowOfEquiv e n) (equivQuotientZPowOfEquiv d n)) x =
    ↑(equivQuotientZPowOfEquiv (MulEquiv.trans e d) n) x
[PROOFSTEP]
rw [← Quotient.out_eq' x]
[GOAL]
case h
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
x : A ⧸ range (zpowGroupHom n)
⊢ ↑(MulEquiv.trans (equivQuotientZPowOfEquiv e n) (equivQuotientZPowOfEquiv d n)) (Quotient.mk'' (Quotient.out' x)) =
    ↑(equivQuotientZPowOfEquiv (MulEquiv.trans e d) n) (Quotient.mk'' (Quotient.out' x))
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
⊢ ∀ (a : { x // x ∈ H ⊔ N }), ∃ a_1, ↑φ a_1 = Quotient.mk'' a
[PROOFSTEP]
rintro ⟨y, hy : y ∈ (H ⊔ N)⟩
[GOAL]
case mk
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
y : G
hy : y ∈ H ⊔ N
⊢ ∃ a, ↑φ a = Quotient.mk'' { val := y, property := hy }
[PROOFSTEP]
rw [← SetLike.mem_coe] at hy 
[GOAL]
case mk
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
y : G
hy✝ : y ∈ H ⊔ N
hy : y ∈ ↑(H ⊔ N)
⊢ ∃ a, ↑φ a = Quotient.mk'' { val := y, property := hy✝ }
[PROOFSTEP]
rw [mul_normal H N] at hy 
[GOAL]
case mk
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
y : G
hy✝ : y ∈ H ⊔ N
hy : y ∈ ↑H * ↑N
⊢ ∃ a, ↑φ a = Quotient.mk'' { val := y, property := hy✝ }
[PROOFSTEP]
rcases hy with ⟨h, n, hh, hn, rfl⟩
[GOAL]
case mk.intro.intro.intro.intro
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
h n : G
hh : h ∈ ↑H
hn : n ∈ ↑N
hy : (fun x x_1 => x * x_1) h n ∈ H ⊔ N
⊢ ∃ a, ↑φ a = Quotient.mk'' { val := (fun x x_1 => x * x_1) h n, property := hy }
[PROOFSTEP]
use⟨h, hh⟩
[GOAL]
case h
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
h n : G
hh : h ∈ ↑H
hn : n ∈ ↑N
hy : (fun x x_1 => x * x_1) h n ∈ H ⊔ N
⊢ ↑φ { val := h, property := hh } = Quotient.mk'' { val := (fun x x_1 => x * x_1) h n, property := hy }
[PROOFSTEP]
let _ : Setoid ↑(H ⊔ N) :=
  (@leftRel ↑(H ⊔ N) (H ⊔ N : Subgroup G).toGroup (N.subgroupOf (H ⊔ N)))
    -- porting note: Lean couldn't find this automatically
[GOAL]
case h
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
h n : G
hh : h ∈ ↑H
hn : n ∈ ↑N
hy : (fun x x_1 => x * x_1) h n ∈ H ⊔ N
x✝ : Setoid { x // x ∈ H ⊔ N } := leftRel (subgroupOf N (H ⊔ N))
⊢ ↑φ { val := h, property := hh } = Quotient.mk'' { val := (fun x x_1 => x * x_1) h n, property := hy }
[PROOFSTEP]
refine Quotient.eq.mpr ?_
[GOAL]
case h
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
h n : G
hh : h ∈ ↑H
hn : n ∈ ↑N
hy : (fun x x_1 => x * x_1) h n ∈ H ⊔ N
x✝ : Setoid { x // x ∈ H ⊔ N } := leftRel (subgroupOf N (H ⊔ N))
⊢ ↑(inclusion (_ : H ≤ H ⊔ N)) { val := h, property := hh } ≈ { val := (fun x x_1 => x * x_1) h n, property := hy }
[PROOFSTEP]
change Setoid.r _ _
[GOAL]
case h
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
h n : G
hh : h ∈ ↑H
hn : n ∈ ↑N
hy : (fun x x_1 => x * x_1) h n ∈ H ⊔ N
x✝ : Setoid { x // x ∈ H ⊔ N } := leftRel (subgroupOf N (H ⊔ N))
⊢ Setoid.r (↑(inclusion (_ : H ≤ H ⊔ N)) { val := h, property := hh })
    { val := (fun x x_1 => x * x_1) h n, property := hy }
[PROOFSTEP]
rw [leftRel_apply]
[GOAL]
case h
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
h n : G
hh : h ∈ ↑H
hn : n ∈ ↑N
hy : (fun x x_1 => x * x_1) h n ∈ H ⊔ N
x✝ : Setoid { x // x ∈ H ⊔ N } := leftRel (subgroupOf N (H ⊔ N))
⊢ (↑(inclusion (_ : H ≤ H ⊔ N)) { val := h, property := hh })⁻¹ *
      { val := (fun x x_1 => x * x_1) h n, property := hy } ∈
    subgroupOf N (H ⊔ N)
[PROOFSTEP]
change h⁻¹ * (h * n) ∈ N
[GOAL]
case h
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
h n : G
hh : h ∈ ↑H
hn : n ∈ ↑N
hy : (fun x x_1 => x * x_1) h n ∈ H ⊔ N
x✝ : Setoid { x // x ∈ H ⊔ N } := leftRel (subgroupOf N (H ⊔ N))
⊢ h⁻¹ * (h * n) ∈ N
[PROOFSTEP]
rwa [← mul_assoc, inv_mul_self, one_mul]
[GOAL]
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
φ_surjective : Surjective ↑φ
⊢ subgroupOf N H = ker φ
[PROOFSTEP]
simp [← comap_ker]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
M : Subgroup G
nM : Subgroup.Normal M
h : N ≤ M
⊢ ∀ (x : G ⧸ N), x ∈ Subgroup.map (mk' N) M → ↑(map N M (MonoidHom.id G) h) x = 1
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
M : Subgroup G
nM : Subgroup.Normal M
h : N ≤ M
x : G
hx : x ∈ ↑M
⊢ ↑(map N M (MonoidHom.id G) h) (↑(mk' N) x) = 1
[PROOFSTEP]
rw [map_mk' N M _ _ x]
[GOAL]
case intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
M : Subgroup G
nM : Subgroup.Normal M
h : N ≤ M
x : G
hx : x ∈ ↑M
⊢ ↑(↑(MonoidHom.id G) x) = 1
[PROOFSTEP]
exact (QuotientGroup.eq_one_iff _).mpr hx
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
M : Subgroup G
nM : Subgroup.Normal M
h : N ≤ M
⊢ MonoidHom.comp (map M (Subgroup.map (mk' N) M) (mk' N) (_ : M ≤ Subgroup.comap (mk' N) (Subgroup.map (mk' N) M)))
      (quotientQuotientEquivQuotientAux N M h) =
    MonoidHom.id ((G ⧸ N) ⧸ Subgroup.map (mk' N) M)
[PROOFSTEP]
ext
[GOAL]
case h.h.h
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
M : Subgroup G
nM : Subgroup.Normal M
h : N ≤ M
x✝ : G
⊢ ↑(MonoidHom.comp
          (MonoidHom.comp
            (MonoidHom.comp
              (map M (Subgroup.map (mk' N) M) (mk' N) (_ : M ≤ Subgroup.comap (mk' N) (Subgroup.map (mk' N) M)))
              (quotientQuotientEquivQuotientAux N M h))
            (mk' (Subgroup.map (mk' N) M)))
          (mk' N))
      x✝ =
    ↑(MonoidHom.comp (MonoidHom.comp (MonoidHom.id ((G ⧸ N) ⧸ Subgroup.map (mk' N) M)) (mk' (Subgroup.map (mk' N) M)))
          (mk' N))
      x✝
[PROOFSTEP]
simp
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
M : Subgroup G
nM : Subgroup.Normal M
h : N ≤ M
⊢ MonoidHom.comp (quotientQuotientEquivQuotientAux N M h)
      (map M (Subgroup.map (mk' N) M) (mk' N) (_ : M ≤ Subgroup.comap (mk' N) (Subgroup.map (mk' N) M))) =
    MonoidHom.id (G ⧸ M)
[PROOFSTEP]
ext
[GOAL]
case h.h
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
M : Subgroup G
nM : Subgroup.Normal M
h : N ≤ M
x✝ : G
⊢ ↑(MonoidHom.comp
          (MonoidHom.comp (quotientQuotientEquivQuotientAux N M h)
            (map M (Subgroup.map (mk' N) M) (mk' N) (_ : M ≤ Subgroup.comap (mk' N) (Subgroup.map (mk' N) M))))
          (mk' M))
      x✝ =
    ↑(MonoidHom.comp (MonoidHom.id (G ⧸ M)) (mk' M)) x✝
[PROOFSTEP]
simp
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Subsingleton (G ⧸ ⊤)
[PROOFSTEP]
dsimp [HasQuotient.Quotient, QuotientGroup.instHasQuotientSubgroup, Quotient]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Subsingleton (Quot Setoid.r)
[PROOFSTEP]
rw [leftRel_eq]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Subsingleton (Quot fun x y => x⁻¹ * y ∈ ⊤)
[PROOFSTEP]
exact Trunc.instSubsingletonTrunc
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H✝ : Type v
inst✝ : Group H✝
φ : G →* H✝
H : Subgroup G
h : Subsingleton (G ⧸ H)
x : G
x✝ : x ∈ ⊤
⊢ x ∈ H
[PROOFSTEP]
have this : 1⁻¹ * x ∈ H := QuotientGroup.eq.1 (Subsingleton.elim _ _)
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H✝ : Type v
inst✝ : Group H✝
φ : G →* H✝
H : Subgroup G
h : Subsingleton (G ⧸ H)
x : G
x✝ : x ∈ ⊤
this : 1⁻¹ * x ∈ H
⊢ x ∈ H
[PROOFSTEP]
rwa [inv_one, one_mul] at this 
[GOAL]
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
φ : G →* H
H₁ : Subgroup G
inst✝¹ : Subgroup.Normal H₁
H₂ : Subgroup (G ⧸ H₁)
inst✝ : Subgroup.Normal H₂
⊢ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) =
    Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))
[PROOFSTEP]
ext x
[GOAL]
case h
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
φ : G →* H
H₁ : Subgroup G
inst✝¹ : Subgroup.Normal H₁
H₂ : Subgroup (G ⧸ H₁)
inst✝ : Subgroup.Normal H₂
x : G
⊢ x ∈ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) ↔
    x ∈ Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))
[PROOFSTEP]
simp only [mk'_apply, Subgroup.mem_comap, Subgroup.mem_center_iff, forall_mk, ← mk_mul, eq_iff_div_mem, mk_div]
