A B : AddGroupCat
f : A ⟶ B
i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)
⊢ Epi f ↔ Function.Surjective ↑f
A B : AddGroupCat
f : A ⟶ B
⊢ Epi f ↔ Function.Surjective ↑f
have i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f) := by
  refine' ⟨_, groupAddGroupEquivalence.inverse.epi_of_epi_map⟩
  intro e'
  apply groupAddGroupEquivalence.inverse.map_epi
no goals
A B : AddGroupCat
f : A ⟶ B
i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)
⊢ Epi f ↔ Function.Surjective ↑f
rwa [GroupCat.epi_iff_surjective] at i1
A B : AddGroupCat
f : A ⟶ B
⊢ Epi f → Epi (groupAddGroupEquivalence.inverse.map f)
A B : AddGroupCat
f : A ⟶ B
⊢ Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)
refine' ⟨_, groupAddGroupEquivalence.inverse.epi_of_epi_map⟩
A B : AddGroupCat
f : A ⟶ B
e' : Epi f
⊢ Epi (groupAddGroupEquivalence.inverse.map f)
A B : AddGroupCat
f : A ⟶ B
⊢ Epi f → Epi (groupAddGroupEquivalence.inverse.map f)
intro e'
no goals
A B : AddGroupCat
f : A ⟶ B
e' : Epi f
⊢ Epi (groupAddGroupEquivalence.inverse.map f)
apply groupAddGroupEquivalence.inverse.map_epi