awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
refine : ∀ (c : ℝ≥0∞) (hca : c < a), c < ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b
⊢ a ≤ ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b

Tactic:
refine le_of_forall_lt fun c hca ↦ ?_

Premises used: le_of_forall_lt
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a c : ℝ≥0∞
hca : c < a
obtain : ∀ (d : ℝ≥0∞) (hcd : c < d) (hdb : d < a), c < ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b
⊢ c < ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b

Tactic:
obtain ⟨d, hcd, hdb⟩ := exists_between hca

Premises used: exists_between
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a c : ℝ≥0∞
hca : c < a
d : ℝ≥0∞
hcd : c < d
hdb : d < a
⊢ c < ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b

Tactic:
hcd.trans_le <| le_iSup₂_of_le d hdb le_rfl

Premises used: le_rfl, LT.lt.trans_le, le_iSup₂_of_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a c : ℝ≥0∞
hca : c < a
d : ℝ≥0∞
hcd : c < d
hdb : d < a
⊢ c < ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b

Tactic:
exact hcd.trans_le <| le_iSup₂_of_le d hdb le_rfl

Premises used: le_rfl, LT.lt.trans_le, le_iSup₂_of_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x y z : ℝ≥0∞
h : x < y + z
hy : y ≠ 0
hz : z ≠ 0
contrapose! : ∀ (h : ∀ (y' : ℝ≥0∞) (_ : y' < y) (z' : ℝ≥0∞) (_ : z' < z), y' + z' ≤ x), y + z ≤ x
⊢ ∃ y' < y, ∃ z' < z, x < y' + z'

Tactic:
contrapose! h
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ (y' : ℝ≥0∞) (_ : y' < y) (z' : ℝ≥0∞) (_ : z' < z), y' + z' ≤ x
⊢ ∃ (i : ℝ≥0∞), i < y

Tactic:
⟨0, hy.bot_lt⟩

Premises used: Exists.intro, OfNat.ofNat, Ne.bot_lt
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ (y' : ℝ≥0∞) (_ : y' < y) (z' : ℝ≥0∞) (_ : z' < z), y' + z' ≤ x
⊢ ∃ (i : ℝ≥0∞), i < y

Tactic:
exact ⟨0, hy.bot_lt⟩
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ (y' : ℝ≥0∞) (_ : y' < y) (z' : ℝ≥0∞) (_ : z' < z), y' + z' ≤ x
⊢ ∃ (j : ℝ≥0∞), j < z

Tactic:
⟨0, hz.bot_lt⟩

Premises used: Exists.intro, OfNat.ofNat, Ne.bot_lt
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ (y' : ℝ≥0∞) (_ : y' < y) (z' : ℝ≥0∞) (_ : z' < z), y' + z' ≤ x
⊢ ∃ (j : ℝ≥0∞), j < z

Tactic:
exact ⟨0, hz.bot_lt⟩
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ (y' : ℝ≥0∞) (_ : y' < y) (z' : ℝ≥0∞) (_ : z' < z), y' + z' ≤ x
⊢ y + z ≤ x

Tactic:
simpa using biSup_add_biSup_le' (by exact ⟨0, hy.bot_lt⟩) (by exact ⟨0, hz.bot_lt⟩) h

Premises used: ENNReal.biSup_add_biSup_le'
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
⊢ a ≠ ∞

Tactic:
ha
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
lift : ∀ (a : ℝ≥0), ((↑a : ℝ≥0∞) + b).toReal = (↑a : ℝ≥0∞).toReal + b.toReal
⊢ (a + b).toReal = a.toReal + b.toReal

Tactic:
lift a to ℝ≥0 using ha
-- Module: Mathlib.Data.ENNReal.Real
Goal:
b : ℝ≥0∞
hb : b ≠ ∞
a : ℝ≥0
⊢ b ≠ ∞

Tactic:
hb
-- Module: Mathlib.Data.ENNReal.Real
Goal:
b : ℝ≥0∞
hb : b ≠ ∞
a : ℝ≥0
lift : ∀ (b : ℝ≥0), ((↑a : ℝ≥0∞) + (↑b : ℝ≥0∞)).toReal = (↑a : ℝ≥0∞).toReal + (↑b : ℝ≥0∞).toReal
⊢ ((↑a : ℝ≥0∞) + b).toReal = (↑a : ℝ≥0∞).toReal + b.toReal

Tactic:
lift b to ℝ≥0 using hb
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0
⊢ ((↑a : ℝ≥0∞) + (↑b : ℝ≥0∞)).toReal = (↑a : ℝ≥0∞).toReal + (↑b : ℝ≥0∞).toReal

Tactic:
rfl
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
ha : a = ∞
⊢ (a + b).toReal ≤ a.toReal + b.toReal

Tactic:
simp only [ha, top_add, toReal_top, zero_add, toReal_nonneg]

Premises used: ENNReal.toReal_nonneg, zero_add, top_add, ENNReal.toReal_top
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
ha : ¬a = ∞
hb : b = ∞
⊢ (a + b).toReal ≤ a.toReal + b.toReal

Tactic:
simp only [hb, add_top, toReal_top, add_zero, toReal_nonneg]

Premises used: add_top, ENNReal.toReal_nonneg, ENNReal.toReal_top, add_zero
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
rw : (↑(p + q).toNNReal : ℝ≥0∞) = ENNReal.ofReal p + ENNReal.ofReal q
rw₁ : (↑(p + q).toNNReal : ℝ≥0∞) = (↑p.toNNReal : ℝ≥0∞) + ENNReal.ofReal q
rw₂ : (↑(p + q).toNNReal : ℝ≥0∞) = (↑p.toNNReal : ℝ≥0∞) + (↑q.toNNReal : ℝ≥0∞)
rw₃ : (↑(p + q).toNNReal : ℝ≥0∞) = (↑(p.toNNReal + q.toNNReal) : ℝ≥0∞)
rw₄ : (p + q).toNNReal = p.toNNReal + q.toNNReal
rw₅ rw₆ : p.toNNReal + q.toNNReal = p.toNNReal + q.toNNReal
⊢ ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q

Tactic:
rw [ENNReal.ofReal, ENNReal.ofReal, ENNReal.ofReal, ← coe_add, coe_inj,
    Real.toNNReal_add hp hq]

Premises used: ENNReal.ofReal, Real.toNNReal_add, ENNReal.coe_inj, ENNReal.coe_add
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p q : ℝ
⊢ ENNReal.ofReal (p + q) ≤ ENNReal.ofReal p + ENNReal.ofReal q

Tactic:
coe_le_coe.2 Real.toNNReal_add_le

Premises used: Iff.mpr, ENNReal.ofNNReal, ENNReal.ofReal, WithTop.map₂, ENNReal.coe_le_coe, Real.toNNReal_add_le, WithTop.some, Option.map₂
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
lift : ∀ (a : ℝ≥0), (↑a : ℝ≥0∞).toReal ≤ b.toReal ↔ (↑a : ℝ≥0∞) ≤ b
⊢ a.toReal ≤ b.toReal ↔ a ≤ b

Tactic:
lift a to ℝ≥0 using ha
-- Module: Mathlib.Data.ENNReal.Real
Goal:
b : ℝ≥0∞
hb : b ≠ ∞
a : ℝ≥0
lift : ∀ (b : ℝ≥0), (↑a : ℝ≥0∞).toReal ≤ (↑b : ℝ≥0∞).toReal ↔ (↑a : ℝ≥0∞) ≤ (↑b : ℝ≥0∞)
⊢ (↑a : ℝ≥0∞).toReal ≤ b.toReal ↔ (↑a : ℝ≥0∞) ≤ b

Tactic:
lift b to ℝ≥0 using hb
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑a : ℝ≥0∞).toReal ≤ (↑b : ℝ≥0∞).toReal ↔ a ≤ b
⊢ (↑a : ℝ≥0∞).toReal ≤ (↑b : ℝ≥0∞).toReal ↔ (↑a : ℝ≥0∞) ≤ (↑b : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
hb : b ≠ ∞
h : a ≤ b
⊢ a.toReal ≤ b.toReal

Tactic:
(toReal_le_toReal (ne_top_of_le_ne_top hb h) hb).2 h

Premises used: Iff.mpr, ne_top_of_le_ne_top, ENNReal.toReal_le_toReal
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
h : a ≤ b
ht : b = ∞ → a = ∞
inl : ∀ (h : ∞ ≤ b) (ht : b = ∞ → Eq (α := ℝ≥0∞) ∞ ∞), ENNReal.toReal ∞ ≤ b.toReal
inr : ∀ (ha : a ≠ ∞), a.toReal ≤ b.toReal
⊢ a.toReal ≤ b.toReal

Tactic:
rcases eq_or_ne a ∞ with rfl | ha

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.ENNReal.Real
Goal:
b : ℝ≥0∞
h : ∞ ≤ b
ht : b = ∞ → Eq (α := ℝ≥0∞) ∞ ∞
⊢ ENNReal.toReal ∞ ≤ b.toReal

Tactic:
toReal_nonneg

Premises used: ENNReal.toReal_nonneg, ENNReal.toReal, NNReal.toReal
-- Module: Mathlib.Data.ENNReal.Real
Goal:
b : ℝ≥0∞
h : ∞ ≤ b
ht : b = ∞ → Eq (α := ℝ≥0∞) ∞ ∞
⊢ ENNReal.toReal ∞ ≤ b.toReal

Tactic:
exact toReal_nonneg

Premises used: ENNReal.toReal_nonneg
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
h : a ≤ b
ht : b = ∞ → a = ∞
ha : a ≠ ∞
⊢ a.toReal ≤ b.toReal

Tactic:
toReal_mono (mt ht ha) h

Premises used: mt, ENNReal.toReal_mono
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
h : a ≤ b
ht : b = ∞ → a = ∞
ha : a ≠ ∞
⊢ a.toReal ≤ b.toReal

Tactic:
exact toReal_mono (mt ht ha) h

Premises used: mt, ENNReal.toReal_mono
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
lift : ∀ (a : ℝ≥0), (↑a : ℝ≥0∞).toReal < b.toReal ↔ (↑a : ℝ≥0∞) < b
⊢ a.toReal < b.toReal ↔ a < b

Tactic:
lift a to ℝ≥0 using ha
-- Module: Mathlib.Data.ENNReal.Real
Goal:
b : ℝ≥0∞
hb : b ≠ ∞
a : ℝ≥0
lift : ∀ (b : ℝ≥0), (↑a : ℝ≥0∞).toReal < (↑b : ℝ≥0∞).toReal ↔ (↑a : ℝ≥0∞) < (↑b : ℝ≥0∞)
⊢ (↑a : ℝ≥0∞).toReal < b.toReal ↔ (↑a : ℝ≥0∞) < b

Tactic:
lift b to ℝ≥0 using hb
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑a : ℝ≥0∞).toReal < (↑b : ℝ≥0∞).toReal ↔ a < b
⊢ (↑a : ℝ≥0∞).toReal < (↑b : ℝ≥0∞).toReal ↔ (↑a : ℝ≥0∞) < (↑b : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
hb : b ≠ ∞
h : a < b
⊢ a.toReal < b.toReal

Tactic:
(toReal_lt_toReal h.ne_top hb).2 h

Premises used: Iff.mpr, LT.lt.ne_top, ENNReal.toReal_lt_toReal
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
hb : b ≠ ∞
h : a ≤ b
⊢ a.toNNReal ≤ b.toNNReal

Tactic:
toReal_mono hb h

Premises used: ENNReal.toReal, ENNReal.toReal_mono, NNReal.toReal
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
p : ℝ≥0
h : (↑p : ℝ≥0∞) ≤ a
ha : a ≠ ∞
⊢ p ≤ a.toNNReal

Tactic:
@toNNReal_coe p ▸ toNNReal_mono ha h

Premises used: ENNReal.toNNReal_coe, Eq.rec, ENNReal.toNNReal_mono
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal ≤ b.toNNReal
rwa : (↑a.toNNReal : ℝ≥0∞) ≤ b
rwa₁ : (↑a.toNNReal : ℝ≥0∞) ≤ (↑b.toNNReal : ℝ≥0∞)
rwa₂ rwa₃ rwa₄ rwa₅ : a.toNNReal ≤ b.toNNReal
⊢ a ≤ b

Tactic:
rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_le_coe]

Premises used: ENNReal.coe_toNNReal, ENNReal.coe_le_coe
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
hb : b ≠ ∞
h : a < b
⊢ a.toNNReal < b.toNNReal

Tactic:
simpa [← ENNReal.coe_lt_coe, hb, h.ne_top]

Premises used: LT.lt.ne_top, ENNReal.coe_lt_coe
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal < b.toNNReal
rwa : (↑a.toNNReal : ℝ≥0∞) < b
rwa₁ : (↑a.toNNReal : ℝ≥0∞) < (↑b.toNNReal : ℝ≥0∞)
rwa₂ rwa₃ rwa₄ rwa₅ : a.toNNReal < b.toNNReal
⊢ a < b

Tactic:
rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_lt_coe]

Premises used: ENNReal.coe_toNNReal, ENNReal.coe_lt_coe
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
p : ℝ≥0
h : a < (↑p : ℝ≥0∞)
⊢ a.toNNReal < p

Tactic:
@toNNReal_coe p ▸ toNNReal_strict_mono coe_ne_top h

Premises used: ENNReal.toNNReal_coe, Eq.rec, ENNReal.toNNReal_strict_mono, ENNReal.coe_ne_top
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
hr : a ≠ ∞
hp : b ≠ ∞
h : a ≤ b
⊢ (max a b).toReal = max a.toReal b.toReal

