awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D) (Functor.obj (presheafToSheaf J D) P))
      (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P)
      (Functor.map (sheafToPresheaf J D) (Functor.map (presheafToSheaf J D) η) ≫
        InducedCategory.Hom.hom
          (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
    η
have simp : η ≫
    CategoryStruct.comp (Y :=
      Functor.obj (sheafToPresheaf J D)
        (Functor.obj (presheafToSheaf J D)
          (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))))
      (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D))
        (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)))
      (InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
  η
Tactic: simp only [Adjunction.unit_naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ η ≫
      CategoryStruct.comp (Y :=
        Functor.obj (presheafToSheaf J D ⋙ sheafToPresheaf J D)
          (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)))
        (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D))
          (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)))
        (InducedCategory.Hom.hom
          (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
    η
have change : η ≫
    CategoryStruct.comp (Y :=
      Functor.obj (sheafToPresheaf J D)
        (Functor.obj (presheafToSheaf J D)
          (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))))
      (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D))
        (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)))
      (Functor.map (sheafToPresheaf J D)
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
  η
Tactic: change _ ≫ _ ≫ (sheafToPresheaf J D).map _ = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ η ≫
      CategoryStruct.comp (Y :=
        Functor.obj (sheafToPresheaf J D)
          (Functor.obj (presheafToSheaf J D)
            (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))))
        (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D))
          (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)))
        (Functor.map (sheafToPresheaf J D)
          (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
    η
have rw : η ≫ 𝟙 (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)) = η
Tactic: rw [sheafificationAdjunction J D |>.right_triangle_components (Y := ⟨Q, hQ⟩)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : sheafify J P ⟶ Q
h : toSheafify J P ≫ γ = η
⊢ γ = sheafifyLift J η hQ
have h₁ : NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P ≫ γ = η
Tactic: rw [toSheafify] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : sheafify J P ⟶ Q
h : NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P ≫ γ = η
γ' : Functor.obj (presheafToSheaf J D) P ⟶ ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ :=
  { hom := γ }
⊢ γ =
    InducedCategory.Hom.hom
      ((Equiv.symm
            (Adjunction.homEquiv (sheafificationAdjunction J D) P
              (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)) :
          (a : P ⟶ (sheafToPresheaf J D).obj { obj := Q, property := hQ }) →
            (presheafToSheaf J D).obj P ⟶ { obj := Q, property := hQ })
        η)
have change : γ'.hom =
  InducedCategory.Hom.hom
    ((Equiv.symm
          (Adjunction.homEquiv (sheafificationAdjunction J D) P
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)) :
        (a : P ⟶ (sheafToPresheaf J D).obj { obj := Q, property := hQ }) →
          (presheafToSheaf J D).obj P ⟶ { obj := Q, property := hQ })
      η)
Tactic: change γ'.hom = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : sheafify J P ⟶ Q
h : NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P ≫ γ = η
γ' : Functor.obj (presheafToSheaf J D) P ⟶ ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ :=
  { hom := γ }
⊢ γ'.hom =
    InducedCategory.Hom.hom
      ((Equiv.symm
            (Adjunction.homEquiv (sheafificationAdjunction J D) P
              (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)) :
          (a : P ⟶ (sheafToPresheaf J D).obj { obj := Q, property := hQ }) →
            (presheafToSheaf J D).obj P ⟶ { obj := Q, property := hQ })
        η)
have rw : CategoryStruct.comp (Y := Functor.obj (presheafToSheaf J D ⋙ sheafToPresheaf J D) P)
    (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P) (Functor.map (sheafToPresheaf J D) γ') =
  η
Tactic: rw [← Sheaf.hom_ext_iff, ← Adjunction.homEquiv_apply_eq, Adjunction.homEquiv_unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ Eq (α := sheafify J P ⟶ P) (Iso.inv (isoSheafify J hP)) (sheafifyLift J (𝟙 P) hP)
have a : CategoryStruct.comp (Y := sheafify J P) (toSheafify J P) (Iso.inv (isoSheafify J hP)) = 𝟙 P
Tactic: apply sheafifyLift_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η γ : sheafify J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toSheafify J P ≫ η = toSheafify J P ≫ γ
⊢ η = γ
have rw : sheafifyLift J (toSheafify J P ≫ η) hQ = γ
Tactic: rw [sheafifyLift_unique J _ hQ _ h, ← h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q R : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ Eq (α := sheafify J P ⟶ R) (sheafifyMap J η ≫ sheafifyLift J γ hR) (sheafifyLift J (η ≫ γ) hR)
have a : CategoryStruct.comp (Y := sheafify J P) (toSheafify J P) (sheafifyMap J η ≫ sheafifyLift J γ hR) = η ≫ γ
Tactic: apply sheafifyLift_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q R : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ CategoryStruct.comp (Y := sheafify J P) (toSheafify J P) (sheafifyMap J η ≫ sheafifyLift J γ hR) = η ≫ γ
have a : CategoryStruct.comp (Y := sheafify J Q) (toSheafify J P ≫ sheafifyMap J η) (sheafifyLift J γ hR) = η ≫ γ
Tactic: rw [← Category.assoc, ← toSheafify_naturality, Category.assoc, toSheafify_sheafifyLift]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q R : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
a : CategoryStruct.comp (Y := sheafify J Q) (toSheafify J P ≫ sheafifyMap J η) (sheafifyLift J γ hR) = η ≫ γ
⊢ CategoryStruct.comp (Y := sheafify J P) (toSheafify J P) (sheafifyMap J η ≫ sheafifyLift J γ hR) = η ≫ γ
have a₁ : CategoryStruct.comp (Y := sheafify J Q) (η ≫ toSheafify J Q) (sheafifyLift J γ hR) = η ≫ γ
Tactic: rw [← Category.assoc, ← toSheafify_naturality, Category.assoc, toSheafify_sheafifyLift]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q R : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
a : CategoryStruct.comp (Y := sheafify J Q) (toSheafify J P ≫ sheafifyMap J η) (sheafifyLift J γ hR) = η ≫ γ
a₁ : CategoryStruct.comp (Y := sheafify J Q) (η ≫ toSheafify J Q) (sheafifyLift J γ hR) = η ≫ γ
⊢ CategoryStruct.comp (Y := sheafify J P) (toSheafify J P) (sheafifyMap J η ≫ sheafifyLift J γ hR) = η ≫ γ
have a₂ : η ≫ CategoryStruct.comp (Y := sheafify J Q) (toSheafify J Q) (sheafifyLift J γ hR) = η ≫ γ
Tactic: rw [← Category.assoc, ← toSheafify_naturality, Category.assoc, toSheafify_sheafifyLift]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q R : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
a : CategoryStruct.comp (Y := sheafify J Q) (toSheafify J P ≫ sheafifyMap J η) (sheafifyLift J γ hR) = η ≫ γ
a₁ : CategoryStruct.comp (Y := sheafify J Q) (η ≫ toSheafify J Q) (sheafifyLift J γ hR) = η ≫ γ
a₂ : η ≫ CategoryStruct.comp (Y := sheafify J Q) (toSheafify J Q) (sheafifyLift J γ hR) = η ≫ γ
⊢ CategoryStruct.comp (Y := sheafify J P) (toSheafify J P) (sheafifyMap J η ≫ sheafifyLift J γ hR) = η ≫ γ
have a₃ : η ≫ γ = η ≫ γ
Tactic: rw [← Category.assoc, ← toSheafify_naturality, Category.assoc, toSheafify_sheafifyLift]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Sheaf.{v₁, v_1, u₁, u_1} J D
⊢ CategoryStruct.comp (Y := Functor.obj (presheafToSheaf J D) (P.obj (P := Presheaf.IsSheaf J)))
      { hom := Iso.hom (isoSheafify J ⋯) } { hom := Iso.inv (isoSheafify J ⋯) } =
    𝟙 P
have h : InducedCategory.Hom.hom
    (CategoryStruct.comp (Y := Functor.obj (presheafToSheaf J D) (P.obj (P := Presheaf.IsSheaf J)))
      { hom := Iso.hom (isoSheafify J sorry) } { hom := Iso.inv (isoSheafify J sorry) }) =
  InducedCategory.Hom.hom (𝟙 P)
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Sheaf.{v₁, v_1, u₁, u_1} J D
⊢ { hom := Iso.inv (isoSheafify J ⋯) } ≫
      { hom := Iso.hom (isoSheafify J ⋯) :
        InducedCategory.Hom (D := Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D) (F :=
          ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)) P
          (Functor.obj (presheafToSheaf J D) (P.obj (P := Presheaf.IsSheaf J))) } =
    𝟙 (Functor.obj (presheafToSheaf J D) (P.obj (P := Presheaf.IsSheaf J)))
have h : InducedCategory.Hom.hom
    ({ hom := Iso.inv (isoSheafify J sorry) } ≫
      { hom := Iso.hom (isoSheafify J sorry) :
        InducedCategory.Hom (D := Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D) (F :=
          ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)) P
          (Functor.obj (presheafToSheaf J D) (P.obj (P := Presheaf.IsSheaf J))) }) =
  InducedCategory.Hom.hom (𝟙 (Functor.obj (presheafToSheaf J D) (P.obj (P := Presheaf.IsSheaf J))))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ sheafifyLift J (𝟙 P) hP ≫ toSheafify J P = 𝟙 (sheafify J P)
have rw : CategoryStruct.comp (Y :=
    (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D)
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)).obj
      (P := Presheaf.IsSheaf J))
    (sheafifyLift J (𝟙 P) hP ≫ toSheafify J P)
    (InducedCategory.Hom.hom
      (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))) =
  𝟙 (sheafify J P) ≫
    InducedCategory.Hom.hom
      (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))
Tactic: rw [← cancel_mono ((sheafificationAdjunction J D).counit.app ⟨P, hP⟩).hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z_1 : C
f : Y ⟶ X
S : Presieve.{v₁, u₁} X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Presieve.{v₁, u₁} Y
Z : C
h : Z ⟶ X
H : S.bind R h
⊢ Nonempty (S.BindStruct R h)
have obtain : ∀ (Y : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S f) (hg : R hf g) (fac : g ≫ f = h), Nonempty (S.BindStruct R h)
Tactic: obtain ⟨Y, g, f, hf, hg, fac⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ singleton f g ↔ f = g
have mp : singleton f g → f = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
mp : singleton f g → f = g
⊢ singleton f g ↔ f = g
have mpr : f = g → singleton f g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : HasPullback g f
⊢ pullbackArrows f (singleton g) = singleton (Y := pullback g f) (pullback.snd g f)
have h : ∀ (W : C), Eq (α := (W ⟶ Y) → Prop) (pullbackArrows f (singleton g)) (singleton (Y := pullback g f) (pullback.snd g f))
Tactic: funext W
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : HasPullback g f
W : C
⊢ Eq (α := (W ⟶ Y) → Prop) (pullbackArrows f (singleton g)) (singleton (Y := pullback g f) (pullback.snd g f))
have h : ∀ (h : W ⟶ Y), pullbackArrows f (singleton g) h ↔ singleton (Y := pullback g f) (pullback.snd g f) h
Tactic: ext h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : HasPullback g f
W : C
h : W ⟶ Y
⊢ pullbackArrows f (singleton g) h ↔ singleton (Y := pullback g f) (pullback.snd g f) h
have h₁ : pullbackArrows f (singleton g) h → singleton (Y := pullback g f) (pullback.snd g f) h
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : HasPullback g f
W : C
h : W ⟶ Y
h₁ : pullbackArrows f (singleton g) h → singleton (Y := pullback g f) (pullback.snd g f) h
⊢ pullbackArrows f (singleton g) h ↔ singleton (Y := pullback g f) (pullback.snd g f) h
have h₂ : singleton (Y := pullback g f) (pullback.snd g f) h → pullbackArrows f (singleton g) h
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
g : Z ⟶ X
i : ι
h : Z = Y i
hg : g = eqToHom h ≫ f i
⊢ ofArrows Y f g
have subst : ∀ {g : Y i ⟶ X} (hg : g = eqToHom sorry ≫ f i), ofArrows Y f g
Tactic: subst h
Cleared hypotheses: Z, g, h, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
g : Y i ⟶ X
hg : g = eqToHom ⋯ ≫ f i
⊢ ofArrows Y f g
have hg₁ : g = f i
Tactic: simp only [eqToHom_refl, id_comp] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
g : Y i ⟶ X
hg : g = f i
⊢ ofArrows Y f g
have subst : ofArrows Y f (f i)
Tactic: subst hg
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst_1 : ∀ (i : ι), HasPullback (g i) f
⊢ (ofArrows (fun (i : ι) ↦ pullback (g i) f) fun (x : ι) ↦ pullback.snd (g x) f) = pullbackArrows f (ofArrows Z g)
have h : ∀ (T : C),
  Eq (α := (T ⟶ Y) → Prop) (ofArrows (fun (i : ι) ↦ pullback (g i) f) fun (x : ι) ↦ pullback.snd (g x) f)
    (pullbackArrows f (ofArrows Z g))
Tactic: funext T
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst_1 : ∀ (i : ι), HasPullback (g i) f
T : C
⊢ Eq (α := (T ⟶ Y) → Prop) (ofArrows (fun (i : ι) ↦ pullback (g i) f) fun (x : ι) ↦ pullback.snd (g x) f)
    (pullbackArrows f (ofArrows Z g))
have h : ∀ (h : T ⟶ Y),
  ofArrows (fun (i : ι) ↦ pullback (g i) f) (fun (x : ι) ↦ pullback.snd (g x) f) h ↔ pullbackArrows f (ofArrows Z g) h
Tactic: ext h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst_1 : ∀ (i : ι), HasPullback (g i) f
T : C
h : T ⟶ Y
⊢ ofArrows (fun (i : ι) ↦ pullback (g i) f) (fun (x : ι) ↦ pullback.snd (g x) f) h ↔ pullbackArrows f (ofArrows Z g) h
have h₁ : ofArrows (fun (i : ι) ↦ pullback (g i) f) (fun (x : ι) ↦ pullback.snd (g x) f) h → pullbackArrows f (ofArrows Z g) h
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst_1 : ∀ (i : ι), HasPullback (g i) f
T : C
h : T ⟶ Y
h₁ :
  ofArrows (fun (i : ι) ↦ pullback (g i) f) (fun (x : ι) ↦ pullback.snd (g x) f) h → pullbackArrows f (ofArrows Z g) h
⊢ ofArrows (fun (i : ι) ↦ pullback (g i) f) (fun (x : ι) ↦ pullback.snd (g x) f) h ↔ pullbackArrows f (ofArrows Z g) h
have h₂ : pullbackArrows f (ofArrows Z g) h → ofArrows (fun (i : ι) ↦ pullback (g i) f) (fun (x : ι) ↦ pullback.snd (g x) f) h
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
⊢ ((ofArrows Z g).bind fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H)) =
    ofArrows
      (fun (i : (i : ι) × j (g i) ⋯) ↦
        W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
      fun (ij : (i : ι) × j (g i) ⋯) ↦
      k (g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))
