[GOAL]
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : ReflectsIsomorphisms (forget C)
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
⊢ IsIso f
[PROOFSTEP]
skip
[GOAL]
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : ReflectsIsomorphisms (forget C)
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
⊢ IsIso f
[PROOFSTEP]
haveI i' : IsIso ((forget D).map ((forget₂ C D).map f)) := Functor.map_isIso (forget D) _
[GOAL]
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : ReflectsIsomorphisms (forget C)
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
[PROOFSTEP]
haveI : IsIso ((forget C).map f) := by
  have := @HasForget₂.forget_comp C D
  rw [← this]
  exact i'
[GOAL]
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : ReflectsIsomorphisms (forget C)
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)
[PROOFSTEP]
have := @HasForget₂.forget_comp C D
[GOAL]
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : ReflectsIsomorphisms (forget C)
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.1872, u + 1} C] [inst_1 : ConcreteCategory C] [inst_2 : Category.{?u.1871, u + 1} D]
    [inst_3 : ConcreteCategory D] [self : HasForget₂ C D], HasForget₂.forget₂ ⋙ forget D = forget C
⊢ IsIso ((forget C).map f)
[PROOFSTEP]
rw [← this]
[GOAL]
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : ReflectsIsomorphisms (forget C)
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_1, u + 1} C] [inst_1 : ConcreteCategory C] [inst_2 : Category.{u_2, u + 1} D]
    [inst_3 : ConcreteCategory D] [self : HasForget₂ C D], HasForget₂.forget₂ ⋙ forget D = forget C
⊢ IsIso ((HasForget₂.forget₂ ⋙ forget D).map f)
[PROOFSTEP]
exact i'
[GOAL]
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : ReflectsIsomorphisms (forget C)
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
[PROOFSTEP]
apply isIso_of_reflects_iso f (forget C)
