awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{w, u} (precoverage P) S
inst : QuasiCompactCover 𝒰.toPreZeroHypercover
i : (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).I₀
⊢ P ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f i)
have inl : ∀ (val : 𝒰.ulift (P := P).I₀),
  P (X := (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).X (Sum.inl val))
    ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f (Sum.inl val))
Tactic: induction i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{w, u} (precoverage P) S
inst : QuasiCompactCover 𝒰.toPreZeroHypercover
i : (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).I₀
inl :
  ∀ (val : 𝒰.ulift (P := P).I₀),
    P (X := (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).X (Sum.inl val))
      ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f (Sum.inl val))
⊢ P ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f i)
have inr : ∀ (val : (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover).I₀),
  P (X := (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).X (Sum.inr val))
    ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f (Sum.inr val))
Tactic: induction i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ Precoverage.ZeroHypercover.Small 𝒰
have refine_1 : (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
      (Sum.elim 𝒰.forgetQc (P := P).idx
        (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).presieve₀ ∈
  qcPrecoverage.coverings S
Tactic: refine ⟨𝒰.forgetQc.qculift.I₀, Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom _).s₀,
      ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
refine_1 :
  (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
        (Sum.elim 𝒰.forgetQc (P := P).idx
          (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).presieve₀ ∈
    qcPrecoverage.coverings S
⊢ Precoverage.ZeroHypercover.Small 𝒰
have refine_2 : (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
      (Sum.elim 𝒰.forgetQc (P := P).idx
        (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).presieve₀ ∈
  (precoverage P).coverings S
Tactic: refine ⟨𝒰.forgetQc.qculift.I₀, Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom _).s₀,
      ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
        (Sum.elim 𝒰.forgetQc (P := P).idx
          (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).presieve₀ ∈
    qcPrecoverage.coverings S
have refine_1 : QuasiCompactCover
  (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
    (Sum.elim 𝒰.forgetQc (P := P).idx
      (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover))))
Tactic: rw [Scheme.presieve₀_mem_qcPrecoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
        (Sum.elim 𝒰.forgetQc (P := P).idx
          (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).presieve₀ ∈
    (precoverage P).coverings S
have refine_2 : (∀ (x : ↥S),
    ∃ (i :
      (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
          (Sum.elim 𝒰.forgetQc (P := P).idx
            (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).I₀),
      Membership.mem (γ := Set ↥S)
        (Set.range (ι :=
          ↥((𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
                  (Sum.elim 𝒰.forgetQc (P := P).idx
                    (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).X
              i))
          ⇑((𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
                  (Sum.elim 𝒰.forgetQc (P := P).idx
                    (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).f
              i))
        x) ∧
  ∀
    (i :
      (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
          (Sum.elim 𝒰.forgetQc (P := P).idx
            (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).I₀),
    P
      ((𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
            (Sum.elim 𝒰.forgetQc (P := P).idx
              (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).f
        i)
Tactic: rw [Scheme.presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
R : Presieve S
⊢ R ∈ (propQCPrecoverage P).coverings S ↔
    ∃ (𝒰 : Cover (precoverage P) S), QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀
have rw : (∃ (𝒰 : (propQCPrecoverage P).ZeroHypercover S), R = Presieve.ofArrows 𝒰.X 𝒰.f) ↔
  ∃ (𝒰 : Cover (precoverage P) S), QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀
Tactic: rw [Precoverage.mem_iff_exists_zeroHypercover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
R : Presieve S
⊢ (∃ (𝒰 : (propQCPrecoverage P).ZeroHypercover S), R = Presieve.ofArrows 𝒰.X 𝒰.f) ↔
    ∃ (𝒰 : Cover (precoverage P) S), QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀
have refine : (∃ (𝒰 : (propQCPrecoverage P).ZeroHypercover S), R = Presieve.ofArrows 𝒰.X 𝒰.f) →
  ∀ (𝒰 : (propQCPrecoverage P).ZeroHypercover S) (h : R = Presieve.ofArrows 𝒰.X 𝒰.f),
    QuasiCompactCover (𝒰.weaken sorry).toPreZeroHypercover
Tactic: refine ⟨fun ⟨𝒰, h⟩ ↦ ⟨𝒰.weaken propQCPrecoverage_le_precoverage, ?_, h⟩,
    fun ⟨𝒰, _, h⟩ ↦ ⟨⟨𝒰.1, ⟨by simpa, 𝒰.mem₀⟩⟩, h⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
R : Presieve S
h_1 : ∃ (𝒰 : (propQCPrecoverage P).ZeroHypercover S), R = Presieve.ofArrows 𝒰.X 𝒰.f
𝒰 : (propQCPrecoverage P).ZeroHypercover S
h : R = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ QuasiCompactCover (𝒰.weaken ⋯).toPreZeroHypercover
have rw : (𝒰.weaken sorry).presieve₀ ∈ qcPrecoverage.coverings S
Tactic: rw [← Scheme.presieve₀_mem_qcPrecoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : P f
inst : Surjective f
inst_1 : QuasiCompact f
⊢ Presieve.singleton f ∈ (propQCPrecoverage P).coverings Y
have refine : Presieve.singleton f ∈ (precoverage P).coverings Y
Tactic: refine ⟨f.singleton_mem_qcPrecoverage, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : IsEmpty.{u + 1} ↥X
⊢ ⊥ ∈ (propQCTopology P : (a : Scheme) → Set (Sieve a)) X
have rw : Sieve.generate ⊥ ∈ (propQCTopology P : (a : Scheme) → Set (Sieve a)) X
Tactic: rw [← Sieve.generate_bot]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : P f
inst : Surjective f
inst_1 : QuasiCompact f
⊢ Sieve.generate (Presieve.singleton f) ∈ (propQCTopology P : (a : Scheme) → Set (Sieve a)) Y
have hR : Presieve.singleton f ∈ (propQCPrecoverage P).coverings Y
Tactic: apply Precoverage.generate_mem_toGrothendieck
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst : QuasiCompactCover 𝒰.toPreZeroHypercover
⊢ Sieve.ofArrows 𝒰.X 𝒰.f ∈ (propQCTopology P : (a : Scheme) → Set (Sieve a)) S
have refine : Presieve.ofArrows 𝒰.X 𝒰.f ∈ qcPrecoverage.coverings S
Tactic: refine Precoverage.generate_mem_toGrothendieck ⟨?_, 𝒰.mem₀⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j k i : ι
⊢ ⋯.symmetry ⋯ =
    𝟙
      (match (motive := ι × ι → Scheme) (i, i) with
      | (i, j) => ⋯.pullback (f j))
have h₁ : sorry.symmetry sorry ≫ sorry.fst' (f i) =
  𝟙
      (match (motive := ι × ι → Scheme) (i, i) with
      | (i, j) => sorry.pullback (f j)) ≫
    sorry.fst' (f i)
Tactic: apply (hf i).rep.hom_ext'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j k i : ι
h₁ :
  ⋯.symmetry ⋯ ≫ ⋯.fst' (f i) =
    𝟙
        (match (motive := ι × ι → Scheme) (i, i) with
        | (i, j) => ⋯.pullback (f j)) ≫
      ⋯.fst' (f i)
⊢ ⋯.symmetry ⋯ =
    𝟙
      (match (motive := ι × ι → Scheme) (i, i) with
      | (i, j) => ⋯.pullback (f j))
have h₂ : sorry.symmetry sorry ≫ sorry.snd (f i) =
  𝟙
      (match (motive := ι × ι → Scheme) (i, i) with
      | (i, j) => sorry.pullback (f j)) ≫
    sorry.snd (f i)
Tactic: apply (hf i).rep.hom_ext'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i : ι
⊢ CategoryTheory.Functor.map yoneda (toGlued hf i) ≫ (yonedaGluedToSheaf hf).hom = f i
have a : Eq (α := F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
  ((yonedaEquiv : (a : yoneda.obj (X i) ⟶ F.obj) → F.obj.obj (op (X i)))
      (CategoryTheory.Functor.map yoneda (toGlued hf i) ≫ (yonedaGluedToSheaf hf).hom) :
    F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
  ((yonedaEquiv : (a : yoneda.obj (X i) ⟶ F.obj) → F.obj.obj (op (X i))) (f i) :
    F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
Tactic: apply yonedaEquiv.injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i : ι
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((yonedaEquiv : (a : yoneda.obj (X i) ⟶ F.obj) → F.obj.obj (op (X i)))
        (CategoryTheory.Functor.map yoneda (toGlued hf i) ≫ (yonedaGluedToSheaf hf).hom) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((yonedaEquiv : (a : yoneda.obj (X i) ⟶ F.obj) → F.obj.obj (op (X i))) (f i) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
have a : Eq (α := F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (InducedCategory.Hom.hom
              {
                hom :=
                  (Equiv.symm yonedaEquiv :
                      (a : F.obj.obj (op (glueData hf).glued)) → yoneda.obj (glueData hf).glued ⟶ F.obj)
                    ((glueData hf).sheafValGluedMk
                      (fun (i : (glueData hf).J) ↦
                        (yonedaEquiv :
                            (a : yoneda.obj ((glueData hf).U i) ⟶ F.obj) → F.obj.obj (op ((glueData hf).U i)))
                          (f i))
                      sorry) :
                InducedCategory.Hom (D := Schemeᵒᵖ ⥤ Type u) (F :=
                  ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf zariskiTopology))
                  (zariskiTopology.yoneda.obj (glueData hf).glued) F })
            (op (X i))) :
        (a : (yoneda.obj (glueData hf).glued).obj (op (X i))) → F.obj.obj (op (X i)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun
                  (g :
                    Functor.obj
                      { obj := fun (Y : Schemeᵒᵖ) ↦ unop Y ⟶ X i,
                        map := fun {X_1 Y : Schemeᵒᵖ} (f : X_1 ⟶ Y) ↦ ↾fun (g : unop X_1 ⟶ X i) ↦ f.unop ≫ g,
                        map_id := sorry, map_comp := sorry : Schemeᵒᵖ ⥤ Type u }
                      (op (X i))) ↦
                g ≫ toGlued hf i) :
            (a : (yoneda.obj (X i)).obj (op (X i))) → (yoneda.obj (glueData hf).glued).obj (op (X i)))
          (𝟙 (X i)) :
        Functor.obj (Functor.obj yoneda (glueData hf).glued) (op (X i))) :
    F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((f i).app (op (X i))) :
        (a : (fun (X : Type u) ↦ X) ((yoneda.obj (X i)).obj (op (X i)))) →
          (fun (X : Type u) ↦ X) (F.obj.obj (op (X i))))
      (𝟙 (X i)) :
    (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i))))
Tactic: rw [yonedaGluedToSheaf, yonedaEquiv_apply, yonedaEquiv_apply,
    NatTrans.comp_app_apply, yoneda_map_app]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i : ι
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op (X i))) :
          (a : X i ⟶ (glueData hf).glued) → F.obj.obj (op (X i)))
        (toGlued hf i) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((yonedaEquiv : (a : yoneda.obj (X i) ⟶ F.obj) → F.obj.obj (op (X i))) (f i) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
have rw : Eq (α := F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op (X i))) :
        (a : X i ⟶ (glueData hf).glued) → F.obj.obj (op (X i)))
      (toGlued hf i) :
    F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op (X i))) :
        (a : (fun (X : Type u) ↦ X) ((yoneda.obj (glueData hf).glued).obj (op (X i)))) →
          (fun (X : Type u) ↦ X) (F.obj.obj (op (X i))))
      (toGlued hf i) :
    (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i))))
Tactic: rw [← yoneda_toGlued_yonedaGluedToSheaf hf i, yonedaEquiv_comp,
    yonedaEquiv_yoneda_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
U : Scheme
i j : ι
a : U ⟶ X i
b : U ⟶ X j
h : CategoryTheory.Functor.map yoneda a ≫ f i = CategoryTheory.Functor.map yoneda b ≫ f j
⊢ a ≫ toGlued hf i = b ≫ toGlued hf j
have rw : sorry.lift' a b h ≫ sorry.fst' (f j) ≫ toGlued hf i = b ≫ toGlued hf j
Tactic: rw [← (hf i).rep.lift'_fst a b h, assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
U : Scheme
i j : ι
a : U ⟶ X i
b : U ⟶ X j
h : CategoryTheory.Functor.map yoneda a ≫ f i = CategoryTheory.Functor.map yoneda b ≫ f j
| b ≫ toGlued hf j
have rw : sorry.lift' a b h ≫ sorry.snd (f j) ≫ toGlued hf j
Tactic: rw [← (hf i).rep.lift'_snd a b h, assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
U : Scheme
i j : ι
a : U ⟶ X i
b : U ⟶ X j
h : CategoryTheory.Functor.map yoneda a ≫ f i = CategoryTheory.Functor.map yoneda b ≫ f j
⊢ ⋯.lift' a b h ≫ ⋯.fst' (f j) ≫ toGlued hf i = b ≫ toGlued hf j
have conv_rhs : sorry.lift' a b h ≫ sorry.fst' (f j) ≫ toGlued hf i = sorry.lift' a b h ≫ sorry.snd (f j) ≫ toGlued hf j
Tactic: conv_rhs => rw [← (hf i).rep.lift'_snd a b h, assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
U : Scheme
i j : ι
a : U ⟶ X i
b : U ⟶ X j
h : CategoryTheory.Functor.map yoneda a ≫ f i = CategoryTheory.Functor.map yoneda b ≫ f j
⊢ ⋯.lift' a b h ≫ ⋯.fst' (f j) ≫ toGlued hf i = ⋯.lift' a b h ≫ ⋯.snd (f j) ≫ toGlued hf j
have e_a : sorry.fst' (f j) ≫ toGlued hf i = sorry.snd (f j) ≫ toGlued hf j
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (hypothesis)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        α :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        β :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
⊢ Membership.mem (γ := Set (Sieve (unop (op U)))) ((zariskiTopology : (a : Scheme) → Set (Sieve a)) (unop (op U)))
    (Presheaf.equalizerSieve (FD := TypeCat.Fun) (F :=
      (zariskiTopology.yoneda.obj (glueData hf).glued).obj (P := Presheaf.IsSheaf zariskiTopology)) α β)
have mem : Membership.mem (γ := Set (Sieve (glueData hf).glued))
  ((grothendieckTopology IsOpenImmersion : (a : Scheme) → Set (Sieve a)) (glueData hf).glued)
  (Sieve.ofArrows (I :=
    PreZeroHypercover.I₀ (S := (glueData hf).glued)
      (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
    (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)))
Tactic: have mem := (glueData hf).openCover.mem_grothendieckTopology
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        α :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        β :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
mem :
  Membership.mem (γ := Set (Sieve (glueData hf).glued))
    ((grothendieckTopology IsOpenImmersion : (a : Scheme) → Set (Sieve a)) (glueData hf).glued)
    (Sieve.ofArrows (I :=
      PreZeroHypercover.I₀ (S := (glueData hf).glued)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)))
⊢ Membership.mem (γ := Set (Sieve (unop (op U)))) ((zariskiTopology : (a : Scheme) → Set (Sieve a)) (unop (op U)))
    (Presheaf.equalizerSieve (FD := TypeCat.Fun) (F :=
      (zariskiTopology.yoneda.obj (glueData hf).glued).obj (P := Presheaf.IsSheaf zariskiTopology)) α β)
have refine : Sieve.pullback α
      (Sieve.ofArrows (I :=
        PreZeroHypercover.I₀ (S := (glueData hf).glued)
          (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
        (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))) ⊓
    Sieve.pullback β
      (Sieve.ofArrows (I :=
        PreZeroHypercover.I₀ (S := (glueData hf).glued)
          (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
        (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))) ≤
  Presheaf.equalizerSieve (FD := TypeCat.Fun) (F :=
    (zariskiTopology.yoneda.obj (glueData hf).glued).obj (P := Presheaf.IsSheaf zariskiTopology)) α β
Tactic: refine GrothendieckTopology.superset_covering _ ?_
      (zariskiTopology.intersection_covering (zariskiTopology.pullback_stable α mem)
        (zariskiTopology.pullback_stable β mem))