awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x y : ℝ≥0
⊢ (↑(x * y) : ℝ≥0∞) = (↑x : ℝ≥0∞) * (↑y : ℝ≥0∞)

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.some, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
x : ℝ≥0
⊢ (↑(n • x) : ℝ≥0∞) = n • (↑x : ℝ≥0∞)

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.some, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x : ℝ≥0
n : ℕ
⊢ (↑(x ^ n) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ n

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.some, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ (↑(OfNat.ofNat n) : ℝ≥0∞) = OfNat.ofNat n

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.some, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ (↑2 : ℝ≥0∞) = 2

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.some, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x y : ℝ≥0∞
⊢ x.toNNReal = y.toNNReal ↔ x = y ∨ x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0

Tactic:
WithTop.untopD_eq_untopD_iff

Premises used: ENNReal.ofNNReal, ENNReal.toNNReal, WithTop.some, ENNReal, WithTop.untopD_eq_untopD_iff
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x y : ℝ≥0∞
⊢ x.toReal = y.toReal ↔ x = y ∨ x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0

Tactic:
simp only [ENNReal.toReal, NNReal.coe_inj, toNNReal_eq_toNNReal_iff]

Premises used: ENNReal.toNNReal_eq_toNNReal_iff, ENNReal.toReal, NNReal.coe_inj
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x y : ℝ≥0∞
hx : x ≠ ∞
hy : y ≠ ∞
⊢ x.toNNReal = y.toNNReal ↔ x = y

Tactic:
simp only [ENNReal.toNNReal_eq_toNNReal_iff x y, hx, hy, and_false, false_and, or_false]

Premises used: ENNReal.toNNReal_eq_toNNReal_iff, false_and, or_false, and_false
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x y : ℝ≥0∞
hx : x ≠ ∞
hy : y ≠ ∞
⊢ x.toReal = y.toReal ↔ x = y

Tactic:
simp only [ENNReal.toReal, NNReal.coe_inj, toNNReal_eq_toNNReal_iff' hx hy]

Premises used: ENNReal.toNNReal_eq_toNNReal_iff', ENNReal.toReal, NNReal.coe_inj
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ LT.lt (α := ℝ≥0∞) 1 2

Tactic:
Nat.one_lt_ofNat

Premises used: Nat.one_lt_ofNat
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
⊢ Fact (LE.le (α := ℝ≥0∞) 1 1)

Tactic:
⟨le_rfl⟩

Premises used: le_rfl, Fact.mk
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
⊢ Fact (LE.le (α := ℝ≥0∞) 1 2)

Tactic:
⟨one_le_two⟩

Premises used: Fact.mk, one_le_two
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
⊢ Fact (LE.le (α := ℝ≥0∞) 1 ∞)

Tactic:
⟨le_top⟩

Premises used: Fact.mk, le_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
inst : InfSet α
f : ℝ≥0∞ → α
⊢ Eq.{u_1 + 1} (α := α) (⨅ (x : { x : ℝ≥0∞ // x ≠ ∞ }), f (↑x : ℝ≥0∞)) (⨅ (x : ℝ≥0), f (↑x : ℝ≥0∞))

Tactic:
Eq.symm <| neTopEquivNNReal.symm.surjective.iInf_congr _ fun _ => rfl

Premises used: ENNReal.neTopEquivNNReal, Function.Surjective.iInf_congr, Equiv.surjective, Equiv.symm, Eq.symm, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℝ≥0∞ → α
rw : Eq.{u_1 + 1} (α := α) (⨅ (x : { x : ℝ≥0∞ // x ≠ ∞ }), f (↑x : ℝ≥0∞)) (⨅ (x : ℝ≥0), f (↑x : ℝ≥0∞))
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (⨅ (x : ℝ≥0), f (↑x : ℝ≥0∞)) (⨅ (x : ℝ≥0), f (↑x : ℝ≥0∞))
⊢ Eq.{u_1 + 1} (α := α) (⨅ (x : ℝ≥0∞), ⨅ (_ : x ≠ ∞), f x) (⨅ (x : ℝ≥0), f (↑x : ℝ≥0∞))

Tactic:
rw [iInf_subtype', cinfi_ne_top]

Premises used: iInf_subtype', ENNReal.cinfi_ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
inst : SupSet α
f : ℝ≥0∞ → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : { x : ℝ≥0∞ // x ≠ ∞ }), f (↑x : ℝ≥0∞)) (⨆ (x : ℝ≥0), f (↑x : ℝ≥0∞))

Tactic:
@cinfi_ne_top αᵒᵈ _ _

Premises used: iSup, ENNReal.cinfi_ne_top, OrderDual
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℝ≥0∞ → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ℝ≥0∞), ⨆ (_ : x ≠ ∞), f x) (⨆ (x : ℝ≥0), f (↑x : ℝ≥0∞))

Tactic:
@iInf_ne_top αᵒᵈ _ _

Premises used: iSup, ENNReal.iInf_ne_top, OrderDual
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
f : ℝ≥0∞ → α
⊢ ⨅ (n : ℝ≥0∞), f n = (⨅ (n : ℝ≥0), f (↑n : ℝ≥0∞)) ⊓ f ∞

Tactic:
(iInf_option f).trans (inf_comm _ _)

Premises used: iInf_option, inf_comm, ENNReal, Eq.trans, WithTop
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
f : ℝ≥0∞ → α
⊢ ⨆ (n : ℝ≥0∞), f n = (⨆ (n : ℝ≥0), f (↑n : ℝ≥0∞)) ⊔ f ∞

Tactic:
@iInf_ennreal αᵒᵈ _ _

Premises used: ENNReal.iInf_ennreal, iSup, OrderDual
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ Eq (α := (a : ℝ≥0) → ℝ≥0∞) (⇑ofNNRealHom : (a : ℝ≥0) → ℝ≥0∞) WithTop.some

Tactic:
rfl

Premises used: WithTop.some, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ Eq (α := ℝ≥0∞) ⊥ 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
⊢ ¬∞ ≤ (↑r : ℝ≥0∞)

Tactic:
WithTop.not_top_le_coe r

Premises used: ENNReal.ofNNReal, WithTop.not_top_le_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
⊢ 1 ≤ (↑r : ℝ≥0∞) ↔ 1 ≤ r

Tactic:
coe_le_coe

Premises used: ENNReal.coe_le_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) ≤ 1 ↔ r ≤ 1

Tactic:
coe_le_coe

Premises used: ENNReal.coe_le_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
p : ℝ≥0
⊢ (↑p : ℝ≥0∞) < 1 ↔ p < 1

Tactic:
coe_lt_coe

Premises used: ENNReal.coe_lt_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
p : ℝ≥0
⊢ 1 < (↑p : ℝ≥0∞) ↔ 1 < p

Tactic:
coe_lt_coe

Premises used: ENNReal.coe_lt_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
⊢ (↑(↑n : ℝ≥0) : ℝ≥0∞) = (↑n : ℝ≥0∞)

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.some, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
⊢ ENNReal.ofReal (↑n : ℝ) = (↑n : ℝ≥0∞)

Tactic:
simp [ENNReal.ofReal]

Premises used: ENNReal.ofReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ ENNReal.ofReal (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
ofReal_natCast n

Premises used: ENNReal.ofReal_natCast
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
⊢ Ne (α := ℝ≥0∞) (↑n : ℝ≥0∞) ∞

Tactic:
WithTop.natCast_ne_top n

Premises used: WithTop.natCast_ne_top, ENNReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) (↑n : ℝ≥0∞) ∞

Tactic:
WithTop.natCast_lt_top n

Premises used: WithTop.natCast_lt_top, ENNReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ Ne (α := ℝ≥0∞) (OfNat.ofNat n) ∞

Tactic:
natCast_ne_top n

Premises used: ENNReal.natCast_ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ LT.lt (α := ℝ≥0∞) (OfNat.ofNat n) ∞

Tactic:
natCast_lt_top n

Premises used: ENNReal.natCast_lt_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
⊢ Ne (α := ℝ≥0∞) ∞ (↑n : ℝ≥0∞)

Tactic:
WithTop.top_ne_natCast n

Premises used: ENNReal, WithTop.top_ne_natCast
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ Ne (α := ℝ≥0∞) ∞ (OfNat.ofNat n)

Tactic:
ofNat_ne_top.symm

Premises used: ENNReal.ofNat_ne_top, Ne.symm
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
n : ℕ
⊢ (↑n : ℝ≥0∞) ≤ (↑r : ℝ≥0∞) ↔ (↑n : ℝ≥0) ≤ r

Tactic:
simp [← coe_le_coe]

Premises used: ENNReal.coe_le_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
n : ℕ
⊢ (↑r : ℝ≥0∞) ≤ (↑n : ℝ≥0∞) ↔ r ≤ (↑n : ℝ≥0)

Tactic:
simp [← coe_le_coe]

Premises used: ENNReal.coe_le_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
n : ℕ
⊢ (↑(r + (↑n : ℝ≥0)) : ℝ≥0∞) = (↑r : ℝ≥0∞) + (↑n : ℝ≥0∞)

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.map₂, WithTop.some, rfl, Option.map₂
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
r : ℝ≥0
⊢ (↑((↑n : ℝ≥0) + r) : ℝ≥0∞) = (↑n : ℝ≥0∞) + (↑r : ℝ≥0∞)

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.map₂, WithTop.some, rfl, Option.map₂
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
n : ℕ
⊢ (↑(r - (↑n : ℝ≥0)) : ℝ≥0∞) = (↑r : ℝ≥0∞) - (↑n : ℝ≥0∞)

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.some, WithTop.sub, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
r : ℝ≥0
⊢ (↑((↑n : ℝ≥0) - r) : ℝ≥0∞) = (↑n : ℝ≥0∞) - (↑r : ℝ≥0∞)

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.some, WithTop.sub, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ LT.lt (α := ℝ≥0∞) 1 ∞

Tactic:
coe_lt_top

Premises used: ENNReal.coe_lt_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
rw : (↑(↑n : ℝ≥0) : ℝ≥0∞).toNNReal = (↑n : ℝ≥0)
rw₁ rw₂ : Eq (α := ℝ≥0) (↑n : ℝ≥0) (↑n : ℝ≥0)
⊢ ENNReal.toNNReal (↑n : ℝ≥0∞) = (↑n : ℝ≥0)

Tactic:
rw [← ENNReal.coe_natCast n, ENNReal.toNNReal_coe]

Premises used: ENNReal.toNNReal_coe, ENNReal.coe_natCast
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ ENNReal.toNNReal (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
toNNReal_natCast n

Premises used: ENNReal.toNNReal_natCast
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
rw : (ENNReal.ofReal (↑n : ℝ)).toReal = (↑n : ℝ)
rw₁ rw₂ : Eq (α := ℝ) (↑n : ℝ) (↑n : ℝ)
⊢ ENNReal.toReal (↑n : ℝ≥0∞) = (↑n : ℝ)

Tactic:
rw [← ENNReal.ofReal_natCast n, ENNReal.toReal_ofReal (Nat.cast_nonneg _)]

Premises used: Nat.cast_nonneg, ENNReal.toReal_ofReal, ENNReal.ofReal_natCast
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ ENNReal.toReal (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
toReal_natCast n

Premises used: ENNReal.toReal_natCast
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
⊢ LE.le (α := ℝ) 0 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
n : ℕ
rw : ENNReal.toNNReal (↑n : ℝ≥0∞) = NNReal.mk (↑n : ℝ) ⋯
rw₁ : (↑n : ℝ≥0) = NNReal.mk (↑n : ℝ) ⋯
rw₂ rw₃ : Eq (α := ℝ≥0) (↑n : ℝ≥0) (↑n : ℝ≥0)
⊢ ENNReal.toNNReal (↑n : ℝ≥0∞) = Real.toNNReal (↑n : ℝ)

Tactic:
rw [Real.toNNReal_of_nonneg (by positivity), ENNReal.toNNReal_natCast, mk_natCast]

Premises used: ENNReal.toNNReal_natCast, Real.toNNReal_of_nonneg, NNReal.mk_natCast
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
r : ℝ≥0
⊢ a ≤ (↑r : ℝ≥0∞) ↔ ∃ (p : ℝ≥0), a = (↑p : ℝ≥0∞) ∧ p ≤ r

Tactic:
WithTop.le_coe_iff

Premises used: ENNReal.ofNNReal, WithTop.le_coe_iff, ENNReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) ≤ a ↔ ∀ (p : ℝ≥0), a = (↑p : ℝ≥0∞) → r ≤ p

Tactic:
WithTop.coe_le_iff

Premises used: ENNReal.ofNNReal, WithTop.coe_le_iff, ENNReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
⊢ a < b ↔ ∃ (p : ℝ≥0), a = (↑p : ℝ≥0∞) ∧ (↑p : ℝ≥0∞) < b

Tactic:
WithTop.lt_iff_exists_coe

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.lt_iff_exists_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
b : ℝ≥0
h : a ≤ (↑b : ℝ≥0∞)
⊢ a ≠ ∞

Tactic:
ne_top_of_le_ne_top coe_ne_top h

Premises used: ne_top_of_le_ne_top, ENNReal.coe_ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
b : ℝ≥0
h : a ≤ (↑b : ℝ≥0∞)
lift : ∀ (a : ℝ≥0) (h : (↑a : ℝ≥0∞) ≤ (↑b : ℝ≥0∞)), (↑a : ℝ≥0∞).toReal ≤ (↑b : ℝ)
⊢ a.toReal ≤ (↑b : ℝ)

Tactic:
lift a to ℝ≥0 using ne_top_of_le_ne_top coe_ne_top h

Premises used: ne_top_of_le_ne_top, ENNReal.coe_ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
b a : ℝ≥0
h : (↑a : ℝ≥0∞) ≤ (↑b : ℝ≥0∞)
⊢ (↑a : ℝ≥0∞).toReal ≤ (↑b : ℝ)

Tactic:
simpa using h
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
⊢ max a b = 0 ↔ a = 0 ∧ b = 0

Tactic:
max_eq_bot

Premises used: max_eq_bot
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
⊢ min a b = 0 ↔ a = 0 ∨ b = 0

Tactic:
min_eq_bot

Premises used: min_eq_bot
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
⊢ max 0 a = a

Tactic:
max_eq_right zero_le

Premises used: zero_le, max_eq_right
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
⊢ max a 0 = a

Tactic:
max_eq_left zero_le

Premises used: zero_le, max_eq_left
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
h : a < b
rcases :
  ∀ (p : ℝ≥0),
    (↑p : ℝ≥0∞) < b →
      ∀ (h : (↑p : ℝ≥0∞) < b),
        ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b
⊢ ∃ (q : ℚ), 0 ≤ q ∧ a < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b

Tactic:
rcases lt_iff_exists_coe.1 h with ⟨p, rfl, _⟩

Premises used: ENNReal.lt_iff_exists_coe, Iff.mp, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
b : ℝ≥0∞
p : ℝ≥0
right h : (↑p : ℝ≥0∞) < b
rcases :
  ∀ (c : ℝ≥0∞) (pc : (↑p : ℝ≥0∞) < c) (cb : c < b),
    ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b
⊢ ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b

Tactic:
rcases exists_between h with ⟨c, pc, cb⟩

Premises used: exists_between
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
b : ℝ≥0∞
p : ℝ≥0
right h : (↑p : ℝ≥0∞) < b
c : ℝ≥0∞
pc : (↑p : ℝ≥0∞) < c
cb : c < b
rcases :
  ∀ (r : ℝ≥0),
    (↑r : ℝ≥0∞) < b →
      ∀ (pc : (↑p : ℝ≥0∞) < (↑r : ℝ≥0∞)) (cb : (↑r : ℝ≥0∞) < b),
        ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b
⊢ ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b

Tactic:
rcases lt_iff_exists_coe.1 cb with ⟨r, rfl, _⟩

Premises used: ENNReal.lt_iff_exists_coe, Iff.mp, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
b : ℝ≥0∞
p : ℝ≥0
right h : (↑p : ℝ≥0∞) < b
r : ℝ≥0
right_1 : (↑r : ℝ≥0∞) < b
pc : (↑p : ℝ≥0∞) < (↑r : ℝ≥0∞)
cb : (↑r : ℝ≥0∞) < b
rcases :
  ∀ (q : ℚ) (hq0 : 0 ≤ q) (pq : p < Real.toNNReal (↑q : ℝ)) (qr : Real.toNNReal (↑q : ℝ) < r),
    ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b
⊢ ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b

Tactic:
rcases (NNReal.lt_iff_exists_rat_btwn _ _).1 (coe_lt_coe.1 pc) with ⟨q, hq0, pq, qr⟩

Premises used: NNReal.lt_iff_exists_rat_btwn, ENNReal.coe_lt_coe, Iff.mp
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
b : ℝ≥0∞
p : ℝ≥0
right h : (↑p : ℝ≥0∞) < b
r : ℝ≥0
right_1 : (↑r : ℝ≥0∞) < b
pc : (↑p : ℝ≥0∞) < (↑r : ℝ≥0∞)
cb : (↑r : ℝ≥0∞) < b
q : ℚ
hq0 : 0 ≤ q
pq : p < Real.toNNReal (↑q : ℝ)
qr : Real.toNNReal (↑q : ℝ) < r
⊢ ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b

Tactic:
⟨q, hq0, coe_lt_coe.2 pq, lt_trans (coe_lt_coe.2 qr) cb⟩

Premises used: Iff.mpr, lt_trans, ENNReal.coe_lt_coe, And.intro, Exists.intro
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
b : ℝ≥0∞
p : ℝ≥0
right h : (↑p : ℝ≥0∞) < b
r : ℝ≥0
right_1 : (↑r : ℝ≥0∞) < b
pc : (↑p : ℝ≥0∞) < (↑r : ℝ≥0∞)
cb : (↑r : ℝ≥0∞) < b
q : ℚ
hq0 : 0 ≤ q
pq : p < Real.toNNReal (↑q : ℝ)
qr : Real.toNNReal (↑q : ℝ) < r
⊢ ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b

Tactic:
exact ⟨q, hq0, coe_lt_coe.2 pq, lt_trans (coe_lt_coe.2 qr) cb⟩
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
⊢ a < b ↔ ∃ (r : ℝ), 0 ≤ r ∧ a < ENNReal.ofReal r ∧ ENNReal.ofReal r < b

Tactic:
⟨fun h =>
    let ⟨q, q0, aq, qb⟩ := ENNReal.lt_iff_exists_rat_btwn.1 h
    ⟨q, Rat.cast_nonneg.2 q0, aq, qb⟩,
    fun ⟨_, _, qa, qb⟩ => lt_trans qa qb⟩

Premises used: Iff.mpr, ENNReal.ofReal, lt_trans, _private.0.ENNReal.lt_iff_exists_real_btwn.match_2, Exists, Rat.cast, LE.le, And, Rat.cast_nonneg, And.intro, LT.lt, Iff.intro, Exists.intro, Iff.mp, ENNReal.lt_iff_exists_rat_btwn, _private.0.ENNReal.lt_iff_exists_real_btwn.match_1, OfNat.ofNat
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
⊢ a < b ↔ ∃ (r : ℝ≥0), a < (↑r : ℝ≥0∞) ∧ (↑r : ℝ≥0∞) < b

Tactic:
WithTop.lt_iff_exists_coe_btwn

Premises used: ENNReal.ofNNReal, WithTop.lt_iff_exists_coe_btwn
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
⊢ a < b ↔ ∃ (r : ℝ≥0), 0 < r ∧ a + (↑r : ℝ≥0∞) < b

Tactic:
⟨fun hab => ?_, fun ⟨r, _, hr⟩ => lt_of_le_of_lt le_self_add hr⟩

Premises used: lt_of_le_of_lt, LT.lt, Iff.intro, le_self_add, _private.0.ENNReal.lt_iff_exists_add_pos_lt.match_1
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
refine : ∀ (hab : a < b), ∃ (r : ℝ≥0), 0 < r ∧ a + (↑r : ℝ≥0∞) < b
⊢ a < b ↔ ∃ (r : ℝ≥0), 0 < r ∧ a + (↑r : ℝ≥0∞) < b

Tactic:
refine ⟨fun hab => ?_, fun ⟨r, _, hr⟩ => lt_of_le_of_lt le_self_add hr⟩
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
hab : a < b
rcases : ∀ (c : ℝ≥0) (ac : a < (↑c : ℝ≥0∞)) (cb : (↑c : ℝ≥0∞) < b), ∃ (r : ℝ≥0), 0 < r ∧ a + (↑r : ℝ≥0∞) < b
⊢ ∃ (r : ℝ≥0), 0 < r ∧ a + (↑r : ℝ≥0∞) < b

Tactic:
rcases lt_iff_exists_nnreal_btwn.1 hab with ⟨c, ac, cb⟩

Premises used: ENNReal.lt_iff_exists_nnreal_btwn, Iff.mp
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
hab : a < b
c : ℝ≥0
ac : a < (↑c : ℝ≥0∞)
cb : (↑c : ℝ≥0∞) < b
⊢ a ≠ ∞

Tactic:
ac.ne_top

Premises used: LT.lt.ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
hab : a < b
c : ℝ≥0
ac : a < (↑c : ℝ≥0∞)
cb : (↑c : ℝ≥0∞) < b
lift :
  ∀ (a : ℝ≥0) (hab : (↑a : ℝ≥0∞) < b) (ac : (↑a : ℝ≥0∞) < (↑c : ℝ≥0∞)),
    ∃ (r : ℝ≥0), 0 < r ∧ (↑a : ℝ≥0∞) + (↑r : ℝ≥0∞) < b
⊢ ∃ (r : ℝ≥0), 0 < r ∧ a + (↑r : ℝ≥0∞) < b

Tactic:
lift a to ℝ≥0 using ac.ne_top

Premises used: LT.lt.ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
b : ℝ≥0∞
c : ℝ≥0
cb : (↑c : ℝ≥0∞) < b
a : ℝ≥0
hab : (↑a : ℝ≥0∞) < b
ac : (↑a : ℝ≥0∞) < (↑c : ℝ≥0∞)
⊢ a < c

Tactic:
rw [coe_lt_coe] at ac

Premises used: ENNReal.coe_lt_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
b : ℝ≥0∞
c : ℝ≥0
cb : (↑c : ℝ≥0∞) < b
a : ℝ≥0
hab : (↑a : ℝ≥0∞) < b
ac : a < c
⊢ ∃ (r : ℝ≥0), 0 < r ∧ (↑a : ℝ≥0∞) + (↑r : ℝ≥0∞) < b

Tactic:
⟨c - a, tsub_pos_iff_lt.2 ac, ?_⟩

Premises used: Iff.mpr, tsub_pos_iff_lt, HSub.hSub, And.intro, Exists.intro
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
b : ℝ≥0∞
c : ℝ≥0
cb : (↑c : ℝ≥0∞) < b
a : ℝ≥0
hab : (↑a : ℝ≥0∞) < b
ac : a < c
refine : (↑a : ℝ≥0∞) + (↑(c - a) : ℝ≥0∞) < b
⊢ ∃ (r : ℝ≥0), 0 < r ∧ (↑a : ℝ≥0∞) + (↑r : ℝ≥0∞) < b

Tactic:
refine ⟨c - a, tsub_pos_iff_lt.2 ac, ?_⟩
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
b : ℝ≥0∞
c : ℝ≥0
cb : (↑c : ℝ≥0∞) < b
a : ℝ≥0
hab : (↑a : ℝ≥0∞) < b
ac : a < c
rwa : (↑(a + (c - a)) : ℝ≥0∞) < b
rwa₁ rwa₂ rwa₃ rwa₄ : (↑c : ℝ≥0∞) < b
⊢ (↑a : ℝ≥0∞) + (↑(c - a) : ℝ≥0∞) < b

Tactic:
rwa [← coe_add, add_tsub_cancel_of_le ac.le]

Premises used: LT.lt.le, ENNReal.coe_add, add_tsub_cancel_of_le
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
h : ∀ (ε : ℝ≥0), 0 < ε → b < ∞ → a ≤ b + (↑ε : ℝ≥0∞)
contrapose! : ∀ (h : b < a), ∃ (ε : ℝ≥0), 0 < ε ∧ b < ∞ ∧ b + (↑ε : ℝ≥0∞) < a
⊢ a ≤ b

Tactic:
contrapose! h
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
h : b < a
rcases : ∀ (r : ℝ≥0) (hr0 : 0 < r) (hr : b + (↑r : ℝ≥0∞) < a), ∃ (ε : ℝ≥0), 0 < ε ∧ b < ∞ ∧ b + (↑ε : ℝ≥0∞) < a
⊢ ∃ (ε : ℝ≥0), 0 < ε ∧ b < ∞ ∧ b + (↑ε : ℝ≥0∞) < a

Tactic:
rcases lt_iff_exists_add_pos_lt.1 h with ⟨r, hr0, hr⟩

Premises used: ENNReal.lt_iff_exists_add_pos_lt, Iff.mp
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
h : b < a
r : ℝ≥0
hr0 : 0 < r
hr : b + (↑r : ℝ≥0∞) < a
⊢ ∃ (ε : ℝ≥0), 0 < ε ∧ b < ∞ ∧ b + (↑ε : ℝ≥0∞) < a

Tactic:
⟨r, hr0, h.trans_le le_top, hr⟩

Premises used: LT.lt.trans_le, le_top, And.intro, Exists.intro
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
h : b < a
r : ℝ≥0
hr0 : 0 < r
hr : b + (↑r : ℝ≥0∞) < a
⊢ ∃ (ε : ℝ≥0), 0 < ε ∧ b < ∞ ∧ b + (↑ε : ℝ≥0∞) < a

Tactic:
exact ⟨r, hr0, h.trans_le le_top, hr⟩
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
n : ℕ
⊢ (↑n : ℝ≥0∞) < (↑r : ℝ≥0∞) ↔ (↑n : ℝ≥0) < r

Tactic:
ENNReal.coe_natCast n ▸ coe_lt_coe

Premises used: ENNReal.coe_lt_coe, Eq.rec, ENNReal.coe_natCast
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
n : ℕ
⊢ (↑r : ℝ≥0∞) < (↑n : ℝ≥0∞) ↔ r < (↑n : ℝ≥0)

Tactic:
ENNReal.coe_natCast n ▸ coe_lt_coe

Premises used: ENNReal.coe_lt_coe, Eq.rec, ENNReal.coe_natCast
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0∞
h : r ≠ ∞
⊢ r ≠ ∞

Tactic:
h
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0∞
h : r ≠ ∞
lift : ∀ (r : ℝ≥0), ∃ (n : ℕ), (↑r : ℝ≥0∞) < (↑n : ℝ≥0∞)
⊢ ∃ (n : ℕ), r < (↑n : ℝ≥0∞)

Tactic:
lift r to ℝ≥0 using h
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
rcases : ∀ (n : ℕ) (hn : r < (↑n : ℝ≥0)), ∃ (n : ℕ), (↑r : ℝ≥0∞) < (↑n : ℝ≥0∞)
⊢ ∃ (n : ℕ), (↑r : ℝ≥0∞) < (↑n : ℝ≥0∞)

Tactic:
rcases exists_nat_gt r with ⟨n, hn⟩

Premises used: exists_nat_gt
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
n : ℕ
hn : r < (↑n : ℝ≥0)
⊢ ∃ (n : ℕ), (↑r : ℝ≥0∞) < (↑n : ℝ≥0∞)

Tactic:
⟨n, coe_lt_natCast.2 hn⟩

Premises used: Iff.mpr, ENNReal.coe_lt_natCast, Exists.intro
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
n : ℕ
hn : r < (↑n : ℝ≥0)
⊢ ∃ (n : ℕ), (↑r : ℝ≥0∞) < (↑n : ℝ≥0∞)

Tactic:
exact ⟨n, coe_lt_natCast.2 hn⟩
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
h : ∀ (x : ℝ≥0∞), Membership.mem (γ := Set ℝ≥0∞) (⋃ (n : ℕ), Iio (↑n : ℝ≥0∞)) x ↔ Membership.mem (γ := Set ℝ≥0∞) {∞}ᶜ x
⊢ Eq (α := Set ℝ≥0∞) (⋃ (n : ℕ), Iio (↑n : ℝ≥0∞)) {∞}ᶜ

Tactic:
ext x
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x : ℝ≥0∞
h : (∃ (i : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Iio (↑i : ℝ≥0∞)) x) ↔ Membership.mem (γ := Set ℝ≥0∞) {∞}ᶜ x
⊢ Membership.mem (γ := Set ℝ≥0∞) (⋃ (n : ℕ), Iio (↑n : ℝ≥0∞)) x ↔ Membership.mem (γ := Set ℝ≥0∞) {∞}ᶜ x

Tactic:
rw [mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x : ℝ≥0∞
⊢ (∃ (i : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Iio (↑i : ℝ≥0∞)) x) ↔ Membership.mem (γ := Set ℝ≥0∞) {∞}ᶜ x

Tactic:
⟨fun ⟨n, hn⟩ => ne_top_of_lt hn, ENNReal.exists_nat_gt⟩

Premises used: Compl.compl, ENNReal.exists_nat_gt, _private.0.ENNReal.iUnion_Iio_coe_nat.match_1, Membership.mem, Iff.intro, Top.top, Singleton.singleton, ne_top_of_lt
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x : ℝ≥0∞
⊢ (∃ (i : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Iio (↑i : ℝ≥0∞)) x) ↔ Membership.mem (γ := Set ℝ≥0∞) {∞}ᶜ x

Tactic:
exact ⟨fun ⟨n, hn⟩ => ne_top_of_lt hn, ENNReal.exists_nat_gt⟩
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ Eq (α := Set ℝ≥0∞) (⋃ (n : ℕ), Iic (↑n : ℝ≥0∞)) {∞}ᶜ

Tactic:
Subset.antisymm (iUnion_subset fun n _x hx => ne_top_of_le_ne_top (natCast_ne_top n) hx) <|
    iUnion_Iio_coe_nat ▸ iUnion_mono fun _ => Iio_subset_Iic_self

Premises used: Set.Subset.antisymm, ENNReal.iUnion_Iio_coe_nat, Set.iUnion_subset, ENNReal.natCast_ne_top, Eq.rec, ne_top_of_le_ne_top, Set.Iio_subset_Iic_self, Set.iUnion_mono
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
⊢ ⋃ (n : ℕ), Ioc a (↑n : ℝ≥0∞) = Ioi a \ {∞}

Tactic:
simp only [← Ioi_inter_Iic, ← inter_iUnion, iUnion_Iic_coe_nat, diff_eq]

Premises used: Set.Ioi_inter_Iic, ENNReal.iUnion_Iic_coe_nat, Set.diff_eq, Set.inter_iUnion
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
⊢ ⋃ (n : ℕ), Ioo a (↑n : ℝ≥0∞) = Ioi a \ {∞}

Tactic:
simp only [← Ioi_inter_Iio, ← inter_iUnion, iUnion_Iio_coe_nat, diff_eq]

Premises used: ENNReal.iUnion_Iio_coe_nat, Set.diff_eq, Set.Ioi_inter_Iio, Set.inter_iUnion
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
⊢ ⋃ (n : ℕ), Icc a (↑n : ℝ≥0∞) = Ici a \ {∞}

Tactic:
simp only [← Ici_inter_Iic, ← inter_iUnion, iUnion_Iic_coe_nat, diff_eq]

Premises used: ENNReal.iUnion_Iic_coe_nat, Set.diff_eq, Set.inter_iUnion, Set.Ici_inter_Iic
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
⊢ ⋃ (n : ℕ), Ico a (↑n : ℝ≥0∞) = Ici a \ {∞}

Tactic:
simp only [← Ici_inter_Iio, ← inter_iUnion, iUnion_Iio_coe_nat, diff_eq]

Premises used: ENNReal.iUnion_Iio_coe_nat, Set.Ici_inter_Iio, Set.diff_eq, Set.inter_iUnion
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ Eq (α := Set ℝ≥0∞) (⋂ (n : ℕ), Ici (↑n : ℝ≥0∞)) {∞}

Tactic:
simp only [← compl_Iio, ← compl_iUnion, iUnion_Iio_coe_nat, compl_compl]

Premises used: ENNReal.iUnion_Iio_coe_nat, compl_compl, Set.compl_iUnion, Set.compl_Iio
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ Eq (α := Set ℝ≥0∞) (⋂ (n : ℕ), Ioi (↑n : ℝ≥0∞)) {∞}

Tactic:
simp only [← compl_Iic, ← compl_iUnion, iUnion_Iic_coe_nat, compl_compl]

Premises used: compl_compl, ENNReal.iUnion_Iic_coe_nat, Set.compl_Iic, Set.compl_iUnion
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r p : ℝ≥0
⊢ (↑(min r p) : ℝ≥0∞) = min (↑r : ℝ≥0∞) (↑p : ℝ≥0∞)

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.some, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r p : ℝ≥0
⊢ (↑(max r p) : ℝ≥0∞) = max (↑r : ℝ≥0∞) (↑p : ℝ≥0∞)

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.map₂, WithTop.some, rfl, Option.map₂
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
h : a = ∞ → b = ∞
h_nnreal : a ≠ ∞ → b ≠ ∞ → a.toNNReal ≤ b.toNNReal
by_contra! : ∀ (hlt : b < a), False
⊢ a ≤ b

Tactic:
by_contra! hlt
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
h : a = ∞ → b = ∞
h_nnreal : a ≠ ∞ → b ≠ ∞ → a.toNNReal ≤ b.toNNReal
hlt : b < a
⊢ b ≠ ∞

Tactic:
hlt.ne_top

Premises used: LT.lt.ne_top