mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case pos
ι : Sort u_1
f : ι → ℝ≥0
h : BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i

pp: case neg
ι : Sort u_1
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i

Tactic:
·

Goal state after:
case pos
ι : Sort u_1
f : ι → ℝ≥0
h : BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case neg
ι : Sort u_1
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i

Tactic:
·

Goal state after:
case neg
ι : Sort u_1
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
⊢ ∞ + ⨆ i, f i = ⨆ i, ∞ + f i

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

Tactic:
·

Goal state after:
case inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
⊢ ∞ + ⨆ i, f i = ⨆ i, ∞ + f i
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ iSup f + iSup g ≤ a

Tactic:
by simp_rw [iSup_add, add_iSup]; exact iSup₂_le h

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

Goal state before:
pp: case inl
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : IsEmpty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

pp: case inr
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
·

Goal state after:
case inl
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : IsEmpty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
·

Goal state after:
case inr
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot
hx : ⊥ ≠ ⊤ ∧ ⊥ ≠ ⊥
⊢ ∃ y, ↑y = ⊥

pp: case coe
a✝ : ℝ
hx : ↑a✝ ≠ ⊤ ∧ ↑a✝ ≠ ⊥
⊢ ∃ y, ↑y = ↑a✝

pp: case top
hx : ⊤ ≠ ⊤ ∧ ⊤ ≠ ⊥
⊢ ∃ y, ↑y = ⊤

Tactic:
·

Goal state after:
case bot
hx : ⊥ ≠ ⊤ ∧ ⊥ ≠ ⊥
⊢ ∃ y, ↑y = ⊥
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case coe
a✝ : ℝ
hx : ↑a✝ ≠ ⊤ ∧ ↑a✝ ≠ ⊥
⊢ ∃ y, ↑y = ↑a✝

pp: case top
hx : ⊤ ≠ ⊤ ∧ ⊤ ≠ ⊥
⊢ ∃ y, ↑y = ⊤

Tactic:
·

Goal state after:
case coe
a✝ : ℝ
hx : ↑a✝ ≠ ⊤ ∧ ↑a✝ ≠ ⊥
⊢ ∃ y, ↑y = ↑a✝
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
⊢ a - ⨆ i, f i = ⨅ i, a - f i

pp: case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
h : ¬∃ i, a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
·

Goal state after:
case inl
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top
hx : ⊤ ≠ ⊤ ∧ ⊤ ≠ ⊥
⊢ ∃ y, ↑y = ⊤

Tactic:
·

Goal state after:
case top
hx : ⊤ ≠ ⊤ ∧ ⊤ ≠ ⊥
⊢ ∃ y, ↑y = ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot
hx : 0 ≤ ⊥
⊢ 0 ≤ ⊥.toReal

pp: case coe
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ 0 ≤ (↑a✝).toReal

pp: case top
hx : 0 ≤ ⊤
⊢ 0 ≤ ⊤.toReal

Tactic:
·

Goal state after:
case bot
hx : 0 ≤ ⊥
⊢ 0 ≤ ⊥.toReal
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case coe
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ 0 ≤ (↑a✝).toReal

pp: case top
hx : 0 ≤ ⊤
⊢ 0 ≤ ⊤.toReal

Tactic:
·

Goal state after:
case coe
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ 0 ≤ (↑a✝).toReal
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top
hx : 0 ≤ ⊤
⊢ 0 ≤ ⊤.toReal

Tactic:
·

Goal state after:
case top
hx : 0 ≤ ⊤
⊢ 0 ≤ ⊤.toReal
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot
hx : ⊥ ≤ 0
⊢ ⊥.toReal ≤ 0

pp: case coe
a✝ : ℝ
hx : ↑a✝ ≤ 0
⊢ (↑a✝).toReal ≤ 0

pp: case top
hx : ⊤ ≤ 0
⊢ ⊤.toReal ≤ 0

Tactic:
·

