case mp
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
⊢ StrongEpi (F.map f) → StrongEpi f

case mpr
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
⊢ StrongEpi f → StrongEpi (F.map f)
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
⊢ StrongEpi (F.map f) ↔ StrongEpi f
constructor
case mp
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
a✝ : StrongEpi (F.map f)
⊢ StrongEpi f
case mp
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
⊢ StrongEpi (F.map f) → StrongEpi f
intro
case mp
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk ((inv F).map (F.map f))
⊢ StrongEpi f
case mp
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
a✝ : StrongEpi (F.map f)
⊢ StrongEpi f
have e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f)) :=
  Arrow.isoOfNatIso F.asEquivalence.unitIso (Arrow.mk f)
case mp
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk ((inv F).map (F.map f))
⊢ StrongEpi ((inv F).map (F.map f))
case mp
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk ((inv F).map (F.map f))
⊢ StrongEpi f
rw [StrongEpi.iff_of_arrow_iso e]
no goals
case mp
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk ((inv F).map (F.map f))
⊢ StrongEpi ((inv F).map (F.map f))
infer_instance
case mpr
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
a✝ : StrongEpi f
⊢ StrongEpi (F.map f)
case mpr
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
⊢ StrongEpi f → StrongEpi (F.map f)
intro
no goals
case mpr
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
a✝ : StrongEpi f
⊢ StrongEpi (F.map f)
infer_instance