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

Goal state before:
pp: case top
a : ℝ≥0
h : ↑a < ∞
⊢ ∞⁻¹ < (↑a)⁻¹

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

Tactic:
·

Goal state after:
case top
a : ℝ≥0
h : ↑a < ∞
⊢ ∞⁻¹ < (↑a)⁻¹
Module: Mathlib.Data.ENNReal.Inv

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

pp: case coe.inr
a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ (↑x✝)⁻¹ < (↑a)⁻¹

Tactic:
·

Goal state after:
case coe.inl
x✝ : ℝ≥0
h : 0 < x✝
⊢ (↑x✝)⁻¹ < (↑0)⁻¹
Module: Mathlib.Data.ENNReal.Inv

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

pp: case inr
a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
ha : a ≠ 0
⊢ a / (a / b) = b

Tactic:
·

Goal state after:
case inl
b : ℝ≥0∞
h₀ : 0 = 0 → b = 0
h₁ : 0 = ∞ → b = 0
⊢ 0 / (0 / b) = b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl
b : ℝ≥0∞
h₀ : ∞ = 0 → b = 0
h₁ : ∞ = ∞ → b = 0
ha : ∞ ≠ 0
⊢ ∞ / (∞ / b) = b

pp: case inr.inr
a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
ha : a ≠ 0
ha' : a ≠ ∞
⊢ a / (a / b) = b

Tactic:
·

Goal state after:
case inr.inl
b : ℝ≥0∞
h₀ : ∞ = 0 → b = 0
h₁ : ∞ = ∞ → b = 0
ha : ∞ ≠ 0
⊢ ∞ / (∞ / b) = b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inl
a c : ℝ≥0∞
h0 : ↑0 ≠ 0 ∨ c ≠ 0
ht : ↑0 ≠ ∞ ∨ c ≠ ∞
⊢ a ≤ c / ↑0 ↔ a * ↑0 ≤ c

pp: case coe.inr
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
hb : b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c

Tactic:
·

Goal state after:
case coe.inl
a c : ℝ≥0∞
h0 : ↑0 ≠ 0 ∨ c ≠ 0
ht : ↑0 ≠ ∞ ∨ c ≠ ∞
⊢ a ≤ c / ↑0 ↔ a * ↑0 ≤ c
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inr
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
hb : b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c

Tactic:
·

Goal state after:
case coe.inr
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
hb : b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case ofNat
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 : ℕ
⊢ count K v (I ^ ofNat n) = ofNat n * count K v I

pp: case negSucc
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 : ℕ
⊢ count K v (I ^ -[n+1]) = -[n+1] * count K v I

Tactic:
·

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

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

pp: case neg
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
⊢ a / c ≤ b

Tactic:
·

Goal state after:
case pos
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
⊢ a / c ≤ b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case pos
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
hinf : c = ∞
⊢ a / c ≤ b

pp: case neg
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
hinf : ¬c = ∞
⊢ a / c ≤ b

Tactic:
·

Goal state after:
case pos
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
hinf : c = ∞
⊢ a / c ≤ b
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case negSucc
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 : ℕ
⊢ count K v (I ^ -[n+1]) = -[n+1] * count K v I

Tactic:
·

Goal state after:
case negSucc
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 : ℕ
⊢ count K v (I ^ -[n+1]) = -[n+1] * count K v I
Module: Mathlib.Data.ENNReal.Inv

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

pp: case inr
a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ ∃ c, 0 < c ∧ c * a < b

Tactic:
·

Goal state after:
case inl
a : ℝ≥0∞
ha : a ≠ ∞
hb₀ : ∞ ≠ 0
⊢ ∃ c, 0 < c ∧ c * a < ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case h0
a b : ℝ≥0∞
⊢ b ≠ 0 ∨ 1 ≠ 0

Tactic:
·

Goal state after:
case h0
a b : ℝ≥0∞
⊢ b ≠ 0 ∨ 1 ≠ 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ht
a b : ℝ≥0∞
⊢ b ≠ ∞ ∨ 1 ≠ ∞

Tactic:
·

Goal state after:
case ht
a b : ℝ≥0∞
⊢ b ≠ ∞ ∨ 1 ≠ ∞
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 w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
h : w = v
⊢ count K v ↑w.asIdeal = 1

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 w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
h : ¬w = v
⊢ count K v ↑w.asIdeal = 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 w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
h : w = v
⊢ count K v ↑w.asIdeal = 1
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 w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
h : ¬w = v
⊢ count K v ↑w.asIdeal = 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 w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
h : ¬w = v
⊢ count K v ↑w.asIdeal = 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case hp₀
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 1 = 0

pp: case hp₁
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 → ℤ
⊢ ∀ (x y : FractionalIdeal R⁰ K), count K v x = 0 → count K v y = 0 → count K v (x * y) = 0

pp: case hp₂
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 → ℤ
⊢ ∀ x ∈ fun i ↦ i = v → False, count K v (↑x.asIdeal ^ exps x) = 0

Tactic:
·

Goal state after:
case hp₀
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 1 = 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case hp₁
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 → ℤ
⊢ ∀ (x y : FractionalIdeal R⁰ K), count K v x = 0 → count K v y = 0 → count K v (x * y) = 0

pp: case hp₂
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 → ℤ
⊢ ∀ x ∈ fun i ↦ i = v → False, count K v (↑x.asIdeal ^ exps x) = 0

Tactic:
·

Goal state after:
case hp₁
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 → ℤ
⊢ ∀ (x y : FractionalIdeal R⁰ K), count K v x = 0 → count K v y = 0 → count K v (x * y) = 0
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)

pp: case ha
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ 0 ∨ c⁻¹ ≠ ∞

pp: case hb
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ ∞ ∨ c⁻¹ ≠ 0

Tactic:
·

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

Goal state before:
pp: case ha
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ 0 ∨ c⁻¹ ≠ ∞

pp: case hb
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ ∞ ∨ c⁻¹ ≠ 0

Tactic:
·

Goal state after:
case ha
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ 0 ∨ c⁻¹ ≠ ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case hb
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ ∞ ∨ c⁻¹ ≠ 0

Tactic:
·

Goal state after:
case hb
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ ∞ ∨ c⁻¹ ≠ 0
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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : I ≠ 0 ∧ I' ≠ 0
⊢ count K v (I * I') = 0

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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v 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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : I ≠ 0 ∧ 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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v 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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : ¬(I ≠ 0 ∧ I' ≠ 0)
⊢ count K v (I * I') = 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case hp₂
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 → ℤ
⊢ ∀ x ∈ fun i ↦ i = v → False, count K v (↑x.asIdeal ^ exps x) = 0

Tactic:
·

Goal state after:
case hp₂
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 → ℤ
⊢ ∀ x ∈ fun i ↦ i = v → False, count K v (↑x.asIdeal ^ exps x) = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case refine_1
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
hxy : x < y
⊢ (fun x ↦ ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) x < (fun x ↦ ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) y

pp: case refine_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ↑(Iic 1)
⊢ ↑((fun x ↦ ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) ((fun x ↦ ((↑x)⁻¹ - 1)⁻¹) x)) = ↑x

Tactic:
·

Goal state after:
case refine_1
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
hxy : x < y
⊢ (fun x ↦ ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) x < (fun x ↦ ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) y
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case refine_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ↑(Iic 1)
⊢ ↑((fun x ↦ ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) ((fun x ↦ ((↑x)⁻¹ - 1)⁻¹) x)) = ↑x

Tactic:
·

Goal state after:
case refine_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ↑(Iic 1)
⊢ ↑((fun x ↦ ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) ((fun x ↦ ((↑x)⁻¹ - 1)⁻¹) 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
exps : HeightOneSpectrum R →₀ ℤ
⊢ ∑ i ∈ exps.support, count K v (↑i.asIdeal ^ exps i) = exps v

pp: case hS
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 →₀ ℤ
⊢ ∀ i ∈ exps.support, ↑i.asIdeal ^ exps i ≠ 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
exps : HeightOneSpectrum R →₀ ℤ
⊢ ∑ i ∈ exps.support, count K v (↑i.asIdeal ^ exps i) = exps v
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case hS
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 →₀ ℤ
⊢ ∀ i ∈ exps.support, ↑i.asIdeal ^ exps i ≠ 0

Tactic:
·

Goal state after:
case hS
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 →₀ ℤ
⊢ ∀ i ∈ exps.support, ↑i.asIdeal ^ exps i ≠ 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.ofNat n) = ↑r ^ Int.ofNat n

pp: case negSucc
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n

Tactic:
·

Goal state after:
case ofNat
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.ofNat n) = ↑r ^ Int.ofNat n
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z ≤ edist y z

pp: case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist y z ≤ edist x z

Tactic:
·

Goal state after:
case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z ≤ edist y z
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case negSucc
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n

Tactic:
·

Goal state after:
case negSucc
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist y z ≤ edist x z

Tactic:
·

Goal state after:
case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist y z ≤ edist x z
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case mp
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s) → ∃ i, p i ∧ {p | edist p.1 p.2 < f i} ⊆ s

pp: case mpr
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | edist p.1 p.2 < f i} ⊆ s) → ∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s

Tactic:
·

Goal state after:
case mp
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s) → ∃ i, p i ∧ {p | edist p.1 p.2 < f i} ⊆ s
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case e'_2
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 → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ ∏ i ∈ Finite.toFinset h_exps, ↑i.asIdeal ^ exps i =
    ∏ a ∈ { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ }.support,
      ↑a.asIdeal ^ { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ } a

pp: case e'_2.h
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 → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ (mulSupport fun v ↦ ↑v.asIdeal ^ exps v) ⊆ ↑(Finite.toFinset h_exps)

Tactic:
·

Goal state after:
case e'_2
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 → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ ∏ i ∈ Finite.toFinset h_exps, ↑i.asIdeal ^ exps i =
    ∏ a ∈ { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ }.support,
      ↑a.asIdeal ^ { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ } a
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case mpr
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | edist p.1 p.2 < f i} ⊆ s) → ∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s

Tactic:
·

Goal state after:
case mpr
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | edist p.1 p.2 < f i} ⊆ s) → ∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ 0 < a ^ Int.ofNat a✝

pp: case negSucc
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ 0 < a ^ Int.negSucc a✝

Tactic:
·

Goal state after:
case ofNat
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ 0 < a ^ Int.ofNat a✝
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case negSucc
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ 0 < a ^ Int.negSucc a✝

Tactic:
·

Goal state after:
case negSucc
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ 0 < a ^ Int.negSucc a✝
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case e'_2.h
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 → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ (mulSupport fun v ↦ ↑v.asIdeal ^ exps v) ⊆ ↑(Finite.toFinset h_exps)

Tactic:
·

Goal state after:
case e'_2.h
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 → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ (mulSupport fun v ↦ ↑v.asIdeal ^ exps v) ⊆ ↑(Finite.toFinset h_exps)
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case mp
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s) → ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s

pp: case mpr
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s) → ∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s

Tactic:
·

Goal state after:
case mp
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s) → ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ a ^ Int.ofNat a✝ < ∞

pp: case negSucc
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ a ^ Int.negSucc a✝ < ∞

Tactic:
·

Goal state after:
case ofNat
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ a ^ Int.ofNat a✝ < ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case negSucc
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ a ^ Int.negSucc a✝ < ∞

Tactic:
·

Goal state after:
case negSucc
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ a ^ Int.negSucc a✝ < ∞
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case mpr
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s) → ∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s

Tactic:
·

Goal state after:
case mpr
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s) → ∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case refine_1
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ↑y ^ n ≤ ↑x

pp: case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ↑x < ↑y ^ (n + 1)

Tactic:
·

Goal state after:
case refine_1
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ↑y ^ n ≤ ↑x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ↑x < ↑y ^ (n + 1)

Tactic:
·

Goal state after:
case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ↑x < ↑y ^ (n + 1)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case inl
α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
hs : ∅ ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
⊢ ∅ ∪ t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}

pp: case inr
α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : s ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
x : α
hx : x ∈ s
⊢ s ∪ t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}

Tactic:
·

Goal state after:
case inl
α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
hs : ∅ ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
⊢ ∅ ∪ t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case refine_1
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑y ^ n < ↑x

pp: case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑x ≤ ↑y ^ (n + 1)

Tactic:
·

Goal state after:
case refine_1
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑y ^ n < ↑x