mathlib-initiative/mathlib-tactics huggingface dataset:
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 ≤ ↑a + ↑(-a)

Tactic:
]

Goal state after:
α : Type u_1
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
a : AddUnits ℝ≥0∞
⊢ ↑a ≤ ↑a + ↑(-a)
Module: Mathlib.Data.ENNReal.Basic

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
a : ℝ≥0∞
h : ENNReal.ofReal a.toReal = a
⊢ ENNReal.ofReal a.toReal ≠ ∞
Module: Mathlib.Data.ENNReal.Basic

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

Tactic:
]

Goal state after:
a : ℝ
h : (ENNReal.ofReal a).toReal = a
⊢ 0 ≤ (ENNReal.ofReal a).toReal
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
⊢ ∀ (s : Finset (HeightOneSpectrum A)) (v : HeightOneSpectrum A → M),
    (∀ i ∈ s, v i ∈ primaryComponent M i.asIdeal) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

Tactic:
]

Goal state after:
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
⊢ ∀ (s : Finset (HeightOneSpectrum A)) (v : HeightOneSpectrum A → M),
    (∀ i ∈ s, v i ∈ primaryComponent M i.asIdeal) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
Module: Mathlib.Data.ENNReal.Basic

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

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
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})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors)) =
    (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)) *
      ∏ᶠ (x : HeightOneSpectrum R),
        (↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk (span {a})).factors))⁻¹

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
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})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors)) =
    (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)) *
      ∏ᶠ (x : HeightOneSpectrum R),
        (↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk (span {a})).factors))⁻¹
Module: Mathlib.Data.ENNReal.Basic

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

Tactic:
]

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
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hsum : ∑ i ∈ s, p i = 0
f : HeightOneSpectrum A → ℕ
hmem : ∀ i ∈ s, p i ∈ torsionBySet A M ↑(i.asIdeal ^ f i)
m : ℕ := s.sup f
⊢ ∀ (s : Finset (HeightOneSpectrum A)), s.SupIndep fun i ↦ torsionBySet A M ↑(i.asIdeal ^ m)

Tactic:
]

Goal state after:
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hsum : ∑ i ∈ s, p i = 0
f : HeightOneSpectrum A → ℕ
hmem : ∀ i ∈ s, p i ∈ torsionBySet A M ↑(i.asIdeal ^ f i)
m : ℕ := s.sup f
⊢ ∀ (s : Finset (HeightOneSpectrum A)), s.SupIndep fun i ↦ torsionBySet A M ↑(i.asIdeal ^ m)
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 (range fun p ↦ ↑p x) = sSup ((fun x_1 ↦ x_1 x) '' s)

Tactic:
]

Goal state after:
E : Type u_3
inst✝ : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
⊢ sSup (range fun p ↦ ↑p x) = sSup ((fun x_1 ↦ x_1 x) '' s)
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: b : ℝ≥0∞
c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ∃ r, 0 < r ∧ ↑a + ↑r < b

Tactic:
]

Goal state after:
b : ℝ≥0∞
c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ∃ r, 0 < r ∧ ↑a + ↑r < b
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : Group E
ι : Type u_6
f : ι → GroupSeminorm E
h : BddAbove (range f)
x : E
⊢ ⨆ p, ↑p x = ⨆ i, (f i) x

Tactic:
]

Goal state after:
E : Type u_3
inst✝ : Group E
ι : Type u_6
f : ι → GroupSeminorm E
h : BddAbove (range f)
x : E
⊢ ⨆ p, ↑p x = ⨆ i, (f i) x
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: b : ℝ≥0∞
c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ↑c < b

Tactic:
]

Goal state after:
b : ℝ≥0∞
c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ↑c < b
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
⊢ 0 ≤ 0

Tactic:
]

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
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hsum : ∑ i ∈ s, p i = 0
f : HeightOneSpectrum A → ℕ
hmem : ∀ i ∈ s, p i ∈ torsionBySet A M ↑(i.asIdeal ^ f i)
m : ℕ := s.sup f
hSupIndep :
  ∀ (s : Finset (HeightOneSpectrum A)) (v : HeightOneSpectrum A → M),
    (∀ i ∈ s, v i ∈ torsionBySet A M ↑(i.asIdeal ^ m)) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
⊢ ∀ i ∈ s, p i = 0

Tactic:
]

Goal state after:
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hsum : ∑ i ∈ s, p i = 0
f : HeightOneSpectrum A → ℕ
hmem : ∀ i ∈ s, p i ∈ torsionBySet A M ↑(i.asIdeal ^ f i)
m : ℕ := s.sup f
hSupIndep :
  ∀ (s : Finset (HeightOneSpectrum A)) (v : HeightOneSpectrum A → M),
    (∀ i ∈ s, v i ∈ torsionBySet A M ↑(i.asIdeal ^ m)) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
⊢ ∀ i ∈ s, p i = 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
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})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors)) =
    ∏ᶠ (i : HeightOneSpectrum R),
      ↑i.asIdeal ^ ↑((Associates.mk i.asIdeal).count (Associates.mk J).factors) *
        ↑i.asIdeal ^ (-↑((Associates.mk i.asIdeal).count (Associates.mk (span {a})).factors))

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
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})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors)) =
    ∏ᶠ (i : HeightOneSpectrum R),
      ↑i.asIdeal ^ ↑((Associates.mk i.asIdeal).count (Associates.mk J).factors) *
        ↑i.asIdeal ^ (-↑((Associates.mk i.asIdeal).count (Associates.mk (span {a})).factors))
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
⊢ max (p x) (q x) = max (p x) (q x)

Tactic:
]

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

Goal state before:
pp: x : ℝ≥0∞
⊢ (∃ i, x ∈ Iio ↑i) ↔ x ∈ {∞}ᶜ

Tactic:
]

Goal state after:
x : ℝ≥0∞
⊢ (∃ i, x ∈ Iio ↑i) ↔ x ∈ {∞}ᶜ
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✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x : E
p q : GroupSeminorm E
r : ℝ
hr : 0 < r
⊢ 0 < r

Tactic:
]

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x : E
p q : GroupSeminorm E
r : ℝ
hr : 0 < r
⊢ 0 < r
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✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x y u v : E
⊢ p (u * v) + q (x / u * (y / v)) ≤ p u + p v + (q (x / u) + q (y / v))

Tactic:
]

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x y u v : E
⊢ p (u * v) + q (x / u * (y / v)) ≤ p u + p v + (q (x / u) + q (y / v))
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✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x : E
⊢ p x ≤ p x

Tactic:
]

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b - φ ↑(f P) = 0

Tactic:
]

Goal state after:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b - φ ↑(f P) = 0
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if y = 0 then 0 else 1) ≤ if y = 0 then 0 else 1

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
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})
v : HeightOneSpectrum R
⊢ ↑v.asIdeal ^
      (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) +
        -↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors)) =
    ↑v.asIdeal ^
      (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) +
        -↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors))

Tactic:
]

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

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ p.toNNReal + q.toNNReal = p.toNNReal + q.toNNReal

Tactic:
]

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal ≤ b.toNNReal
⊢ a.toNNReal ≤ b.toNNReal

Tactic:
]

Goal state after:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal ≤ b.toNNReal
⊢ a.toNNReal ≤ b.toNNReal
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ 1 + if y = 0 then 0 else 1

Tactic:
]

Goal state after:
case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ 1 + if y = 0 then 0 else 1
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal < b.toNNReal
⊢ a.toNNReal < b.toNNReal

Tactic:
]

Goal state after:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal < b.toNNReal
⊢ a.toNNReal < b.toNNReal
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✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x : E
⊢ (if -x = 0 then 0 else 1) = if x = 0 then 0 else 1

Tactic:
neg_eq_zero

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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : (algebraMap R K) ↑d ≠ 0
⊢ ¬(algebraMap R K) n = 0 ∧ ¬(algebraMap R K) ↑d = 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : (algebraMap R K) ↑d ≠ 0
⊢ ¬(algebraMap R K) n = 0 ∧ ¬(algebraMap R K) ↑d = 0
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b = ∑ x ∈ f.support, φ ↑(f x)

Tactic:
]

Goal state after:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b = ∑ x ∈ f.support, φ ↑(f x)
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
h : 0 ≤ q
⊢ p ≤ q ↔ p ≤ q

Tactic:
]

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

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ p = q ↔ p = q

Tactic:
]

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

Goal state before:
pp: p q : ℝ
h : 0 < q
⊢ p < q ↔ p < q

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : (algebraMap R K) ↑d ≠ 0
h0 : spanSingleton R⁰ (mk' K n d) ≠ 0
⊢ spanSingleton R⁰ (mk' K n d) = spanSingleton R⁰ (((algebraMap R K) ↑d)⁻¹ * (algebraMap R K) n)

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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : (algebraMap R K) ↑d ≠ 0
h0 : spanSingleton R⁰ (mk' K n d) ≠ 0
⊢ spanSingleton R⁰ (mk' K n d) = spanSingleton R⁰ (((algebraMap R K) ↑d)⁻¹ * (algebraMap R K) n)
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
⊢ p < q ↔ p < q

Tactic:
]

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

Goal state before:
pp: r : ℝ
⊢ 0 < r ↔ 0 < r

Tactic:
]

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

Goal state before:
pp: case refine_2
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
hdiff : φ b - φ ↑(f P) = ∑ Q ∈ f.support \ {P}, φ ↑(f Q)
⊢ ∑ Q ∈ f.support \ {P}, φ ↑(f Q) ∈ ⨆ j, ⨆ (_ : j ≠ P), (fun P ↦ primaryComponent M₂ P.asIdeal) j

Tactic:
]

Goal state after:
case refine_2
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
hdiff : φ b - φ ↑(f P) = ∑ Q ∈ f.support \ {P}, φ ↑(f Q)
⊢ ∑ Q ∈ f.support \ {P}, φ ↑(f Q) ∈ ⨆ j, ⨆ (_ : j ≠ P), (fun P ↦ primaryComponent M₂ P.asIdeal) j
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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : (algebraMap R K) ↑d ≠ 0
h0 : spanSingleton R⁰ (mk' K n d) ≠ 0
⊢ ((algebraMap R K) ↑d)⁻¹ * (algebraMap R K) n = ((algebraMap R K) ↑d)⁻¹ * (algebraMap R K) n

Tactic:
]

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✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
r s : E
⊢ 0 ≤ 0

pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
r s : E
⊢ 0 ≤ 0

Tactic:
]

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
r s : E
⊢ 0 ≤ 0
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a : ℝ
b : ℝ≥0
ha : 0 ≤ a
⊢ a < ↑b ↔ a < ↑b

Tactic:
]

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

Goal state before:
pp: p q : ℝ
hq : 0 ≤ q
⊢ ENNReal.ofReal p * ENNReal.ofReal q = ENNReal.ofReal p * ENNReal.ofReal q

Tactic:
]

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

Goal state before:
pp: p : ℝ
hp : 0 ≤ p
n : ℕ
⊢ ENNReal.ofReal (p ^ n) = ENNReal.ofReal (p ^ n)

Tactic:
]

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

Goal state before:
pp: E : Type u_3
inst✝ : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
⊢ sSup (range fun p ↦ ↑p x) = sSup ((fun x_1 ↦ x_1 x) '' s)

Tactic:
]

Goal state after:
E : Type u_3
inst✝ : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
⊢ sSup (range fun p ↦ ↑p x) = sSup ((fun x_1 ↦ x_1 x) '' s)
Module: Mathlib.Data.ENNReal.Real

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
k : K
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hk : I = 0
hnd : mk' K n d = k
h : n = 0
⊢ False

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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
k : K
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hk : I = 0
hnd : mk' K n d = k
h : n = 0
⊢ False
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a : ℝ≥0∞
⊢ (a * ∞).toReal = 0

Tactic:
]

Goal state after:
a : ℝ≥0∞
⊢ (a * ∞).toReal = 0
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : AddGroup E
ι : Type u_6
f : ι → NonarchAddGroupSeminorm E
h : BddAbove (range f)
x : E
⊢ ⨆ p, ↑p x = ⨆ i, (f i) x

Tactic:
]

Goal state after:
E : Type u_3
inst✝ : AddGroup E
ι : Type u_6
f : ι → NonarchAddGroupSeminorm E
h : BddAbove (range f)
x : E
⊢ ⨆ p, ↑p x = ⨆ i, (f i) x
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✝ : AddGroup E
p✝ q✝ p q : NonarchAddGroupSeminorm E
⊢ 0 ≤ 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hnd : mk' K n d = k
hn0 : n ≠ 0
⊢ spanSingleton R⁰ k = spanSingleton R⁰ k

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 1
⊢ (if y = 1 then 0 else 1) ≤ if y = 1 then 0 else 1

Tactic:
]

Goal state after: