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
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (sieveOfSubfunctor (functorInclusion S)).arrows f✝ ↔ S.arrows f✝
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
⊢ sieveOfSubfunctor (functorInclusion S) = S
ext
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
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (∃ t, ↑t = f✝) ↔ S.arrows f✝
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
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (sieveOfSubfunctor (functorInclusion S)).arrows f✝ ↔ S.arrows f✝
simp only [functorInclusion_app, sieveOfSubfunctor_apply]
case 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
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (∃ t, ↑t = f✝) → S.arrows f✝

case 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
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ S.arrows f✝ → ∃ t, ↑t = f✝
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
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (∃ t, ↑t = f✝) ↔ S.arrows f✝
constructor
case h.mp.intro.mk
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
Y✝ : C
f : Y✝.op.unop ⟶ X
hf : S.arrows f
⊢ S.arrows ↑{ val := f, property := hf }
case 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
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (∃ t, ↑t = f✝) → S.arrows f✝
rintro ⟨⟨f, hf⟩, rfl⟩
no goals
case h.mp.intro.mk
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
Y✝ : C
f : Y✝.op.unop ⟶ X
hf : S.arrows f
⊢ S.arrows ↑{ val := f, property := hf }
exact hf
case 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
Y✝ : C
f✝ : Y✝ ⟶ X
hf : S.arrows f✝
⊢ ∃ t, ↑t = f✝
case 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
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ S.arrows f✝ → ∃ t, ↑t = f✝
intro hf
no goals
case 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
Y✝ : C
f✝ : Y✝ ⟶ X
hf : S.arrows f✝
⊢ ∃ t, ↑t = f✝
exact ⟨⟨_, hf⟩, rfl⟩