awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0
inl : (↑(∞ * (↑0 : ℝ≥0∞)) : EReal) = ⊤ * (↑(↑0 : ℝ≥0∞) : EReal)
inr : ∀ (h0 : x ≠ 0), (↑(∞ * (↑x : ℝ≥0∞)) : EReal) = ⊤ * (↑(↑x : ℝ≥0∞) : EReal)
⊢ (↑(∞ * (↑x : ℝ≥0∞)) : EReal) = ⊤ * (↑(↑x : ℝ≥0∞) : EReal)

Tactic:
rcases eq_or_ne x 0 with (rfl | h0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ (↑(∞ * (↑0 : ℝ≥0∞)) : EReal) = ⊤ * (↑(↑0 : ℝ≥0∞) : EReal)

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0
h0 : x ≠ 0
inr : (↑∞ : EReal) = ⊤ * (↑(↑x : ℝ≥0∞) : EReal)
⊢ (↑(∞ * (↑x : ℝ≥0∞)) : EReal) = ⊤ * (↑(↑x : ℝ≥0∞) : EReal)

Tactic:
rw [ENNReal.top_mul (ENNReal.coe_ne_zero.2 h0)]

Premises used: Iff.mpr, ENNReal.coe_ne_zero, ENNReal.top_mul
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0
h0 : x ≠ 0
⊢ (↑∞ : EReal) = ⊤ * (↑(↑x : ℝ≥0∞) : EReal)

Tactic:
Eq.symm <| if_pos <| NNReal.coe_pos.2 h0.bot_lt

Premises used: Iff.mpr, if_pos, NNReal.coe_pos, Eq.symm, Ne.bot_lt
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0
h0 : x ≠ 0
⊢ (↑∞ : EReal) = ⊤ * (↑(↑x : ℝ≥0∞) : EReal)

Tactic:
exact Eq.symm <| if_pos <| NNReal.coe_pos.2 h0.bot_lt

Premises used: Iff.mpr, if_pos, NNReal.coe_pos, Eq.symm, Ne.bot_lt
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0
rw : (↑(∞ * (↑x : ℝ≥0∞)) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
rw₁ : ⊤ * (↑(↑x : ℝ≥0∞) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
rw₂ : (↑(↑x : ℝ≥0∞) : EReal) * ⊤ = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
rw₃ rw₄ : (↑(↑x : ℝ≥0∞) : EReal) * ⊤ = (↑(↑x : ℝ≥0∞) : EReal) * ⊤
⊢ (↑((↑x : ℝ≥0∞) * ∞) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)

Tactic:
rw [mul_comm, coe_ennreal_top_mul, EReal.mul_comm, coe_ennreal_top]

Premises used: EReal.mul_comm, mul_comm, _private.0.EReal.coe_ennreal_top_mul, EReal.coe_ennreal_top
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ≥0
⊢ (↑((↑x : ℝ≥0∞) * (↑y : ℝ≥0∞)) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) * (↑(↑y : ℝ≥0∞) : EReal)

Tactic:
simp only [← ENNReal.coe_mul, coe_nnreal_eq_coe_real, NNReal.coe_mul, EReal.coe_mul]

Premises used: ENNReal.coe_mul, EReal.coe_mul, EReal.coe_nnreal_eq_coe_real, NNReal.coe_mul
-- Module: Mathlib.Data.EReal.Basic
Goal:
n : ℕ
x : ℝ≥0∞
⊢ (↑(n • x) : EReal) = n • (↑x : EReal)

Tactic:
map_nsmul (⟨⟨(↑), coe_ennreal_zero⟩, coe_ennreal_add⟩ : ℝ≥0∞ →+ EReal) _ _

Premises used: EReal.coe_ennreal_add, EReal.coe_ennreal_zero, AddMonoidHom.mk, ZeroHom.mk, ENNReal.toEReal, map_nsmul
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ toENNReal ⊤ = ∞

Tactic:
rfl

Premises used: EReal.toENNReal, rfl, ite
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : x ≠ ⊤
⊢ x.toENNReal = ENNReal.ofReal x.toReal

Tactic:
if_neg hx

Premises used: EReal.toENNReal, if_neg
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
pos : ∀ (h : x = ⊤), x.toENNReal = ∞ ↔ x = ⊤
neg : ∀ (h : ¬x = ⊤), x.toENNReal = ∞ ↔ x = ⊤
⊢ x.toENNReal = ∞ ↔ x = ⊤

Tactic:
by_cases h : x = ⊤
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
h : x = ⊤
⊢ x.toENNReal = ∞ ↔ x = ⊤

Tactic:
simp [h]
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
h : ¬x = ⊤
⊢ x.toENNReal = ∞ ↔ x = ⊤

Tactic:
simp [h, toENNReal]

Premises used: EReal.toENNReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
⊢ x.toENNReal ≠ ∞ ↔ x ≠ ⊤

Tactic:
toENNReal_eq_top_iff.not

Premises used: EReal.toENNReal_eq_top_iff, Iff.not
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : x ≤ 0
rw : ENNReal.ofReal x.toReal = 0
rw₁ : ∀ (h : x = ⊤), False
⊢ x.toENNReal = 0

Tactic:
rw [toENNReal, if_neg (fun h ↦ ?_)]

Premises used: EReal.toENNReal, if_neg
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : x ≤ 0
⊢ ENNReal.ofReal x.toReal = 0

Tactic:
ENNReal.ofReal_of_nonpos (toReal_nonpos hx)

Premises used: EReal.toReal_nonpos, ENNReal.ofReal_of_nonpos
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : x ≤ 0
⊢ ENNReal.ofReal x.toReal = 0

Tactic:
exact ENNReal.ofReal_of_nonpos (toReal_nonpos hx)

Premises used: EReal.toReal_nonpos, ENNReal.ofReal_of_nonpos
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : x ≤ 0
h : x = ⊤
⊢ False

Tactic:
zero_ne_top <| top_le_iff.mp <| h ▸ hx

Premises used: Eq.rec, EReal.zero_ne_top, top_le_iff, Iff.mp
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : x ≤ 0
h : x = ⊤
⊢ False

Tactic:
exact zero_ne_top <| top_le_iff.mp <| h ▸ hx

Premises used: EReal.zero_ne_top, top_le_iff, Iff.mp
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ toENNReal ⊥ = 0

Tactic:
toENNReal_of_nonpos bot_le

Premises used: bot_le, EReal.toENNReal_of_nonpos
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ toENNReal 0 = 0

Tactic:
toENNReal_of_nonpos le_rfl

Premises used: le_rfl, EReal.toENNReal_of_nonpos
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
bot : toENNReal ⊥ = 0 ↔ LE.le (α := EReal) ⊥ 0
coe : ∀ (a : ℝ), (↑a : EReal).toENNReal = 0 ↔ (↑a : EReal) ≤ 0
top : toENNReal ⊤ = 0 ↔ LE.le (α := EReal) ⊤ 0
⊢ x.toENNReal = 0 ↔ x ≤ 0

Tactic:
induction x
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ toENNReal ⊥ = 0 ↔ LE.le (α := EReal) ⊥ 0

Tactic:
simp [toENNReal]

Premises used: EReal.toENNReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ (↑a : EReal).toENNReal = 0 ↔ (↑a : EReal) ≤ 0

Tactic:
simp [toENNReal]

Premises used: EReal.toENNReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ toENNReal ⊤ = 0 ↔ LE.le (α := EReal) ⊤ 0

Tactic:
simp [toENNReal]

Premises used: EReal.toENNReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
⊢ x.toENNReal ≠ 0 ↔ 0 < x

Tactic:
simp [toENNReal_eq_zero_iff.not]

Premises used: EReal.toENNReal_eq_zero_iff, Iff.not
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
rw : x.toENNReal ≠ 0 ↔ 0 < x
rw₁ rw₂ : 0 < x ↔ 0 < x
⊢ 0 < x.toENNReal ↔ 0 < x

Tactic:
rw [pos_iff_ne_zero, toENNReal_ne_zero_iff]

Premises used: EReal.toENNReal_ne_zero_iff, pos_iff_ne_zero
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : 0 ≤ x
pos : ∀ (h_top : x = ⊤), (↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) : EReal) = x
neg : ∀ (h_top : ¬x = ⊤), (↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) : EReal) = x
⊢ (↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) : EReal) = x

