awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
U : Sieve.{v₁, u₁} X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve.{v₁, u₁} Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible (R := (Sieve.bind U.arrows B).arrows)
y_1 : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows :=
  fun (Y : C) (f : Y ⟶ X) (hf : U.arrows f) (Z : C) (g : Z ⟶ Y) (hg : (B hf).arrows g) ↦ s (g ≫ f) ⋯
hy_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y_1 hf).Compatible (R := (B hf).arrows)
t : FamilyOfElements P U.arrows :=
  fun (Y : C) (f : Y ⟶ X) (hf : U.arrows f) ↦ ⋯.amalgamate (R := (B hf).arrows) (y_1 hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y_1 hf).IsAmalgamation (R := (B hf).arrows) (t f hf)
hT : t.Compatible (R := U.arrows)
y : P.obj (op X)
hy : s.IsAmalgamation (R := (Sieve.bind U.arrows B).arrows) y
⊢ y = hU.amalgamate (R := U.arrows) t hT
have refine_2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
  U.arrows f →
    Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
            (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
          y :
        (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
            (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
          (hU.amalgamate (R := U.arrows) t hT) :
        (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
Tactic: apply hU.isSeparatedFor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
U : Sieve.{v₁, u₁} X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve.{v₁, u₁} Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible (R := (Sieve.bind U.arrows B).arrows)
y_1 : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows :=
  fun (Y : C) (f : Y ⟶ X) (hf : U.arrows f) (Z : C) (g : Z ⟶ Y) (hg : (B hf).arrows g) ↦ s (g ≫ f) ⋯
hy_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y_1 hf).Compatible (R := (B hf).arrows)
t : FamilyOfElements P U.arrows :=
  fun (Y : C) (f : Y ⟶ X) (hf : U.arrows f) ↦ ⋯.amalgamate (R := (B hf).arrows) (y_1 hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y_1 hf).IsAmalgamation (R := (B hf).arrows) (t f hf)
hT : t.Compatible (R := U.arrows)
y : P.obj (op X)
hy : s.IsAmalgamation (R := (Sieve.bind U.arrows B).arrows) y
Y : C
f : Y ⟶ X
hf : U.arrows f
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
        y :
      (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
        (hU.amalgamate (R := U.arrows) t hT) :
      (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
have refine_2 : ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
  (B hf).arrows f_1 →
    Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (op Y_1)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f_1.op) :
            (a : (fun (X : Type u_1) ↦ X) (P.obj (op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y_1)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
                (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
              y :
            (fun (X : Type u_1) ↦ X) (P.obj (op Y))) :
        (fun (X : Type u_1) ↦ X) (P.obj (op Y_1)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f_1.op) :
            (a : (fun (X : Type u_1) ↦ X) (P.obj (op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y_1)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
                (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
              (hU.amalgamate (R := U.arrows) t hT) :
            (fun (X : Type u_1) ↦ X) (P.obj (op Y))) :
        (fun (X : Type u_1) ↦ X) (P.obj (op Y_1)))
Tactic: apply (hB hf).isSeparatedFor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
U : Sieve.{v₁, u₁} X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve.{v₁, u₁} Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible (R := (Sieve.bind U.arrows B).arrows)
y_1 : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows :=
  fun (Y : C) (f : Y ⟶ X) (hf : U.arrows f) (Z : C) (g : Z ⟶ Y) (hg : (B hf).arrows g) ↦ s (g ≫ f) ⋯
hy_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y_1 hf).Compatible (R := (B hf).arrows)
t : FamilyOfElements P U.arrows :=
  fun (Y : C) (f : Y ⟶ X) (hf : U.arrows f) ↦ ⋯.amalgamate (R := (B hf).arrows) (y_1 hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y_1 hf).IsAmalgamation (R := (B hf).arrows) (t f hf)
hT : t.Compatible (R := U.arrows)
y : P.obj (op X)
hy : s.IsAmalgamation (R := (Sieve.bind U.arrows B).arrows) y
Y : C
f : Y ⟶ X
hf : U.arrows f
Z : C
g : Z ⟶ Y
hg : (B hf).arrows g
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
              (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
            y :
          (fun (X : Type u_1) ↦ X) (P.obj (op Y))) :
      (fun (X : Type u_1) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
              (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
            (hU.amalgamate (R := U.arrows) t hT) :
          (fun (X : Type u_1) ↦ X) (P.obj (op Y))) :
      (fun (X : Type u_1) ↦ X) (P.obj (op Z)))
have refine_2 : Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (op Z)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op ≫ P.map g.op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → P.obj (op Z))
      y :
    P.obj (op Z))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
            (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
          (hU.amalgamate (R := U.arrows) t hT) :
        (fun (X : Type u_1) ↦ X) (P.obj (op Y))) :
    (fun (X : Type u_1) ↦ X) (P.obj (op Z)))
Tactic: rw [← comp_apply, ← Functor.map_comp, ← op_comp, hy _ (Presieve.bind_comp _ _ hg),
      hU.valid_glue _ _ hf, ht hf _ hg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
⊢ IsSheafFor P S.arrows
have this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Tactic: have : (Sieve.bind R fun Y f _ => S.pullback f : Presieve X) ≤ S := by
    rintro Z f ⟨W, f, g, hg, hf : S _, rfl⟩
    apply hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
⊢ IsSheafFor P S.arrows
have hS₁ : IsSheafFor P (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows
Tactic: apply Presieve.isSheafFor_subsieve_aux P this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
hS₁ : IsSheafFor P (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows
⊢ IsSheafFor P S.arrows
have trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
  S.arrows f →
    IsSeparatedFor P
      (Sieve.pullback f (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S)).arrows
Tactic: apply Presieve.isSheafFor_subsieve_aux P this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
⊢ IsSheafFor P (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows
have hS₁ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : R.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y),
  IsSeparatedFor P (Sieve.pullback g (Sieve.pullback f S)).arrows
Tactic: apply isSheafFor_bind _ _ _ hR hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : R.arrows f
Z : C
g : Z ⟶ Y
⊢ IsSeparatedFor P (Sieve.pullback g (Sieve.pullback f S)).arrows
have hS₁ : IsSeparatedFor P (Sieve.pullback (g ≫ f) S).arrows
Tactic: rw [← pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S) =
    Sieve.pullback f R
have h : ∀ ⦃Z : C⦄ (g : Z ⟶ Y),
  (Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S)).arrows g ↔
    (Sieve.pullback f R).arrows g
Tactic: ext Z g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S)).arrows g ↔
    (Sieve.pullback f R).arrows g
have h : (Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S)).arrows g →
  (Sieve.pullback f R).arrows g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
h :
  (Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S)).arrows g →
    (Sieve.pullback f R).arrows g
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S)).arrows g ↔
    (Sieve.pullback f R).arrows g
