awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
F : CategoryTheory.Functor.{u, v, u + 1, v + 1} Schemeᵒᵖ (Type v)
ι : Type u_1
inst : Small.{u, u_1} ι
inst_1 : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
X : ι → Schemeᵒᵖ
this :
  ∀ (i : ι),
    Mono (X := (unop ∘ X) i) (Y :=
      Cocone.pt (F := Discrete.functor (unop ∘ X)) (Sigma.cocone (Discrete.functor (unop ∘ X))))
      (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
⊢ Eq.{u + 2} (α := Sieve (⊥_ Scheme))
    (Sieve.generate
      (Presieve.ofArrows Empty.elim fun (a : Empty) ↦
        Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ ⊥_ Scheme) a))
    ⊥
have h : LE.le.{u + 1} (α := Sieve (⊥_ Scheme))
  (Sieve.generate
    (Presieve.ofArrows Empty.elim fun (a : Empty) ↦
      Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ ⊥_ Scheme) a))
  ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ Scheme.forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{u_1, u_2} J
inst_4 : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
⊢ Membership.mem (γ := Set (Sieve c.pt)) ((Scheme.zariskiTopology : (a : Scheme) → Set (Sieve a)) c.pt)
    (Sieve.ofArrows F.obj c.ι.app)
have rw : Membership.mem (γ := Set (Sieve (colimit F))) ((Scheme.zariskiTopology : (a : Scheme) → Set (Sieve a)) (colimit F))
  (Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app))
Tactic: rw [← GrothendieckTopology.pullback_mem_iff_of_isIso (i := iso.inv)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ Scheme.forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{u_1, u_2} J
inst_4 : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
⊢ Membership.mem (γ := Set (Sieve (colimit F))) ((Scheme.zariskiTopology : (a : Scheme) → Set (Sieve a)) (colimit F))
    (Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app))
have apply : Sieve (colimit F)
Tactic: apply GrothendieckTopology.superset_covering _ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ Scheme.forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{u_1, u_2} J
inst_4 : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
apply : Sieve (colimit F)
⊢ Membership.mem (γ := Set (Sieve (colimit F))) ((Scheme.zariskiTopology : (a : Scheme) → Set (Sieve a)) (colimit F))
    (Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app))
have apply₁ : Sieve.ofArrows F.obj (colimit.ι F) ≤ Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app)
Tactic: apply GrothendieckTopology.superset_covering _ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ Scheme.forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{u_1, u_2} J
inst_4 : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
apply : Sieve (colimit F)
apply₁ : Sieve.ofArrows F.obj (colimit.ι F) ≤ Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app)
⊢ Membership.mem (γ := Set (Sieve (colimit F))) ((Scheme.zariskiTopology : (a : Scheme) → Set (Sieve a)) (colimit F))
    (Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app))
have apply₂ : Membership.mem (γ := Set (Sieve (colimit F))) ((Scheme.zariskiTopology : (a : Scheme) → Set (Sieve a)) (colimit F))
  (Sieve.ofArrows F.obj (colimit.ι F))
Tactic: apply GrothendieckTopology.superset_covering _ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ Scheme.forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{u_1, u_2} J
inst_4 : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
⊢ Sieve.ofArrows F.obj (colimit.ι F) ≤ Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app)
have rw : Presieve.ofArrows F.obj (colimit.ι F) ≤ (Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app)).arrows
Tactic: rw [Sieve.ofArrows, Sieve.generate_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (hypothesis)
Goal:
P : MorphismProperty Scheme
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst_1 : Finite.{u + 1} 𝒰.I₀
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.sigma (P := P).X 𝒰.sigma (P := P).f) ↔
    Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
have this : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
Tactic: have : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F :=
    preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology hF
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (hypothesis)
Goal:
P : MorphismProperty Scheme
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst_1 : Finite.{u + 1} 𝒰.I₀
this : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.sigma (P := P).X 𝒰.sigma (P := P).f) ↔
    Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
have this₁ : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
Tactic: have : PreservesLimitsOfShape (Discrete 𝒰.I₀) F :=
    preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology hF
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
P : MorphismProperty Scheme
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst_1 : Finite.{u + 1} 𝒰.I₀
this_1 : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
this : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
c : Cofan 𝒰.X := Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.sigma (P := P).X 𝒰.sigma (P := P).f) ↔
    Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
have rw : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.sigma (P := P).X 𝒰.sigma (P := P).f) ↔
  Presieve.IsSheafFor F
    (Presieve.singleton (Y := (Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)).pt)
      (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f))
Tactic: rw [← Presieve.isSheafFor_sigmaDesc_iff 𝒰.f (coproductIsCoproduct _)
    (FinitaryExtensive.isVanKampen_finiteCoproducts (coproductIsCoproduct _)).isUniversal]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
P : MorphismProperty Scheme
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst_1 : Finite.{u + 1} 𝒰.I₀
this_1 : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
this : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
c : Cofan 𝒰.X := Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.sigma (P := P).X 𝒰.sigma (P := P).f) ↔
    Presieve.IsSheafFor F
      (Presieve.singleton (Y := (Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)).pt)
        (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f))
have a : Presieve.ofArrows 𝒰.sigma (P := P).X 𝒰.sigma (P := P).f =
  Presieve.singleton (Y := (Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)).pt) (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f)
Tactic: congr!
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
P : MorphismProperty Scheme
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst_1 : Finite.{u + 1} 𝒰.I₀
this_1 : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
this : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
c : Cofan 𝒰.X := Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)
⊢ Presieve.ofArrows 𝒰.sigma (P := P).X 𝒰.sigma (P := P).f =
    Presieve.singleton (Y := (Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)).pt) (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f)
have a : Presieve.singleton (Y := ∐ 𝒰.X) (Sigma.desc 𝒰.f) =
  Presieve.singleton (Y := (Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)).pt) (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f)
Tactic: rw [← PreZeroHypercover.presieve₀, 𝒰.presieve₀_sigma]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
⊢ Presheaf.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)
have rw : Presheaf.IsSheaf Scheme.zariskiTopology
  (Scheme.forgetToTop.op ⋙ TopCat.uliftFunctor.op ⋙ Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))
Tactic: rw [Presheaf.isSheaf_of_iso_iff (continuousMapPresheafIsoUlift T)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
⊢ Presheaf.IsSheaf Scheme.zariskiTopology
    (Scheme.forgetToTop.op ⋙ TopCat.uliftFunctor.op ⋙ Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))
have h : Presheaf.IsSheaf TopCat.grothendieckTopology
  (TopCat.uliftFunctor.op ⋙ Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))
Tactic: apply Scheme.forgetToTop.op_comp_isSheaf_of_isSheaf _ TopCat.grothendieckTopology
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
⊢ Presheaf.IsSheaf TopCat.grothendieckTopology
    (TopCat.uliftFunctor.op ⋙ Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))
have h : Presheaf.IsSheaf TopCat.grothendieckTopology (Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))
Tactic: apply TopCat.uliftFunctor.op_comp_isSheaf_of_isSheaf _ TopCat.grothendieckTopology
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
⊢ Presheaf.IsSheaf TopCat.grothendieckTopology (Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))
have h : Presieve.IsSheaf TopCat.grothendieckTopology (Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))
Tactic: rw [isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
⊢ Presheaf.IsSheaf Scheme.fpqcTopology (continuousMapPresheaf T)
have rw : Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T) ∧
  ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S),
    Flat (Spec.map f) →
      Surjective (Spec.map f) → Presieve.IsSheafFor (continuousMapPresheaf T) (Presieve.singleton (Spec.map f))
Tactic: rw [isSheaf_iff_isSheaf_of_type, Scheme.fpqcTopology_eq_propQCTopology,
    isSheaf_type_propQCTopology_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
⊢ Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T) ∧
    ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S),
      Flat (Spec.map f) →
        Surjective (Spec.map f) → Presieve.IsSheafFor (continuousMapPresheaf T) (Presieve.singleton (Spec.map f))
have refine_1 : Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)
Tactic: refine ⟨?_, fun {R S} f hf₁ hf₂ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
refine_1 : Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)
⊢ Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T) ∧
    ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S),
      Flat (Spec.map f) →
        Surjective (Spec.map f) → Presieve.IsSheafFor (continuousMapPresheaf T) (Presieve.singleton (Spec.map f))
have refine_2 : ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S) (hf₁ : Flat (Spec.map f)) (hf₂ : Surjective (Spec.map f)),
  Presieve.IsSheafFor (continuousMapPresheaf T) (Presieve.singleton (Spec.map f))
Tactic: refine ⟨?_, fun {R S} f hf₁ hf₂ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
⊢ Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)
have refine_1 : Presheaf.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)
Tactic: rw [← isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
⊢ Presieve.IsSheafFor (continuousMapPresheaf T) (Presieve.singleton (Spec.map f))
have refine_2 : ∀ (x : (continuousMapPresheaf T).obj (Opposite.op (Spec S))),
  (∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
      p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
        Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
                (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                  (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
              x :
            (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
                (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                  (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
              x :
            (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))) →
    ∃! y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R))),
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
            (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
              (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
          y =
        x
Tactic: rw [Presieve.isSheafFor_singleton]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (hypothesis)
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
⊢ ∀ (x : (continuousMapPresheaf T).obj (Opposite.op (Spec S))),
    (∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
        p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
          Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
                  (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                    (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
                x :
              (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
                  (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                    (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
                x :
              (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))) →
      ∃! y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R))),
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
            y =
          x
have this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
Tactic: have : Topology.IsQuotientMap (Spec.map f) := Flat.isQuotientMap_of_surjective _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
x : ContinuousMap.{u_1, v} (↥(Spec S)) T
h :
  ∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
⊢ ∃! y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
          (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
            (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
        y =
      x
have refine_2 : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
x : ContinuousMap.{u_1, v} (↥(Spec S)) T
h :
  ∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
refine_2 : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))
⊢ ∃! y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
          (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
            (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
        y =
      x
have refine_2₁ : (fun (y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
          (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
            (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
        y =
      x)
  (this.lift x sorry)
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
x : ContinuousMap.{u_1, v} (↥(Spec S)) T
h :
  ∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
refine_2 : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))
refine_2₁ :
  (fun (y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
            (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
              (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
          y =
        x)
    (this.lift x ⋯)
⊢ ∃! y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
          (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
            (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
        y =
      x
have refine_2₂ : ∀ (y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))),
  (fun (y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
            y =
          x)
      y →
    y = this.lift x sorry
Tactic: refine ⟨?_, ?_, ?_⟩