awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over.{v₁, u₁} B'
g₁ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₂
h :
  Eq (α := Z ⟶ (Over.map p).obj X) (g₁ ≫ (fun (i : I) ↦ (Over.map p).map (f i)) i₁)
    (g₂ ≫ (fun (i : I) ↦ (Over.map p).map (f i)) i₂)
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op ((fun (i : I) ↦ (Over.map p).obj (Y i)) i₁)))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) i₁) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op ((fun (i : I) ↦ (Over.map p).obj (Y i)) i₂)))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) i₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
have h₁ : Eq (α := Functor.obj (Over.forget B') Z ⟶ Functor.obj (Over.forget B') ((Over.map p).obj X))
  (Functor.map (Over.forget B') (g₁ ≫ (fun (i : I) ↦ (Over.map p).map (f i)) i₁))
  (Functor.map (Over.forget B') (g₂ ≫ (fun (i : I) ↦ (Over.map p).map (f i)) i₂))
Tactic: replace h := (Over.forget _).congr_map h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over.{v₁, u₁} B'
g₁ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
⊢ Over.Hom.left g₂ ≫ (Y i₂).hom = (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)).hom
have this : Over.Hom.left (f i₂) ≫ X.hom = (Y i₂).hom
Tactic: have := Over.w (f i₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over.{v₁, u₁} B'
g₁ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
this : Over.Hom.left (f i₂) ≫ X.hom = (Y i₂).hom
⊢ Over.Hom.left g₂ ≫ (Y i₂).hom = (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)).hom
have dsimp : Over.Hom.left g₂ ≫ (Y i₂).hom = Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over.{v₁, u₁} B'
g₁ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
this : Over.Hom.left (f i₂) ≫ X.hom = (Y i₂).hom
⊢ Over.Hom.left g₂ ≫ (Y i₂).hom = Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom
have rw : Over.Hom.left g₂ ≫ (Y i₂).hom = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂) ≫ X.hom
Tactic: rw [reassoc_of% h, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over.{v₁, u₁} B'
g₁ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
this : Over.Hom.left (f i₂) ≫ X.hom = (Y i₂).hom
rw : Over.Hom.left g₂ ≫ (Y i₂).hom = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂) ≫ X.hom
⊢ Over.Hom.left g₂ ≫ (Y i₂).hom = Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom
have rw₁ : Over.Hom.left g₂ ≫ (Y i₂).hom = Over.Hom.left g₂ ≫ (Y i₂).hom
Tactic: rw [reassoc_of% h, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over.{v₁, u₁} B'
g₁ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op ((fun (i : I) ↦ (Over.map p).obj (Y i)) i₁)))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) i₁) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op ((fun (i : I) ↦ (Over.map p).obj (Y i)) i₂)))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) i₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
have this : Eq (α :=
  (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (((Over.map p).op ⋙ P).map (Over.homMk (Over.Hom.left g₁) sorry).op) :
        (a : (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Y i₁)))) →
          (fun (X : Type w) ↦ X)
            (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
      ((↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i₁) :
    (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (((Over.map p).op ⋙ P).map (Over.homMk (Over.Hom.left g₂) sorry).op) :
        (a : (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Y i₂)))) →
          (fun (X : Type w) ↦ X)
            (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
      ((↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i₂) :
    (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
Tactic: have := s.property i₁ i₂ (Over.mk (g₁.left ≫ (f i₁).left ≫ X.hom))
          (Over.homMk g₁.left) (Over.homMk g₂.left (by
            have := Over.w (f i₂)
            dsimp at this ⊢
            rw [reassoc_of% h, this])) (by cat_disch)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over.{v₁, u₁} B'
g₁ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
φ : Z ⟶ (Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)) := Over.homMk (𝟙 Z.left) ⋯
this :
  Eq (α := P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op) :
          (a : P.obj (op ((Over.map p).obj (Y i₁)))) → P.obj (op Z))
        ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₁) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op) :
          (a : P.obj (op ((Over.map p).obj (Y i₂)))) → P.obj (op Z))
        ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₂) :
      P.obj (op Z))
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op ((fun (i : I) ↦ (Over.map p).obj (Y i)) i₁)))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) i₁) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op ((fun (i : I) ↦ (Over.map p).obj (Y i)) i₂)))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) i₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
have h₁ : g₁ = φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) sorry)
Tactic: convert! this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over.{v₁, u₁} B'
g₁ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
φ : Z ⟶ (Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)) := Over.homMk (𝟙 Z.left) ⋯
this :
  Eq (α := P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op) :
          (a : P.obj (op ((Over.map p).obj (Y i₁)))) → P.obj (op Z))
        ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₁) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op) :
          (a : P.obj (op ((Over.map p).obj (Y i₂)))) → P.obj (op Z))
        ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₂) :
      P.obj (op Z))
h₁ : g₁ = φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op ((fun (i : I) ↦ (Over.map p).obj (Y i)) i₁)))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) i₁) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op ((fun (i : I) ↦ (Over.map p).obj (Y i)) i₂)))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) i₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
have h₂ : g₂ = φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) sorry)
Tactic: convert! this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
e : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f) ≃
  Subtype (α := (i : I) → P.obj (op ((Over.map p).obj (Y i))))
    (Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i)) :=
  {
    toFun := fun (s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)) ↦
      Subtype.mk (p := Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i))
        (fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) ⋯,
    invFun :=
      fun
        (s :
          Subtype (α := (i : I) → P.obj (op ((Over.map p).obj (Y i))))
            (Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i))) ↦
      Subtype.mk (p := Arrows.Compatible ((Over.map p).op ⋙ P) f)
        (fun (i : I) ↦ (↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
⊢ IsSheafFor ((Over.map p).op ⋙ P) (ofArrows Y f) ↔
    IsSheafFor (X := (Over.map p).obj X) P
      (ofArrows (fun (i : I) ↦ (Over.map p).obj (Y i)) fun (i : I) ↦ (Over.map p).map (f i))
have simp : Function.Bijective (β :=
    Subtype (α := (i : I) → P.obj (op ((Over.map p).obj (Y i))))
      (Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i)))
    ((⇑e :
        (a : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)) →
          Subtype (Arrows.Compatible P fun (i : I) ↦ (Over.map p).map (f i))) ∘
      Arrows.toCompatible ((Over.map p).op ⋙ P) f) ↔
  Function.Bijective (α := P.obj (op ((Over.map p).obj X))) (β :=
    Subtype (α := (i : I) → P.obj (op ((Over.map p).obj (Y i))))
      (Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i)))
    (Arrows.toCompatible P fun (i : I) ↦ (Over.map p).map (f i))
Tactic: simp only [isSheafFor_ofArrows_iff_bijective_toCompabible,
    ← e.bijective.of_comp_iff']
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
R : Sieve X
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
⊢ IsSheafFor ((Over.map p).op ⋙ P) R.arrows ↔
    IsSheafFor P (Sieve.pullback e.inv (Sieve.functorPushforward (Over.map p) R)).arrows
have obtain : ∀ (ι : Type (max u₁ v₁)) (Z : ι → Over.{v₁, u₁} B) (g : (i : ι) → Z i ⟶ X),
  IsSheafFor ((Over.map p).op ⋙ P) (Sieve.ofArrows Z g).arrows ↔
    IsSheafFor P (Sieve.pullback e.inv (Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g))).arrows
Tactic: obtain ⟨ι, Z, g, rfl⟩ := R.exists_eq_ofArrows
Cleared hypotheses: R
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
⊢ IsSheafFor ((Over.map p).op ⋙ P) (Sieve.ofArrows Z g).arrows ↔
    IsSheafFor P (Sieve.pullback e.inv (Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g))).arrows
have rw : IsSheafFor (X := (Over.map p).obj X) P
    (arrows (generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i)))) ↔
  IsSheafFor P (Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g)).arrows
Tactic: rw [← isSheafFor_iff_generate, isSheafFor_pullback_iff,
    isSheafFor_over_map_op_comp_ofArrows_iff, isSheafFor_iff_generate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
⊢ IsSheafFor (X := (Over.map p).obj X) P
      (arrows (generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i)))) ↔
    IsSheafFor P (Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g)).arrows
have h : Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g) =
  generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i))
Tactic: convert! Iff.rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
⊢ Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g) =
    generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i))
have h : Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g) ≤
  generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
h :
  Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g) ≤
    generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i))
⊢ Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g) =
    generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i))
have h₁ : generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i)) ≤
  Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
W : Over.{v₁, u₁} B'
T : Over.{v₁, u₁} B
a : W ⟶ (Over.map p).obj T
Y : Over.{v₁, u₁} B
i : ι
b : T ⟶ Z i
⊢ arrows (generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i)))
    (a ≫ (Over.map p).map (b ≫ g i))
have h : (Over.Hom.left a ≫ Over.Hom.left b) ≫ ((Over.map p).obj (Z i)).hom = W.hom
Tactic: refine ⟨(Over.map p).obj (Z i), Over.homMk (a.left ≫ b.left) ?_, _, ⟨i⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
W : Over.{v₁, u₁} B'
T : Over.{v₁, u₁} B
a : W ⟶ (Over.map p).obj T
Y : Over.{v₁, u₁} B
i : ι
b : T ⟶ Z i
h : (Over.Hom.left a ≫ Over.Hom.left b) ≫ ((Over.map p).obj (Z i)).hom = W.hom
⊢ arrows (generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i)))
    (a ≫ (Over.map p).map (b ≫ g i))
have h₁ : Over.homMk (Over.Hom.left a ≫ Over.Hom.left b) sorry ≫ (Over.map p).map (g i) = a ≫ (Over.map p).map (b ≫ g i)
Tactic: refine ⟨(Over.map p).obj (Z i), Over.homMk (a.left ≫ b.left) ?_, _, ⟨i⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst_1 : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
⊢ Compatible P π x ↔ PullbackCompatible P π x
have refine_1 : ∀ (t : Compatible P π x) (i j : I),
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst (π i) (π j)))) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X i)))) →
            (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
        (x i) :
      (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd (π i) (π j)))) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) →
            (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
        (x j) :
      (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
Tactic: refine ⟨fun t i j ↦ ?_, fun t i j Z gi gj comm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst_1 : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
refine_1 :
  ∀ (t : Compatible P π x) (i j : I),
    Eq (α := (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst (π i) (π j)))) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op (X i)))) →
              (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
          (x i) :
        (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd (π i) (π j)))) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) →
              (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
          (x j) :
        (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
⊢ Compatible P π x ↔ PullbackCompatible P π x
have refine_2 : ∀ (t : PullbackCompatible P π x) (i j : I) (Z : C) (gi : Z ⟶ X i) (gj : Z ⟶ X j) (comm : gi ≫ π i = gj ≫ π j),
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gi.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X i)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x i) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gj.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x j) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
Tactic: refine ⟨fun t i j ↦ ?_, fun t i j Z gi gj comm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst_1 : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
t : Compatible P π x
i j : I
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst (π i) (π j)))) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X i)))) →
            (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
        (x i) :
      (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd (π i) (π j)))) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) →
            (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
        (x j) :
      (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
have refine_1 : Eq (α := Limits.pullback (π i) (π j) ⟶ B) (pullback.fst (π i) (π j) ≫ π i) (pullback.snd (π i) (π j) ≫ π j)
Tactic: apply t