have h₁ : (Sieve.pullback f R).arrows g →
  (Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S)).arrows g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
W : C
k : Z ⟶ W
l : W ⟶ X
hl : R.arrows l
left : arrows ((fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S) W l hl) k
comm : k ≫ l = g ≫ f
⊢ (Sieve.pullback f R).arrows g
have h : R.arrows (k ≫ l)
Tactic: rw [pullback_apply, ← comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
a : (Sieve.pullback f R).arrows g
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S)).arrows g
have h : (fun (x : C) (x_1 : x ⟶ X) (h : R.arrows x_1) ↦
      (arrows ((fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S) x x_1 h) : Presieve.{v₁, u₁} x))
    Z (g ≫ f) a (𝟙 Z) ∧
  𝟙 Z ≫ g ≫ f = g ≫ f
Tactic: refine ⟨Z, 𝟙 Z, _, a, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ IsSeparatedFor P
    (Sieve.pullback f (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S)).arrows
have this₁ : Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S) =
  Sieve.pullback f R
Tactic: have : Sieve.pullback f (Sieve.bind R fun T (k : T ⟶ X) (_ : R k) => pullback k S) =
        R.pullback f := by
      ext Z g
      constructor
      · rintro ⟨W, k, l, hl, _, comm⟩
        rw [pullback_apply, ← comm]
        simp [hl]
      · intro a
        refine ⟨Z, 𝟙 Z, _, a, ?_⟩
        simp [hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this_1 : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
this :
  Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S) =
    Sieve.pullback f R
⊢ IsSeparatedFor P
    (Sieve.pullback f (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S)).arrows
have trans : IsSeparatedFor P (Sieve.pullback f R).arrows
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
Goal:
X Y : Type u
f : X ⟶ Y
⊢ (∀ (x : Y),
      ∃ (Y_1 : Type u) (g : Y_1 ⟶ Y),
        Presieve.singleton f g ∧
          Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
            (Set.range (ι := (fun (X : Type u) ↦ X) Y_1)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
                (a : (fun (X : Type u) ↦ X) Y_1) → (fun (X : Type u) ↦ X) Y))
            x) ↔
    Function.Surjective (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
have refine : ∀
  (hf :
    ∀ (x : Y),
      ∃ (Y_1 : Type u) (g : Y_1 ⟶ Y),
        Presieve.singleton f g ∧
          Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
            (Set.range (ι := (fun (X : Type u) ↦ X) Y_1)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
                (a : (fun (X : Type u) ↦ X) Y_1) → (fun (X : Type u) ↦ X) Y))
            x)
  (x : (fun (X : Type u) ↦ X) Y),
  ∃ (a : (fun (X : Type u) ↦ X) X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) a = x
Tactic: refine ⟨fun hf x ↦ ?_, fun hf x ↦ ⟨X, f, ⟨⟩, by simp [hf.range_eq]⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
Goal:
X Y : Type u
f : X ⟶ Y
hf :
  ∀ (x : Y),
    ∃ (Y_1 : Type u) (g : Y_1 ⟶ Y),
      Presieve.singleton f g ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
          (Set.range (ι := (fun (X : Type u) ↦ X) Y_1)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
              (a : (fun (X : Type u) ↦ X) Y_1) → (fun (X : Type u) ↦ X) Y))
          x
x : (fun (X : Type u) ↦ X) Y
⊢ ∃ (a : (fun (X : Type u) ↦ X) X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) a = x
have obtain : ∀ ⦃Y_1 : Type u⦄
  (hx :
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
      (Set.range (ι := (fun (X : Type u) ↦ X) X)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
      x),
  ∃ (a : (fun (X : Type u) ↦ X) X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) a = x
Tactic: obtain ⟨_, _, ⟨⟩, hx⟩ := hf x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
Goal:
X : Type u
ι : Type u_1
Y : ι → Type u
f : (i : ι) → Y i ⟶ X
⊢ Presieve.ofArrows Y f ∈ jointlySurjectivePrecoverage.coverings X ↔
    ∀ (x : (fun (X : Type u) ↦ X) X),
      ∃ (i : ι),
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
          (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
              (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
          x
have refine_1 : ∀ (h : Presieve.ofArrows Y f ∈ jointlySurjectivePrecoverage.coverings X) (x : (fun (X : Type u) ↦ X) X),
  ∃ (i : ι),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
      (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
          (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
      x
Tactic: refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
Goal:
X : Type u
ι : Type u_1
Y : ι → Type u
f : (i : ι) → Y i ⟶ X
refine_1 :
  ∀ (h : Presieve.ofArrows Y f ∈ jointlySurjectivePrecoverage.coverings X) (x : (fun (X : Type u) ↦ X) X),
    ∃ (i : ι),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
        (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
            (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
        x
⊢ Presieve.ofArrows Y f ∈ jointlySurjectivePrecoverage.coverings X ↔
    ∀ (x : (fun (X : Type u) ↦ X) X),
      ∃ (i : ι),
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
          (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
              (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
          x
have refine_2 : ∀
  (h :
    ∀ (x : (fun (X : Type u) ↦ X) X),
      ∃ (i : ι),
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
          (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
              (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
          x)
  (x : X),
  ∃ (Y_1 : Type u) (g : Y_1 ⟶ X),
    Presieve.ofArrows Y f g ∧
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
        (Set.range (ι := (fun (X : Type u) ↦ X) Y_1)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y_1) → (fun (X : Type u) ↦ X) X))
        x
Tactic: refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
Goal:
X : Type u
ι : Type u_1
Y : ι → Type u
f : (i : ι) → Y i ⟶ X
h : Presieve.ofArrows Y f ∈ jointlySurjectivePrecoverage.coverings X
x : (fun (X : Type u) ↦ X) X
⊢ ∃ (i : ι),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
      (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
          (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
      x
have refine_1 : ∀ ⦃Y_1 : Type u⦄ (i : ι)
  (hx :
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
      (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
          (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
      x),
  ∃ (i : ι),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
      (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
          (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
      x
Tactic: obtain ⟨Y, g, ⟨i⟩, hx⟩ := h x