awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover.{u_3, v_1, u_1} S
inst_1 : E.HasPullbacks
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
heq :
  Eq (α := F.obj (op (pullback (E.f i) (E.f j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.fst (E.f i) (E.f j)))) :
          (a : F.obj (op (E.X i))) → F.obj (op (pullback (E.f i) (E.f j))))
        (s.val i) :
      F.obj (op (pullback (E.f i) (E.f j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.snd (E.f i) (E.f j)))) :
          (a : F.obj (op (E.X j))) → F.obj (op (pullback (E.f i) (E.f j))))
        (s.val j) :
      F.obj (op (pullback (E.f i) (E.f j))))
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (pullback.lift gi gj hgij)
                  (pullback.fst (E.f i) (E.f j))).op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val i) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map gj.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val j) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
have conv_rhs : Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map
            (CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (pullback.lift gi gj hgij)
                (pullback.fst (E.f i) (E.f j))).op) :
        (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
      (s.val i) :
    (fun (X : Type u_2) ↦ X) (F.obj (op W)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map
            (CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (pullback.lift gi gj hgij)
                (pullback.snd (E.f i) (E.f j))).op) :
        (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
      (s.val j) :
    (fun (X : Type u_2) ↦ X) (F.obj (op W)))
Tactic: conv_rhs => rw [← pullback.lift_snd _ _ hgij]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover.{u_3, v_1, u_1} S
inst_1 : E.HasPullbacks
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
heq :
  Eq (α := F.obj (op (pullback (E.f i) (E.f j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.fst (E.f i) (E.f j)))) :
          (a : F.obj (op (E.X i))) → F.obj (op (pullback (E.f i) (E.f j))))
        (s.val i) :
      F.obj (op (pullback (E.f i) (E.f j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.snd (E.f i) (E.f j)))) :
          (a : F.obj (op (E.X j))) → F.obj (op (pullback (E.f i) (E.f j))))
        (s.val j) :
      F.obj (op (pullback (E.f i) (E.f j))))
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (pullback.lift gi gj hgij)
                  (pullback.fst (E.f i) (E.f j))).op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val i) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (pullback.lift gi gj hgij)
                  (pullback.snd (E.f i) (E.f j))).op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val j) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
have rw : Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := F.obj (op (pullback (E.f i) (E.f j))))
            (F.map (Quiver.Hom.op (pullback.fst (E.f i) (E.f j)))) (F.map (Quiver.Hom.op (pullback.lift gi gj hgij)))) :
        (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
      (s.val i) :
    (fun (X : Type u_2) ↦ X) (F.obj (op W)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := F.obj (op (pullback (E.f i) (E.f j))))
            (F.map (Quiver.Hom.op (pullback.snd (E.f i) (E.f j)))) (F.map (Quiver.Hom.op (pullback.lift gi gj hgij)))) :
        (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
      (s.val j) :
    (fun (X : Type u_2) ↦ X) (F.obj (op W)))
