awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
this :
  ∀ {X : Scheme.{u_1}} (x : ↥X) (h : ∃ (R : CommRingCat.{u_1}), X = Spec R),
    ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
h : ¬∃ (R : CommRingCat.{u_1}), X = Spec R
R : CommRingCat
f : Spec R ⟶ X
hf : IsOpenImmersion f
y : ↥(Spec R)
hsub :
  Membership.mem (α := ↥X) (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) (f y : ↥X) ∧
    Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑⊤ : Set ↥X)
⊢ ringKrullDim.{u_1} (↑(X.presheaf.stalk (f y)) : Type u_1) = (↑(coheight (α := ↥X) (f y : ↥X)) : WithBot ℕ∞)
have inr : ringKrullDim.{u_1} (↑(X.presheaf.stalk (f y)) : Type u_1) = ringKrullDim.{u_1} (↑((Spec R).presheaf.stalk y) : Type u_1)
Tactic: rw [coheight_eq_of_isOpenImmersion, ← this _ ⟨R, rfl⟩]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
x : ↥X
h : ∃ (R : CommRingCat.{u_1}), X = Spec R
⊢ ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
have obtain : ∀ (R : CommRingCat.{u_1}) (x : ↥(Spec R)),
  ringKrullDim.{u_1} (↑((Spec R).presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
Tactic: obtain ⟨R, rfl⟩ := h
Cleared hypotheses: X, x, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
R : CommRingCat
x : ↥(Spec R)
k : Algebra (↑R : Type u_1) (↑((Spec R).presheaf.stalk x) : Type u_1) := StructureSheaf.stalkAlgebra (↑R : Type u_1) x
⊢ ringKrullDim.{u_1} (↑((Spec R).presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
have this : IsLocalization.AtPrime (↑((Spec R).presheaf.stalk x) : Type u_1) x.asIdeal
Tactic: have : IsLocalization.AtPrime (↑((Spec R).presheaf.stalk x)) x.asIdeal :=
    StructureSheaf.IsLocalization.to_stalk R x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
R : CommRingCat
x : ↥(Spec R)
k : Algebra (↑R : Type u_1) (↑((Spec R).presheaf.stalk x) : Type u_1) := StructureSheaf.stalkAlgebra (↑R : Type u_1) x
this : IsLocalization.AtPrime (↑((Spec R).presheaf.stalk x) : Type u_1) x.asIdeal
⊢ ringKrullDim.{u_1} (↑((Spec R).presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
have rw : (↑x.asIdeal.height : WithBot ℕ∞) = (↑(coheight x) : WithBot ℕ∞)
Tactic: rw [IsLocalization.AtPrime.ringKrullDim_eq_height x.asIdeal ((Spec R).presheaf.stalk x)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
R : CommRingCat
x : ↥(Spec R)
k : Algebra (↑R : Type u_1) (↑((Spec R).presheaf.stalk x) : Type u_1) := StructureSheaf.stalkAlgebra (↑R : Type u_1) x
this : IsLocalization.AtPrime (↑((Spec R).presheaf.stalk x) : Type u_1) x.asIdeal
⊢ (↑x.asIdeal.height : WithBot ℕ∞) = (↑(coheight x) : WithBot ℕ∞)
have apply : x.asIdeal.height = coheight x
Tactic: apply WithBot.coe_eq_coe.mpr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
inst_1 : Subsingleton.{u + 1} ↥X
⊢ IsField.{u} (↑Γ(X, ⊤) : Type u)
have rw : T1Space.{u} (PrimeSpectrum (↑Γ(X, ⊤) : Type u))
Tactic: rw [← PrimeSpectrum.t1Space_iff_isField]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t₁ t₂ : Triplet f g
ex : t₁.x = t₂.x
ey : t₁.y = t₂.y
⊢ t₁ = t₂
have mk : ∀ (x : ↥X) (y : ↥Y) (s : ↥S) (hx : f x = s) (hy : g y = s)
  (ex : { x := x, y := y, s := s, hx := hx, hy := hy : Triplet f g }.x = t₂.x)
  (ey : { x := x, y := y, s := s, hx := hx, hy := hy : Triplet f g }.y = t₂.y),
  { x := x, y := y, s := s, hx := hx, hy := hy : Triplet f g } = t₂
Tactic: cases t₁
Cleared hypotheses: t₁, ex, ey
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t₂ : Triplet f g
x : ↥X
y : ↥Y
s : ↥S
hx : f x = s
hy : g y = s
ex : { x := x, y := y, s := s, hx := hx, hy := hy : Triplet f g }.x = t₂.x
ey : { x := x, y := y, s := s, hx := hx, hy := hy : Triplet f g }.y = t₂.y
⊢ { x := x, y := y, s := s, hx := hx, hy := hy : Triplet f g } = t₂
have mk : ∀ (x_1 : ↥X) (y_1 : ↥Y) (s_1 : ↥S) (hx_1 : f x_1 = s_1) (hy_1 : g y_1 = s_1)
  (ex :
    { x := x, y := y, s := s, hx := hx, hy := hy : Triplet f g }.x =
      { x := x_1, y := y_1, s := s_1, hx := hx_1, hy := hy_1 : Triplet f g }.x)
  (ey :
    { x := x, y := y, s := s, hx := hx, hy := hy : Triplet f g }.y =
      { x := x_1, y := y_1, s := s_1, hx := hx_1, hy := hy_1 : Triplet f g }.y),
  { x := x, y := y, s := s, hx := hx, hy := hy : Triplet f g } =
    { x := x_1, y := y_1, s := s_1, hx := hx_1, hy := hy_1 }
Tactic: cases t₂
Cleared hypotheses: t₂, ex, ey
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
y : ↥Y
s : ↥S
hx : f x = s
hy : g y = s
x_1 : ↥X
y_1 : ↥Y
s_1 : ↥S
hx_1 : f x_1 = s_1
hy_1 : g y_1 = s_1
ex :
  { x := x, y := y, s := s, hx := hx, hy := hy : Triplet f g }.x =
    { x := x_1, y := y_1, s := s_1, hx := hx_1, hy := hy_1 : Triplet f g }.x
ey :
  { x := x, y := y, s := s, hx := hx, hy := hy : Triplet f g }.y =
    { x := x_1, y := y_1, s := s_1, hx := hx_1, hy := hy_1 : Triplet f g }.y
⊢ { x := x, y := y, s := s, hx := hx, hy := hy : Triplet f g } =
    { x := x_1, y := y_1, s := s_1, hx := hx_1, hy := hy_1 }
have mk : x = x_1 ∧ y = y_1 ∧ s = s_1
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : Triplet f g
e : T₁ = T₂
⊢ T₁.tensor = T₂.tensor
have subst : T₁.tensor = T₁.tensor
Tactic: subst e
Cleared hypotheses: T₂, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x y z : Triplet f g
e : x = y
e' : y = z
⊢ tensorCongr e ≪≫ tensorCongr e' = tensorCongr ⋯
have subst : tensorCongr sorry ≪≫ tensorCongr sorry = tensorCongr sorry
Tactic: subst e e'
Cleared hypotheses: y, z, e, e'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x y z : Triplet f g
e : x = y
e' : y = z
⊢ (tensorCongr e).hom ≫ (tensorCongr e').hom = (tensorCongr ⋯).hom
have subst : (tensorCongr sorry).hom ≫ (tensorCongr sorry).hom = (tensorCongr sorry).hom
Tactic: subst e e'
Cleared hypotheses: y, z, e, e'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x) ≫ f = (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ≫ g
have simp : Eq (α := Spec T.tensor ⟶ S)
  (Spec.map
      (pushout.inl ((residueFieldCongr sorry).hom ≫ Hom.residueFieldMap f T.x)
        ((residueFieldCongr sorry).hom ≫ Hom.residueFieldMap g T.y)) ≫
    Spec.map (Hom.residueFieldMap f T.x) ≫ S.fromSpecResidueField (f T.x))
  (Spec.map
      (pushout.inr ((residueFieldCongr sorry).hom ≫ Hom.residueFieldMap f T.x)
        ((residueFieldCongr sorry).hom ≫ Hom.residueFieldMap g T.y)) ≫
    Spec.map (Hom.residueFieldMap g T.y) ≫ S.fromSpecResidueField (g T.y))
Tactic: simp only [residueFieldCongr_inv, Category.assoc, tensorInl, tensorInr,
    ← Hom.SpecMap_residueFieldMap_fromSpecResidueField]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ Eq (α := Spec T.tensor ⟶ S)
    (Spec.map
        (pushout.inl ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap f T.x) ≫ S.fromSpecResidueField (f T.x))
    (Spec.map
        (pushout.inr ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap g T.y) ≫ S.fromSpecResidueField (g T.y))
have rw : Eq (α := Spec T.tensor ⟶ S)
  (Spec.map
      (pushout.inl ((residueFieldCongr sorry).hom ≫ Hom.residueFieldMap f T.x)
        ((residueFieldCongr sorry).hom ≫ Hom.residueFieldMap g T.y)) ≫
    Spec.map (Hom.residueFieldMap f T.x) ≫ Spec.map (residueFieldCongr sorry).hom ≫ S.fromSpecResidueField T.s)
  (Spec.map
      (pushout.inr ((residueFieldCongr sorry).hom ≫ Hom.residueFieldMap f T.x)
        ((residueFieldCongr sorry).hom ≫ Hom.residueFieldMap g T.y)) ≫
    Spec.map (Hom.residueFieldMap g T.y) ≫ Spec.map (residueFieldCongr sorry).hom ≫ S.fromSpecResidueField T.s)
Tactic: rw [← residueFieldCongr_fromSpecResidueField T.hx.symm,
    ← residueFieldCongr_fromSpecResidueField T.hy.symm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ ofPoint (T.SpecTensorTo p) = T
have ex : x (Y := Y) (S := S) (f := f) (g := g) (ofPoint (T.SpecTensorTo p)) = T.x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
ex : x (Y := Y) (S := S) (f := f) (g := g) (ofPoint (T.SpecTensorTo p)) = T.x
⊢ ofPoint (T.SpecTensorTo p) = T
have ey : y (X := X) (S := S) (f := f) (g := g) (ofPoint (T.SpecTensorTo p)) = T.y
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo = (pullback f g).fromSpecResidueField t
have h₀ : (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.fst f g =
  (pullback f g).fromSpecResidueField t ≫ pullback.fst f g
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
h₀ :
  (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.fst f g =
    (pullback f g).fromSpecResidueField t ≫ pullback.fst f g
⊢ Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo = (pullback f g).fromSpecResidueField t
have h₁ : (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.snd f g =
  (pullback f g).fromSpecResidueField t ≫ pullback.snd f g
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.fst f g =
    (pullback f g).fromSpecResidueField t ≫ pullback.fst f g
have h₀ : (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.fst f g =
  CategoryStruct.comp (Y := Spec (X.residueField ((pullback.fst f g) t)))
    (Spec.map (Hom.residueFieldMap (pullback.fst f g) t)) (X.fromSpecResidueField ((pullback.fst f g) t))
Tactic: rw [← Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.fst f g =
    CategoryStruct.comp (Y := Spec (X.residueField ((pullback.fst f g) t)))
      (Spec.map (Hom.residueFieldMap (pullback.fst f g) t)) (X.fromSpecResidueField ((pullback.fst f g) t))
have h₀ : Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInl ≫ X.fromSpecResidueField ((pullback.fst f g) t) =
  CategoryStruct.comp (Y := Spec (X.residueField ((pullback.fst f g) t)))
    (Spec.map (Hom.residueFieldMap (pullback.fst f g) t)) (X.fromSpecResidueField ((pullback.fst f g) t))
Tactic: simp only [Category.assoc, Triplet.specTensorTo_fst, Triplet.ofPoint_x]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInl ≫ X.fromSpecResidueField ((pullback.fst f g) t) =
    CategoryStruct.comp (Y := Spec (X.residueField ((pullback.fst f g) t)))
      (Spec.map (Hom.residueFieldMap (pullback.fst f g) t)) (X.fromSpecResidueField ((pullback.fst f g) t))
have h₀ : Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInl ≫ X.fromSpecResidueField ((pullback.fst f g) t) =
  CategoryStruct.comp (Y :=
      Spec
        (pushout ((residueFieldCongr sorry).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x)
          ((residueFieldCongr sorry).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y)))
      (Spec.map (pushout.desc (Hom.residueFieldMap (pullback.fst f g) t) (Hom.residueFieldMap (pullback.snd f g) t) sorry))
      (Spec.map
        (pushout.inl ((residueFieldCongr sorry).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x)
          ((residueFieldCongr sorry).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y))) ≫
    X.fromSpecResidueField ((pullback.fst f g) t)
Tactic: rw [← pushout.inl_desc _ _ (residueFieldCongr_inv_residueFieldMap_ofPoint t), Spec.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.snd f g =
    (pullback f g).fromSpecResidueField t ≫ pullback.snd f g
have h₁ : (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.snd f g =
  CategoryStruct.comp (Y := Spec (Y.residueField ((pullback.snd f g) t)))
    (Spec.map (Hom.residueFieldMap (pullback.snd f g) t)) (Y.fromSpecResidueField ((pullback.snd f g) t))
Tactic: rw [← Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.snd f g =
    CategoryStruct.comp (Y := Spec (Y.residueField ((pullback.snd f g) t)))
      (Spec.map (Hom.residueFieldMap (pullback.snd f g) t)) (Y.fromSpecResidueField ((pullback.snd f g) t))
have h₁ : Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInr ≫ Y.fromSpecResidueField ((pullback.snd f g) t) =
  CategoryStruct.comp (Y := Spec (Y.residueField ((pullback.snd f g) t)))
    (Spec.map (Hom.residueFieldMap (pullback.snd f g) t)) (Y.fromSpecResidueField ((pullback.snd f g) t))
Tactic: simp only [Category.assoc, Triplet.specTensorTo_snd, Triplet.ofPoint_y]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInr ≫ Y.fromSpecResidueField ((pullback.snd f g) t) =
    CategoryStruct.comp (Y := Spec (Y.residueField ((pullback.snd f g) t)))
      (Spec.map (Hom.residueFieldMap (pullback.snd f g) t)) (Y.fromSpecResidueField ((pullback.snd f g) t))
have h₁ : Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInr ≫ Y.fromSpecResidueField ((pullback.snd f g) t) =
  CategoryStruct.comp (Y :=
      Spec
        (pushout ((residueFieldCongr sorry).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x)
          ((residueFieldCongr sorry).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y)))
      (Spec.map (pushout.desc (Hom.residueFieldMap (pullback.fst f g) t) (Hom.residueFieldMap (pullback.snd f g) t) sorry))
      (Spec.map
        (pushout.inr ((residueFieldCongr sorry).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x)
          ((residueFieldCongr sorry).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y))) ≫
    Y.fromSpecResidueField ((pullback.snd f g) t)
Tactic: rw [← pushout.inr_desc _ _ (residueFieldCongr_inv_residueFieldMap_ofPoint t), Spec.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T T' : Triplet f g
h : T = T'
⊢ Spec.map (Triplet.tensorCongr h).hom ≫ T.SpecTensorTo = T'.SpecTensorTo
have subst : Spec.map (Triplet.tensorCongr sorry).hom ≫ T.SpecTensorTo = T.SpecTensorTo
Tactic: subst h
Cleared hypotheses: T', h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom =
    (Spec T.tensor).fromSpecResidueField p
have h₀ : (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr sorry).hom) ≫
    Spec.map T.tensorInl =
  (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl
Tactic: apply T.isPullback_SpecMap_tensor.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
h₀ :
  (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInl =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom =
    (Spec T.tensor).fromSpecResidueField p
have h₁ : (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr sorry).hom) ≫
    Spec.map T.tensorInr =
  (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr
Tactic: apply T.isPullback_SpecMap_tensor.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInl =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl
have h₀ : ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr sorry).hom) ≫
      Spec.map T.tensorInl) ≫
    X.fromSpecResidueField T.x =
  ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl) ≫ X.fromSpecResidueField T.x
Tactic: rw [← cancel_mono <| X.fromSpecResidueField T.x]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
          Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
        Spec.map T.tensorInl) ≫
      X.fromSpecResidueField T.x =
    ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl) ≫ X.fromSpecResidueField T.x
have h₀ : Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
    Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.fst f g =
  (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.fst f g
Tactic: simp_rw [Category.assoc, ← T.specTensorTo_fst, tensorCongr_SpecTensorTo_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.fst f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.fst f g
have h₀ : Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
    Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.fst f g =
  Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
    (pullback f g).fromSpecResidueField (T.SpecTensorTo p) ≫ pullback.fst f g
Tactic: rw [← Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, ofPointTensor_SpecTensorTo_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
h₀ :
  Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.fst f g =
    Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      (pullback f g).fromSpecResidueField (T.SpecTensorTo p) ≫ pullback.fst f g
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.fst f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.fst f g
have h₁ : Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
    (pullback f g).fromSpecResidueField (T.SpecTensorTo p) ≫ pullback.fst f g =
  Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
    (pullback f g).fromSpecResidueField (T.SpecTensorTo p) ≫ pullback.fst f g
Tactic: rw [← Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, ofPointTensor_SpecTensorTo_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInr =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr
have h₁ : ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr sorry).hom) ≫
      Spec.map T.tensorInr) ≫
    Y.fromSpecResidueField T.y =
  ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr) ≫ Y.fromSpecResidueField T.y
Tactic: rw [← cancel_mono <| Y.fromSpecResidueField T.y]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
          Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
        Spec.map T.tensorInr) ≫
      Y.fromSpecResidueField T.y =
    ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr) ≫ Y.fromSpecResidueField T.y
have h₁ : Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
    Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.snd f g =
  (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.snd f g
Tactic: simp_rw [Category.assoc, ← T.specTensorTo_snd, tensorCongr_SpecTensorTo_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.snd f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.snd f g
have h₁ : Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
    Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.snd f g =
  Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
    (pullback f g).fromSpecResidueField (T.SpecTensorTo p) ≫ pullback.snd f g
Tactic: rw [← Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, ofPointTensor_SpecTensorTo_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
h₁ :
  Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.snd f g =
    Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      (pullback f g).fromSpecResidueField (T.SpecTensorTo p) ≫ pullback.snd f g
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.snd f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.snd f g
have h₂ : Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
    (pullback f g).fromSpecResidueField (T.SpecTensorTo p) ≫ pullback.snd f g =
  Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
    (pullback f g).fromSpecResidueField (T.SpecTensorTo p) ≫ pullback.snd f g
Tactic: rw [← Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, ofPointTensor_SpecTensorTo_assoc]