have h : ∀ (Y : C),
  Eq (α := (Y ⟶ X) → Prop) ((ofArrows Z g).bind fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H))
    (ofArrows
      (fun (i : (i : ι) × j (g i) sorry) ↦
        W (g (i.fst (β := fun (i : ι) ↦ j (g i) sorry))) sorry (i.snd (β := fun (i : ι) ↦ j (g i) sorry)))
      fun (ij : (i : ι) × j (g i) sorry) ↦
      k (g (ij.fst (β := fun (i : ι) ↦ j (g i) sorry))) sorry (ij.snd (β := fun (i : ι) ↦ j (g i) sorry)) ≫
        g (ij.fst (β := fun (i : ι) ↦ j (g i) sorry)))
Tactic: funext Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
⊢ Eq (α := (Y ⟶ X) → Prop) ((ofArrows Z g).bind fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H))
    (ofArrows
      (fun (i : (i : ι) × j (g i) ⋯) ↦
        W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
      fun (ij : (i : ι) × j (g i) ⋯) ↦
      k (g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯)))
have h : ∀ (f : Y ⟶ X),
  (ofArrows Z g).bind (fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H)) f ↔
    ofArrows
      (fun (i : (i : ι) × j (g i) sorry) ↦
        W (g (i.fst (β := fun (i : ι) ↦ j (g i) sorry))) sorry (i.snd (β := fun (i : ι) ↦ j (g i) sorry)))
      (fun (ij : (i : ι) × j (g i) sorry) ↦
        k (g (ij.fst (β := fun (i : ι) ↦ j (g i) sorry))) sorry (ij.snd (β := fun (i : ι) ↦ j (g i) sorry)) ≫
          g (ij.fst (β := fun (i : ι) ↦ j (g i) sorry)))
      f
Tactic: ext f