Tactic:
simp only [h, ENNReal.toReal_mono hp h, max_eq_right]

Premises used: max_eq_right, ENNReal.toReal_mono
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
hr : a ≠ ∞
hp : b ≠ ∞
h : b ≤ a
⊢ (max a b).toReal = max a.toReal b.toReal

Tactic:
simp only [h, ENNReal.toReal_mono hr h, max_eq_left]

Premises used: max_eq_left, ENNReal.toReal_mono
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
hr : a ≠ ∞
hp : b ≠ ∞
h : a ≤ b
⊢ (min a b).toReal = min a.toReal b.toReal

Tactic:
simp only [h, ENNReal.toReal_mono hp h, min_eq_left]

Premises used: min_eq_left, ENNReal.toReal_mono
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
hr : a ≠ ∞
hp : b ≠ ∞
h : b ≤ a
⊢ (min a b).toReal = min a.toReal b.toReal

Tactic:
simp only [h, ENNReal.toReal_mono hr h, min_eq_right]

Premises used: min_eq_right, ENNReal.toReal_mono
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
⊢ a ≠ ∞ → b ≠ ∞ → (max a b).toReal = max a.toReal b.toReal

Tactic:
toReal_max

Premises used: ENNReal.toReal_max
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
⊢ a ≠ ∞ → b ≠ ∞ → (min a b).toReal = min a.toReal b.toReal

Tactic:
toReal_min

Premises used: ENNReal.toReal_min
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
top : 0 < ENNReal.toNNReal ∞ ↔ LT.lt (α := ℝ≥0∞) 0 ∞ ∧ LT.lt (α := ℝ≥0∞) ∞ ∞
coe : ∀ (x : ℝ≥0), 0 < (↑x : ℝ≥0∞).toNNReal ↔ 0 < (↑x : ℝ≥0∞) ∧ (↑x : ℝ≥0∞) < ∞
⊢ 0 < a.toNNReal ↔ 0 < a ∧ a < ∞

Tactic:
induction a
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
⊢ 0 < ENNReal.toNNReal ∞ ↔ LT.lt (α := ℝ≥0∞) 0 ∞ ∧ LT.lt (α := ℝ≥0∞) ∞ ∞

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
x : ℝ≥0
⊢ 0 < (↑x : ℝ≥0∞).toNNReal ↔ 0 < (↑x : ℝ≥0∞) ∧ (↑x : ℝ≥0∞) < ∞

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
ha₀ : a ≠ 0
ha_top : a ≠ ∞
⊢ 0 < a.toNNReal

Tactic:
toNNReal_pos_iff.mpr ⟨bot_lt_iff_ne_bot.mpr ha₀, lt_top_iff_ne_top.mpr ha_top⟩

Premises used: Iff.mpr, bot_lt_iff_ne_bot, lt_top_iff_ne_top, And.intro, ENNReal.toNNReal_pos_iff
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
⊢ 0 < a.toReal ↔ 0 < a ∧ a < ∞

Tactic:
NNReal.coe_pos.trans toNNReal_pos_iff

Premises used: ENNReal.toReal, Iff.trans, NNReal.coe_pos, ENNReal.toNNReal_pos_iff
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
ha₀ : a ≠ 0
ha_top : a ≠ ∞
⊢ 0 < a.toReal

Tactic:
toReal_pos_iff.mpr ⟨bot_lt_iff_ne_bot.mpr ha₀, lt_top_iff_ne_top.mpr ha_top⟩

Premises used: Iff.mpr, ENNReal.toReal_pos_iff, bot_lt_iff_ne_bot, lt_top_iff_ne_top, And.intro
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p q : ℝ
h : p ≤ q
⊢ ENNReal.ofReal p ≤ ENNReal.ofReal q

Tactic:
simp [ENNReal.ofReal, Real.toNNReal_le_toNNReal h]

Premises used: ENNReal.ofReal, Real.toNNReal_le_toNNReal
-- Module: Mathlib.Data.ENNReal.Real
Goal:
⊢ Monotone ENNReal.ofReal

Tactic:
fun _ _ ↦ ENNReal.ofReal_le_ofReal

Premises used: Monotone, ENNReal.ofReal_le_ofReal
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ
b : ℝ≥0∞
h : a ≤ b.toReal
⊢ ENNReal.ofReal a ≤ b

Tactic:
(ofReal_le_ofReal h).trans ofReal_toReal_le

