C : Type (u + 1)
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category 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
C : Type (u + 1)
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category 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
skip
C : Type (u + 1)
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category 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
C : Type (u + 1)
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category 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
haveI i' : IsIso ((forget D).map ((forget₂ C D).map f)) := Functor.map_isIso (forget D) _
C : Type (u + 1)
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category 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
C : Type (u + 1)
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category 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
haveI : IsIso ((forget C).map f) := by
  have := @HasForget₂.forget_comp C D
  rw [← this]
  exact i'
no goals
C : Type (u + 1)
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category 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
apply isIso_of_reflects_iso f (forget C)
C : Type (u + 1)
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category 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 C] [inst_1 : ConcreteCategory C] [inst_2 : Category D] [inst_3 : ConcreteCategory D]
    [self : HasForget₂ C D], HasForget₂.forget₂ ⋙ forget D = forget C
⊢ IsIso ((forget C).map f)
C : Type (u + 1)
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category 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)
have := @HasForget₂.forget_comp C D
C : Type (u + 1)
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category 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 C] [inst_1 : ConcreteCategory C] [inst_2 : Category D] [inst_3 : ConcreteCategory D]
    [self : HasForget₂ C D], HasForget₂.forget₂ ⋙ forget D = forget C
⊢ IsIso ((HasForget₂.forget₂ ⋙ forget D).map f)
C : Type (u + 1)
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category 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 C] [inst_1 : ConcreteCategory C] [inst_2 : Category D] [inst_3 : ConcreteCategory D]
    [self : HasForget₂ C D], HasForget₂.forget₂ ⋙ forget D = forget C
⊢ IsIso ((forget C).map f)
rw [← this]
no goals
C : Type (u + 1)
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category 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 C] [inst_1 : ConcreteCategory C] [inst_2 : Category D] [inst_3 : ConcreteCategory D]
    [self : HasForget₂ C D], HasForget₂.forget₂ ⋙ forget D = forget C
⊢ IsIso ((HasForget₂.forget₂ ⋙ forget D).map f)
exact i'