-- Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean
theorem reflectsIsomorphisms_forget₂ [HasForget₂ C D] [(forget C).ReflectsIsomorphisms] :
    (forget₂ C D).ReflectsIsomorphisms :=
  { reflects := fun X Y f {i} => by
      haveI i' : IsIso ((forget D).map ((forget₂ C D).map f)) := Functor.map_isIso (forget D) _
      haveI : IsIso ((forget C).map f)

Proof state:
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : HasForget C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : HasForget D
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
⊢ IsIso ((forget C).map f)

Tactic:
have := @HasForget₂.forget_comp C D

Result:
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : HasForget C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : HasForget D
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
this :
  ∀ {inst : Category.{?u.985, u + 1} C} {inst_1 : HasForget C} {inst_2 : Category.{?u.984, u + 1} D}
    {inst_3 : HasForget D} [self : HasForget₂ C D], HasForget₂.forget₂ ⋙ forget D = forget C
⊢ IsIso ((forget C).map f)

Proof state:
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : HasForget C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : HasForget D
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
this :
  ∀ {inst : Category.{?u.985, u + 1} C} {inst_1 : HasForget C} {inst_2 : Category.{?u.984, u + 1} D}
    {inst_3 : HasForget D} [self : HasForget₂ C D], HasForget₂.forget₂ ⋙ forget D = forget C
⊢ IsIso ((forget C).map f)

Tactic:
rwa [← this]

Result:
no goals

Proof state:
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : HasForget C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : HasForget D
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
⊢ IsIso f

Tactic:
haveI : IsIso ((forget C).map f) := by
  have := @HasForget₂.forget_comp C D
  rwa [← this]

Result:
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : HasForget C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : HasForget D
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
this : IsIso ((forget C).map f)
⊢ IsIso f

Proof state:
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : HasForget C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : HasForget D
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
⊢ IsIso f

Tactic:
haveI i' : IsIso ((forget D).map ((forget₂ C D).map f)) := Functor.map_isIso (forget D) _

Result:
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : HasForget C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : HasForget D
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
⊢ IsIso f

Proof state:
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : HasForget C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : HasForget D
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
this : IsIso ((forget C).map f)
⊢ IsIso f

Tactic:
apply isIso_of_reflects_iso f (forget C)

Result:
no goals