-- Mathlib/CategoryTheory/Functor/EpiMono.lean
theorem strongEpi_map_iff_strongEpi_of_isEquivalence [IsEquivalence F] :
    StrongEpi (F.map f) ↔ StrongEpi f

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
⊢ StrongEpi (F.map f) → StrongEpi f

Tactic:
intro

Result:
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
a✝ : StrongEpi (F.map f)
⊢ StrongEpi f

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f))
⊢ StrongEpi (F.inv.map (F.map f))

Tactic:
infer_instance

Result:
no goals

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
a✝ : StrongEpi f
⊢ StrongEpi (F.map f)

Tactic:
infer_instance

Result:
no goals

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f))
⊢ StrongEpi f

Tactic:
rw [StrongEpi.iff_of_arrow_iso e]

Result:
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f))
⊢ StrongEpi (F.inv.map (F.map f))

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
⊢ StrongEpi f → StrongEpi (F.map f)

Tactic:
intro

Result:
case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
a✝ : StrongEpi f
⊢ StrongEpi (F.map f)

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
⊢ StrongEpi (F.map f) ↔ StrongEpi f

Tactic:
constructor

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

case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
⊢ StrongEpi f → StrongEpi (F.map f)

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
a✝ : StrongEpi (F.map f)
⊢ StrongEpi f

Tactic:
have e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f)) :=
  Arrow.isoOfNatIso F.asEquivalence.unitIso (Arrow.mk f)

Result:
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f))
⊢ StrongEpi f