awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf.{v, v', u, u'} J A
c : Cone (F.obj (P := Presheaf.IsSheaf J))
hc : IsLimit c
X : A
f g : X ⟶ c.pt
h :
  ∀ (i : I),
    Eq (α := X ⟶ F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op (Y i))) (f ≫ c.π.app (Opposite.op (Y i)))
      (g ≫ c.π.app (Opposite.op (Y i)))
⊢ f = g
have refine : ∀ (Z : Cᵒᵖ) (I_1 : Cover.Arrow (X := Opposite.unop Z) (hY.cover (Opposite.unop Z))),
  (f ≫ c.π.app Z) ≫ F.obj (P := Presheaf.IsSheaf J).map I_1.f.op =
    (g ≫ c.π.app Z) ≫ F.obj (P := Presheaf.IsSheaf J).map I_1.f.op
Tactic: refine hc.hom_ext (fun Z => F.2.hom_ext (hY.cover Z.unop) _ _ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u u_2))
h : ∀ (i : I), (↑x : (j : Cᵒᵖ) → F.obj.obj j) (Opposite.op (Y i)) = (↑y : (j : Cᵒᵖ) → F.obj.obj j) (Opposite.op (Y i))
⊢ x = y
have a : ∀ (W : Cᵒᵖ), (↑x : (j : Cᵒᵖ) → F.obj.obj j) W = (↑y : (j : Cᵒᵖ) → F.obj.obj j) W
Tactic: ext W
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u u_2))
h : ∀ (i : I), (↑x : (j : Cᵒᵖ) → F.obj.obj j) (Opposite.op (Y i)) = (↑y : (j : Cᵒᵖ) → F.obj.obj j) (Opposite.op (Y i))
W : Cᵒᵖ
⊢ (↑x : (j : Cᵒᵖ) → F.obj.obj j) W = (↑y : (j : Cᵒᵖ) → F.obj.obj j) W
have a : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Opposite.unop W⦄,
  Sieve.arrows (Sieve.ofObjects Y (Opposite.unop W)) f →
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y_1)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj.obj (Opposite.op (Opposite.unop W)))) →
              (fun (X : Type u_2) ↦ X) (F.obj.obj (Opposite.op Y_1)))
          ((↑x : (j : Cᵒᵖ) → F.obj.obj j) W) :
        (fun (X : Type u_2) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y_1)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj.obj (Opposite.op (Opposite.unop W)))) →
              (fun (X : Type u_2) ↦ X) (F.obj.obj (Opposite.op Y_1)))
          ((↑y : (j : Cᵒᵖ) → F.obj.obj j) W) :
        (fun (X : Type u_2) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y_1)))
