case left
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z),
    MorphismProperty.inverseImage P F f → MorphismProperty.inverseImage P F (e.hom ≫ f)

case right
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y),
    MorphismProperty.inverseImage P F f → MorphismProperty.inverseImage P F (f ≫ e.hom)
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
⊢ RespectsIso (MorphismProperty.inverseImage P F)
constructor
case left
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : MorphismProperty.inverseImage P F f
⊢ P (F.map e.hom ≫ F.map f)

case right
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : MorphismProperty.inverseImage P F f
⊢ P (F.map f ≫ F.map e.hom)
case left
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z),
    MorphismProperty.inverseImage P F f → MorphismProperty.inverseImage P F (e.hom ≫ f)

case right
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y),
    MorphismProperty.inverseImage P F f → MorphismProperty.inverseImage P F (f ≫ e.hom)
all_goals
  intro X Y Z e f hf
  dsimp [MorphismProperty.inverseImage]
  rw [F.map_comp]
no goals
case left
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : MorphismProperty.inverseImage P F f
⊢ P (F.map e.hom ≫ F.map f)

case right
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : MorphismProperty.inverseImage P F f
⊢ P (F.map f ≫ F.map e.hom)
exacts [h.1 (F.mapIso e) (F.map f) hf, h.2 (F.mapIso e) (F.map f) hf]
case right
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : MorphismProperty.inverseImage P F f
⊢ MorphismProperty.inverseImage P F (f ≫ e.hom)
case right
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y),
    MorphismProperty.inverseImage P F f → MorphismProperty.inverseImage P F (f ≫ e.hom)
intro X Y Z e f hf
case right
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : MorphismProperty.inverseImage P F f
⊢ P (F.map (f ≫ e.hom))
case right
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : MorphismProperty.inverseImage P F f
⊢ MorphismProperty.inverseImage P F (f ≫ e.hom)
dsimp [MorphismProperty.inverseImage]
case right
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : MorphismProperty.inverseImage P F f
⊢ P (F.map f ≫ F.map e.hom)
case right
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : MorphismProperty.inverseImage P F f
⊢ P (F.map (f ≫ e.hom))
rw [F.map_comp]