mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
inst✝ : Finite σ
⊢ ringKrullDim R + ↑(Nat.card σ) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
this : ringKrullDim (MvPolynomial σ R) = ⊤
⊢ ringKrullDim R + ⊤ ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ ord R 1 = 0

Tactic:
by

Goal state after:
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
⊢ I = Submodule.comap ((mul R R) a) (a • I)

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ (α ▷ 𝟙 e ≫ (l₁ ≫ h) ◁ adj₄.unit) ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ β ≫ adj₁.counit ▷ (l₃ ≫ k)) ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂)

Tactic:
whisker_exchange

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ (α ▷ 𝟙 e ≫ (l₁ ≫ h) ◁ adj₄.unit) ▷ r₂ ⊗≫
          r₃ ◁ (adj₁.counit ▷ (h ≫ l₄) ≫ 𝟙 b ◁ β) ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
⊢ Function.Surjective ⇑(quotOfMul a I)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
⊢ (quotOfMul a I).ker = a • ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
⊢ Function.Exact ⇑(mulQuot a I) ⇑(quotOfMul a I)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
hb : b ∈ nonZeroDivisors R
this : Module.length R (R ⧸ b • span {a}) = Module.length R (R ⧸ span {a}) + Module.length R (R ⧸ span {b})
⊢ {b} • span {a} = span {b * a}

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
hb : b ∈ nonZeroDivisors R
⊢ ord R (a * b) = ord R a + ord R b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
ha : a ∈ nonZeroDivisors R
⊢ ord R (a * b) = ord R a + ord R b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ ord R 0 = Module.length R R

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
n : ℕ
⊢ ord R (x ^ n) = n • ord R x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
h : IsUnit a
x : R
⊢ ord R (a * x) = ord R x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
h : IsUnit a
x : R
⊢ ord R (x * a) = ord R x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
h : Associated x y
⊢ ord R x = ord R y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
⊢ Associated (-x) x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
⊢ ord R (-x) = ord R x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra S R
a : S
h : IsUnit a
x : R
⊢ ord R (a • x) = ord R x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a x : R
this : span {a * x} ≤ span {x}
⊢ Module.length R (R ⧸ span {x}) ≤ Module.length R (R ⧸ span {a * x})

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a x : R
⊢ ord R x ≤ ord R (a * x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a x : R
h : a ∣ x
⊢ ord R a ≤ ord R x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra S R
a : S
x : R
⊢ ord R x ≤ ord R (a • x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
hx : IsUnit x
⊢ ord R x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
ϖ : R
hϖ : Irreducible ϖ
⊢ ord R ϖ = 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
⊢ (if 1 ∈ nonZeroDivisors R then ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R 1) else 0) = 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ ((g ≫ l₂) ◁ adj₄.unit ≫ α ▷ (l₄ ≫ r₄)) ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ β ≫ adj₁.counit ▷ (l₃ ≫ k)) ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
y : ↥(nonZeroDivisors R)
⊢ (ordMonoidWithZeroHom R) ↑y = 0 ↔ ord R ↑y = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
x : R
hx : x ∈ nonZeroDivisors R
n : ℕ
hn : ord R x = ↑n
⊢ (ordMonoidWithZeroHom R) x = ↑(Multiplicative.ofAdd ↑n)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    (α_ r₃ r₁ g).hom ≫
      r₃ ◁ (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)) ≫
        (α_ r₃ h r₂).inv ≫
          (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄)) ▷ r₂ ≫
            (α_ k r₄ r₂).hom

Tactic:
whisker_exchange

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ (adj₁.counit ▷ (h ≫ 𝟙 e) ≫ 𝟙 b ◁ h ◁ adj₄.unit) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    (α_ r₃ r₁ g).hom ≫
      r₃ ◁ (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)) ≫
        (α_ r₃ h r₂).inv ≫
          (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄)) ▷ r₂ ≫
            (α_ k r₄ r₂).hom
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : KrullDimLE 1 R
x : R
hx : x ∈ nonZeroDivisors R
⊢ IsFiniteLength R (R ⧸ span {x})

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : KrullDimLE 1 R
a : R
ha : a ∈ nonZeroDivisors R
⊢ ord R a ≠ ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
y : ↥(nonZeroDivisors R)
⊢ IsUnit ((ordMonoidWithZeroHom R) ↑y)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsNoetherianRing R
inst✝⁴ : KrullDimLE 1 R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : Nontrivial R
x : R
hx : x ≠ 0
⊢ (ordFrac R) ((algebraMap R K) x) = (ordMonoidWithZeroHom R) x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsNoetherianRing R
inst✝⁴ : KrullDimLE 1 R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : Nontrivial R
a b : ↥(nonZeroDivisors R)
⊢ (ordFrac R) (mk' K (↑a) b) = (ordMonoidWithZeroHom R) ↑a / (ordMonoidWithZeroHom R) ↑b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    (α_ r₃ r₁ g).hom ≫
      r₃ ◁ (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)) ≫
        (α_ r₃ h r₂).inv ≫
          (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄)) ▷ r₂ ≫
            (α_ k r₄ r₂).hom

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁶ : CommRing R✝
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsNoetherianRing R
inst✝³ : KrullDimLE 1 R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ Multiplicative.ofAdd (ord R ↑1).toNat = 1

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁶ : CommRing R✝
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsNoetherianRing R
inst✝³ : KrullDimLE 1 R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : ↥R⁰
⊢ Multiplicative.ofAdd (ord R ↑(x * y)).toNat =
    Multiplicative.ofAdd (ord R ↑x).toNat * Multiplicative.ofAdd (ord R ↑y).toNat

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
x : ↥R⁰
⊢ ↑(Multiplicative.ofAdd ↑(Multiplicative.toAdd (ordMonoidHom x))) = (ordMonoidWithZeroHom R) ↑x

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
a : R
ha : a ∈ R⁰
⊢ (ordMonoidWithZeroHom R) a ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
a b : R
ha : a ∈ R⁰
hb : b ∈ R⁰
⊢ ord R a ≤ ord R b ↔ (ordMonoidWithZeroHom R) a ≤ (ordMonoidWithZeroHom R) b