Tactic: apply (((isSheaf_iff_isSheaf_of_type _ _).1 F.2).isSeparated _ (hY W.unop)).ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
⊢ ∀ (h₁ : Sieve.arrows (Sieve.ofObjects Y X) f₁) (h₂ : Sieve.arrows (Sieve.ofObjects Y X) f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      Eq (α := (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₁.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
            (x.familyOfElements X f₁ h₁) :
          (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
            (x.familyOfElements X f₂ h₂) :
          (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
have this : ∀ (i₁ : I) (φ₁ : Y₁ ⟶ Y i₁) (h₂ : Sieve.arrows (Sieve.ofObjects Y X) f₂),
  g₁ ≫ f₁ = g₂ ≫ f₂ →
    Eq (α := (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₁.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
          (x.familyOfElements X f₁ sorry) :
        (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
          (x.familyOfElements X f₂ h₂) :
        (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
Tactic: ⟨i₁, ⟨φ₁⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
i₁ : I
φ₁ : Y₁ ⟶ Y i₁
⊢ ∀ (h₂ : Sieve.arrows (Sieve.ofObjects Y X) f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      Eq (α := (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₁.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
            (x.familyOfElements X f₁ ⋯) :
          (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
            (x.familyOfElements X f₂ h₂) :
          (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
have this : ∀ (i₂ : I) (φ₂ : Y₂ ⟶ Y i₂),
  g₁ ≫ f₁ = g₂ ≫ f₂ →
    Eq (α := (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₁.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
          (x.familyOfElements X f₁ sorry) :
        (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
          (x.familyOfElements X f₂ sorry) :
        (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
Tactic: ⟨i₂, ⟨φ₂⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
⊢ ∃! s : (↑F.sections : Type (max u w)), ∀ (i : I), (↑s : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
have H : Presieve.IsSheaf J F
Tactic: have H := (isSheaf_iff_isSheaf_of_type _ _).1 hF
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
⊢ ∃! s : (↑F.sections : Type (max u w)), ∀ (i : I), (↑s : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
have hex : ∃ (x_1 : (↑F.sections : Type (max u w))), ∀ (i : I), (↑x_1 : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
Tactic: apply existsUnique_of_exists_of_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
hex : ∃ (x_1 : (↑F.sections : Type (max u w))), ∀ (i : I), (↑x_1 : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
⊢ ∃! s : (↑F.sections : Type (max u w)), ∀ (i : I), (↑s : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
have hunique : ∀ (y₁ y₂ : (↑F.sections : Type (max u w))),
  (∀ (i : I), (↑y₁ : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i) →
    (∀ (i : I), (↑y₂ : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i) → y₁ = y₂
Tactic: apply existsUnique_of_exists_of_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) :=
  fun (X : C) ↦ ⋯.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) ⋯
X : C
i : I
f : X ⟶ Y i
⊢ s X =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op (Y i)))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
      (x i)
have h : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (𝟙 X))) :
      (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op X))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
    (sorry.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) sorry) =
  x.familyOfElements X (𝟙 X) sorry
Tactic: have h := Presieve.IsSheafFor.valid_glue (H _ (hY X))
          (hx.familyOfElements_isCompatible _) (𝟙 _) ⟨i, ⟨f⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) :=
  fun (X : C) ↦ ⋯.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) ⋯
X : C
i : I
f : X ⟶ Y i
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (𝟙 X))) :
        (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op X))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
      (⋯.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) ⋯) =
    x.familyOfElements X (𝟙 X) ⋯
⊢ s X =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op (Y i)))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
      (x i)
have h₁ : sorry.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) sorry = x.familyOfElements X (𝟙 X) sorry
Tactic: simp only [op_id, F.map_id, types_id_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) :=
  fun (X : C) ↦ ⋯.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) ⋯
⊢ ∃ (x_1 : (↑F.sections : Type (max u w))), ∀ (i : I), (↑x_1 : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
have hs : ∀ {X : C} (i : I) (f : X ⟶ Y i),
  s X =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op (Y i)))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
      (x i)
Tactic: have hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = F.map f.op (x i) := fun {X} i f => by
      have h := Presieve.IsSheafFor.valid_glue (H _ (hY X))
          (hx.familyOfElements_isCompatible _) (𝟙 _) ⟨i, ⟨f⟩⟩
      simp only [op_id, F.map_id, types_id_apply] at h
      exact h.trans (hx.familyOfElements_apply _ _ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) :=
  fun (X : C) ↦ ⋯.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) ⋯
hs :
  ∀ {X : C} (i : I) (f : X ⟶ Y i),
    s X =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op (Y i)))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
        (x i)
W X : C
a : W ⟶ X
i : I
b : W ⟶ Y i
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map a.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op X))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
      (s X) =
    s W
have rw : Eq (α := (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map a.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op X))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
      (s X) :
    (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map b.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op (Y i)))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
      (x i) :
    (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
Tactic: rw [hs i b]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) :=
  fun (X : C) ↦ ⋯.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) ⋯
hs :
  ∀ {X : C} (i : I) (f : X ⟶ Y i),
    s X =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op (Y i)))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
        (x i)
⊢ ∃ (x_1 : (↑F.sections : Type (max u w))), ∀ (i : I), (↑x_1 : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
have hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map a.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op X))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
      (s X) =
    s W
Tactic: have hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (_ : W ⟶ Y i), F.map a.op (s X) = s W := by
      intro W X a i b
      rw [hs i b]
      exact (Presieve.IsSheafFor.valid_glue (H _ (hY X))
        (hx.familyOfElements_isCompatible _) a ⟨i, ⟨b⟩⟩).trans (familyOfElements_apply hx _ _ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) :=
  fun (X : C) ↦ ⋯.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) ⋯
hs :
  ∀ {X : C} (i : I) (f : X ⟶ Y i),
    s X =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op (Y i)))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
        (x i)
hs' :
  ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map a.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op X))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
        (s X) =
      s W
⊢ ∃ (x_1 : (↑F.sections : Type (max u w))), ∀ (i : I), (↑x_1 : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
have hex : (fun (X : Cᵒᵖ) ↦ s (Opposite.unop X)) ∈ F.sections
Tactic: refine ⟨⟨fun X => s X.unop, ?_⟩, fun i => (hs i (𝟙 (Y i))).trans (by simp)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) :=
  fun (X : C) ↦ ⋯.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) ⋯
hs :
  ∀ {X : C} (i : I) (f : X ⟶ Y i),
    s X =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op (Y i)))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
        (x i)
hs' :
  ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map a.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op X))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
        (s X) =
      s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
⊢ Eq (α := (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Opposite.op f)) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
        ((fun (X : Cᵒᵖ) ↦ (s (Opposite.unop X) : F.obj (Opposite.op (Opposite.unop X)))) (Opposite.op Y₁)) :
      (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
    ((fun (X : Cᵒᵖ) ↦ (s (Opposite.unop X) : F.obj (Opposite.op (Opposite.unop X)))) (Opposite.op Y₂) :
      F.obj (Opposite.op (Opposite.unop (Opposite.op Y₂))))
have hex : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
      (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
    (s Y₁) =
  s Y₂
Tactic: change F.map f.op (s Y₁) = s Y₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) :=
  fun (X : C) ↦ ⋯.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) ⋯
hs :
  ∀ {X : C} (i : I) (f : X ⟶ Y i),
    s X =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op (Y i)))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
        (x i)
hs' :
  ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map a.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op X))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
        (s X) =
      s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
      (s Y₁) =
    s Y₂
have hex : ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y₂⦄,
  Sieve.arrows (Sieve.ofObjects Y Y₂) f_1 →
    Eq (α := (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y_1)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y_1)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
                (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
              (s Y₁) :
            (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) :
        (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y_1)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y_1)))
          (s Y₂) :
        (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y_1)))
Tactic: apply (H.isSeparated _ (hY Y₂)).ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) :=
  fun (X : C) ↦ ⋯.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) ⋯
hs :
  ∀ {X : C} (i : I) (f : X ⟶ Y i),
    s X =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op (Y i)))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
        (x i)
hs' :
  ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map a.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op X))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
        (s X) =
      s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
Z : C
φ : Z ⟶ Y₂
i : I
g : Z ⟶ Y i
⊢ Eq (α := (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
            (s Y₁) :
          (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) :
      (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
        (s Y₂) :
      (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
have hex : Eq (α := (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
          (s Y₁) :
        (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) :
    (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op ≫ F.map φ.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
      (s Y₁) :
    (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
Tactic: rw [hs' φ i g, ← hs' (φ ≫ f) i g, op_comp, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
y₁ y₂ : (↑F.sections : Type (max u w))
hy₁ : ∀ (i : I), (↑y₁ : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
hy₂ : ∀ (i : I), (↑y₂ : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
i : I
⊢ (↑y₁ : (j : Cᵒᵖ) → { obj := F, property := hF }.obj.obj j) (Opposite.op (Y i)) =
    (↑y₂ : (j : Cᵒᵖ) → { obj := F, property := hF }.obj.obj j) (Opposite.op (Y i))
have rw : x i = (↑y₂ : (j : Cᵒᵖ) → { obj := F, property := hF }.obj.obj j) (Opposite.op (Y i))
Tactic: rw [hy₁, hy₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
y₁ y₂ : (↑F.sections : Type (max u w))
hy₁ : ∀ (i : I), (↑y₁ : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
hy₂ : ∀ (i : I), (↑y₂ : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
i : I
rw : x i = (↑y₂ : (j : Cᵒᵖ) → { obj := F, property := hF }.obj.obj j) (Opposite.op (Y i))
⊢ (↑y₁ : (j : Cᵒᵖ) → { obj := F, property := hF }.obj.obj j) (Opposite.op (Y i)) =
    (↑y₂ : (j : Cᵒᵖ) → { obj := F, property := hF }.obj.obj j) (Opposite.op (Y i))
have rw₁ : x i = x i
Tactic: rw [hy₁, hy₂]