Premises used: ENNReal.ofReal_toReal_le, ENNReal.ofReal_le_ofReal, LE.le.trans
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p q : ℝ
h : 0 ≤ q
rw : (↑p.toNNReal : ℝ≥0∞) ≤ ENNReal.ofReal q ↔ p ≤ q
rw₁ : (↑p.toNNReal : ℝ≥0∞) ≤ (↑q.toNNReal : ℝ≥0∞) ↔ p ≤ q
rw₂ : p.toNNReal ≤ q.toNNReal ↔ p ≤ q
rw₃ rw₄ : p ≤ q ↔ p ≤ q
⊢ ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q

Tactic:
rw [ENNReal.ofReal, ENNReal.ofReal, coe_le_coe, Real.toNNReal_le_toNNReal_iff h]

Premises used: ENNReal.ofReal, Real.toNNReal_le_toNNReal_iff, ENNReal.coe_le_coe
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p q : ℝ
⊢ ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q ∨ p ≤ 0

Tactic:
coe_le_coe.trans Real.toNNReal_le_toNNReal_iff'

Premises used: Real.toNNReal_le_toNNReal_iff', ENNReal.ofReal, ENNReal.coe_le_coe, Iff.trans
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ
b : ℝ≥0
⊢ ENNReal.ofReal a ≤ (↑b : ℝ≥0∞) ↔ a ≤ (↑b : ℝ)

Tactic:
simp [← ofReal_le_ofReal_iff]

Premises used: ENNReal.ofReal_le_ofReal_iff
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p q : ℝ
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q ∧ 0 < q

Tactic:
coe_lt_coe.trans Real.toNNReal_lt_toNNReal_iff'

Premises used: ENNReal.ofReal, ENNReal.coe_lt_coe, Iff.trans, Real.toNNReal_lt_toNNReal_iff'
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
rw : (↑p.toNNReal : ℝ≥0∞) = ENNReal.ofReal q ↔ p = q
rw₁ : (↑p.toNNReal : ℝ≥0∞) = (↑q.toNNReal : ℝ≥0∞) ↔ p = q
rw₂ : p.toNNReal = q.toNNReal ↔ p = q
rw₃ rw₄ : p = q ↔ p = q
⊢ ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q

Tactic:
rw [ENNReal.ofReal, ENNReal.ofReal, coe_inj, Real.toNNReal_eq_toNNReal_iff hp hq]

Premises used: ENNReal.ofReal, ENNReal.coe_inj, Real.toNNReal_eq_toNNReal_iff
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p q : ℝ
h : 0 < q
rw : (↑p.toNNReal : ℝ≥0∞) < ENNReal.ofReal q ↔ p < q
rw₁ : (↑p.toNNReal : ℝ≥0∞) < (↑q.toNNReal : ℝ≥0∞) ↔ p < q
rw₂ : p.toNNReal < q.toNNReal ↔ p < q
rw₃ rw₄ : p < q ↔ p < q
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q

Tactic:
rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff h]

Premises used: ENNReal.ofReal, ENNReal.coe_lt_coe, Real.toNNReal_lt_toNNReal_iff
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p q : ℝ
hp : 0 ≤ p
rw : (↑p.toNNReal : ℝ≥0∞) < ENNReal.ofReal q ↔ p < q
rw₁ : (↑p.toNNReal : ℝ≥0∞) < (↑q.toNNReal : ℝ≥0∞) ↔ p < q
rw₂ : p.toNNReal < q.toNNReal ↔ p < q
rw₃ rw₄ : p < q ↔ p < q
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q

Tactic:
rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff_of_nonneg hp]

Premises used: ENNReal.ofReal, Real.toNNReal_lt_toNNReal_iff_of_nonneg, ENNReal.coe_lt_coe
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p : ℝ
⊢ 0 < ENNReal.ofReal p ↔ 0 < p

Tactic:
simp [ENNReal.ofReal]

Premises used: ENNReal.ofReal
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p : ℝ
⊢ ENNReal.ofReal p = 0 ↔ p ≤ 0

Tactic:
simp [ENNReal.ofReal]

Premises used: ENNReal.ofReal
-- Module: Mathlib.Data.ENNReal.Real
Goal:
x y : ℝ
⊢ ENNReal.ofReal (min x y) = min (ENNReal.ofReal x) (ENNReal.ofReal y)

Tactic:
ofReal_mono.map_min

Premises used: Monotone.map_min, ENNReal.ofReal_mono
-- Module: Mathlib.Data.ENNReal.Real
Goal:
x y : ℝ
⊢ ENNReal.ofReal (max x y) = max (ENNReal.ofReal x) (ENNReal.ofReal y)

Tactic:
ofReal_mono.map_max

Premises used: Monotone.map_max, ENNReal.ofReal_mono
-- Module: Mathlib.Data.ENNReal.Real
Goal:
r : ℝ
rw : 0 < ENNReal.ofReal r ↔ 0 < r
rw₁ rw₂ : 0 < r ↔ 0 < r
⊢ ENNReal.ofReal r ≠ 0 ↔ 0 < r

