mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f], finrank f = 1 → (∃ S, X = Spec S) → IsIso f
hX : ¬∃ S, X = Spec S
⊢ IsIso f

pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
hX : ∃ S, X = Spec S
⊢ IsIso f

Tactic:
·

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f], finrank f = 1 → (∃ S, X = Spec S) → IsIso f
hX : ¬∃ S, X = Spec S
⊢ IsIso f
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
⊢ Smooth f

pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
h : ∃ R, Y = Spec R
⊢ Smooth f

Tactic:
·

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
⊢ Smooth f
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: case inr.hg
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ Smooth (Scheme.Hom.fiberToSpecResidueField f ((Y.affineCover.f i) y))

Tactic:
·

Goal state after:
case inr.hg
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ Smooth (Scheme.Hom.fiberToSpecResidueField f ((Y.affineCover.f i) y))
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X : Scheme} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ S, X = Spec S) → Smooth f
h : ¬∃ S, X = Spec S
⊢ Smooth f

pp: X✝ Y : Scheme
f✝ : X✝ ⟶ Y
R : CommRingCat
X : Scheme
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
h : ∃ S, X = Spec S
⊢ Smooth f

Tactic:
·

Goal state after:
case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X : Scheme} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ S, X = Spec S) → Smooth f
h : ¬∃ S, X = Spec S
⊢ Smooth f
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : Ideal.span {r} = ⊤
⊢ ringKrullDim (R ⧸ Ideal.span {r}) + 1 ≤ ringKrullDim R

pp: case neg
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
⊢ ringKrullDim (R ⧸ Ideal.span {r}) + 1 ≤ ringKrullDim R

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : Ideal.span {r} = ⊤
⊢ ringKrullDim (R ⧸ Ideal.span {r}) + 1 ≤ ringKrullDim R
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case e'_3
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
inst✝ : Finite σ
α✝ β✝ : Type u_3
e : α✝ ≃ β✝
H : ringKrullDim R + ↑(Nat.card α✝) ≤ ringKrullDim (MvPolynomial α✝ R)
⊢ ringKrullDim R + ↑(Nat.card α✝) = ringKrullDim R + ↑(Nat.card β✝)

pp: case e'_4
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
inst✝ : Finite σ
α✝ β✝ : Type u_3
e : α✝ ≃ β✝
H : ringKrullDim R + ↑(Nat.card α✝) ≤ ringKrullDim (MvPolynomial α✝ R)
⊢ ringKrullDim (MvPolynomial α✝ R) = ringKrullDim (MvPolynomial β✝ R)

Tactic:
·

Goal state after:
case e'_3
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
inst✝ : Finite σ
α✝ β✝ : Type u_3
e : α✝ ≃ β✝
H : ringKrullDim R + ↑(Nat.card α✝) ≤ ringKrullDim (MvPolynomial α✝ R)
⊢ ringKrullDim R + ↑(Nat.card α✝) = ringKrullDim R + ↑(Nat.card β✝)
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case e'_4
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
inst✝ : Finite σ
α✝ β✝ : Type u_3
e : α✝ ≃ β✝
H : ringKrullDim R + ↑(Nat.card α✝) ≤ ringKrullDim (MvPolynomial α✝ R)
⊢ ringKrullDim (MvPolynomial α✝ R) = ringKrullDim (MvPolynomial β✝ R)

Tactic:
·

Goal state after:
case e'_4
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
inst✝ : Finite σ
α✝ β✝ : Type u_3
e : α✝ ≃ β✝
H : ringKrullDim R + ↑(Nat.card α✝) ≤ ringKrullDim (MvPolynomial α✝ R)
⊢ ringKrullDim (MvPolynomial α✝ R) = ringKrullDim (MvPolynomial β✝ R)
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Finite σ
⊢ ringKrullDim R + ↑(ENat.card σ) ≤ ringKrullDim (MvPolynomial σ R)

pp: case inr
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
⊢ ringKrullDim R + ↑(ENat.card σ) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Finite σ
⊢ ringKrullDim R + ↑(ENat.card σ) ≤ ringKrullDim (MvPolynomial σ R)
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
⊢ ringKrullDim R + ↑(ENat.card σ) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
⊢ ringKrullDim R + ↑(ENat.card σ) ≤ ringKrullDim (MvPolynomial σ R)
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := ⋯
this : Function.Surjective (Function.invFun ι)
⊢ ↑n ≤ ↑n + 1

pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := ⋯
this : Function.Surjective (Function.invFun ι)
⊢ ↑n + 1 ≤ ringKrullDim R + (↑n + 1)

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := ⋯
this : Function.Surjective (Function.invFun ι)
⊢ ↑n ≤ ↑n + 1
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := ⋯
this : Function.Surjective (Function.invFun ι)
⊢ ↑n + 1 ≤ ringKrullDim R + (↑n + 1)

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := ⋯
this : Function.Surjective (Function.invFun ι)
⊢ ↑n + 1 ≤ ringKrullDim R + (↑n + 1)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
⊢ I ≤ (Submodule.mkQ (a • I) ∘ₗ (mul R R) a).ker

pp: case a
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
⊢ (Submodule.mkQ (a • I) ∘ₗ (mul R R) a).ker ≤ I

Tactic:
·

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
⊢ I ≤ (Submodule.mkQ (a • I) ∘ₗ (mul R R) a).ker
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
⊢ (Submodule.mkQ (a • I) ∘ₗ (mul R R) a).ker ≤ I

Tactic:
·

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
⊢ (Submodule.mkQ (a • I) ∘ₗ (mul R R) a).ker ≤ I
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
⊢ Function.Injective ⇑(mulQuot a I)

Tactic:
simp only [mulQuot, Submodule.mapQ, ← ker_eq_bot]
  apply Submodule.ker_liftQ_eq_bot'
  apply le_antisymm
  · have : Submodule.map (mul R R a) I = a • I := rfl
    rw [le_ker_iff_map, Submodule.map_comp, this, Submodule.mkQ_map_self]
  · have m : I = Submodule.comap (mul R R a) (a • I) := by
      ext b
      exact (Submodule.mul_mem_smul_iff ha).symm
    simp [← m, ker_comp]

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R (x * y)) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R x) *
      ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R y)

pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∉ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R (x * y)) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R x) * 0

pp: case pos
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∉ nonZeroDivisors R
h✝ : y ∈ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R (x * y)) =
    0 * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R y)

pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∉ nonZeroDivisors R
h✝ : y ∉ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R (x * y)) = 0 * 0

pp: case pos
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_ : x * y ∉ nonZeroDivisors R
h✝¹ : x ∈ nonZeroDivisors R
h✝ : y ∈ nonZeroDivisors R
⊢ 0 =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R x) *
      ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R y)

pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_ : x * y ∉ nonZeroDivisors R
h✝¹ : x ∈ nonZeroDivisors R
h✝ : y ∉ nonZeroDivisors R
⊢ 0 = ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R x) * 0

pp: case pos
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_ : x * y ∉ nonZeroDivisors R
h✝¹ : x ∉ nonZeroDivisors R
h✝ : y ∈ nonZeroDivisors R
⊢ 0 = 0 * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R y)

pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_ : x * y ∉ nonZeroDivisors R
h✝¹ : x ∉ nonZeroDivisors R
h✝ : y ∉ nonZeroDivisors R
⊢ 0 = 0 * 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R (x * y)) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R x) *
      ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R y)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∉ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R (x * y)) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R x) * 0

Tactic:
simp_all [mul_mem_nonZeroDivisors]

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∉ nonZeroDivisors R
h✝ : y ∈ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R (x * y)) =
    0 * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R y)

Tactic:
simp_all [mul_mem_nonZeroDivisors]

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∉ nonZeroDivisors R
h✝ : y ∉ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R (x * y)) = 0 * 0

Tactic:
simp_all [mul_mem_nonZeroDivisors]

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_ : x * y ∉ nonZeroDivisors R
h✝¹ : x ∈ nonZeroDivisors R
h✝ : y ∈ nonZeroDivisors R
⊢ 0 =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R x) *
      ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R y)

Tactic:
simp_all [mul_mem_nonZeroDivisors]

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_ : x * y ∉ nonZeroDivisors R
h✝¹ : x ∈ nonZeroDivisors R
h✝ : y ∉ nonZeroDivisors R
⊢ 0 = ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R x) * 0

Tactic:
simp_all [mul_mem_nonZeroDivisors]

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_ : x * y ∉ nonZeroDivisors R
h✝¹ : x ∉ nonZeroDivisors R
h✝ : y ∈ nonZeroDivisors R
⊢ 0 = 0 * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R y)

Tactic:
simp_all [mul_mem_nonZeroDivisors]

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_ : x * y ∉ nonZeroDivisors R
h✝¹ : x ∉ nonZeroDivisors R
h✝ : y ∉ nonZeroDivisors R
⊢ 0 = 0 * 0

Tactic:
simp_all [mul_mem_nonZeroDivisors]

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x = 0
⊢ ord R x = (IsDiscreteValuationRing.addVal R) x

pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : ¬x = 0
⊢ ord R x = (IsDiscreteValuationRing.addVal R) x

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x = 0
⊢ ord R x = (IsDiscreteValuationRing.addVal R) x
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬↑α * ϖ ^ m = 0
⊢ ord R ↑α + m • 1 = (IsDiscreteValuationRing.addVal R) (↑α * ϖ ^ m)

pp: case neg.hx
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬↑α * ϖ ^ m = 0
⊢ ϖ ∈ nonZeroDivisors R

pp: case neg.hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬↑α * ϖ ^ m = 0
⊢ ϖ ^ m ∈ nonZeroDivisors R

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬↑α * ϖ ^ m = 0
⊢ ord R ↑α + m • 1 = (IsDiscreteValuationRing.addVal R) (↑α * ϖ ^ m)
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: case pos
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsNoetherianRing R
inst✝⁷ : KrullDimLE 1 R
K : Type u_2
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : Algebra S K
inst✝ : IsScalarTower S R K
a : S
ha : (algebraMap S R) a ≠ 0
f : K
j : f = 0
⊢ (ordFrac R) f ≤ (ordFrac R) (a • f)

pp: case neg
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsNoetherianRing R
inst✝⁷ : KrullDimLE 1 R
K : Type u_2
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : Algebra S K
inst✝ : IsScalarTower S R K
a : S
ha : (algebraMap S R) a ≠ 0
f : K
j : ¬f = 0
⊢ (ordFrac R) f ≤ (ordFrac R) (a • f)

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsNoetherianRing R
inst✝⁷ : KrullDimLE 1 R
K : Type u_2
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : Algebra S K
inst✝ : IsScalarTower S R K
a : S
ha : (algebraMap S R) a ≠ 0
f : K
j : f = 0
⊢ (ordFrac R) f ≤ (ordFrac R) (a • f)
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : K
ha : a = 0
⊢ (ordFrac R) a =
    (MonoidWithZero.inverse.comp
        (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)).toMonoidWithZeroHom)
      a

pp: case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : K
ha : ¬a = 0
⊢ (ordFrac R) a =
    (MonoidWithZero.inverse.comp
        (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)).toMonoidWithZeroHom)
      a

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : K
ha : a = 0
⊢ (ordFrac R) a =
    (MonoidWithZero.inverse.comp
        (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)).toMonoidWithZeroHom)
      a
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case pos
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
z : ↥X
h : coheight z = 1
⊢ ord 0 z = 0 z

pp: case neg
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
z : ↥X
h : ¬coheight z = 1
⊢ ord 0 z = 0 z

Tactic:
·

Goal state after:
case pos
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
z : ↥X
h : coheight z = 1
⊢ ord 0 z = 0 z
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case neg
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
z : ↥X
h : ¬coheight z = 1
⊢ ord 0 z = 0 z

Tactic:
·

Goal state after:
case neg
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
z : ↥X
h : ¬coheight z = 1
⊢ ord 0 z = 0 z
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case pos
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
hx : coheight x ≠ 1
⊢ ord (f * g) x = ord f x + ord g x

pp: case neg
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
hx : coheight x = 1
⊢ ord (f * g) x = ord f x + ord g x

Tactic:
·

Goal state after:
case pos
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
hx : coheight x ≠ 1
⊢ ord (f * g) x = ord f x + ord g x
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case neg
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
hx : coheight x = 1
⊢ ord (f * g) x = ord f x + ord g x

Tactic:
ord_eq_iff hx <| (mul_ne_zero_iff_right hg).mpr hf

Goal state after:
case neg
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
hx : coheight x = 1
⊢ (ordHom x hx) (f * g) = ↑(Multiplicative.ofAdd (ord f x + ord g x))
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case pos
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx' : x ∈ U
hx : coheight x ≠ 1
⊢ ord ((ConcreteCategory.hom (X.germToFunctionField U)) f) x = 0

pp: case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx' : x ∈ U
hx : coheight x = 1
⊢ ord ((ConcreteCategory.hom (X.germToFunctionField U)) f) x = 0

Tactic:
·

Goal state after:
case pos
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx' : x ∈ U
hx : coheight x ≠ 1
⊢ ord ((ConcreteCategory.hom (X.germToFunctionField U)) f) x = 0
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case pos
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : f = 0
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x

pp: case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : ¬f = 0
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x

Tactic:
·

Goal state after:
case pos
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : f = 0
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case pos
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : ¬f = 0
hg : g = 0
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x

pp: case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : ¬f = 0
hg : ¬g = 0
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x

Tactic:
·

Goal state after:
case pos
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : ¬f = 0
hg : g = 0
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x