Goal state after:
case bot
hx : ⊥ ≤ 0
⊢ ⊥.toReal ≤ 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case coe
a✝ : ℝ
hx : ↑a✝ ≤ 0
⊢ (↑a✝).toReal ≤ 0

pp: case top
hx : ⊤ ≤ 0
⊢ ⊤.toReal ≤ 0

Tactic:
·

Goal state after:
case coe
a✝ : ℝ
hx : ↑a✝ ≤ 0
⊢ (↑a✝).toReal ≤ 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top
hx : ⊤ ≤ 0
⊢ ⊤.toReal ≤ 0

Tactic:
·

Goal state after:
case top
hx : ⊤ ≤ 0
⊢ ⊤.toReal ≤ 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case mp
x : ℝ
⊢ x ∈ toReal '' Ioo 0 ⊤ → x ∈ Ioi 0

pp: case mpr
x : ℝ
⊢ x ∈ Ioi 0 → x ∈ toReal '' Ioo 0 ⊤

Tactic:
·

Goal state after:
case mp
x : ℝ
⊢ x ∈ toReal '' Ioo 0 ⊤ → x ∈ Ioi 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case mpr
x : ℝ
⊢ x ∈ Ioi 0 → x ∈ toReal '' Ioo 0 ⊤

Tactic:
·

Goal state after:
case mpr
x : ℝ
⊢ x ∈ Ioi 0 → x ∈ toReal '' Ioo 0 ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case mp
x : ℝ
⊢ x ∈ toReal '' Ioo ⊥ 0 → x ∈ Iio 0

pp: case mpr
x : ℝ
⊢ x ∈ Iio 0 → x ∈ toReal '' Ioo ⊥ 0

Tactic:
·

Goal state after:
case mp
x : ℝ
⊢ x ∈ toReal '' Ioo ⊥ 0 → x ∈ Iio 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case mpr
x : ℝ
⊢ x ∈ Iio 0 → x ∈ toReal '' Ioo ⊥ 0

Tactic:
·

Goal state after:
case mpr
x : ℝ
⊢ x ∈ Iio 0 → x ∈ toReal '' Ioo ⊥ 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
⊢ ↑x.toReal = x

Tactic:
lift x to ℝ using ⟨hx, h'x⟩
  rfl

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

Goal state before:
pp: case pos
x : EReal
h : x ≠ ⊤
h' : x = ⊥
⊢ x ≤ ↑x.toReal

pp: case neg
x : EReal
h : x ≠ ⊤
h' : ¬x = ⊥
⊢ x ≤ ↑x.toReal

Tactic:
·

Goal state after:
case pos
x : EReal
h : x ≠ ⊤
h' : x = ⊥
⊢ x ≤ ↑x.toReal
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case neg
x : EReal
h : x ≠ ⊤
h' : ¬x = ⊥
⊢ x ≤ ↑x.toReal

Tactic:
·

Goal state after:
case neg
x : EReal
h : x ≠ ⊤
h' : ¬x = ⊥
⊢ x ≤ ↑x.toReal
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case pos
x : EReal
h : x ≠ ⊥
h' : x = ⊤
⊢ ↑x.toReal ≤ x

pp: case neg
x : EReal
h : x ≠ ⊥
h' : ¬x = ⊤
⊢ ↑x.toReal ≤ x

Tactic:
·

Goal state after:
case pos
x : EReal
h : x ≠ ⊥
h' : x = ⊤
⊢ ↑x.toReal ≤ x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case neg
x : EReal
h : x ≠ ⊥
h' : ¬x = ⊤
⊢ ↑x.toReal ≤ x

Tactic:
·

Goal state after:
case neg
x : EReal
h : x ≠ ⊥
h' : ¬x = ⊤
⊢ ↑x.toReal ≤ x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case mp
x : EReal
⊢ x = ⊤ → ∀ (y : ℝ), ↑y < x

pp: case mpr
x : EReal
⊢ (∀ (y : ℝ), ↑y < x) → x = ⊤

Tactic:
·

Goal state after:
case mp
x : EReal
⊢ x = ⊤ → ∀ (y : ℝ), ↑y < x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case mpr
x : EReal
⊢ (∀ (y : ℝ), ↑y < x) → x = ⊤

Tactic:
·

Goal state after:
case mpr
x : EReal
⊢ (∀ (y : ℝ), ↑y < x) → x = ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case mp
x : EReal
⊢ x = ⊥ → ∀ (y : ℝ), x < ↑y

pp: case mpr
x : EReal
⊢ (∀ (y : ℝ), x < ↑y) → x = ⊥

Tactic:
·

Goal state after:
case mp
x : EReal
⊢ x = ⊥ → ∀ (y : ℝ), x < ↑y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case mpr
x : EReal
⊢ (∀ (y : ℝ), x < ↑y) → x = ⊥

Tactic:
·

Goal state after:
case mpr
x : EReal
⊢ (∀ (y : ℝ), x < ↑y) → x = ⊥
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 I' : FractionalIdeal R⁰ K
inst✝ : Decidable (I ≠ 0 ∧ I' ≠ 0)
h : I ≠ 0 ∧ I' ≠ 0
⊢ count K v (I * I') = count K v I + count K v I'

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 ≠ 0 ∧ I' ≠ 0)
⊢ count K v (I * I') = 0

Tactic:
·

Goal state after:
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 I' : FractionalIdeal R⁰ K
inst✝ : Decidable (I ≠ 0 ∧ I' ≠ 0)
h : I ≠ 0 ∧ I' ≠ 0
⊢ count K v (I * I') = count K v I + count K v I'
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 ≠ 0 ∧ 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 ≠ 0 ∧ I' ≠ 0)
⊢ count K v (I * I') = 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' Ioo ↑x ↑y = Ioo x y

Tactic:
by
  simp_rw [← Ioi_inter_Iio]
  simp

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
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = ↑(n + 1) * count K v I

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
⊢ (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 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
⊢ (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: case inl
⊢ ↑(∞ * ↑0) = ⊤ * ↑↑0

pp: case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑(∞ * ↑x) = ⊤ * ↑↑x

Tactic:
·

Goal state after:
case inl
⊢ ↑(∞ * ↑0) = ⊤ * ↑↑0
Module: Mathlib.Data.EReal.Basic

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

Tactic:
·

Goal state after:
case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑(∞ * ↑x) = ⊤ * ↑↑x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inl
n : ℕ
⊢ (↑0 ^ (n + 1))⁻¹ = (↑0)⁻¹ ^ (n + 1)

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

Tactic:
·

Goal state after:
case inl
n : ℕ
⊢ (↑0 ^ (n + 1))⁻¹ = (↑0)⁻¹ ^ (n + 1)
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case pos
x : EReal
h : x = ⊤
⊢ x.toENNReal = ∞ ↔ x = ⊤

pp: case neg
x : EReal
h : ¬x = ⊤
⊢ x.toENNReal = ∞ ↔ x = ⊤

Tactic:
·

Goal state after:
case pos
x : EReal
h : x = ⊤
⊢ x.toENNReal = ∞ ↔ x = ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case neg
x : EReal
h : ¬x = ⊤
⊢ x.toENNReal = ∞ ↔ x = ⊤

Tactic:
·

Goal state after:
case neg
x : EReal
h : ¬x = ⊤
⊢ x.toENNReal = ∞ ↔ x = ⊤
Module: Mathlib.Data.ENNReal.Inv

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

Tactic:
·

Goal state after:
case inr
a : ℝ≥0
n : ℕ
ha : a ≠ 0
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)
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
Module: Mathlib.Data.EReal.Basic

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

Tactic:
·

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

Goal state before:
pp: case inl
b : ℝ≥0∞
ha₀ : 0 = 0 → b = 0
ha : 0 = ∞ → b = 0
⊢ 0⁻¹ * (0 * b) = b

pp: case inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha : a = ∞ → b = 0
ha₀ : a ≠ 0
⊢ a⁻¹ * (a * b) = b

Tactic:
·

Goal state after:
case inl
b : ℝ≥0∞
ha₀ : 0 = 0 → b = 0
ha : 0 = ∞ → b = 0
⊢ 0⁻¹ * (0 * b) = b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl
b : ℝ≥0∞
ha₀✝ : ∞ = 0 → b = 0
ha : ∞ = ∞ → b = 0
ha₀ : ∞ ≠ 0
⊢ ∞⁻¹ * (∞ * b) = b

pp: case inr.inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha✝ : a = ∞ → b = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a⁻¹ * (a * b) = b

Tactic:
·

Goal state after:
case inr.inl
b : ℝ≥0∞
ha₀✝ : ∞ = 0 → b = 0
ha : ∞ = ∞ → b = 0
ha₀ : ∞ ≠ 0
⊢ ∞⁻¹ * (∞ * b) = b
Module: Mathlib.Data.EReal.Basic

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

pp: case neg
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ ↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) = x

Tactic:
·

Goal state after:
case pos
x : EReal
hx : 0 ≤ x
h_top : x = ⊤
⊢ ↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) = x
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
⊢ (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 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
⊢ (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.ENNReal.Inv

Goal state before:
pp: case inr.inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha✝ : a = ∞ → b = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a⁻¹ * (a * b) = b

Tactic:
·

Goal state after:
case inr.inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha✝ : a = ∞ → b = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a⁻¹ * (a * b) = b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inl
b : ℝ≥0∞
ha₀ : 0 = 0 → b = 0
ha : 0 = ∞ → b = 0
⊢ 0 * (0⁻¹ * b) = b

pp: case inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha : a = ∞ → b = 0
ha₀ : a ≠ 0
⊢ a * (a⁻¹ * b) = b

Tactic:
·

Goal state after:
case inl
b : ℝ≥0∞
ha₀ : 0 = 0 → b = 0
ha : 0 = ∞ → b = 0
⊢ 0 * (0⁻¹ * b) = b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl
b : ℝ≥0∞
ha₀✝ : ∞ = 0 → b = 0
ha : ∞ = ∞ → b = 0
ha₀ : ∞ ≠ 0
⊢ ∞ * (∞⁻¹ * b) = b

pp: case inr.inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha✝ : a = ∞ → b = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * (a⁻¹ * b) = b

Tactic:
·

Goal state after:
case inr.inl
b : ℝ≥0∞
ha₀✝ : ∞ = 0 → b = 0
ha : ∞ = ∞ → b = 0
ha₀ : ∞ ≠ 0
⊢ ∞ * (∞⁻¹ * b) = b
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case inl
x : EReal
hx : 0 ≤ x
⊢ ↑x.toENNReal = max 0 x

pp: case inr
x : EReal
hx : x ≤ 0
⊢ ↑x.toENNReal = max 0 x

Tactic:
·

Goal state after:
case inl
x : EReal
hx : 0 ≤ x
⊢ ↑x.toENNReal = max 0 x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha✝ : a = ∞ → b = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * (a⁻¹ * b) = b

Tactic:
·

Goal state after:
case inr.inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha✝ : a = ∞ → b = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * (a⁻¹ * b) = b
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case inr
x : EReal
hx : x ≤ 0
⊢ ↑x.toENNReal = max 0 x

Tactic:
·

Goal state after:
case inr
x : EReal
hx : x ≤ 0
⊢ ↑x.toENNReal = max 0 x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case pos
x : ℝ≥0∞
h_top : x = ∞
⊢ (↑x).toENNReal = x

pp: case neg
x : ℝ≥0∞
h_top : ¬x = ∞
⊢ (↑x).toENNReal = x

Tactic:
·

Goal state after:
case pos
x : ℝ≥0∞
h_top : x = ∞
⊢ (↑x).toENNReal = x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inl
a : ℝ≥0∞
hb₀ : 0 = 0 → a = 0
hb : 0 = ∞ → a = 0
⊢ a * 0 * 0⁻¹ = a

pp: case inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb : b = ∞ → a = 0
hb₀ : b ≠ 0
⊢ a * b * b⁻¹ = a

Tactic:
·

Goal state after:
case inl
a : ℝ≥0∞
hb₀ : 0 = 0 → a = 0
hb : 0 = ∞ → a = 0
⊢ a * 0 * 0⁻¹ = a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl
a : ℝ≥0∞
hb₀✝ : ∞ = 0 → a = 0
hb : ∞ = ∞ → a = 0
hb₀ : ∞ ≠ 0
⊢ a * ∞ * ∞⁻¹ = a

pp: case inr.inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb✝ : b = ∞ → a = 0
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a * b * b⁻¹ = a

Tactic:
·

Goal state after:
case inr.inl
a : ℝ≥0∞
hb₀✝ : ∞ = 0 → a = 0
hb : ∞ = ∞ → a = 0
hb₀ : ∞ ≠ 0
⊢ a * ∞ * ∞⁻¹ = a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb✝ : b = ∞ → a = 0
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a * b * b⁻¹ = a

Tactic:
·

Goal state after:
case inr.inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb✝ : b = ∞ → a = 0
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a * b * b⁻¹ = a
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case pos
x : EReal
hx : 0 ≤ x
h : x = ⊤
⊢ x.toENNReal.toReal = x.toReal

pp: case neg
x : EReal
hx : 0 ≤ x
h : ¬x = ⊤
⊢ x.toENNReal.toReal = x.toReal

Tactic:
·

Goal state after:
case pos
x : EReal
hx : 0 ≤ x
h : x = ⊤
⊢ x.toENNReal.toReal = x.toReal
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case neg
x : EReal
hx : 0 ≤ x
h : ¬x = ⊤
⊢ x.toENNReal.toReal = x.toReal

Tactic:
·

Goal state after:
case neg
x : EReal
hx : 0 ≤ x
h : ¬x = ⊤
⊢ x.toENNReal.toReal = x.toReal
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inl
a : ℝ≥0∞
hb₀ : 0 = 0 → a = 0
hb : 0 = ∞ → a = 0
⊢ a * 0⁻¹ * 0 = a

pp: case inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb : b = ∞ → a = 0
hb₀ : b ≠ 0
⊢ a * b⁻¹ * b = a

Tactic:
·

Goal state after:
case inl
a : ℝ≥0∞
hb₀ : 0 = 0 → a = 0
hb : 0 = ∞ → a = 0
⊢ a * 0⁻¹ * 0 = a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl
a : ℝ≥0∞
hb₀✝ : ∞ = 0 → a = 0
hb : ∞ = ∞ → a = 0
hb₀ : ∞ ≠ 0
⊢ a * ∞⁻¹ * ∞ = a

pp: case inr.inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb✝ : b = ∞ → a = 0
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a * b⁻¹ * b = a

Tactic:
·

Goal state after:
case inr.inl
a : ℝ≥0∞
hb₀✝ : ∞ = 0 → a = 0
hb : ∞ = ∞ → a = 0
hb₀ : ∞ ≠ 0
⊢ a * ∞⁻¹ * ∞ = a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb✝ : b = ∞ → a = 0
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a * b⁻¹ * b = a

Tactic:
·

Goal state after:
case inr.inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb✝ : b = ∞ → a = 0
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a * b⁻¹ * b = a
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot
y : EReal
h : ⊥ ≤ y
⊢ ⊥.toENNReal ≤ y.toENNReal

pp: case coe
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
⊢ (↑a✝).toENNReal ≤ y.toENNReal

pp: case top
y : EReal
h : ⊤ ≤ y
⊢ ⊤.toENNReal ≤ y.toENNReal

Tactic:
·

Goal state after:
case bot
y : EReal
h : ⊥ ≤ y
⊢ ⊥.toENNReal ≤ y.toENNReal
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case coe
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
⊢ (↑a✝).toENNReal ≤ y.toENNReal

pp: case top
y : EReal
h : ⊤ ≤ y
⊢ ⊤.toENNReal ≤ y.toENNReal

Tactic:
·

Goal state after:
case coe
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
⊢ (↑a✝).toENNReal ≤ y.toENNReal
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case pos
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
hy_top : y = ⊤
⊢ (↑a✝).toENNReal ≤ y.toENNReal

pp: case neg
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
hy_top : ¬y = ⊤
⊢ (↑a✝).toENNReal ≤ y.toENNReal

Tactic:
·

Goal state after:
case pos
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
hy_top : y = ⊤
⊢ (↑a✝).toENNReal ≤ y.toENNReal
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top
y : EReal
h : ⊤ ≤ y
⊢ ⊤.toENNReal ≤ y.toENNReal

Tactic:
·

Goal state after:
case top
y : EReal
h : ⊤ ≤ y
⊢ ⊤.toENNReal ≤ y.toENNReal
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x✝ : ↑{⊥, ⊤}ᶜ
x : EReal
hx : x ∈ {⊥, ⊤}ᶜ
⊢ x ≠ ⊤ ∧ x ≠ ⊥

pp: x✝ : ↑{⊥, ⊤}ᶜ
x : ℝ
hx : ↑x ∈ {⊥, ⊤}ᶜ
⊢ (fun x ↦ ⟨↑x, ⋯⟩) ((fun x ↦ (↑x).toReal) ⟨↑x, hx⟩) = ⟨↑x, hx⟩

Tactic:
·

Goal state after:
x✝ : ↑{⊥, ⊤}ᶜ
x : EReal
hx : x ∈ {⊥, ⊤}ᶜ
⊢ x ≠ ⊤ ∧ x ≠ ⊥
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x✝ : ↑{⊥, ⊤}ᶜ
x : ℝ
hx : ↑x ∈ {⊥, ⊤}ᶜ
⊢ (fun x ↦ ⟨↑x, ⋯⟩) ((fun x ↦ (↑x).toReal) ⟨↑x, hx⟩) = ⟨↑x, hx⟩

Tactic:
·

Goal state after:
x✝ : ↑{⊥, ⊤}ᶜ
x : ℝ
hx : ↑x ∈ {⊥, ⊤}ᶜ
⊢ (fun x ↦ ⟨↑x, ⋯⟩) ((fun x ↦ (↑x).toReal) ⟨↑x, hx⟩) = ⟨↑x, hx⟩
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
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)

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 (I ^ (-n)) = -count K v (I ^ n)

Tactic:
·

Goal state after:
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
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)
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
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)

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
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)

Tactic:
·

Goal state after:
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
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case pos.top
a b c d : ℝ≥0∞
r p q : ℝ≥0
h✝ : ∞ = 0
⊢ ∞⁻¹⁻¹ = ∞

Tactic:
simp_all [-coe_inv, (coe_inv _).symm]

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

Goal state before:
pp: case pos.coe
a b c d : ℝ≥0∞
r p q x✝ : ℝ≥0
h✝ : ↑x✝ = 0
⊢ (↑x✝)⁻¹⁻¹ = ↑x✝

Tactic:
simp_all [-coe_inv, (coe_inv _).symm]

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

Goal state before:
pp: case neg.top
a b c d : ℝ≥0∞
r p q : ℝ≥0
h✝ : ¬∞ = 0
⊢ ∞⁻¹⁻¹ = ∞

Tactic:
simp_all [-coe_inv, (coe_inv _).symm]

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

Goal state before:
pp: case neg.coe
a b c d : ℝ≥0∞
r p q x✝ : ℝ≥0
h✝ : ¬↑x✝ = 0
⊢ (↑x✝)⁻¹⁻¹ = ↑x✝

Tactic:
simp_all [-coe_inv, (coe_inv _).symm]

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
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)

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
hn : ¬n = 0
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)
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 (I ^ (-n)) = -count K v (I ^ n)

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 (I ^ (-n)) = -count K v (I ^ n)