Tactic:
by_cases h_top : x = ⊤
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : 0 ≤ x
h_top : x = ⊤
pos : (↑∞ : EReal) = ⊤
⊢ (↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) : EReal) = x

Tactic:
rw [if_pos h_top, h_top]

Premises used: if_pos
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : 0 ≤ x
h_top : x = ⊤
⊢ (↑∞ : EReal) = ⊤

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
neg : (↑(ENNReal.ofReal x.toReal) : EReal) = x
⊢ (↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) : EReal) = x

Tactic:
rw [if_neg h_top]

Premises used: if_neg
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
neg : (↑x.toReal : EReal) = x
⊢ (↑(ENNReal.ofReal x.toReal) : EReal) = x

Tactic:
simp only [coe_ennreal_ofReal, hx, toReal_nonneg, max_eq_left]

Premises used: max_eq_left, EReal.coe_ennreal_ofReal, EReal.toReal_nonneg
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
h : x = ⊥
⊢ False

Tactic:
simp_all only [le_bot_iff, zero_ne_bot]

Premises used: le_bot_iff, EReal.zero_ne_bot
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ (↑x.toReal : EReal) = x

Tactic:
exact coe_toReal h_top fun _ ↦ by simp_all only [le_bot_iff, zero_ne_bot]

Premises used: EReal.coe_toReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
inl : ∀ (hx : 0 ≤ x), (↑x.toENNReal : EReal) = max 0 x
inr : ∀ (hx : x ≤ 0), (↑x.toENNReal : EReal) = max 0 x
⊢ (↑x.toENNReal : EReal) = max 0 x

Tactic:
rcases le_total 0 x with (hx | hx)

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : 0 ≤ x
inl : x = max 0 x
inl₁ inl₂ : x = x
⊢ (↑x.toENNReal : EReal) = max 0 x

Tactic:
rw [coe_toENNReal hx, max_eq_right hx]

Premises used: max_eq_right, EReal.coe_toENNReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : x ≤ 0
inr : (↑0 : EReal) = max 0 x
inr₁ : (↑0 : EReal) = 0
inr₂ inr₃ : Eq (α := EReal) 0 0
⊢ (↑x.toENNReal : EReal) = max 0 x

Tactic:
rw [toENNReal_of_nonpos hx, max_eq_left hx, coe_ennreal_zero]

Premises used: EReal.coe_ennreal_zero, max_eq_left, EReal.toENNReal_of_nonpos
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
pos : ∀ (h_top : x = ∞), (↑x : EReal).toENNReal = x
neg : ∀ (h_top : ¬x = ∞), (↑x : EReal).toENNReal = x
⊢ (↑x : EReal).toENNReal = x

Tactic:
by_cases h_top : x = ⊤
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
h_top : x = ∞
pos : (↑∞ : EReal).toENNReal = ∞
pos₁ : toENNReal ⊤ = ∞
pos₂ pos₃ : Eq (α := ℝ≥0∞) ∞ ∞
⊢ (↑x : EReal).toENNReal = x

Tactic:
rw [h_top, coe_ennreal_top, toENNReal_top]

Premises used: EReal.toENNReal_top, EReal.coe_ennreal_top
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
h_top : ¬x = ∞
rwa : ¬(↑x : EReal) = ⊤
⊢ (↑x : EReal).toENNReal = x

Tactic:
rwa [toENNReal, if_neg _, toReal_coe_ennreal, ENNReal.ofReal_toReal_eq_iff]

Premises used: ENNReal.ofReal_toReal_eq_iff, EReal.toENNReal, EReal.toReal_coe_ennreal, if_neg
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
h_top : ¬x = ∞
⊢ ¬(↑x : EReal) = ⊤

Tactic:
simp [h_top]
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ (↑x : EReal).toENNReal = ENNReal.ofReal x

Tactic:
rfl

Premises used: ENNReal.ofNNReal, ENNReal.ofReal, EReal.toENNReal, EReal.toReal, rfl, ite
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : 0 ≤ x
pos : ∀ (h : x = ⊤), x.toENNReal.toReal = x.toReal
neg : ∀ (h : ¬x = ⊤), x.toENNReal.toReal = x.toReal
⊢ x.toENNReal.toReal = x.toReal