Tactic:
by

Goal state after:
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)

Tactic:
simp [IsDiscreteValuationRing.addVal_uniformizer hϖ]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ (mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (leftAdjointSquare.hcomp α β) =
    rightAdjointSquare.hcomp ((mateEquiv adj₁ adj₂) α) ((mateEquiv adj₃ adj₄) β)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
⊢ ord R x = ord R y ↔ Associated x y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
⊢ min (ord R x) (ord R y) ≤ ord R (x + y)

Tactic:
by

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

Goal state before:
pp: 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
x : R
hx : x ≠ 0
⊢ x ∈ nonZeroDivisors R

Tactic:
by

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

Goal state before:
pp: 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
x : R
hx : x ≠ 0
m : ℕ
hm : ↑m = ord R x
⊢ x ∈ nonZeroDivisors R

Tactic:
by

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

Goal state before:
pp: 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
x : R
hx : x ≠ 0
⊢ 1 ≤ (ordFrac R) ((algebraMap R K) x)

Tactic:
by

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

Goal state before:
pp: 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
this : (ordFrac R) f ≤ (ordFrac R) ((algebraMap S K) a • f)
⊢ (ordFrac R) f ≤ (ordFrac R) (a • f)

Tactic:
by

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

Goal state before:
pp: 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
⊢ (ordFrac R) f ≤ (ordFrac R) (a • f)

Tactic:
by

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

Goal state before:
pp: 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
x : R
hx : IsUnit x
⊢ (ordFrac R) ((algebraMap R K) x) = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
h : x ∈ nonZeroDivisors R
⊢ (ordMonoidWithZeroHom R) x = ((IsDiscreteValuationRing.maximalIdeal R).intValuation x)⁻¹

Tactic:
by

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

Goal state before:
pp: 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
x : R
h : x ≠ 0
⊢ (ordFrac R) ((algebraMap R K) x) = ((IsDiscreteValuationRing.maximalIdeal R).intValuation x)⁻¹

Tactic:
by

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

Goal state before:
pp: 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
⊢ ordFrac R =
    MonoidWithZero.inverse.comp
      (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)).toMonoidWithZeroHom

Tactic:
by

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

Goal state before:
pp: 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
x : K
⊢ (ordFrac R) x = ((IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) x)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ (α_ g₁ g₂ (l₅ ≫ l₆)).hom ≫
      g₁ ◁ ((α_ g₂ l₅ l₆).inv ≫ γ ▷ l₆ ≫ (α_ l₃ h₂ l₆).hom ≫ l₃ ◁ δ ≫ (α_ l₃ l₄ k₂).inv) ≫
        (α_ g₁ (l₃ ≫ l₄) k₂).inv ≫
          ((α_ g₁ l₃ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h₁ l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₂ k₁).inv) ▷ k₂ ≫
            (α_ (l₁ ≫ l₂) k₁ k₂).hom =
    𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂)

Tactic:
by

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

Goal state before:
pp: 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
ϖ : R
hϖ : Irreducible ϖ
⊢ (ordFrac R) ((algebraMap R K) ϖ) = WithZero.exp 1

Tactic:
by

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

Goal state before:
pp: 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
x : R
⊢ IsUnit x ↔ (ordFrac R) ((algebraMap R K) x) = 1

Tactic:
by

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

Goal state before:
pp: 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
⊢ MonoidHom.mker (ordFrac R) = Submonoid.map (algebraMap R K) (IsUnit.submonoid R)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ 𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂) =
    (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
      ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
        (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
          l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv

Tactic:
whisker_exchange

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ 𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ (α ▷ (h₂ ≫ l₆) ≫ (l₁ ≫ h₁) ◁ δ) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂) =
    (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
      ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
        (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
          l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv