awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this_3 : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this_4 :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
    (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
this :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S := (↑((pullback i₂ f).presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
⊢ Eq (α := CommRingCat.of R ⟶ CommRingCat.of K)
    (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of R)) ≫
      Scheme.Hom.app (lft ≫ pullback.fst i₂ f) ⊤ ≫ Iso.hom (Scheme.ΓSpecIso (CommRingCat.of K)))
    (CommRingCat.ofHom (algebraMap R K))
have rw : Eq (α := CommRingCat.of R ⟶ CommRingCat.of K)
  (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of R)) ≫
    CategoryStruct.comp (Y := Γ(Spec (CommRingCat.of K), Spec.map (CommRingCat.ofHom (algebraMap R K)) ⁻¹ᵁ ⊤))
      (Scheme.Hom.app (Spec.map (CommRingCat.ofHom (algebraMap R K))) ⊤) (Iso.hom (Scheme.ΓSpecIso (CommRingCat.of K))))
  (CommRingCat.ofHom (algebraMap R K))
Tactic: rw [pullback.lift_fst]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this_3 : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this_4 :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
    (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
this :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S := (↑((pullback i₂ f).presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
⊢ ⋯.HasLift
have hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
Tactic: have hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K) := by
    simp only [CommRingCat.coe_of, Iso.trans_hom, Iso.symm_hom, TopCat.Presheaf.stalkCongr_hom,
      Category.assoc, α, e, β, stalkClosedPointIso_inv, StructureSheaf.toStalk]
    change (Scheme.ΓSpecIso (.of R)).inv ≫ (Spec <| .of R).presheaf.germ _ _ _ ≫ _ = _
    simp only [TopCat.Presheaf.germ_stalkSpecializes_assoc, Scheme.Hom.germ_stalkMap_assoc]
    -- `map_top` introduces defeq problems, according to `check_compositions`.
    -- This is probably the cause of the `erw` needed below.
    simp only [TopologicalSpace.Opens.map_top]
    rw [Scheme.germ_stalkClosedPointTo lft ⊤ trivial]
    erw [← Scheme.Hom.comp_app_assoc lft (pullback.fst i₂ f)]
    rw [pullback.lift_fst]
    simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this_3 : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this_4 :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
    (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
this :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S := (↑((pullback i₂ f).presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
⊢ ⋯.HasLift
have hbij : Function.Bijective (α := R) (β := ↥(CommRingCat.Hom.hom β).range)
  (⇑(RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) :
    (a : R) → ↥(CommRingCat.Hom.hom β).range)
Tactic: have hbij := (bijective_rangeRestrict_comp_of_valuationRing (R := R) (K := K) α.hom β.hom
    (CommRingCat.hom_ext_iff.mp hαβ))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this_3 : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this_4 :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
    (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
this :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S := (↑((pullback i₂ f).presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
hbij :
  Function.Bijective (α := R) (β := ↥(CommRingCat.Hom.hom β).range)
    (⇑(RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) :
      (a : R) → ↥(CommRingCat.Hom.hom β).range)
φ : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of R :=
  CommRingCat.ofHom
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm
          (RingEquiv.ofBijective (RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) hbij)))
      (CommRingCat.Hom.hom β).rangeRestrict)
⊢ α ≫ φ = 𝟙 (CommRingCat.of R)
have hf : ∀ (x_1 : (↑(CommRingCat.of R) : Type u)),
  Eq (α := (↑(CommRingCat.of R) : Type u))
    ((CommRingCat.Hom.hom (α ≫ φ) : (a : (↑(CommRingCat.of R) : Type u)) → (↑(CommRingCat.of R) : Type u)) x_1 :
      (↑(CommRingCat.of R) : Type u))
    ((CommRingCat.Hom.hom (𝟙 (CommRingCat.of R)) :
          (a : (↑(CommRingCat.of R) : Type u)) → (↑(CommRingCat.of R) : Type u))
        x_1 :
      (↑(CommRingCat.of R) : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this_3 : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this_4 :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
    (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
this :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S := (↑((pullback i₂ f).presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
hbij :
  Function.Bijective (α := R) (β := ↥(CommRingCat.Hom.hom β).range)
    (⇑(RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) :
      (a : R) → ↥(CommRingCat.Hom.hom β).range)
φ : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of R :=
  CommRingCat.ofHom
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm
          (RingEquiv.ofBijective (RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) hbij)))
      (CommRingCat.Hom.hom β).rangeRestrict)
⊢ ⋯.HasLift
have hαφ : α ≫ φ = 𝟙 (CommRingCat.of R)
Tactic: have hαφ : α ≫ φ = 𝟙 _ := by ext x; exact (RingEquiv.ofBijective _ hbij).symm_apply_apply x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this_3 : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this_4 :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
    (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
this :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S := (↑((pullback i₂ f).presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
hbij :
  Function.Bijective (α := R) (β := ↥(CommRingCat.Hom.hom β).range)
    (⇑(RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) :
      (a : R) → ↥(CommRingCat.Hom.hom β).range)
φ : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of R :=
  CommRingCat.ofHom
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm
          (RingEquiv.ofBijective (RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) hbij)))
      (CommRingCat.Hom.hom β).rangeRestrict)
hαφ : α ≫ φ = 𝟙 (CommRingCat.of R)
⊢ Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.inv
have rw : e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.hom ≫ e.inv
Tactic: rw [← cancel_epi e.hom, ← Category.assoc, hαφ, e.hom_inv_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this_3 : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this_4 :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
    (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
this :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S := (↑((pullback i₂ f).presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
hbij :
  Function.Bijective (α := R) (β := ↥(CommRingCat.Hom.hom β).range)
    (⇑(RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) :
      (a : R) → ↥(CommRingCat.Hom.hom β).range)
φ : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of R :=
  CommRingCat.ofHom
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm
          (RingEquiv.ofBijective (RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) hbij)))
      (CommRingCat.Hom.hom β).rangeRestrict)
hαφ : α ≫ φ = 𝟙 (CommRingCat.of R)
rw : e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.hom ≫ e.inv
⊢ Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.inv
have rw₁ : (e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x) ≫ φ = e.hom ≫ e.inv
Tactic: rw [← cancel_epi e.hom, ← Category.assoc, hαφ, e.hom_inv_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this_3 : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this_4 :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
    (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
this :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S := (↑((pullback i₂ f).presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
hbij :
  Function.Bijective (α := R) (β := ↥(CommRingCat.Hom.hom β).range)
    (⇑(RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) :
      (a : R) → ↥(CommRingCat.Hom.hom β).range)
φ : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of R :=
  CommRingCat.ofHom
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm
          (RingEquiv.ofBijective (RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) hbij)))
      (CommRingCat.Hom.hom β).rangeRestrict)
hαφ : α ≫ φ = 𝟙 (CommRingCat.of R)
rw : e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.hom ≫ e.inv
rw₁ : (e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x) ≫ φ = e.hom ≫ e.inv
⊢ Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.inv
have rw₂ : 𝟙 (CommRingCat.of R) = e.hom ≫ e.inv
Tactic: rw [← cancel_epi e.hom, ← Category.assoc, hαφ, e.hom_inv_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this_3 : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this_4 :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
    (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
this :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S := (↑((pullback i₂ f).presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
hbij :
  Function.Bijective (α := R) (β := ↥(CommRingCat.Hom.hom β).range)
    (⇑(RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) :
      (a : R) → ↥(CommRingCat.Hom.hom β).range)
φ : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of R :=
  CommRingCat.ofHom
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm
          (RingEquiv.ofBijective (RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) hbij)))
      (CommRingCat.Hom.hom β).rangeRestrict)
hαφ : α ≫ φ = 𝟙 (CommRingCat.of R)
rw : e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.hom ≫ e.inv
rw₁ : (e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x) ≫ φ = e.hom ≫ e.inv
rw₂ : 𝟙 (CommRingCat.of R) = e.hom ≫ e.inv
⊢ Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.inv
have rw₃ : 𝟙 (CommRingCat.of R) = 𝟙 (CommRingCat.of R)
Tactic: rw [← cancel_epi e.hom, ← Category.assoc, hαφ, e.hom_inv_id]