Tactic:
rw [← pos_iff_ne_zero, ENNReal.ofReal_pos]

Premises used: ENNReal.ofReal_pos, pos_iff_ne_zero
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p : ℝ
⊢ 0 = ENNReal.ofReal p ↔ p ≤ 0

Tactic:
eq_comm.trans ofReal_eq_zero

Premises used: ENNReal.ofReal_eq_zero, eq_comm, Iff.trans
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p : ℝ
n : ℕ
hn : n ≠ 0
⊢ ENNReal.ofReal p < (↑n : ℝ≥0∞) ↔ p < (↑n : ℝ)

Tactic:
exact mod_cast ofReal_lt_ofReal_iff (Nat.cast_pos.2 hn.bot_lt)

Premises used: Iff.mpr, Nat.cast_pos, ENNReal.ofReal_lt_ofReal_iff, Ne.bot_lt
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p : ℝ
⊢ ENNReal.ofReal p < 1 ↔ p < 1

Tactic:
exact mod_cast ofReal_lt_natCast one_ne_zero

Premises used: ENNReal.ofReal_lt_natCast, one_ne_zero
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p : ℝ
n : ℕ
inst : n.AtLeastTwo
⊢ ENNReal.ofReal p < OfNat.ofNat n ↔ p < OfNat.ofNat n

Tactic:
ofReal_lt_natCast (NeZero.ne n)

Premises used: ENNReal.ofReal_lt_natCast, NeZero.ne
-- Module: Mathlib.Data.ENNReal.Real
Goal:
n : ℕ
p : ℝ
hn : n ≠ 0
⊢ (↑n : ℝ≥0∞) ≤ ENNReal.ofReal p ↔ (↑n : ℝ) ≤ p

Tactic:
simp only [← not_lt, ofReal_lt_natCast hn]

Premises used: ENNReal.ofReal_lt_natCast, not_lt
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p : ℝ
⊢ 1 ≤ ENNReal.ofReal p ↔ 1 ≤ p

Tactic:
exact mod_cast natCast_le_ofReal one_ne_zero

Premises used: ENNReal.natCast_le_ofReal, one_ne_zero
-- Module: Mathlib.Data.ENNReal.Real
Goal:
n : ℕ
inst : n.AtLeastTwo
p : ℝ
⊢ OfNat.ofNat n ≤ ENNReal.ofReal p ↔ OfNat.ofNat n ≤ p

Tactic:
natCast_le_ofReal (NeZero.ne n)

Premises used: ENNReal.natCast_le_ofReal, NeZero.ne
-- Module: Mathlib.Data.ENNReal.Real
Goal:
r : ℝ
n : ℕ
⊢ ENNReal.ofReal r ≤ (↑n : ℝ≥0∞) ↔ r ≤ (↑n : ℝ)

Tactic:
coe_le_coe.trans Real.toNNReal_le_natCast

Premises used: ENNReal.ofNNReal, ENNReal.ofReal, Real.toNNReal_le_natCast, ENNReal.coe_le_coe, WithTop.some, Iff.trans
-- Module: Mathlib.Data.ENNReal.Real
Goal:
r : ℝ
⊢ ENNReal.ofReal r ≤ 1 ↔ r ≤ 1

Tactic:
coe_le_coe.trans Real.toNNReal_le_one

Premises used: ENNReal.ofReal, Real.toNNReal_le_one, ENNReal.coe_le_coe, Iff.trans
-- Module: Mathlib.Data.ENNReal.Real
Goal:
r : ℝ
n : ℕ
inst : n.AtLeastTwo
⊢ ENNReal.ofReal r ≤ OfNat.ofNat n ↔ r ≤ OfNat.ofNat n

Tactic:
ofReal_le_natCast

Premises used: ENNReal.ofReal_le_natCast
-- Module: Mathlib.Data.ENNReal.Real
Goal:
n : ℕ
r : ℝ
⊢ (↑n : ℝ≥0∞) < ENNReal.ofReal r ↔ (↑n : ℝ) < r

Tactic:
coe_lt_coe.trans Real.natCast_lt_toNNReal

Premises used: ENNReal.ofNNReal, ENNReal.ofReal, ENNReal.coe_lt_coe, WithTop.some, Iff.trans, Real.natCast_lt_toNNReal
-- Module: Mathlib.Data.ENNReal.Real
Goal:
r : ℝ
⊢ 1 < ENNReal.ofReal r ↔ 1 < r

Tactic:
coe_lt_coe.trans Real.one_lt_toNNReal

