awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h_1 : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f]
    (h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) (h : ∃ (S : CommRingCat.{u}), X = Spec S),
    Smooth f
h : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ Smooth f
have inr : ∀ (i : X.affineCover.I₀), Smooth (X.affineCover.f i ≫ f)
Tactic: rw [IsZariskiLocalAtSource.iff_of_openCover (P := @Smooth) X.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (hypothesis)
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h_1 : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f]
    (h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) (h : ∃ (S : CommRingCat.{u}), X = Spec S),
    Smooth f
h : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
⊢ Smooth (X.affineCover.f i ≫ f)
have x : ∀ (y : ↥(Spec R)),
  Smooth (X := pullback f ((Spec R).fromSpecResidueField y)) (pullback.snd f ((Spec R).fromSpecResidueField y))
Tactic: have _ (y) : Smooth (pullback.snd f ((Spec R).fromSpecResidueField y)) :=
      inferInstanceAs <| Smooth (f.fiberToSpecResidueField y)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h_1 : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f]
    (h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) (h : ∃ (S : CommRingCat.{u}), X = Spec S),
    Smooth f
h : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
h_2 :
  ∀ (y : ↥(Spec R)),
    Smooth (X := pullback f ((Spec R).fromSpecResidueField y)) (pullback.snd f ((Spec R).fromSpecResidueField y))
⊢ Smooth (X.affineCover.f i ≫ f)
have inr : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (X.affineCover.f i ≫ f) y)
Tactic: refine this _ (fun y ↦ ?_) ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h_1 : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f]
    (h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) (h : ∃ (S : CommRingCat.{u}), X = Spec S),
    Smooth f
h : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
h_2 :
  ∀ (y : ↥(Spec R)),
    Smooth (X := pullback f ((Spec R).fromSpecResidueField y)) (pullback.snd f ((Spec R).fromSpecResidueField y))
y : ↥(Spec R)
⊢ Smooth (Scheme.Hom.fiberToSpecResidueField (X.affineCover.f i ≫ f) y)
have inr : Smooth (X := Scheme.Hom.fiber (X.affineCover.f i ≫ f) y)
  (CategoryStruct.comp (Y :=
      pullback (Y := pullback f ((Spec R).fromSpecResidueField y)) (X.affineCover.f i)
        (pullback.fst f ((Spec R).fromSpecResidueField y)))
      (Iso.inv (pullbackRightPullbackFstIso f ((Spec R).fromSpecResidueField y) (X.affineCover.f i)))
      (pullback.snd (X.affineCover.f i) (pullback.fst f ((Spec R).fromSpecResidueField y)) ≫
        pullback.snd f ((Spec R).fromSpecResidueField y)) :
    pullback (X.affineCover.f i ≫ f) ((Spec R).fromSpecResidueField y) ⟶ Spec ((Spec R).residueField y))
Tactic: rw [Scheme.Hom.fiberToSpecResidueField, ← pullbackRightPullbackFstIso_inv_snd_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
R : CommRingCat
X : Scheme
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h_1 : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
h : ∃ (S : CommRingCat.{u}), X = Spec S
⊢ Smooth f
have obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f]
  (h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)), Smooth f
Tactic: obtain ⟨S, rfl⟩ := h
Cleared hypotheses: X, f, inst, inst_1, h_1, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
Goal:
X Y : Scheme
f_1 : X ⟶ Y
R S : CommRingCat
f : Spec S ⟶ Spec R
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
⊢ Smooth f
have obtain : ∀ (φ : R ⟶ S) [LocallyOfFinitePresentation (Spec.map φ)] [Flat (Spec.map φ)]
  (h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)), Smooth (Spec.map φ)
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst, inst_1, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst : LocallyOfFinitePresentation (Spec.map φ)
inst_1 : Flat (Spec.map φ)
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
⊢ Smooth (Spec.map φ)
have simp : (CommRingCat.Hom.hom φ).FinitePresentation → (CommRingCat.Hom.hom φ).Flat → (CommRingCat.Hom.hom φ).Smooth
Tactic: simp only [HasRingHomProperty.Spec_iff] at *
Cleared hypotheses: inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
⊢ (CommRingCat.Hom.hom φ).Smooth
have algebraizeInst : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
⊢ (CommRingCat.Hom.hom φ).Smooth
have algebraizeInst₁ : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
⊢ (CommRingCat.Hom.hom φ).Smooth
have refine : ∀ (p : Ideal (↑R : Type u)) (hp : p.IsPrime), Algebra.FormallySmooth.{u, u} p.ResidueField (p.Fiber (↑S : Type u))
Tactic: refine Algebra.Smooth.of_formallySmooth_fiber fun p hp ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
p : Ideal (↑R : Type u)
hp : p.IsPrime
⊢ Algebra.FormallySmooth.{u, u} p.ResidueField (p.Fiber (↑S : Type u))
have rw : RingHom.FormallySmooth.{u, u} (R := p.ResidueField) (S := p.Fiber (↑S : Type u))
  (algebraMap p.ResidueField (p.Fiber (↑S : Type u)))
Tactic: rw [← RingHom.formallySmooth_algebraMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
p : Ideal (↑R : Type u)
hp : p.IsPrime
⊢ RingHom.FormallySmooth.{u, u} (R := p.ResidueField) (S := p.Fiber (↑S : Type u))
    (algebraMap p.ResidueField (p.Fiber (↑S : Type u)))
have refine : RingHom.Smooth.{u, u} (R := p.ResidueField) (S := p.Fiber (↑S : Type u))
  (algebraMap p.ResidueField (p.Fiber (↑S : Type u)))
Tactic: refine RingHom.Smooth.formallySmooth ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
p : Ideal (↑R : Type u)
hp : p.IsPrime
⊢ RingHom.Smooth.{u, u} (R := p.ResidueField) (S := p.Fiber (↑S : Type u))
    (algebraMap p.ResidueField (p.Fiber (↑S : Type u)))
have rw : Smooth (X :=
  Scheme.Hom.fiber (X := Spec (CommRingCat.of (↑S : Type u)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
    { asIdeal := p, isPrime := hp : PrimeSpectrum (↑R : Type u) })
  (Scheme.Hom.fiberToSpecResidueField (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
    { asIdeal := p, isPrime := hp })
Tactic: rw [← CommRingCat.hom_ofHom (algebraMap p.ResidueField (p.Fiber ↑S)),
    ← HasRingHomProperty.Spec_iff (P := @Smooth), ← MorphismProperty.arrow_mk_iso_iff (P := @Smooth)
    (Spec.fiberToSpecResidueFieldIso R S ⟨p, hp⟩)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (goal)
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : SurjectiveOnStalks f
hg : SurjectiveOnStalks g
⊢ SurjectiveOnStalks (f ≫ g)
have refine : ∀ (x : ↥X),
  Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap (f ≫ g) x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
Tactic: refine ⟨fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (goal)
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : SurjectiveOnStalks f
hg : SurjectiveOnStalks g
x : ↥X
⊢ Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap (f ≫ g) x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
have rw : Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        CommRingCat.carrier) (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)) :
    (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
Tactic: rw [Scheme.Hom.stalkMap_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (goal)
Goal:
⊢ @SurjectiveOnStalks =
    stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
      Function.Surjective (α := R) (β := S) (⇑x : (a : R) → S)
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1),
  SurjectiveOnStalks x_2 ↔
    stalkwise
      (fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
        Function.Surjective (α := R) (β := S) (⇑x : (a : R) → S))
      x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
⊢ SurjectiveOnStalks (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).SurjectiveOnStalks
have rw : stalkwise
    (fun {R S : Type u} [CommRing R] [CommRing S] (x : R →+* S) ↦
      Function.Surjective (α := R) (β := S) (⇑x : (a : R) → S))
    (Spec.map φ) ↔
  (CommRingCat.Hom.hom φ).SurjectiveOnStalks
Tactic: rw [eq_stalkwise, stalkwise_SpecMap_iff RingHom.surjective_respectsIso,
    RingHom.SurjectiveOnStalks]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
rw :
  stalkwise
      (fun {R S : Type u} [CommRing R] [CommRing S] (x : R →+* S) ↦
        Function.Surjective (α := R) (β := S) (⇑x : (a : R) → S))
      (Spec.map φ) ↔
    (CommRingCat.Hom.hom φ).SurjectiveOnStalks
⊢ SurjectiveOnStalks (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).SurjectiveOnStalks
have rw₁ : (∀ (p : Ideal (↑S : Type u)) (x : p.IsPrime),
    Function.Surjective (α := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) (β :=
      Localization.AtPrime p)
      (⇑(Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) sorry) :
        (a : Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) → Localization.AtPrime p)) ↔
  (CommRingCat.Hom.hom φ).SurjectiveOnStalks
Tactic: rw [eq_stalkwise, stalkwise_SpecMap_iff RingHom.surjective_respectsIso,
    RingHom.SurjectiveOnStalks]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
rw :
  stalkwise
      (fun {R S : Type u} [CommRing R] [CommRing S] (x : R →+* S) ↦
        Function.Surjective (α := R) (β := S) (⇑x : (a : R) → S))
      (Spec.map φ) ↔
    (CommRingCat.Hom.hom φ).SurjectiveOnStalks
rw₁ :
  (∀ (p : Ideal (↑S : Type u)) (x : p.IsPrime),
      Function.Surjective (α := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) (β :=
        Localization.AtPrime p)
        (⇑(Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯) :
          (a : Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) → Localization.AtPrime p)) ↔
    (CommRingCat.Hom.hom φ).SurjectiveOnStalks
⊢ SurjectiveOnStalks (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).SurjectiveOnStalks
have rw₂ : (∀ (p : Ideal (↑S : Type u)) (x : p.IsPrime),
    Function.Surjective (α := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) (β :=
      Localization.AtPrime p)
      (⇑(Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) sorry) :
        (a : Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) → Localization.AtPrime p)) ↔
  ∀ (P : Ideal (↑S : Type u)) (x : P.IsPrime),
    Function.Surjective (α := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) P)) (β :=
      Localization.AtPrime P)
      (⇑(Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) sorry) :
        (a : Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) P)) → Localization.AtPrime P)
Tactic: rw [eq_stalkwise, stalkwise_SpecMap_iff RingHom.surjective_respectsIso,
    RingHom.SurjectiveOnStalks]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine X
inst_1 : IsAffine Y
⊢ SurjectiveOnStalks f ↔
    RingHom.SurjectiveOnStalks (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤))
have rw : SurjectiveOnStalks f ↔ SurjectiveOnStalks (X := Spec Γ(X, f ⁻¹ᵁ ⊤)) (Spec.map (Scheme.Hom.app f ⊤))
Tactic: rw [← Spec_iff, MorphismProperty.arrow_mk_iso_iff @SurjectiveOnStalks (arrowIsoSpecΓOfIsAffine f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine X
inst_1 : IsAffine Y
rw : SurjectiveOnStalks f ↔ SurjectiveOnStalks (X := Spec Γ(X, f ⁻¹ᵁ ⊤)) (Spec.map (Scheme.Hom.app f ⊤))
⊢ SurjectiveOnStalks f ↔
    RingHom.SurjectiveOnStalks (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤))
have rw₁ : SurjectiveOnStalks (Spec.map (Scheme.Hom.appTop f)) ↔
  SurjectiveOnStalks (X := Spec Γ(X, f ⁻¹ᵁ ⊤)) (Spec.map (Scheme.Hom.app f ⊤))
Tactic: rw [← Spec_iff, MorphismProperty.arrow_mk_iso_iff @SurjectiveOnStalks (arrowIsoSpecΓOfIsAffine f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : SurjectiveOnStalks (f ≫ g)
⊢ SurjectiveOnStalks f
have refine : ∀ (x : ↥X),
  Function.Surjective (α := (↑(Y.presheaf.stalk (f x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap f x)) :
      (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
Tactic: refine ⟨fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : SurjectiveOnStalks (f ≫ g)
x : ↥X
⊢ Function.Surjective (α := (↑(Y.presheaf.stalk (f x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap f x)) :
      (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
have this : Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (Scheme.Hom.stalkMap (f ≫ g) x)) :
    (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
Tactic: have := (f ≫ g).stalkMap_surjective x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : SurjectiveOnStalks (f ≫ g)
x : ↥X
this :
  Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap (f ≫ g) x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
⊢ Function.Surjective (α := (↑(Y.presheaf.stalk (f x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap f x)) :
      (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
have this₁ : Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)) :
    (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
Tactic: rw [Scheme.Hom.stalkMap_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderBaseChange @SurjectiveOnStalks
have hP : RingHom.IsStableUnderBaseChange.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.SurjectiveOnStalks
Tactic: apply HasRingHomProperty.isStableUnderBaseChange
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ RingHom.IsStableUnderBaseChange.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.SurjectiveOnStalks
have hP : RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.SurjectiveOnStalks
Tactic: apply RingHom.IsStableUnderBaseChange.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hP : RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.SurjectiveOnStalks
⊢ RingHom.IsStableUnderBaseChange.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.SurjectiveOnStalks
have hP₁ : ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  RingHom.SurjectiveOnStalks (algebraMap R T) →
    RingHom.SurjectiveOnStalks (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
Tactic: apply RingHom.IsStableUnderBaseChange.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : SurjectiveOnStalks f
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
⊢ Mono f
have refine : Mono ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f)
Tactic: refine (Scheme.forgetToLocallyRingedSpace ⋙
    LocallyRingedSpace.forgetToSheafedSpace).mono_of_mono_map ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : SurjectiveOnStalks f
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
⊢ Mono ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f)
have h₁ : Function.Injective (α :=
  (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj X).toPresheafedSpace :
        TopCat) :
    Type u))
  (β :=
  (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj Y).toPresheafedSpace :
        TopCat) :
    Type u))
  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
        ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f).hom.base) :
    (a :
        (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj X).toPresheafedSpace :
              TopCat) :
          Type u)) →
      (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj Y).toPresheafedSpace :
            TopCat) :
        Type u))
Tactic: apply SheafedSpace.mono_of_base_injective_of_stalk_epi