mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ ¬Ideal.span {a} = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ ¬Ideal.span {a} = 0
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case neg
ι : Sort u_1
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
i : ι
⊢ a + f i ≤ a + f ?i

pp: case i
ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
i : ι
⊢ ι

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: s : Set ℝ≥0∞
a : ℝ≥0∞
hs : s.Nonempty
⊢ ⨆ i ∈ s, a + i = ⨆ b ∈ s, a + b

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: s : Set ℝ≥0∞
a : ℝ≥0∞
hs : s.Nonempty
⊢ ⨆ i ∈ s, i + a = ⨆ b ∈ s, b + a

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
⊢ ¬a = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
⊢ ¬a = 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
⊢ ¬a' = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
⊢ ¬a' = 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ ↑(a✝ * a✝¹) = ↑(a✝ * a✝¹)

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
⊢ spanSingleton R⁰ (((algebraMap R K) a)⁻¹ * ((algebraMap R K) a')⁻¹) * (↑J' * ↑J) =
    spanSingleton R⁰ (((algebraMap R K) a)⁻¹ * ((algebraMap R K) a')⁻¹) * (↑J' * ↑J)

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
⊢ 0 = 0

pp: case inl
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, a - f i < b

Tactic:
]

Goal state after:
case inl
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, a - f i < b
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ a - (a - f i) ≤ a - ⨅ i, a - f i

Tactic:
]

Goal state after:
case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ a - (a - f i) ≤ a - ⨅ i, a - f i
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ y' < y, ∀ z' < z, y' + z' ≤ x
⊢ ∃ i, i < y

Tactic:
exact ⟨0, hy.bot_lt⟩

Goal state after:
Module: Mathlib.Topology.UniformSpace.OfFun

Goal state before:
pp: X : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
d : X → X → M
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
r : M
x✝ : r > 0
x : X × X
hx : x ∈ {x | d x.1 x.2 < r}
⊢ d x.swap.2 x.swap.1 < r

Tactic:
]

Goal state after:
X : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
d : X → X → M
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
r : M
x✝ : r > 0
x : X × X
hx : x ∈ {x | d x.1 x.2 < r}
⊢ d x.swap.2 x.swap.1 < r
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors +
          (Associates.mk v.asIdeal).count (Associates.mk J').factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors +
          (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a'})).factors) =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) +
      (↑((Associates.mk v.asIdeal).count (Associates.mk J').factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a'})).factors))

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors +
          (Associates.mk v.asIdeal).count (Associates.mk J').factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors +
          (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a'})).factors) =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) +
      (↑((Associates.mk v.asIdeal).count (Associates.mk J').factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a'})).factors))
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
inst✝ : Decidable (I ≠ 0 ∧ I' ≠ 0)
h : I * I' = 0
⊢ count K v (I * I') = 0

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
inst✝ : Decidable (I ≠ 0 ∧ I' ≠ 0)
h : I * I' = 0
⊢ count K v (I * I') = 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
inst✝ : Decidable (I ≠ 0 ∧ I' ≠ 0)
h : I * I' = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Icc ↑↑x ↑↑y = Icc ↑x ↑y

Tactic:
]

Goal state after:
x y : ℝ
⊢ Icc ↑↑x ↑↑y = Icc ↑x ↑y
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
h1 : 1 = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑1
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Ico ↑↑x ↑↑y = Ico ↑x ↑y

Tactic:
]

Goal state after:
x y : ℝ
⊢ Ico ↑↑x ↑↑y = Ico ↑x ↑y
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case empty
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
ι : Type u_3
I : ι → FractionalIdeal R⁰ K
hS : ∀ i ∈ ∅, I i ≠ 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ Ico ↑↑x ↑⊤ = Ico ↑x ⊤

Tactic:
]

Goal state after:
x : ℝ
⊢ Ico ↑↑x ↑⊤ = Ico ↑x ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Ioc ↑↑x ↑↑y = Ioc ↑x ↑y

Tactic:
]

Goal state after:
x y : ℝ
⊢ Ioc ↑↑x ↑↑y = Ioc ↑x ↑y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Ioo ↑↑x ↑↑y = Ioo ↑x ↑y

Tactic:
]

Goal state after:
x y : ℝ
⊢ Ioo ↑↑x ↑↑y = Ioo ↑x ↑y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ Ioo ↑↑x ↑⊤ = Ioo ↑x ⊤

Tactic:
]

Goal state after:
x : ℝ
⊢ Ioo ↑↑x ↑⊤ = Ioo ↑x ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ Ioc ⊥ ↑↑x = Ioc ⊥ ↑x

Tactic:
]

Goal state after:
x : ℝ
⊢ Ioc ⊥ ↑↑x = Ioc ⊥ ↑x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ Ioo ⊥ ↑↑x = Ioo ⊥ ↑x

Tactic:
]

Goal state after:
x : ℝ
⊢ Ioo ⊥ ↑↑x = Ioo ⊥ ↑x
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case insert
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
ι : Type u_3
I : ι → FractionalIdeal R⁰ K
i : ι
s : Finset ι
hi : i ∉ s
hrec : (∀ i ∈ s, I i ≠ 0) → count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)
hS : ∀ i_1 ∈ insert i s, I i_1 ≠ 0
hS' : ∀ i ∈ s, I i ≠ 0
hS0 : ∏ i ∈ s, I i ≠ 0
hi0 : I i ≠ 0
⊢ count K v (I i) + ∑ i ∈ s, count K v (I i) = count K v (I i) + ∑ x ∈ s, count K v (I x)

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ Real.toEReal ⁻¹' (Ici ↑x ∩ Iio ⊤) = Ici x

Tactic:
]

Goal state after:
x : ℝ
⊢ Real.toEReal ⁻¹' (Ici ↑x ∩ Iio ⊤) = Ici x
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case zero
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ↑x ∩ Iio ⊤) = Ioi x

Tactic:
]

Goal state after:
x : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ↑x ∩ Iio ⊤) = Ioi x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iic ↑y) = Iic y

Tactic:
]

Goal state after:
y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iic ↑y) = Iic y
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case succ
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = ↑(n + 1) * count K v I

Tactic:
]

Goal state after:
case succ
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = ↑(n + 1) * count K v I
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iio ↑y) = Iio y

Tactic:
]

Goal state after:
y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iio ↑y) = Iio y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: ⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iio ⊤) = univ

Tactic:
]

Goal state after:
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iio ⊤) = univ
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ b⁻¹ * a = b⁻¹ * a

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ≥0∞
⊢ ↑x = 0 ↔ ↑x = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ≥0∞
⊢ ↑x = 1 ↔ ↑x = 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ≥0∞
⊢ 0 < x ↔ 0 < x

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ≥0∞
⊢ x ≠ 0 ↔ x ≠ 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: r b : ℝ≥0
hb : 1 ≤ r * b
⊢ 1 ≤ r * b

Tactic:
]

Goal state after:
r b : ℝ≥0
hb : 1 ≤ r * b
⊢ 1 ≤ r * b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: r : ℝ≥0
hr : r ≠ 0
⊢ 1 ≤ 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ⊢ 2⁻¹ = 2⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: r p : ℝ≥0
hr : r ≠ 0
⊢ ↑p * (↑r)⁻¹ = ↑p * (↑r)⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑∞ = ⊤ * ↑↑x

Tactic:
]

Goal state after:
case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑∞ = ⊤ * ↑↑x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ≥0
⊢ ↑↑x * ⊤ = ↑↑x * ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
hx : x ≤ 0
⊢ ENNReal.ofReal x.toReal = 0

pp: x : EReal
hx : x ≤ 0
h : x = ⊤
⊢ False

Tactic:
]

Goal state after:
x : EReal
hx : x ≤ 0
⊢ ENNReal.ofReal x.toReal = 0

x : EReal
hx : x ≤ 0
h : x = ⊤
⊢ False
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr
a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
⊢ (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : I = 0
h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
⊢ 0 < x ↔ 0 < x

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
hx : 0 ≤ x
⊢ ↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) = x

Tactic:
]

Goal state after:
x : EReal
hx : 0 ≤ x
⊢ ↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) = x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case pos
x : EReal
hx : 0 ≤ x
h_top : x = ⊤
⊢ ↑∞ = ⊤

Tactic:
]

Goal state after:
case pos
x : EReal
hx : 0 ≤ x
h_top : x = ⊤
⊢ ↑∞ = ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case neg
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ ↑(ENNReal.ofReal x.toReal) = x

Tactic:
]

Goal state after:
case neg
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ ↑(ENNReal.ofReal x.toReal) = x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case inl
x : EReal
hx : 0 ≤ x
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : ¬I = 0
⊢ ↑n * count K v I + count K v I = (↑n + 1) * count K v I

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : ¬I = 0
⊢ ↑n * count K v I + count K v I = (↑n + 1) * count K v I
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case inr
x : EReal
hx : x ≤ 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case pos
x : ℝ≥0∞
h_top : x = ∞
⊢ ∞ = ∞

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case neg
x : ℝ≥0∞
h_top : ¬x = ∞
⊢ x ≠ ∞

pp: x : ℝ≥0∞
h_top : ¬x = ∞
⊢ ¬↑x = ⊤

Tactic:
]

Goal state after:
case neg
x : ℝ≥0∞
h_top : ¬x = ∞
⊢ x ≠ ∞

x : ℝ≥0∞
h_top : ¬x = ∞
⊢ ¬↑x = ⊤
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : ↑v.asIdeal ≠ 0
⊢ ↑v.asIdeal = ↑v.asIdeal

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ∞ → b = 0
⊢ b = b

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: m n : ℕ
⊢ m = n ↔ m = n

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: m n : ℕ
⊢ m ≤ n ↔ m ≤ n

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: m n : ℕ
⊢ m < n ↔ m < n

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: m n : ℕ
⊢ ↑↑m * ↑↑n = ↑↑m * ↑↑n

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : ↑v.asIdeal ≠ 0
h_self : ↑v.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal
hv_irred : Irreducible (Associates.mk v.asIdeal)
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
n : ℕ
⊢ ↑n = ↑n

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
n : ℤ
I : FractionalIdeal R⁰ K
hI : I = 0
hn : n = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
⊢ a = 1 ↔ a = 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y z : ℝ≥0∞
h1 : x ≠ 0
h2 : x ≠ ∞
⊢ y ≤ x * z ↔ y ≤ x * z

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ∞
⊢ x ≤ z * y ↔ x ≤ z * y

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
n : ℤ
I : FractionalIdeal R⁰ K
hI : I = 0
hn : ¬n = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b ≠ 0 ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a

Tactic:
]

Goal state after:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b ≠ 0 ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a

Tactic:
]

Goal state after:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
⊢ a⁻¹ * b = a⁻¹ * b

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ a * b⁻¹ = a * b⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
n : ℤ
I : FractionalIdeal R⁰ K
hI : ¬I = 0
⊢ count K v 1 = 0

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
n : ℤ
I : FractionalIdeal R⁰ K
hI : ¬I = 0
⊢ count K v 1 = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe
a x✝ : ℝ≥0
h : a < x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹

Tactic:
]

Goal state after:
case coe
a x✝ : ℝ≥0
h : a < x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