case h
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y✝ Z : C
f : Y✝ ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
Y : D
⊢ Presieve.functorPushforward F (generate R).arrows = Presieve.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
S R✝ : Sieve X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
⊢ Presieve.functorPushforward F (generate R).arrows = Presieve.functorPushforward F R
funext Y
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
S R✝ : Sieve X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
Y : D
f : Y ⟶ F.obj X
⊢ f ∈ Presieve.functorPushforward F (generate R).arrows ↔ f ∈ Presieve.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
S R✝ : Sieve X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
Y : D
⊢ Presieve.functorPushforward F (generate R).arrows = Presieve.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
S R✝ : Sieve X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
Y : D
f : Y ⟶ F.obj X
⊢ f ∈ Presieve.functorPushforward F (generate R).arrows → f ∈ Presieve.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
S R✝ : Sieve X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
Y : D
f : Y ⟶ F.obj X
⊢ f ∈ Presieve.functorPushforward F R → f ∈ Presieve.functorPushforward F (generate R).arrows
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
S R✝ : Sieve X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
Y : D
f : Y ⟶ F.obj X
⊢ f ∈ Presieve.functorPushforward F (generate R).arrows ↔ f ∈ Presieve.functorPushforward F R
constructor
case h.h.mp.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
S R✝ : Sieve X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
Y : D
X' : C
f' : Y ⟶ F.obj X'
X'' : C
g' : X' ⟶ X''
f'' : X'' ⟶ X
h₁ : R f''
⊢ f' ≫ F.map (g' ≫ f'') ∈ Presieve.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
S R✝ : Sieve X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
Y : D
f : Y ⟶ F.obj X
⊢ f ∈ Presieve.functorPushforward F (generate R).arrows → f ∈ Presieve.functorPushforward F R
rintro ⟨X', g, f', ⟨X'', g', f'', h₁, rfl⟩, rfl⟩
no goals
case h.h.mp.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
S R✝ : Sieve X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
Y : D
X' : C
f' : Y ⟶ F.obj X'
X'' : C
g' : X' ⟶ X''
f'' : X'' ⟶ X
h₁ : R f''
⊢ f' ≫ F.map (g' ≫ f'') ∈ Presieve.functorPushforward F R
exact ⟨X'', f'', f' ≫ F.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
S R✝ : Sieve X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
Y : D
X' : C
f' : Y ⟶ F.obj X'
X'' : C
g' : X' ⟶ X''
f'' : X'' ⟶ X
h₁ : R f''
⊢ f' ≫ F.map (g' ≫ f'') = (f' ≫ F.map g') ≫ F.map f''
simp
case h.h.mpr.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
S R✝ : Sieve X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
Y : D
f : Y ⟶ F.obj X
X' : C
g : X' ⟶ X
f' : Y ⟶ F.obj X'
h₁ : R g
h₂ : f = f' ≫ F.map g
⊢ f ∈ Presieve.functorPushforward F (generate R).arrows
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
S R✝ : Sieve X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
Y : D
f : Y ⟶ F.obj X
⊢ f ∈ Presieve.functorPushforward F R → f ∈ Presieve.functorPushforward F (generate R).arrows
rintro ⟨X', g, f', h₁, h₂⟩
no goals
case h.h.mpr.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
S R✝ : Sieve X
E : Type u₃
inst✝ : Category E
G : D ⥤ E
R : Presieve X
Y : D
f : Y ⟶ F.obj X
X' : C
g : X' ⟶ X
f' : Y ⟶ F.obj X'
h₁ : R g
h₂ : f = f' ≫ F.map g
⊢ f ∈ Presieve.functorPushforward F (generate R).arrows
exact ⟨X', g, f', le_generate R _ h₁, h₂⟩