Tactic: rw [op_comp, Functor.map_comp, op_comp, Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover.{w, v_1, u_1} S
inst_1 : E.HasPullbacks
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
⊢ Nonempty (IsLimit (E.toPreOneHypercover.multifork F)) ↔ Presieve.IsSheafFor F E.presieve₀
have rw : Function.Bijective (E.toPreOneHypercover.multifork F).toSections ↔
  Function.Bijective (β := (E.toPreOneHypercover.multicospanIndex F).sections)
    ((⇑(Equiv.symm (E.sectionsEquivOfHasPullbacks F)) :
        (a : Subtype (Presieve.Arrows.Compatible F E.f)) → (E.toPreOneHypercover.multicospanIndex F).sections) ∘
      Presieve.Arrows.toCompatible F E.f)
Tactic: rw [Multifork.isLimit_types_iff, Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible,
    ← Function.Bijective.of_comp_iff' (E.sectionsEquivOfHasPullbacks F).symm.bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒱.X 𝒱.f)
have rw : Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows
Tactic: rw [Presieve.isSheafFor_iff_generate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows
have h : (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows ≤ (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows
Tactic: apply Presieve.isSheafFor_subsieve_aux (S := .generate (.ofArrows 𝒰.X 𝒰.f))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
h : (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows ≤ (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows
⊢ Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows
have hS : Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows
Tactic: apply Presieve.isSheafFor_subsieve_aux (S := .generate (.ofArrows 𝒰.X 𝒰.f))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
h : (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows ≤ (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows
hS : Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows
⊢ Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows
have trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ S⦄,
  (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows f →
    Presieve.IsSeparatedFor F (Sieve.pullback f (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f))).arrows
Tactic: apply Presieve.isSheafFor_subsieve_aux (S := .generate (.ofArrows 𝒰.X 𝒰.f))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows ≤ (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows
have h : ∀ (i : 𝒰.I₀), (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows (𝒰.f i)
Tactic: rw [← Sieve.generate_le_iff, Sieve.generate_sieve, Sieve.generate_le_iff,
      Presieve.ofArrows_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
i : 𝒰.I₀
⊢ (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows (𝒰.f i)
have h : (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows (f.h₀ i ≫ 𝒱.f (f.s₀ i))
Tactic: rw [← f.w₀]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f_1 : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
Y : C
f : Y ⟶ S
hf : (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows f
⊢ Presieve.IsSeparatedFor F (Sieve.pullback f (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f))).arrows
have trans : Presieve.IsSeparatedFor (X := Y) F
  (Presieve.ofArrows (fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i) f) fun (x : 𝒰.I₀) ↦ pullback.snd (𝒰.f x) f)
Tactic: rw [← Sieve.pullbackArrows_comm, ← Presieve.isSeparatedFor_iff_generate,
      ← Presieve.ofArrows_pullback]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h : E.IsStronglySeparatedFor F
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₁ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x i) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₂ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x j) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
i₁ i₂ : E.I₀
Z : C
g₁ : Z ⟶ E.X i₁
g₂ : Z ⟶ E.X i₂
heq : g₁ ≫ E.f i₁ = g₂ ≫ E.f i₂
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₁.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₁)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
        (x i₁) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₂)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
        (x i₂) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
have refine : ∀ (W : C) (f : W ⟶ Z),
  (E.sieve₁ g₁ g₂).arrows f →
    ∀ (T : E.I₁ i₁ i₂) (u : W ⟶ E.Y T) (h₁ : f ≫ g₁ = u ≫ E.p₁ T) (h₂ : f ≫ g₂ = u ≫ E.p₂ T),
      Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj (op Z))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₁.op) :
                  (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₁)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
                (x i₁) :
              (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
          (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj (op Z))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
                  (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₂)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
                (x i₂) :
              (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
          (fun (X : Type u_2) ↦ X) (F.obj (op W)))
Tactic: refine (h.isSeparatedFor_sieve₁ g₁ g₂ heq).ext fun W f ⟨T, u, h₁, h₂⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h : E.IsStronglySeparatedFor F
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₁ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x i) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₂ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x j) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
i₁ i₂ : E.I₀
Z : C
g₁ : Z ⟶ E.X i₁
g₂ : Z ⟶ E.X i₂
heq : g₁ ≫ E.f i₁ = g₂ ≫ E.f i₂
W : C
f : W ⟶ Z
h_1 : (E.sieve₁ g₁ g₂).arrows f
T : E.I₁ i₁ i₂
u : W ⟶ E.Y T
h₁ : f ≫ g₁ = u ≫ E.p₁ T
h₂ : f ≫ g₂ = u ≫ E.p₂ T
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op Z))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₁.op) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₁)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
            (x i₁) :
          (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op Z))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₂)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
            (x i₂) :
          (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
have rw : Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (u ≫ E.p₁ T).op) :
        (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₁)))) → F.obj (op W))
      (x i₁) :
    F.obj (op W))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type u_2) ↦ X) (F.obj (op Z))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₂)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
          (x i₂) :
        (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
    (fun (X : Type u_2) ↦ X) (F.obj (op W)))
Tactic: rw [← comp_apply, ← Functor.map_comp, ← op_comp, h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h : E.IsStronglySeparatedFor F
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₁ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x i) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₂ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x j) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
i₁ i₂ : E.I₀
Z : C
g₁ : Z ⟶ E.X i₁
g₂ : Z ⟶ E.X i₂
heq : g₁ ≫ E.f i₁ = g₂ ≫ E.f i₂
W : C
f : W ⟶ Z
h_1 : (E.sieve₁ g₁ g₂).arrows f
T : E.I₁ i₁ i₂
u : W ⟶ E.Y T
h₁ : f ≫ g₁ = u ≫ E.p₁ T
h₂ : f ≫ g₂ = u ≫ E.p₂ T
| ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type u_2) ↦ X) (F.obj (op Z))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₂)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
          (x i₂) :
        (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
    (fun (X : Type u_2) ↦ X) (F.obj (op W)))
have rw : ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (u ≫ E.p₂ T).op) :
      (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₂)))) → F.obj (op W))
    (x i₂) :
  F.obj (op W))
Tactic: rw [← comp_apply, ← Functor.map_comp, ← op_comp, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h : E.IsStronglySeparatedFor F
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₁ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x i) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₂ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x j) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
i₁ i₂ : E.I₀
Z : C
g₁ : Z ⟶ E.X i₁
g₂ : Z ⟶ E.X i₂
heq : g₁ ≫ E.f i₁ = g₂ ≫ E.f i₂
W : C
f : W ⟶ Z
h_1 : (E.sieve₁ g₁ g₂).arrows f
T : E.I₁ i₁ i₂
u : W ⟶ E.Y T
h₁ : f ≫ g₁ = u ≫ E.p₁ T
h₂ : f ≫ g₂ = u ≫ E.p₂ T
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (u ≫ E.p₁ T).op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₁)))) → F.obj (op W))
        (x i₁) :
      F.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op Z))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₂)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
            (x i₂) :
          (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
have conv_rhs : Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (u ≫ E.p₁ T).op) :
        (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₁)))) → F.obj (op W))
      (x i₁) :
    F.obj (op W))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (u ≫ E.p₂ T).op) :
        (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₂)))) → F.obj (op W))
      (x i₂) :
    F.obj (op W))
Tactic: conv_rhs => rw [← comp_apply, ← Functor.map_comp, ← op_comp, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h : E.IsStronglySheafFor F
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₁ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x i) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₂ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x j) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
i : E.I₀
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.f i).op) :
        (a : (fun (X : Type u_2) ↦ X) (F.obj (op X))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i))))
      (h.amalgamate x hc) =
    x i
have rw : sorry.familyOfElements (E.f i) sorry = x i
Tactic: rw [amalgamate, Presieve.IsSheafFor.valid_glue _ _ _ ⟨i⟩]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h : E.IsStronglySheafFor F
⊢ IsLimit (E.multifork F)
have refine : Nonempty (IsLimit (E.multifork F))
Tactic: refine Nonempty.some ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h : E.IsStronglySheafFor F
⊢ Nonempty (IsLimit (E.multifork F))
have rw : Function.Bijective (E.multifork F).toSections
Tactic: rw [Multifork.isLimit_types_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h : E.IsStronglySheafFor F
⊢ Function.Bijective (E.multifork F).toSections
have refine_1 : ∀ (s t : (E.multifork F).pt) (hst : (E.multifork F).toSections s = (E.multifork F).toSections t), s = t
Tactic: refine ⟨fun s t hst ↦ ?_, fun s ↦ ?_⟩