Tactic:
by_cases h : x = ⊤
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : 0 ≤ x
h : x = ⊤
⊢ x.toENNReal.toReal = x.toReal

Tactic:
simp [h]
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : 0 ≤ x
h : ¬x = ⊤
⊢ x.toENNReal.toReal = x.toReal

Tactic:
simp [h, toReal_nonneg hx]

Premises used: EReal.toReal_nonneg
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : EReal
hx : 0 ≤ x
hy : 0 ≤ y
bot : ∀ (hx : LE.le (α := EReal) 0 ⊥), toENNReal ⊥ = y.toENNReal ↔ ⊥ = y
coe : ∀ (a : ℝ) (hx : 0 ≤ (↑a : EReal)), (↑a : EReal).toENNReal = y.toENNReal ↔ (↑a : EReal) = y
top : ∀ (hx : LE.le (α := EReal) 0 ⊤), toENNReal ⊤ = y.toENNReal ↔ ⊤ = y
⊢ x.toENNReal = y.toENNReal ↔ x = y

Tactic:
induction x
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊥
bot : ∀ (hy : LE.le (α := EReal) 0 ⊥), toENNReal ⊥ = toENNReal ⊥ ↔ Eq (α := EReal) ⊥ ⊥
bot₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), toENNReal ⊥ = (↑a : EReal).toENNReal ↔ ⊥ = (↑a : EReal)
bot₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), toENNReal ⊥ = toENNReal ⊤ ↔ Eq (α := EReal) ⊥ ⊤
⊢ toENNReal ⊥ = y.toENNReal ↔ ⊥ = y

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
hy : 0 ≤ y
a : ℝ
hx : 0 ≤ (↑a : EReal)
coe : ∀ (hy : LE.le (α := EReal) 0 ⊥), (↑a : EReal).toENNReal = toENNReal ⊥ ↔ (↑a : EReal) = ⊥
coe₁ :
  ∀ (a_1 : ℝ) (hy : 0 ≤ (↑a_1 : EReal)),
    (↑a : EReal).toENNReal = (↑a_1 : EReal).toENNReal ↔ (↑a : EReal) = (↑a_1 : EReal)
coe₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), (↑a : EReal).toENNReal = toENNReal ⊤ ↔ (↑a : EReal) = ⊤
⊢ (↑a : EReal).toENNReal = y.toENNReal ↔ (↑a : EReal) = y

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊤
top : ∀ (hy : LE.le (α := EReal) 0 ⊥), toENNReal ⊤ = toENNReal ⊥ ↔ Eq (α := EReal) ⊤ ⊥
top₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), toENNReal ⊤ = (↑a : EReal).toENNReal ↔ ⊤ = (↑a : EReal)
top₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), toENNReal ⊤ = toENNReal ⊤ ↔ Eq (α := EReal) ⊤ ⊤
⊢ toENNReal ⊤ = y.toENNReal ↔ ⊤ = y

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Basic
Goal:
hx hy : LE.le (α := EReal) 0 ⊥
⊢ toENNReal ⊥ = toENNReal ⊥ ↔ Eq (α := EReal) ⊥ ⊥

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Basic
Goal:
hx : LE.le (α := EReal) 0 ⊥
a : ℝ
hy : 0 ≤ (↑a : EReal)
⊢ toENNReal ⊥ = (↑a : EReal).toENNReal ↔ ⊥ = (↑a : EReal)

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Basic
Goal:
hx : LE.le (α := EReal) 0 ⊥
hy : LE.le (α := EReal) 0 ⊤
⊢ toENNReal ⊥ = toENNReal ⊤ ↔ Eq (α := EReal) ⊥ ⊤

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
hy : LE.le (α := EReal) 0 ⊥
⊢ (↑a : EReal).toENNReal = toENNReal ⊥ ↔ (↑a : EReal) = ⊥

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
a_1 : ℝ
hy : 0 ≤ (↑a_1 : EReal)
⊢ (↑a : EReal).toENNReal = (↑a_1 : EReal).toENNReal ↔ (↑a : EReal) = (↑a_1 : EReal)

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
hy : LE.le (α := EReal) 0 ⊤
⊢ (↑a : EReal).toENNReal = toENNReal ⊤ ↔ (↑a : EReal) = ⊤

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Basic
Goal:
hx : LE.le (α := EReal) 0 ⊤
hy : LE.le (α := EReal) 0 ⊥
⊢ toENNReal ⊤ = toENNReal ⊥ ↔ Eq (α := EReal) ⊤ ⊥

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Basic
Goal:
hx : LE.le (α := EReal) 0 ⊤
a : ℝ
hy : 0 ≤ (↑a : EReal)
⊢ toENNReal ⊤ = (↑a : EReal).toENNReal ↔ ⊤ = (↑a : EReal)

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Basic
Goal:
hx hy : LE.le (α := EReal) 0 ⊤
⊢ toENNReal ⊤ = toENNReal ⊤ ↔ Eq (α := EReal) ⊤ ⊤

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : EReal
h : x ≤ y
bot : ∀ (h : ⊥ ≤ y), toENNReal ⊥ ≤ y.toENNReal
coe : ∀ (a : ℝ) (h : (↑a : EReal) ≤ y), (↑a : EReal).toENNReal ≤ y.toENNReal
top : ∀ (h : ⊤ ≤ y), toENNReal ⊤ ≤ y.toENNReal
⊢ x.toENNReal ≤ y.toENNReal

Tactic:
induction x
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
h : ⊥ ≤ y
⊢ toENNReal ⊥ ≤ y.toENNReal

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
a : ℝ
h : (↑a : EReal) ≤ y
pos : ∀ (hy_top : y = ⊤), (↑a : EReal).toENNReal ≤ y.toENNReal
neg : ∀ (hy_top : ¬y = ⊤), (↑a : EReal).toENNReal ≤ y.toENNReal
⊢ (↑a : EReal).toENNReal ≤ y.toENNReal

Tactic:
by_cases hy_top : y = ⊤
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
a : ℝ
h : (↑a : EReal) ≤ y
hy_top : y = ⊤
⊢ (↑a : EReal).toENNReal ≤ y.toENNReal

Tactic:
simp [hy_top]
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
a : ℝ
h : (↑a : EReal) ≤ y
hy_top : ¬y = ⊤
neg : ENNReal.ofReal a ≤ ENNReal.ofReal y.toReal
⊢ (↑a : EReal).toENNReal ≤ y.toENNReal

Tactic:
simp only [toENNReal, coe_ne_top, ↓reduceIte, toReal_coe, hy_top]

Premises used: EReal.toENNReal, EReal.toReal_coe, EReal.coe_ne_top, reduceIte
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
a : ℝ
h : (↑a : EReal) ≤ y
hy_top : ¬y = ⊤
⊢ ENNReal.ofReal a ≤ ENNReal.ofReal y.toReal

Tactic:
ENNReal.ofReal_le_ofReal <| EReal.toReal_le_toReal h (coe_ne_bot _) hy_top

Premises used: EReal.coe_ne_bot, ENNReal.ofReal_le_ofReal, EReal.toReal_le_toReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
a : ℝ
h : (↑a : EReal) ≤ y
hy_top : ¬y = ⊤
⊢ ENNReal.ofReal a ≤ ENNReal.ofReal y.toReal

Tactic:
exact ENNReal.ofReal_le_ofReal <| EReal.toReal_le_toReal h (coe_ne_bot _) hy_top

Premises used: EReal.coe_ne_bot, ENNReal.ofReal_le_ofReal, EReal.toReal_le_toReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
h : ⊤ ≤ y
⊢ toENNReal ⊤ ≤ y.toENNReal

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : EReal
hx : 0 ≤ x
hxy : x < y
⊢ x.toENNReal < y.toENNReal

Tactic:
lt_of_le_of_ne (toENNReal_le_toENNReal hxy.le)
    fun h ↦ hxy.ne <| (toENNReal_eq_toENNReal hx (hx.trans_lt hxy).le).mp h

Premises used: EReal.toENNReal_le_toENNReal, LT.lt.le, EReal.toENNReal_eq_toENNReal, Iff.mp, LE.le.trans_lt, lt_of_le_of_ne, LT.lt.ne
-- Module: Mathlib.Data.EReal.Basic
Goal:
n : ℕ
⊢ Ne (α := EReal) (↑n : EReal) ⊥

Tactic:
Ne.symm (ne_of_beq_false rfl)

Premises used: ne_of_beq_false, Ne.symm, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
n : ℕ
⊢ Ne (α := EReal) (↑n : EReal) ⊤

Tactic:
Ne.symm (ne_of_beq_false rfl)

Premises used: ne_of_beq_false, Ne.symm, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
m n : ℕ
rw : (↑m : EReal) = (↑(↑n : ℝ) : EReal) ↔ m = n
rw₁ : (↑(↑m : ℝ) : EReal) = (↑(↑n : ℝ) : EReal) ↔ m = n
rw₂ : Eq (α := ℝ) (↑m : ℝ) (↑n : ℝ) ↔ m = n
rw₃ rw₄ : m = n ↔ m = n
⊢ Eq (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m = n

Tactic:
rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_eq_coe_iff, Nat.cast_inj]

Premises used: EReal.coe_coe_eq_natCast, Nat.cast_inj, EReal.coe_eq_coe_iff
-- Module: Mathlib.Data.EReal.Basic
Goal:
m n : ℕ
⊢ Ne (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m ≠ n

Tactic:
not_iff_not.2 natCast_eq_iff

Premises used: not_iff_not, Iff.mpr, EReal.natCast_eq_iff
-- Module: Mathlib.Data.EReal.Basic
Goal:
m n : ℕ
rw : (↑m : EReal) ≤ (↑(↑n : ℝ) : EReal) ↔ m ≤ n
rw₁ : (↑(↑m : ℝ) : EReal) ≤ (↑(↑n : ℝ) : EReal) ↔ m ≤ n
rw₂ : LE.le (α := ℝ) (↑m : ℝ) (↑n : ℝ) ↔ m ≤ n
rw₃ rw₄ : m ≤ n ↔ m ≤ n
⊢ LE.le (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m ≤ n

Tactic:
rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_le_coe_iff, Nat.cast_le]

Premises used: EReal.coe_le_coe_iff, EReal.coe_coe_eq_natCast, Nat.cast_le
-- Module: Mathlib.Data.EReal.Basic
Goal:
m n : ℕ
rw : (↑m : EReal) < (↑(↑n : ℝ) : EReal) ↔ m < n
rw₁ : (↑(↑m : ℝ) : EReal) < (↑(↑n : ℝ) : EReal) ↔ m < n
rw₂ : LT.lt (α := ℝ) (↑m : ℝ) (↑n : ℝ) ↔ m < n
rw₃ rw₄ : m < n ↔ m < n
⊢ LT.lt (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m < n

Tactic:
rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_lt_coe_iff, Nat.cast_lt]

Premises used: EReal.coe_coe_eq_natCast, Nat.cast_lt, EReal.coe_lt_coe_iff
-- Module: Mathlib.Data.EReal.Basic
Goal:
m n : ℕ
rw : (↑(↑(m * n) : ℝ) : EReal) = HMul.hMul (α := EReal) (↑m : EReal) (↑n : EReal)
rw₁ : (↑(↑(m * n) : ℝ) : EReal) = (↑(↑m : ℝ) : EReal) * (↑n : EReal)
rw₂ : (↑(↑(m * n) : ℝ) : EReal) = (↑(↑m : ℝ) : EReal) * (↑(↑n : ℝ) : EReal)
rw₃ : (↑(HMul.hMul (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : EReal) = (↑(↑m : ℝ) : EReal) * (↑(↑n : ℝ) : EReal)
rw₄ rw₅ : (↑(↑m : ℝ) : EReal) * (↑(↑n : ℝ) : EReal) = (↑(↑m : ℝ) : EReal) * (↑(↑n : ℝ) : EReal)
⊢ (↑(m * n) : EReal) = HMul.hMul (α := EReal) (↑m : EReal) (↑n : EReal)

Tactic:
rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, Nat.cast_mul, EReal.coe_mul]

Premises used: EReal.coe_coe_eq_natCast, Nat.cast_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Basic
Goal:
a b : ℝ
h : (↑a : EReal) < (↑b : EReal)
⊢ ∃ (x : ℚ), (↑a : EReal) < (↑(↑x : ℝ) : EReal) ∧ (↑(↑x : ℝ) : EReal) < (↑b : EReal)

Tactic:
simp [exists_rat_btwn (EReal.coe_lt_coe_iff.1 h)]

Premises used: exists_rat_btwn, Iff.mp, EReal.coe_lt_coe_iff
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
h : (↑a : EReal) < ⊤
b : ℚ
hab : a < (↑b : ℝ)
⊢ (↑a : EReal) < (↑(↑b : ℝ) : EReal)

Tactic:
simpa using hab
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
h : ⊥ < (↑a : EReal)
b : ℚ
hab : (↑b : ℝ) < a
⊢ (↑(↑b : ℝ) : EReal) < (↑a : EReal)

Tactic:
simpa using hab
-- Module: Mathlib.Data.EReal.Basic
Goal:
a b : EReal
⊢ a < b ↔ ∃ (x : ℚ), a < (↑(↑x : ℝ) : EReal) ∧ (↑(↑x : ℝ) : EReal) < b

Tactic:
⟨fun hab => exists_rat_btwn_of_lt hab, fun ⟨_x, ax, xb⟩ => ax.trans xb⟩

Premises used: _private.0.EReal.lt_iff_exists_rat_btwn.match_1, LT.lt, Iff.intro, LT.lt.trans, EReal.exists_rat_btwn_of_lt
-- Module: Mathlib.Data.EReal.Basic
Goal:
a b : EReal
⊢ a < b ↔ ∃ (x : ℝ), a < (↑x : EReal) ∧ (↑x : EReal) < b

Tactic:
⟨fun hab =>
    let ⟨x, ax, xb⟩ := exists_rat_btwn_of_lt hab
    ⟨(x : ℝ), ax, xb⟩,
    fun ⟨_x, ax, xb⟩ => ax.trans xb⟩

Premises used: _private.0.EReal.lt_iff_exists_rat_btwn.match_1, Exists, Rat.cast, And, And.intro, LT.lt, Iff.intro, Exists.intro, LT.lt.trans, _private.0.EReal.lt_iff_exists_real_btwn.match_1, EReal.exists_rat_btwn_of_lt, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ (↑x : EReal)

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
x_1 : (↑{⊥, ⊤}ᶜ : Type)
x : EReal
hx : Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x
lift : x ≠ ⊤ ∧ x ≠ ⊥
lift₁ :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ (↑x : EReal)),
    (fun (x : ℝ) ↦ Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) (↑x : EReal) ⋯)
        ((fun (x : (↑{⊥, ⊤}ᶜ : Type)) ↦ (↑x : EReal).toReal)
          (Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) (↑x : EReal) hx)) =
      Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) (↑x : EReal) hx
⊢ (fun (x : ℝ) ↦ Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) (↑x : EReal) ⋯)
      ((fun (x : (↑{⊥, ⊤}ᶜ : Type)) ↦ (↑x : EReal).toReal)
        (Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) x hx)) =
    Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) x hx

Tactic:
lift x to ℝ
-- Module: Mathlib.Data.EReal.Basic
Goal:
x_1 : (↑{⊥, ⊤}ᶜ : Type)
x : EReal
hx : Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
simpa [not_or, and_comm] using hx

Premises used: and_comm, not_or
-- Module: Mathlib.Data.EReal.Basic
Goal:
x_1 : (↑{⊥, ⊤}ᶜ : Type)
x : ℝ
hx : Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ (↑x : EReal)
⊢ (fun (x : ℝ) ↦ Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) (↑x : EReal) ⋯)
      ((fun (x : (↑{⊥, ⊤}ᶜ : Type)) ↦ (↑x : EReal).toReal)
        (Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) (↑x : EReal) hx)) =
    Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) (↑x : EReal) hx

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ (fun (x : (↑{⊥, ⊤}ᶜ : Type)) ↦ (↑x : EReal).toReal)
      ((fun (x : ℝ) ↦ Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) (↑x : EReal) ⋯) x) =
    x

Tactic:
simp
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ EReal.abs ⊤ = ∞

Tactic:
rfl

Premises used: EReal.abs, rfl
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ EReal.abs ⊥ = ∞

Tactic:
rfl

Premises used: EReal.abs, rfl
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
⊢ (↑x : EReal).abs = ENNReal.ofReal |x|

Tactic:
rfl

Premises used: EReal.abs, rfl
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
⊢ (↑x : EReal).abs < ∞

Tactic:
ENNReal.ofReal_lt_top

Premises used: EReal.abs, ENNReal.ofReal_lt_top
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : EReal
bot : EReal.abs ⊥ = 0 ↔ Eq (α := EReal) ⊥ 0
coe : ∀ (a : ℝ), (↑a : EReal).abs = 0 ↔ (↑a : EReal) = 0
top : EReal.abs ⊤ = 0 ↔ Eq (α := EReal) ⊤ 0
⊢ x.abs = 0 ↔ x = 0

Tactic:
induction x
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ EReal.abs ⊥ = 0 ↔ Eq (α := EReal) ⊥ 0

Tactic:
simp
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
⊢ (↑a : EReal).abs = 0 ↔ (↑a : EReal) = 0

Tactic:
simp only [abs_def, coe_eq_zero, ENNReal.ofReal_eq_zero, abs_nonpos_iff]

Premises used: ENNReal.ofReal_eq_zero, abs_nonpos_iff, EReal.coe_eq_zero, EReal.abs_def
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ EReal.abs ⊤ = 0 ↔ Eq (α := EReal) ⊤ 0

Tactic:
simp only [abs_top, ENNReal.top_ne_zero, top_ne_zero]

Premises used: EReal.top_ne_zero, EReal.abs_top, ENNReal.top_ne_zero
-- Module: Mathlib.Data.EReal.Inv
Goal:
rw rw₁ : Eq (α := EReal) 0 0
⊢ EReal.abs 0 = 0

Tactic:
rw [abs_eq_zero_iff]

Premises used: EReal.abs_eq_zero_iff
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
rw : (↑(↑((Real.nnabs : (a : ℝ) → NNReal) x) : ℝ≥0∞) : EReal) = (↑(↑((Real.nnabs : (a : ℝ) → NNReal) x) : ℝ) : EReal)
⊢ (↑(↑x : EReal).abs : EReal) = (↑|x| : EReal)

Tactic:
rw [abs_def, ← Real.coe_nnabs, ENNReal.ofReal_coe_nnreal]

Premises used: Real.coe_nnabs, ENNReal.ofReal_coe_nnreal, EReal.abs_def
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
⊢ (↑(↑((Real.nnabs : (a : ℝ) → NNReal) x) : ℝ≥0∞) : EReal) = (↑(↑((Real.nnabs : (a : ℝ) → NNReal) x) : ℝ) : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
rw : (-(↑x : EReal)).abs = ENNReal.ofReal |x|
rw₁ : (↑(-x) : EReal).abs = ENNReal.ofReal |x|
rw₂ : ENNReal.ofReal |(-x)| = ENNReal.ofReal |x|
rw₃ rw₄ : ENNReal.ofReal |x| = ENNReal.ofReal |x|
⊢ (-(↑x : EReal)).abs = (↑x : EReal).abs

Tactic:
rw [abs_def, ← coe_neg, abs_def, abs_neg]

Premises used: abs_neg, EReal.coe_neg, EReal.abs_def
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ (HMul.hMul (α := EReal) ⊤ 0).abs = EReal.abs ⊤ * EReal.abs 0

Tactic:
simp only [mul_zero, abs_zero]

Premises used: MulZeroClass.mul_zero, EReal.abs_zero
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ (HMul.hMul (α := EReal) ⊤ ⊤).abs = EReal.abs ⊤ * EReal.abs ⊤

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
h : (x * y).abs = x.abs * y.abs
symm : (y * x).abs = x.abs * y.abs
symm₁ symm₂ symm₃ symm₄ : (x * y).abs = x.abs * y.abs
⊢ (y * x).abs = y.abs * x.abs

Tactic:
rwa [mul_comm, EReal.mul_comm]

Premises used: EReal.mul_comm, mul_comm