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
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
ext x
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))
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
rw [← Quotient.out_eq' x]
no goals
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))
rfl