mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ≥0
⊢ ↑(↑x * ∞) = ↑↑x * ↑∞

Tactic:
by

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

Goal state before:
pp: x y : ℝ≥0
⊢ ↑(↑x * ↑y) = ↑↑x * ↑↑y

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : EReal
hx : x ≤ 0
⊢ x.toENNReal = 0

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
h0 : a ≠ 0
ht : a ≠ ∞
⊢ a * a⁻¹ = 1

Tactic:
by

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

Goal state before:
pp: x : EReal
⊢ x.toENNReal = 0 ↔ x ≤ 0

Tactic:
by

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

Goal state before:
pp: x : EReal
⊢ x.toENNReal ≠ 0 ↔ 0 < x

Tactic:
by

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

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

Tactic:
by

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:
· have h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0) := by order
      rw [if_neg h_neg, hI, count_zero, mul_zero]

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: a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ∞ → b = 0
⊢ a⁻¹ * (a * b) = b

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
x✝ : x = ⊥
⊢ False

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : EReal
⊢ ↑x.toENNReal = max 0 x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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 : ℕ
I : FractionalIdeal R⁰ K
⊢ count K v (I ^ n) = ↑n * count K v I

Tactic:
by

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

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

Tactic:
by

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
⊢ ↑v.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal

Tactic:
by

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
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x y : EReal
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x.toENNReal = y.toENNReal ↔ x = y

Tactic:
by

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

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

Tactic:
by_cases hy_top : y = ⊤
    · simp [hy_top]
    simp only [toENNReal, coe_ne_top, ↓reduceIte, toReal_coe, hy_top]
    exact ENNReal.ofReal_le_ofReal <| EReal.toReal_le_toReal h (coe_ne_bot _) hy_top

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

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

Tactic:
by

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

Goal state before:
pp: x y : EReal
h : x ≤ y
⊢ x.toENNReal ≤ y.toENNReal

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b : ℝ
h : ↑a < ↑b
⊢ ∃ x, ↑a < ↑↑x ∧ ↑↑x < ↑b

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
⊢ a / b * c = a * (c / b)

Tactic:
by

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

Goal state before:
pp: a : ℝ
x✝ : ↑a < ⊤
b : ℚ
hab : a < ↑b
⊢ ↑a < ↑↑b

Tactic:
by

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

Goal state before:
pp: a : ℝ
x✝ : ⊥ < ↑a
b : ℚ
hab : ↑b < a
⊢ ↑↑b < ↑a

Tactic:
by

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
⊢ count K v ↑v.asIdeal = 1

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ↑x ∈ {⊥, ⊤}ᶜ

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
⊢ a * b / c = a / c * b

Tactic:
by

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

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

Tactic:
by

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 : ℕ
⊢ count K v (↑v.asIdeal ^ n) = ↑n

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ (fun x ↦ (↑x).toReal) ((fun x ↦ ⟨↑x, ⋯⟩) x) = x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹ ≠ ∞ ↔ a ≠ 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹ ≠ 0 ↔ a ≠ ∞

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : a ≠ ∞ ∨ b ≠ 0
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ c * a / (c * b) = a / b

Tactic:
by

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

Goal state before:
pp: c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ a * c / (b * c) = a / b

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ 0 < b → b < a → c⁻¹ ≠ ∞

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) / c = a / c - b / c

Tactic:
by

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

Goal state before:
pp: ⊢ StrictAnti Inv.inv

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ a⁻¹ < b ↔ b⁻¹ < a

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ a < b⁻¹ ↔ b < a⁻¹

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1

Tactic:
by

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 : ℤ
I : FractionalIdeal R⁰ K
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹ < 1 ↔ 1 < a

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ 1 < a⁻¹ ↔ a < 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ ∞ / a = if a = ∞ then 0 else ∞

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
h : a ≠ ∞
⊢ ∞ / a = ∞

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ a / b = ∞ ↔ a ≠ 0 ∧ b = 0 ∨ a = ∞ ∧ b ≠ ∞

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
⊢ a / (a / b) = b

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
h₀ : a ≠ 0
h₁ : a ≠ ∞
⊢ a = 0 → b = 0

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
h₀ : a ≠ 0
h₁ : a ≠ ∞
⊢ a = ∞ → b = 0

Tactic:
by

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 : FractionalIdeal R⁰ K
⊢ count K v I⁻¹ = -count K v I

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
ht : b ≠ ∞ ∨ c ≠ ∞
⊢ a ≤ c / b ↔ a * b ≤ c

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
this : a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹
⊢ a / b ≤ c ↔ a ≤ c * b

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ a / b ≤ c ↔ a ≤ c * b

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
⊢ a = 0

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
h : a ≤ b * c
⊢ a / c ≤ b

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a ≤ 1 * a

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹ * a ≤ 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
h : a ≤ b / c
⊢ a * c ≤ b

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
h : a < b / c
⊢ a * c < b

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
h : a < b * c
⊢ a < b / c⁻¹

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
h : a < b * c
⊢ a < c * b

Tactic:
by

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

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

