mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ
hp : 0 ≤ p
⊢ r.toNNReal ≤ p.toNNReal ↔ r ≤ p

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ r.toNNReal ≤ 1 ↔ r ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ 1 < r.toNNReal ↔ 1 < r

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
n : ℕ
⊢ r.toNNReal ≤ ↑n ↔ r ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
n : ℕ
⊢ ↑n < r.toNNReal ↔ ↑n < r

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ
hr : 0 ≤ r
hp : 0 ≤ p
⊢ r.toNNReal = p.toNNReal ↔ r = p

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ
⊢ r.toNNReal ≤ p.toNNReal ↔ r ≤ p ∨ r ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ
hr : 0 < r
⊢ r.toNNReal ≤ p.toNNReal ↔ r ≤ p

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ 1 ≤ r.toNNReal ↔ 1 ≤ r

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ r.toNNReal < 1 ↔ r < 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: n : ℕ
r : ℝ
⊢ ↑n ≤ r.toNNReal ↔ ↑n ≤ r ∨ n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: n : ℕ
r : ℝ
⊢ r.toNNReal < ↑n ↔ r < ↑n ∧ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: n : ℕ
r : ℝ
hn : n ≠ 0
⊢ ↑n ≤ r.toNNReal ↔ ↑n ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
n : ℕ
hn : n ≠ 0
⊢ r.toNNReal < ↑n ↔ r < ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ
hr : 0 ≤ r
hp : 0 ≤ p
⊢ ↑(r + p).toNNReal = ↑(r.toNNReal + p.toNNReal)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
⊢ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
p : ℝ
hp : 0 ≤ p
⊢ r ≤ p.toNNReal ↔ ↑r ≤ p

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
p : ℝ
hr : 0 < r
hp : p < 0
⊢ r ≤ p.toNNReal ↔ ↑r ≤ p

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
p : ℝ≥0
ha : 0 ≤ r
⊢ r.toNNReal < p ↔ r < ↑p

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ (x ^ n).toNNReal = x.toNNReal ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℤ
⊢ (x ^ n).toNNReal = x.toNNReal ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
⊢ ↑(p * q).toNNReal = ↑(p.toNNReal * q.toNNReal)

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: a b c : ℝ≥0
h : a ≠ 0
⊢ a * b = a * c ↔ b = c

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: a b : ℝ≥0
ha : 0 < a
hb : b < 1
⊢ ∃ n, b ^ n < a

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ OrderedSub ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ≥0
h : r ≠ 0
⊢ r⁻¹ ≤ p ↔ 1 ≤ r * p

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ≥0
h : 1 ≤ r * p
⊢ r⁻¹ ≤ p

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ≥0
h : p ≠ 0
⊢ r ≤ p⁻¹ ↔ r * p ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ≥0
h : p ≠ 0
⊢ r < p⁻¹ ↔ r * p < 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: a b r : ℝ≥0
h : a < b / r
hr : r = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ x⁻¹ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a * x⁻¹ < 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
⊢ a ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: a b : ℝ≥0
h : a < b
⊢ a / b < 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: f : CauSeq ℝ abs
⊢ ∃ x, f ≈ const abs x

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
⊢ x⁻¹ < 1 ↔ 1 < x

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: s : Set ℝ≥0
hs : ¬BddAbove s
⊢ sSup s = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ Nonempty { r' // x < ↑r' }

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ≥0
⊢ ⨅ i, f i = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: α : Sort u_2
⊢ ⨅ x, 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
    (Associates.mk v.asIdeal).count (Associates.mk I).factors

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inr
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : ↑y ∈ s
hz : z ∈ Icc x.toNNReal (↑y).toNNReal
⊢ z ∈ toNNReal '' s

Tactic:
toNNReal_coe

Goal state after:
case inr
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : ↑y ∈ s
hz : z ∈ Icc x.toNNReal y
⊢ z ∈ toNNReal '' s
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ r, f ↑r = ⨅ q, f ↑↑q

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: s : Set ℝ
h : s.OrdConnected
⊢ (toNNReal '' s).OrdConnected

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ⊢ ¬BddAbove (range fun x ↦ ↑x)

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ ⟨|0|, ⋯⟩ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ⊢ ¬BddBelow (range fun x ↦ ↑x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ⊢ ⋃ r, Iic ↑r = univ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ⊢ ⋂ r, Iic ↑r = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ ⟨|1|, ⋯⟩ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q
⊢ 0 < q.den

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ
⊢ ⟨|x * y|, ⋯⟩ = ⟨|x|, ⋯⟩ * ⟨|y|, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ nnabs x = x.toNNReal

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ
⊢ ↑|x|.toNNReal = ↑(nnabs x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q
⊢ 0 < ↑q.den

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: n : ℕ
⊢ nnabs ↑n = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: n : ℕ
inst✝ : n.AtLeastTwo
⊢ nnabs (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I = I

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: n : ℤ
⊢ ↑n.natAbs = nnabs ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ
⊢ 0 < nnabs x ↔ x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ 0 ≤ r ∨ 0 ≤ -r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q.num / ↑q.den
⊢ 0 < ↑q.den

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ ∃ x, r = ↑x ∨ r = -↑x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : 1 < a
⊢ ∃ k, 0 < k ∧ 1 / ↑k + 1 < a

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ r = 0 ∨ ∃ x, 0 < x ∧ (r = ↑x ∨ r = -↑x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 2 ^ (2 * k) = (1 / ↑k * ↑k + 1) ^ (2 * k)

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: motive : ℝ → Prop
nonneg : ∀ (x : ℝ≥0), motive ↑x
nonpos : ∀ (x : ℝ≥0), motive ↑x → motive (-↑x)
r : ℝ
⊢ motive r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 0 ≤ 1 / ↑k

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive ↑x
neg : ∀ (x : ℝ≥0), 0 < x → motive ↑x → motive (-↑x)
r : ℝ
⊢ motive r

Tactic:
obtain rfl | ⟨r, hr, (rfl | rfl)⟩ := r.nnreal_trichotomy

Goal state after:
case inl
motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive ↑x
neg : ∀ (x : ℝ≥0), 0 < x → motive ↑x → motive (-↑x)
⊢ motive 0

case inr.inl
motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive ↑x
neg : ∀ (x : ℝ≥0), 0 < x → motive ↑x → motive (-↑x)
r : ℝ≥0
hr : 0 < r
⊢ motive ↑r

case inr.inr
motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive ↑x
neg : ∀ (x : ℝ≥0), 0 < x → motive ↑x → motive (-↑x)
r : ℝ≥0
hr : 0 < r
⊢ motive (-↑r)
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ (1 / ↑k * ↑k + 1) ^ (2 * k) ≤ ((1 / ↑k + 1) ^ k) ^ (2 * k)

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive ↑x
neg : ∀ (x : ℝ≥0), 0 < x → motive ↑x → motive (-↑x)
r : ℝ
⊢ motive r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ ((1 / ↑k + 1) ^ k) ^ (2 * k) = (1 / ↑k + 1) ^ (2 * k ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ (1 / ↑k + 1) ^ (2 * k ^ 2) < a ^ (2 * k ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : 1 < a
⊢ ∃ m, ↑m + 1 < a ^ m

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ ⨅ i, i.maxPowDividing I = I

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: b : ℝ
hb : 0 < b
⊢ ∃ n, 0 < n ∧ (↑n)⁻¹ < 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
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = ↑I

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case pos
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : g < 1
⊢ f ↑g < 1

Tactic:
rw [← map_one f]; exact hf hu1

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝² : AddGroup E
inst✝¹ : FunLike F E ℝ
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x y : E
⊢ f (x - y) ≤ max (f x) (f y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : FunLike F E ℝ
inst✝¹ : AddGroup E
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x✝¹ x✝ a : E
⊢ max (f a) (f a) ≤ f a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : FunLike F E ℝ
inst✝¹ : AddGroup E
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x✝¹ x✝ : E
⊢ ∀ (a : E), 0 ≤ f a

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
⊢ f ↑u < 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q f g : GroupSeminorm E
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
⊢ ∃ d, f ↑d < r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q✝ : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
⊢ p 1 + q 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ
hr : 0 < r
⊢ ∃ d, ↑(f ↑d) < r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q✝ : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
x : E
⊢ p x⁻¹ + q x⁻¹ = p x + q x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
⊢ ⨆ p, ↑p 1 = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ 0 = ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
a : AddUnits ℝ≥0∞
⊢ ↑a ≤ 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
f : ι → ℝ≥0∞
hf : ∀ (x : ι), f x ≠ ∞
⊢ (fun x ↦ ↑x) ∘ ENNReal.toNNReal ∘ f = f

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
h : a ≠ ∞
⊢ ENNReal.ofReal a.toReal = a

Tactic:
by

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

Goal state before:
pp: r : ℝ≥0
⊢ ↑(↑r).toNNReal ≤ ↑r

Tactic:
toNNReal_coe

Goal state after:
r : ℝ≥0
⊢ ↑r ≤ ↑r
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: r : ℝ≥0
⊢ ↑(↑r).toNNReal ≤ ↑r

Tactic:
by

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

Goal state before:
pp: r : ℝ≥0
⊢ ↑r = ENNReal.ofReal ↑r

Tactic:
by

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

Goal state before:
pp: z : ℝ≥0∞
⊢ z.toReal.toNNReal = z.toNNReal

Tactic:
by

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

Goal state before:
pp: ⊢ ENNReal.ofReal 0 = 0

Tactic:
by

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

Goal state before:
pp: ⊢ ENNReal.ofReal 1 = 1

Tactic:
by

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

Goal state before:
pp: x : ℝ≥0∞
⊢ x.toReal = 0 ↔ x = 0 ∨ x = ∞

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
h : ENNReal.ofReal a.toReal = a
⊢ a ≠ ∞

Tactic:
by

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

Goal state before:
pp: a : ℝ
h : (ENNReal.ofReal a).toReal = a
⊢ 0 ≤ a

Tactic:
by

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

Goal state before:
pp: x y : ℝ≥0∞
⊢ x.toReal = y.toReal ↔ x = y ∨ x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0

Tactic:
by

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

Goal state before:
pp: x y : ℝ≥0∞
hx : x ≠ ∞
hy : y ≠ ∞
⊢ x.toNNReal = y.toNNReal ↔ x = y

Tactic:
by

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

Goal state before:
pp: x y : ℝ≥0∞
hx : x ≠ ∞
hy : y ≠ ∞
⊢ x.toReal = y.toReal ↔ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
⊢ ⨆ P, primaryComponent M P.asIdeal = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℝ≥0∞ → α
⊢ ⨅ x, ⨅ (_ : x ≠ ∞), f x = ⨅ x, f ↑x

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ENNReal.ofReal ↑n = ↑n

Tactic:
by

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

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ↑n ≤ ↑r ↔ ↑n ≤ r

Tactic:
by

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

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ↑r ≤ ↑n ↔ r ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
x✝¹ x✝ : GroupSeminorm E
h' : x✝¹ ≤ x✝
⊢ x✝¹ x ≤ x✝ x

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (↑n).toNNReal = ↑n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (↑n).toReal = ↑n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ 0 ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
x✝¹ x✝ : GroupSeminorm E
h' : x✝¹ ≤ x✝
⊢ x✝¹ y ≤ x✝ y

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (↑n).toNNReal = (↑n).toNNReal

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
b : ℝ≥0
h : a ≤ ↑b
⊢ a.toReal ≤ ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
⊢ ⨆ p, ↑p (x * y) ≤ (⨆ p, ↑p x) + ⨆ p, ↑p y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x : E
⊢ ⨆ p, ↑p x⁻¹ = ⨆ p, ↑p x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : Group E
s : Set (GroupSeminorm E)
hs : ¬BddAbove s
⊢ sSup s = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
⊢ (sSup s) x = ⨆ p, ↑p x

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
h : a < b
⊢ ∃ q, 0 ≤ q ∧ a < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
⊢ (sSup s) x = sSup ((fun x_1 ↦ x_1 x) '' 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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors) =
    ↑(span {a})
⊢ HasFiniteMulSupport fun v ↦ ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)

Tactic:
by

Goal state after: