mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁶ : Semifield 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup G
inst✝² : PartialOrder G
inst✝¹ : MulActionWithZero 𝕜 G
inst✝ : PosSMulStrictMono 𝕜 G
a : 𝕜
ha : 0 < a
b₁ b₂ : G
h : a • b₁ < a • b₂
⊢ b₁ < b₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst✝ : PosSMulMono 𝕜 G
h : a < 0
⊢ a⁻¹ • b₁ ≤ b₂ ↔ a • b₂ ≤ b₁

Tactic:
by

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

Goal state before:
pp: p : EReal → Prop
⊢ (p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r) → ∃ r, p r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst✝ : PosSMulMono 𝕜 G
h : a < 0
⊢ b₁ ≤ a⁻¹ • b₂ ↔ b₂ ≤ a • b₁

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst✝ : PosSMulStrictMono 𝕜 G
h : a < 0
⊢ a⁻¹ • b₁ < b₂ ↔ a • b₂ < b₁

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst✝ : PosSMulStrictMono 𝕜 G
h : a < 0
⊢ b₁ < a⁻¹ • b₂ ↔ b₂ < a • b₁

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
κ : Sort u_2
q₁ : ι → Sort u_3
q₂ : κ → Sort u_4
f : (i : ι) → q₁ i → ℝ≥0∞
g : (k : κ) → q₂ k → ℝ≥0∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ (⨅ i, ⨅ qi, f i qi) + ⨅ k, ⨅ qk, g k qk

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ ⨅ b, ⨅ (_ : a < b), b = a

Tactic:
by

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

Goal state before:
pp: x y z : ℝ≥0∞
h : y + z < x
⊢ ∃ y' > y, ∃ z' > z, y' + z' < x

Tactic:
by

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

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

Tactic:
toNNReal_coe

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

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

Tactic:
toNNReal_coe

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

Goal state before:
pp: P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P ↑x ⊤
neg_bot : ∀ x < 0, P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ ↑x
bot_bot : P ⊥ ⊥
y : ℝ
⊢ P ⊥ ↑y

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ (iSup f).toNNReal = ⨆ i, (f i).toNNReal

Tactic:
by

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

Goal state before:
pp: s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ∞
⊢ (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ (iSup f).toReal = ⨆ i, (f i).toReal

Tactic:
by

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

Goal state before:
pp: s : Set ℝ≥0∞
hf : ∀ r ∈ s, r ≠ ∞
⊢ (sSup s).toReal = sSup (ENNReal.toReal '' s)

Tactic:
by

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

Goal state before:
pp: P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P ↑x ⊤
neg_bot : ∀ x < 0, P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ ↑x
bot_bot : P ⊥ ⊥
x : ℝ
⊢ P ↑x ⊥

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
⊢ ⨆ x, 0 = 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
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
i : ι
⊢ a + f i ≤ a + ⨆ i, f i

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
⊢ (⨆ i, f i) + a = ⨆ i, f i + 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
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℝ≥0∞
⊢ a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℝ≥0∞
⊢ (⨆ i, ⨆ (_ : p i), f i) + a = ⨆ i, ⨆ (_ : p i), f i + a

Tactic:
by

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

Goal state before:
pp: s : Set ℝ≥0∞
a : ℝ≥0∞
hs : s.Nonempty
⊢ a + sSup s = ⨆ b ∈ s, a + b

Tactic:
by

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

Goal state before:
pp: s : Set ℝ≥0∞
a : ℝ≥0∞
hs : s.Nonempty
⊢ sSup s + a = ⨆ b ∈ s, 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
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
⊢ Associates.mk (Ideal.span {a}) ≠ 0

Tactic:
by

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

Goal state before:
pp: P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P ↑x ⊤
neg_bot : ∀ x < 0, P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ ↑x
bot_bot : P ⊥ ⊥
x : ℝ
⊢ P ↑x ⊤

Tactic:
by

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

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

Tactic:
by

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 I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
⊢ Associates.mk (Ideal.span {a'}) ≠ 0

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ (⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a

Tactic:
by

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

Goal state before:
pp: P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P ↑x ⊤
neg_bot : ∀ x < 0, P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ ↑x
bot_bot : P ⊥ ⊥
y : ℝ
⊢ P ⊤ ↑y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x y : EReal
⊢ x * y = y * x

Tactic:
by

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

Goal state before:
pp: x : EReal
⊢ x * 1 = x

Tactic:
by

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

Goal state before:
pp: x : EReal
⊢ x * 0 = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ f i + g j ≤ f _k + g _k

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 I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
⊢ I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
x : ℝ≥0∞
hx : ⊥ < x
⊢ a - f i < x

Tactic:
by

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

Goal state before:
pp: ⊢ range Real.toEReal = {⊥, ⊤}ᶜ

Tactic:
by

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

Goal state before:
pp: ⊢ range Real.toEReal = Ioo ⊥ ⊤

Tactic:
by

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

Goal state before:
pp: x : EReal
⊢ x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
by

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

Goal state before:
pp: x : EReal
⊢ x.toReal ≠ 0 ↔ x ≠ 0 ∧ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ ⨆ b, ⨆ (_ : b < a), b = a

Tactic:
by

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

Goal state before:
pp: x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ y' < y, ∀ z' < z, y' + z' ≤ x
⊢ ∃ i, i < y

Tactic:
by

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

Goal state before:
pp: x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ y' < y, ∀ z' < z, y' + z' ≤ x
⊢ ∃ j, j < z

Tactic:
by

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

Goal state before:
pp: x y : EReal
hx_top : x ≠ ⊤
hx_bot : x ≠ ⊥
hy_top : y ≠ ⊤
hy_bot : y ≠ ⊥
⊢ x.toReal = y.toReal ↔ x = y

Tactic:
by

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

Goal state before:
pp: x y z : ℝ≥0∞
h : x < y + z
hy : y ≠ 0
hz : z ≠ 0
⊢ ∃ y' < y, ∃ z' < z, x < y' + z'

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : EReal
hx : 0 < x
h'x : x ≠ ⊤
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
by

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

Goal state before:
pp: x : EReal
hx : 0 < x
h'x : x ≠ ⊤
⊢ 0 < x.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.OfFun

Goal state before:
pp: X : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
d : X → X → M
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
r : M
hr : r > 0
⊢ SetRel.id ⊆ {x | d x.1 x.2 < r}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.OfFun

Goal state before:
pp: X : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
d : X → X → M
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
r : M
x✝ : r > 0
x : X × X
hx : x ∈ {x | d x.1 x.2 < r}
⊢ x.swap ∈ {x | d x.1 x.2 < r}

Tactic:
by

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

Goal state before:
pp: x : EReal
hx : x < 0
h'x : x ≠ ⊥
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
by

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

Goal state before:
pp: x : EReal
hx : x < 0
h'x : x ≠ ⊥
⊢ x.toReal < 0

Tactic:
by

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

Goal state before:
pp: y : EReal
hy0 : 0 < y
right✝ : y < ⊤
⊢ y ≠ ⊤ ∧ y ≠ ⊥

Tactic:
by

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

Goal state before:
pp: ⊢ toReal '' Ioo 0 ⊤ = Ioi 0

Tactic:
by

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

Goal state before:
pp: y : EReal
left✝ : ⊥ < y
hy0 : y < 0
⊢ y ≠ ⊤ ∧ y ≠ ⊥

Tactic:
by

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

Goal state before:
pp: ⊢ toReal '' Ioo ⊥ 0 = Iio 0

Tactic:
by

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

Goal state before:
pp: x y : EReal
h : x ≤ y
hx : x ≠ ⊥
hy : y ≠ ⊤
⊢ x.toReal ≤ y.toReal

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : EReal
h : x ≠ ⊤
⊢ x ≤ ↑x.toReal

Tactic:
by

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

Goal state before:
pp: x : EReal
h : x ≠ ⊥
⊢ ↑x.toReal ≤ x

Tactic:
by

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

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

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 I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
⊢ count K v (I * I') = count K v I + count K v I'

Tactic:
by

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

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

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 I' : FractionalIdeal R⁰ K
inst✝ : Decidable (I ≠ 0 ∧ I' ≠ 0)
⊢ count K v (I * I') = if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 0

Tactic:
by

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

Goal state before:
pp: x z : EReal
h : x < z
⊢ ∃ y, x < ↑y ∧ ↑y < z

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

Tactic:
by

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

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal '' Icc x y = Icc ↑x ↑y

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 1 = 0

Tactic:
by

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

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal '' Ico x y = Ico ↑x ↑y

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ Real.toEReal '' Ici x = Ico ↑x ⊤

Tactic:
by

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

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal '' Ioc x y = Ioc ↑x ↑y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ Real.toEReal '' Ioi x = Ioo ↑x ⊤

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ Real.toEReal '' Iic x = Ioc ⊥ ↑x

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ Real.toEReal '' Iio x = Ioo ⊥ ↑x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ Real.toEReal ⁻¹' Ioi ⊥ = univ

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ Real.toEReal ⁻¹' Iio ⊤ = univ

Tactic:
by

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

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

Tactic:
by

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

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

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
ι : Type u_3
s : Finset ι
I : ι → FractionalIdeal R⁰ K
hS : ∀ i ∈ s, I i ≠ 0
⊢ count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ Real.toEReal ⁻¹' Ico ↑x ⊤ = Ici x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: y : ℝ
⊢ Real.toEReal ⁻¹' Ioc ⊥ ↑y = Iic y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ Real.toEReal ⁻¹' Ioo ⊥ ⊤ = univ

Tactic:
by

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

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

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 c : ℝ≥0∞
⊢ a / b / c = a / c / b

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
h : 0 < a
⊢ a ∈ {b | 1 ≤ ∞ * b}

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ≥0∞
⊢ 0 < ↑x ↔ x ≠ 0

Tactic:
by

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

Goal state before:
pp: r : ℝ≥0
b : ℝ≥0∞
hb : 1 ≤ ↑r * b
⊢ ∀ (p : ℝ≥0), b = ↑p → r⁻¹ ≤ p

Tactic:
by

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

Goal state before:
pp: r : ℝ≥0
hr : r ≠ 0
⊢ 1 ≤ ↑r * ↑r⁻¹

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
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : I = 0
⊢ ¬(I ^ n ≠ 0 ∧ I ≠ 0)

Tactic:
by

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

Goal state before:
pp: ⊢ ↑2⁻¹ = 2⁻¹

Tactic:
by

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

Goal state before:
pp: r p : ℝ≥0
hr : r ≠ 0
⊢ ↑(p / r) = ↑p / ↑r

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.ENNReal.Inv

Goal state before:
pp: r p : ℝ≥0
⊢ ↑(p / r) ≤ ↑p / ↑r

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x✝ : ℝ≥0∞
⊢ (x✝ ^ 0)⁻¹ = x✝⁻¹ ^ 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (∞ ^ (n + 1))⁻¹ = ∞⁻¹ ^ (n + 1)

Tactic:
by

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

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

Tactic:
by

Goal state after: