awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
x : (↑Γ(X, V) : Type u_1)
contrapose! : X.basicOpen x ≠ ⊥ → U ⊓ X.basicOpen x ≠ ⊥
⊢ ∀ (hx : U ⊓ X.basicOpen x = ⊥), X.basicOpen x = ⊥

Tactic:
contrapose!
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
x : (↑Γ(X, V) : Type u_1)
simp_rw : (↑(X.basicOpen x) : Set ↥X).Nonempty → (↑(U ⊓ X.basicOpen x) : Set ↥X).Nonempty
⊢ X.basicOpen x ≠ ⊥ → U ⊓ X.basicOpen x ≠ ⊥

Tactic:
simp_rw [Ne, ← Opens.not_nonempty_iff_eq_bot, Classical.not_not]

Premises used: Classical.not_not, Ne, TopologicalSpace.Opens.not_nonempty_iff_eq_bot
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
x : (↑Γ(X, V) : Type u_1)
apply : (↑U : Set ↥X).Nonempty
⊢ (↑(X.basicOpen x) : Set ↥X).Nonempty → (↑(U ⊓ X.basicOpen x) : Set ↥X).Nonempty

Tactic:
apply nonempty_preirreducible_inter U.isOpen (RingedSpace.basicOpen _ _).isOpen

Premises used: AlgebraicGeometry.RingedSpace.basicOpen, TopologicalSpace.Opens.isOpen, nonempty_preirreducible_inter
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
x : (↑Γ(X, V) : Type u_1)
⊢ (↑U : Set ↥X).Nonempty

Tactic:
simpa using H
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
U X : Scheme
x : ↥U
f : U ⟶ X
inst : IsOpenImmersion f
⊢ Order.coheight (α := ↥X) (f x : ↥X) = Order.coheight x

Tactic:
f.isOpenEmbedding.coheight_eq

Premises used: Topology.IsOpenEmbedding.coheight_eq, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
R : CommRingCat
x : ↥(Spec R)
rw : height x = coheight x
rw₁ :
  height x =
    coheight (α := (PrimeSpectrum (↑R : Type u_1))ᵒᵈ)
      ((specOrderIsoPrimeSpectrum R : (a : ↥(Spec R)) → (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) x :
        (PrimeSpectrum (↑R : Type u_1))ᵒᵈ)
rw₂ :
  height x =
    height (α := PrimeSpectrum (↑R : Type u_1))
      ((OrderDual.ofDual : (a : (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) → PrimeSpectrum (↑R : Type u_1))
          ((specOrderIsoPrimeSpectrum R : (a : ↥(Spec R)) → (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) x) :
        PrimeSpectrum (↑R : Type u_1))
rw₃ :
  height x =
    height (α := PrimeSpectrum (↑R : Type u_1))
      ((OrderDual.ofDual : (a : (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) → PrimeSpectrum (↑R : Type u_1))
          ((OrderDual.toDual : (a : PrimeSpectrum (↑R : Type u_1)) → (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) x) :
        PrimeSpectrum (↑R : Type u_1))
rw₄ rw₅ : height x = height x
⊢ x.asIdeal.height = coheight x

Tactic:
rw [PrimeSpectrum.height_eq_orderHeight,
    ← Order.coheight_orderIso (specOrderIsoPrimeSpectrum R), ← height_ofDual,
    specOrderIsoPrimeSpectrum_apply, OrderDual.ofDual_toDual]

Premises used: AlgebraicGeometry.specOrderIsoPrimeSpectrum_apply, Order.height_ofDual, AlgebraicGeometry.specOrderIsoPrimeSpectrum, OrderDual.ofDual_toDual, PrimeSpectrum.height_eq_orderHeight, Order.coheight_orderIso
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
x : ↥X
inr :
  ∀
    (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),
    ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
wlog :
  ∀ {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 ℕ∞)
⊢ ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)

Tactic:
wlog h : ∃ R, X = Spec R
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
x : ↥X
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
inr :
  ∀ (R : CommRingCat.{u_1}) (f : Spec R ⟶ X) (hf : IsOpenImmersion f)
    (hsub :
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑⊤ : Set ↥X)),
    ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
⊢ ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)

Tactic:
obtain ⟨R, f, hf, hsub⟩ := Scheme.exists_affine_mem_range_and_range_subset
      (show x ∈ ⊤ from trivial)

Premises used: trivial, AlgebraicGeometry.Scheme.exists_affine_mem_range_and_range_subset
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
x : ↥X
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
hsub : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑⊤ : Set ↥X)
inr :
  ∀ (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 ℕ∞)
⊢ ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)

Tactic:
obtain ⟨y, rfl⟩ := Set.mem_range.mp hsub.1

Premises used: Set.mem_range, And.left, Iff.mp, rfl
-- Module: Mathlib.AlgebraicGeometry.Properties
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)
inr :
  ringKrullDim.{u_1} (↑(X.presheaf.stalk (f y)) : Type u_1) =
    ringKrullDim.{u_1} (↑((Spec R).presheaf.stalk y) : Type u_1)
⊢ ringKrullDim.{u_1} (↑(X.presheaf.stalk (f y)) : Type u_1) = (↑(coheight (α := ↥X) (f y : ↥X)) : WithBot ℕ∞)

Tactic:
rw [coheight_eq_of_isOpenImmersion, ← this _ ⟨R, rfl⟩]

Premises used: Exists.intro, AlgebraicGeometry.coheight_eq_of_isOpenImmersion, rfl
-- Module: Mathlib.AlgebraicGeometry.Properties
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) =
    ringKrullDim.{u_1} (↑((Spec R).presheaf.stalk y) : Type u_1)

Tactic:
Order.krullDim_eq_of_orderIso
      (PrimeSpectrum.comapEquiv (asIso (Scheme.Hom.stalkMap f y)).commRingCatIsoToRingEquiv)

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, PrimeSpectrum.comapEquiv, Order.krullDim_eq_of_orderIso, ringKrullDim, AlgebraicGeometry.Scheme.Hom.stalkMap, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Properties
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) =
    ringKrullDim.{u_1} (↑((Spec R).presheaf.stalk y) : Type u_1)

Tactic:
exact Order.krullDim_eq_of_orderIso
      (PrimeSpectrum.comapEquiv (asIso (Scheme.Hom.stalkMap f y)).commRingCatIsoToRingEquiv)

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, PrimeSpectrum.comapEquiv, Order.krullDim_eq_of_orderIso, AlgebraicGeometry.Scheme.Hom.stalkMap, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
x : ↥X
h : ∃ (R : CommRingCat.{u_1}), X = Spec R
obtain :
  ∀ (R : CommRingCat.{u_1}) (x : ↥(Spec R)),
    ringKrullDim.{u_1} (↑((Spec R).presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
⊢ ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)

Tactic:
obtain ⟨R, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Properties
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
⊢ 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
-- Module: Mathlib.AlgebraicGeometry.Properties
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
rw : (↑x.asIdeal.height : WithBot ℕ∞) = (↑(coheight x) : WithBot ℕ∞)
⊢ ringKrullDim.{u_1} (↑((Spec R).presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)

Tactic:
rw [IsLocalization.AtPrime.ringKrullDim_eq_height x.asIdeal ((Spec R).presheaf.stalk x)]

Premises used: AlgebraicGeometry.Spec, CommRingCat.carrier, TopCat.Presheaf.stalk, IsLocalization.AtPrime.ringKrullDim_eq_height, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, PrimeSpectrum.asIdeal, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Properties
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
apply : x.asIdeal.height = coheight x
⊢ (↑x.asIdeal.height : WithBot ℕ∞) = (↑(coheight x) : WithBot ℕ∞)

Tactic:
apply WithBot.coe_eq_coe.mpr

Premises used: Iff.mpr, WithBot.coe_eq_coe
-- Module: Mathlib.AlgebraicGeometry.Properties
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 = coheight x

Tactic:
idealHeight_eq_coheight R x

Premises used: AlgebraicGeometry.idealHeight_eq_coheight
-- Module: Mathlib.AlgebraicGeometry.Properties
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 = coheight x

Tactic:
exact idealHeight_eq_coheight R x

Premises used: AlgebraicGeometry.idealHeight_eq_coheight
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
inst_1 : Subsingleton.{u + 1} ↥X
rw : T1Space.{u} (PrimeSpectrum (↑Γ(X, ⊤) : Type u))
⊢ IsField.{u} (↑Γ(X, ⊤) : Type u)

Tactic:
rw [← PrimeSpectrum.t1Space_iff_isField]

Premises used: PrimeSpectrum.t1Space_iff_isField
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
inst_1 : Subsingleton.{u + 1} ↥X
⊢ T1Space.{u} (PrimeSpectrum (↑Γ(X, ⊤) : Type u))

Tactic:
apply X.isoSpec.hom.homeomorph.t1Space

Premises used: AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.Scheme.Hom.homeomorph, Homeomorph.t1Space, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
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
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₂
⊢ t₁ = t₂

Tactic:
cases t₁
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
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
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 }
⊢ { x := x, y := y, s := s, hx := hx, hy := hy : Triplet f g } = t₂

Tactic:
cases t₂
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
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
mk : x = x_1 ∧ y = y_1 ∧ s = s_1
⊢ { 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:
simp
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
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_1 ∧ y = y_1 ∧ s = s_1

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ Nontrivial.{u} (↑T.tensor : Type u)

Tactic:
CommRingCat.nontrivial_of_isPushout_of_isField (Field.toIsField _)
    (IsPushout.of_hasPushout _ _)

Premises used: CategoryTheory.IsPushout.of_hasPushout, CommRingCat.nontrivial_of_isPushout_of_isField
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ IsPullback (Spec.map T.tensorInl) (Spec.map T.tensorInr)
    (Spec.map ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f T.x))
    (Spec.map ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g T.y))

Tactic:
isPullback_SpecMap_pushout _ _

Premises used: AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInl, AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInr, AlgebraicGeometry.Scheme.Pullback.Triplet.tensor, AlgebraicGeometry.isPullback_SpecMap_pushout
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : Triplet f g
e : T₁ = T₂
subst : T₁.tensor = T₁.tensor
⊢ T₁.tensor = T₂.tensor

Tactic:
subst e
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ : Triplet f g
⊢ T₁.tensor = T₁.tensor

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : Triplet f g
⊢ tensorCongr ⋯ = Iso.refl x.tensor

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.eqToIso, CategoryTheory.Iso.refl, AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr, rfl
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x y : Triplet f g
e : x = y
⊢ (tensorCongr e).symm = tensorCongr ⋯

Tactic:
rfl

Premises used: CategoryTheory.Functor.op, Eq.mpr, IsLocalRing.ResidueField.map, Set.Mem, CategoryTheory.eqToHom, setOf, CategoryTheory.eqToIso, CategoryTheory.Functor.comp, IsLocalRing.maximalIdeal, nonunits, CategoryTheory.Limits.WidePushoutShape.wideSpan, AddOpposite, AlgebraicGeometry.Scheme.residueField, TopologicalSpace.OpenNhds.map, CategoryTheory.Limits.colimit, AlgebraicGeometry.Scheme.Pullback.Triplet.tensor, AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr, QuotientAddGroup.con, IsLocalRing.ResidueField, Monotone.functor, Quotient, CategoryTheory.Iso.symm, TopologicalSpace.OpenNhds, Ideal.Quotient.lift, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, CategoryTheory.Limits.span, TopologicalSpace.OpenNhds.inclusion, rfl
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x y : Triplet f g
e : x = y
⊢ (tensorCongr e).inv = (tensorCongr ⋯).hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x y z : Triplet f g
e : x = y
e' : y = z
subst : tensorCongr ⋯ ≪≫ tensorCongr ⋯ = tensorCongr ⋯
⊢ tensorCongr e ≪≫ tensorCongr e' = tensorCongr ⋯

Tactic:
subst e e'
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : Triplet f g
⊢ tensorCongr ⋯ ≪≫ tensorCongr ⋯ = tensorCongr ⋯

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x y z : Triplet f g
e : x = y
e' : y = z
subst : (tensorCongr ⋯).hom ≫ (tensorCongr ⋯).hom = (tensorCongr ⋯).hom
⊢ (tensorCongr e).hom ≫ (tensorCongr e').hom = (tensorCongr ⋯).hom

Tactic:
subst e e'
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : Triplet f g
⊢ (tensorCongr ⋯).hom ≫ (tensorCongr ⋯).hom = (tensorCongr ⋯).hom

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
simp :
  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))
⊢ (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x) ≫ f = (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ≫ g

Tactic:
simp only [residueFieldCongr_inv, Category.assoc, tensorInl, tensorInr,
    ← Hom.SpecMap_residueFieldMap_fromSpecResidueField]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInl, AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInr, AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField, AlgebraicGeometry.Scheme.residueFieldCongr_inv
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
rw :
  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) ≫ Spec.map (residueFieldCongr ⋯).hom ≫ S.fromSpecResidueField T.s)
    (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) ≫ Spec.map (residueFieldCongr ⋯).hom ≫ S.fromSpecResidueField T.s)
⊢ 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))

Tactic:
rw [← residueFieldCongr_fromSpecResidueField T.hx.symm,
    ← residueFieldCongr_fromSpecResidueField T.hy.symm]

Premises used: AlgebraicGeometry.Scheme.Pullback.Triplet.hy, AlgebraicGeometry.Scheme.Pullback.Triplet.hx, AlgebraicGeometry.Scheme.residueFieldCongr_fromSpecResidueField, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
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) ≫ Spec.map (residueFieldCongr ⋯).hom ≫ S.fromSpecResidueField T.s)
    (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) ≫ Spec.map (residueFieldCongr ⋯).hom ≫ S.fromSpecResidueField T.s)

Tactic:
simp only [← Category.assoc, ← Spec.map_comp, pushout.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pushout.condition, AlgebraicGeometry.Spec.map_comp
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (CategoryStruct.comp (Y := pullback f g)
        (pullback.lift (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x)
          (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ⋯)
        (pullback.fst f g))
      p =
    T.x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (CategoryStruct.comp (Y := pullback f g)
        (pullback.lift (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x)
          (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ⋯)
        (pullback.snd f g))
      p =
    T.y

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ T.SpecTensorTo ≫ pullback.fst f g = Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x

Tactic:
pullback.lift_fst _ _ _

Premises used: CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ T.SpecTensorTo ≫ pullback.snd f g = Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y

Tactic:
pullback.lift_snd _ _ _

Premises used: CategoryTheory.Limits.pullback.lift_snd
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
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
ey : y (X := X) (S := S) (f := f) (g := g) (ofPoint (T.SpecTensorTo p)) = T.y
⊢ ofPoint (T.SpecTensorTo p) = T

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ x (Y := Y) (S := S) (f := f) (g := g) (ofPoint (T.SpecTensorTo p)) = T.x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ y (X := X) (S := S) (f := f) (g := g) (ofPoint (T.SpecTensorTo p)) = T.y

Tactic:
simp