Premises used: ENNReal.ofReal, Real.one_lt_toNNReal, ENNReal.coe_lt_coe, Iff.trans
-- Module: Mathlib.Data.ENNReal.Real
Goal:
n : ℕ
inst : n.AtLeastTwo
r : ℝ
⊢ OfNat.ofNat n < ENNReal.ofReal r ↔ OfNat.ofNat n < r

Tactic:
natCast_lt_ofReal

Premises used: ENNReal.natCast_lt_ofReal
-- Module: Mathlib.Data.ENNReal.Real
Goal:
r : ℝ
n : ℕ
h : n ≠ 0
⊢ ENNReal.ofReal r = (↑n : ℝ≥0∞) ↔ r = (↑n : ℝ)

Tactic:
ENNReal.coe_inj.trans <| Real.toNNReal_eq_natCast h

Premises used: ENNReal.ofNNReal, ENNReal.ofReal, ENNReal.coe_inj, Real.toNNReal_eq_natCast, WithTop.some, Iff.trans
-- Module: Mathlib.Data.ENNReal.Real
Goal:
r : ℝ
⊢ ENNReal.ofReal r = 1 ↔ r = 1

Tactic:
ENNReal.coe_inj.trans Real.toNNReal_eq_one

Premises used: ENNReal.ofReal, ENNReal.coe_inj, Iff.trans, Real.toNNReal_eq_one
-- Module: Mathlib.Data.ENNReal.Real
Goal:
r : ℝ
n : ℕ
inst : n.AtLeastTwo
⊢ ENNReal.ofReal r = OfNat.ofNat n ↔ r = OfNat.ofNat n

Tactic:
ofReal_eq_natCast (NeZero.ne n)

Premises used: ENNReal.ofReal_eq_natCast, NeZero.ne
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ
b : ℝ≥0∞
hb : b ≠ ∞
⊢ b ≠ ∞

Tactic:
hb
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ
b : ℝ≥0∞
hb : b ≠ ∞
lift : ∀ (b : ℝ≥0), ENNReal.ofReal a ≤ (↑b : ℝ≥0∞) ↔ a ≤ (↑b : ℝ≥0∞).toReal
⊢ ENNReal.ofReal a ≤ b ↔ a ≤ b.toReal

Tactic:
lift b to ℝ≥0 using hb
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ
b : ℝ≥0
⊢ ENNReal.ofReal a ≤ (↑b : ℝ≥0∞) ↔ a ≤ (↑b : ℝ≥0∞).toReal

Tactic:
simpa [ENNReal.ofReal, ENNReal.toReal] using Real.toNNReal_le_iff_le_coe

Premises used: ENNReal.ofReal, ENNReal.toReal, Real.toNNReal_le_iff_le_coe
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ
b : ℝ≥0∞
ha : 0 ≤ a
hb : b ≠ ∞
⊢ b ≠ ∞

Tactic:
hb
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ
b : ℝ≥0∞
ha : 0 ≤ a
hb : b ≠ ∞
lift : ∀ (b : ℝ≥0), ENNReal.ofReal a < (↑b : ℝ≥0∞) ↔ a < (↑b : ℝ≥0∞).toReal
⊢ ENNReal.ofReal a < b ↔ a < b.toReal

Tactic:
lift b to ℝ≥0 using hb
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ
ha : 0 ≤ a
b : ℝ≥0
⊢ ENNReal.ofReal a < (↑b : ℝ≥0∞) ↔ a < (↑b : ℝ≥0∞).toReal

Tactic:
simpa [ENNReal.ofReal, ENNReal.toReal] using Real.toNNReal_lt_iff_lt_coe ha

Premises used: ENNReal.ofReal, Real.toNNReal_lt_iff_lt_coe, ENNReal.toReal
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0
b : ℝ
⊢ (↑a : ℝ≥0∞) < ENNReal.ofReal b ↔ (↑a : ℝ) < b

Tactic:
simp [ENNReal.ofReal, Real.lt_toNNReal_iff_coe_lt]

Premises used: ENNReal.ofReal, Real.lt_toNNReal_iff_coe_lt
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ
b : ℝ≥0
ha : 0 ≤ a
rw rw₁ : a < (↑b : ℝ) ↔ a < (↑b : ℝ)
⊢ a < (↑b : ℝ≥0∞).toReal ↔ a < (↑b : ℝ)

Tactic:
rw [coe_toReal]

Premises used: ENNReal.coe_toReal
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
b : ℝ
ha : a ≠ ∞
hb : 0 ≤ b
⊢ a ≠ ∞

Tactic:
ha
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
b : ℝ
ha : a ≠ ∞
hb : 0 ≤ b
lift : ∀ (a : ℝ≥0), (↑a : ℝ≥0∞) ≤ ENNReal.ofReal b ↔ (↑a : ℝ≥0∞).toReal ≤ b
⊢ a ≤ ENNReal.ofReal b ↔ a.toReal ≤ b

Tactic:
lift a to ℝ≥0 using ha
-- Module: Mathlib.Data.ENNReal.Real
Goal:
b : ℝ
hb : 0 ≤ b
a : ℝ≥0
⊢ (↑a : ℝ≥0∞) ≤ ENNReal.ofReal b ↔ (↑a : ℝ≥0∞).toReal ≤ b

Tactic:
simpa [ENNReal.ofReal, ENNReal.toReal] using Real.le_toNNReal_iff_coe_le hb

Premises used: Real.le_toNNReal_iff_coe_le, ENNReal.ofReal, ENNReal.toReal
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
b : ℝ
hb : 0 ≤ b
h : a ≤ ENNReal.ofReal b
⊢ a.toReal ≤ b

Tactic:
have ha : a ≠ ∞ := ne_top_of_le_ne_top ofReal_ne_top h
  (le_ofReal_iff_toReal_le ha hb).1 h

Premises used: ne_top_of_le_ne_top, ENNReal.le_ofReal_iff_toReal_le, Iff.mp, ENNReal.ofReal_ne_top
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
b : ℝ
ha : a ≠ ∞
⊢ a ≠ ∞

Tactic:
ha
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
b : ℝ
ha : a ≠ ∞
lift : ∀ (a : ℝ≥0), (↑a : ℝ≥0∞) < ENNReal.ofReal b ↔ (↑a : ℝ≥0∞).toReal < b
⊢ a < ENNReal.ofReal b ↔ a.toReal < b

Tactic:
lift a to ℝ≥0 using ha
-- Module: Mathlib.Data.ENNReal.Real
Goal:
b : ℝ
a : ℝ≥0
⊢ (↑a : ℝ≥0∞) < ENNReal.ofReal b ↔ (↑a : ℝ≥0∞).toReal < b

Tactic:
simpa [ENNReal.ofReal, ENNReal.toReal] using Real.lt_toNNReal_iff_coe_lt

Premises used: ENNReal.ofReal, ENNReal.toReal, Real.lt_toNNReal_iff_coe_lt
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
b : ℝ
h : a < ENNReal.ofReal b
⊢ a.toReal < b

Tactic:
(lt_ofReal_iff_toReal_lt h.ne_top).1 h

Premises used: LT.lt.ne_top, ENNReal.lt_ofReal_iff_toReal_lt, Iff.mp
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p q : ℝ
hp : 0 ≤ p
⊢ ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q

Tactic:
simp only [ENNReal.ofReal, ← coe_mul, Real.toNNReal_mul hp]

Premises used: Real.toNNReal_mul, ENNReal.ofReal, ENNReal.coe_mul
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p q : ℝ
hq : 0 ≤ q
rw : ENNReal.ofReal (q * p) = ENNReal.ofReal p * ENNReal.ofReal q
rw₁ : ENNReal.ofReal q * ENNReal.ofReal p = ENNReal.ofReal p * ENNReal.ofReal q
rw₂ rw₃ : ENNReal.ofReal p * ENNReal.ofReal q = ENNReal.ofReal p * ENNReal.ofReal q
⊢ ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q

Tactic:
rw [mul_comm, ofReal_mul hq, mul_comm]

Premises used: ENNReal.ofReal_mul, mul_comm
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p : ℝ
hp : 0 ≤ p
n : ℕ
rw : ENNReal.ofReal (p ^ n) = (↑(NNReal.mk p hp) : ℝ≥0∞) ^ n
rw₁ : ENNReal.ofReal (p ^ n) = (↑(NNReal.mk p hp ^ n) : ℝ≥0∞)
rw₂ : ENNReal.ofReal (p ^ n) = ENNReal.ofReal (↑(NNReal.mk p hp ^ n) : ℝ)
rw₃ : ENNReal.ofReal (p ^ n) = ENNReal.ofReal ((↑(NNReal.mk p hp) : ℝ) ^ n)
rw₄ rw₅ : ENNReal.ofReal (p ^ n) = ENNReal.ofReal (p ^ n)
⊢ ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n

Tactic:
rw [ofReal_eq_coe_nnreal hp, ← coe_pow, ← ofReal_coe_nnreal, NNReal.coe_pow, NNReal.coe_mk]

Premises used: NNReal.coe_mk, ENNReal.ofReal_eq_coe_nnreal, NNReal.coe_pow, ENNReal.ofReal_coe_nnreal, ENNReal.coe_pow