case h
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
x : E
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)
funext x
case h.h
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
x : E
f : x ⟶ (F ⋙ G).obj X
⊢ f ∈ functorPushforward (F ⋙ G) R ↔ f ∈ functorPushforward G (functorPushforward F R)
case h
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
x : E
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)
ext f
case h.h.mp
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
x : E
f : x ⟶ (F ⋙ G).obj X
⊢ f ∈ functorPushforward (F ⋙ G) R → f ∈ functorPushforward G (functorPushforward F R)

case h.h.mpr
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
x : E
f : x ⟶ (F ⋙ G).obj X
⊢ f ∈ functorPushforward G (functorPushforward F R) → f ∈ functorPushforward (F ⋙ G) R
case h.h
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
x : E
f : x ⟶ (F ⋙ G).obj X
⊢ f ∈ functorPushforward (F ⋙ G) R ↔ f ∈ functorPushforward G (functorPushforward F R)
constructor
case h.h.mp.intro.intro.intro.intro
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X✝
x : E
X : C
f₁ : X ⟶ X✝
g₁ : x ⟶ (F ⋙ G).obj X
h₁ : R f₁
⊢ g₁ ≫ (F ⋙ G).map f₁ ∈ functorPushforward G (functorPushforward F R)
case h.h.mp
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
x : E
f : x ⟶ (F ⋙ G).obj X
⊢ f ∈ functorPushforward (F ⋙ G) R → f ∈ functorPushforward G (functorPushforward F R)
rintro ⟨X, f₁, g₁, h₁, rfl⟩
no goals
case h.h.mp.intro.intro.intro.intro
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X✝
x : E
X : C
f₁ : X ⟶ X✝
g₁ : x ⟶ (F ⋙ G).obj X
h₁ : R f₁
⊢ g₁ ≫ (F ⋙ G).map f₁ ∈ functorPushforward G (functorPushforward F R)
exact ⟨F.obj X, F.map f₁, g₁, ⟨X, f₁, 𝟙 _, h₁, by simp⟩, rfl⟩
no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X✝
x : E
X : C
f₁ : X ⟶ X✝
g₁ : x ⟶ (F ⋙ G).obj X
h₁ : R f₁
⊢ F.map f₁ = 𝟙 (F.obj X) ≫ F.map f₁
simp
case h.h.mpr.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X✝
x : E
X : D
g₁ : x ⟶ G.obj X
X' : C
f₂ : X' ⟶ X✝
g₂ : X ⟶ F.obj X'
h₁ : R f₂
⊢ g₁ ≫ G.map (g₂ ≫ F.map f₂) ∈ functorPushforward (F ⋙ G) R
case h.h.mpr
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
x : E
f : x ⟶ (F ⋙ G).obj X
⊢ f ∈ functorPushforward G (functorPushforward F R) → f ∈ functorPushforward (F ⋙ G) R
rintro ⟨X, f₁, g₁, ⟨X', f₂, g₂, h₁, rfl⟩, rfl⟩
no goals
case h.h.mpr.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X✝
x : E
X : D
g₁ : x ⟶ G.obj X
X' : C
f₂ : X' ⟶ X✝
g₂ : X ⟶ F.obj X'
h₁ : R f₂
⊢ g₁ ≫ G.map (g₂ ≫ F.map f₂) ∈ functorPushforward (F ⋙ G) R
exact ⟨X', f₂, g₁ ≫ G.map g₂, h₁, by simp⟩
no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X✝
x : E
X : D
g₁ : x ⟶ G.obj X
X' : C
f₂ : X' ⟶ X✝
g₂ : X ⟶ F.obj X'
h₁ : R f₂
⊢ g₁ ≫ G.map (g₂ ≫ F.map f₂) = (g₁ ≫ G.map g₂) ≫ (F ⋙ G).map f₂
simp