Tactic:
by

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 : ℤ
I : FractionalIdeal R⁰ K
⊢ count K v (I ^ n) = n * count K v I

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ b⁻¹ < c⁻¹ ↔ c < b

Tactic:
by

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 : ℤ
⊢ count K v (↑v.asIdeal ^ n) = n

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ ∞
hb₀ : ∞ ≠ 0
⊢ 0 < 1 ∧ 1 * a < ∞

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a + 1 ≠ ∞

Tactic:
by

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 w : HeightOneSpectrum R
hw : w ≠ v
⊢ ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
⊢ ∃ c, 0 < c ∧ c * a < b

Tactic:
by

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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
by

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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ Irreducible (Associates.mk w.asIdeal)

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
h₁ : b = ∞ → a ≠ 0
h₂ : a = ∞ → b ≠ 0
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ a ≤ b⁻¹ ↔ a * b ≤ 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b r : ℝ≥0∞
hr₀ : r ≠ 0
hr₁ : r ≠ ∞
⊢ r * a ≤ b ↔ a ≤ r⁻¹ * b

Tactic:
by

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

Goal state before:
pp: x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y
⊢ x ≤ y

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : b = c / a
⊢ a * b = c

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : a * b = c
⊢ b = c / a

Tactic:
by

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

Goal state before:
pp: a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
⊢ c / b = d / a ↔ a * c = b * d

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
hb₀ : b ≠ 0
hb₁ : b ≠ ∞
h : a / b = 1
⊢ a = b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ 3⁻¹ + 3⁻¹ + 3⁻¹ = 1

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a / 2 + a / 2 = a

Tactic:
by

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 w : HeightOneSpectrum R
hw : w ≠ v
⊢ count K v ↑w.asIdeal = 0

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a / 3 + a / 3 + a / 3 = a

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ a / b = 0 ↔ a = 0 ∨ b = ∞

Tactic:
by

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 w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
⊢ count K v ↑w.asIdeal = if w = v then 1 else 0

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ 0 < a / b ↔ a ≠ 0 ∧ b ≠ ∞

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ ∞

Tactic:
by

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

Goal state before:
pp: b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ a / b * c = a / (b / c)

Tactic:
by

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

Goal state before:
pp: a b c d : ℝ≥0∞
hc : c ≠ 0 ∨ d ≠ ∞
hd : c ≠ ∞ ∨ d ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
hz : a ≠ 0
ht : a ≠ ∞
⊢ a / 2 < a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
hc✝ : c < a * b
a' : ℝ≥0∞
hc : c / b < a'
ha' : a' < a
⊢ b ≠ 0

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
hc✝ : c < a * b
a' : ℝ≥0∞
hc : c / b < a'
ha' : a' < a
⊢ c ≠ ∞

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
hc : c < a * b
⊢ ∃ a' < a, c < a' * b

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
hc : c < a * b
⊢ ∃ b' < b, c < a * b'

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
by

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
exps : HeightOneSpectrum R → ℤ
⊢ count K v (∏ᶠ (w : HeightOneSpectrum R) (_ : w ≠ v), ↑w.asIdeal ^ exps w) = 0

Tactic:
by

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

Goal state before:
pp: a b c : ℝ≥0∞
h₁ : a ≠ 0 ∨ b ≠ ∞
h₂ : a ≠ ∞ ∨ b ≠ 0
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ c ≤ a * b

Tactic:
by

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

Goal state before:
pp: a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ℝ≥0∞ ≃o ↑(Iic 1)

Tactic:
by

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

Goal state before:
pp: a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
x✝¹ x✝ : ↑(Iic a)
⊢ { toFun := fun x ↦ ⟨↑↑x, ⋯⟩, invFun := fun x ↦ ⟨(↑x).toNNReal, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } x✝¹ ≤
      { toFun := fun x ↦ ⟨↑↑x, ⋯⟩, invFun := fun x ↦ ⟨(↑x).toNNReal, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } x✝ ↔
    x✝¹ ≤ x✝

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
h : a ≠ 0
⊢ ∃ n, (↑n)⁻¹ < a⁻¹⁻¹

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ 0
hb : b ≠ ∞
n : ℕ
hn : b / a < ↑n
⊢ b < ↑n * a

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
⊢ ∃ n > 0, (↑n)⁻¹ * a < b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝ : LT β
U : Filter (α × α)
z : β
D : α → α → β
H : ∀ (s : Set (α × α)), s ∈ U ↔ ∃ ε > z, ∀ {a b : α}, D a b < ε → (a, b) ∈ s
s : Set (α × α)
⊢ s ∈ U ↔ ∃ i > z, {p | D p.1 p.2 < i} ⊆ s

Tactic:
by

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
exps : HeightOneSpectrum R →₀ ℤ
⊢ count K v (exps.prod fun x1 x2 ↦ ↑x1.asIdeal ^ x2) = exps v

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
⊢ ∃ n > 0, ↑n * a < b

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ 0
⊢ ∃ n, 2⁻¹ ^ n < a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u_2
m m' : PseudoEMetricSpace α
h : m.toEDist = m'.toEDist
⊢ m = m'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist z x + edist z y

Tactic:
by

Goal state after: