awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
A : Membership.mem (γ := Set ℝ) (Set.Ici 0) (sSup (Subtype.val (p := fun (r : ℝ) ↦ 0 ≤ r) '' s))
⊢ (↑(sSup s) : ℝ) = sSup (toReal '' s)

Tactic:
exact (@subset_sSup_of_within ℝ (Set.Ici (0 : ℝ)) _ _ (_) s hs H A).symm

Premises used: Set.Ici, subset_sSup_of_within, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
neg : 0 = sSup (toReal '' s)
⊢ (↑(sSup s) : ℝ) = sSup (toReal '' s)

Tactic:
simp only [csSup_of_not_bddAbove H, csSup_empty, bot_eq_zero', NNReal.coe_zero]

Premises used: NNReal.coe_zero, csSup_empty, csSup_of_not_bddAbove, bot_eq_zero'
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
apply : ¬BddAbove (toReal '' s)
⊢ 0 = sSup (toReal '' s)

Tactic:
apply (Real.sSup_of_not_bddAbove ?_).symm

Premises used: Real.sSup_of_not_bddAbove, Eq.symm
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
contrapose : ∀ (H : BddAbove (toReal '' s)), BddAbove s
⊢ ¬BddAbove (toReal '' s)

Tactic:
contrapose H
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove (toReal '' s)
⊢ BddAbove s

Tactic:
bddAbove_coe.1 H

Premises used: Iff.mp, NNReal.bddAbove_coe
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove (toReal '' s)
⊢ BddAbove s

Tactic:
exact bddAbove_coe.1 H

Premises used: Iff.mp, NNReal.bddAbove_coe
-- Module: Mathlib.Data.NNReal.Defs
Goal:
ι : Sort u_2
s : ι → ℝ≥0
rw : sSup (Set.range.{0, u_2} (ι := ι) (toReal ∘ fun (i : ι) ↦ s i)) = sSup (Set.range fun (i : ι) ↦ (↑(s i) : ℝ))
⊢ (↑(⨆ (i : ι), s i) : ℝ) = ⨆ (i : ι), (↑(s i) : ℝ)

Tactic:
rw [iSup, iSup, coe_sSup, ← Set.range_comp]

Premises used: Set.range_comp, NNReal.coe_sSup, iSup
-- Module: Mathlib.Data.NNReal.Defs
Goal:
ι : Sort u_2
s : ι → ℝ≥0
⊢ sSup (Set.range.{0, u_2} (ι := ι) (toReal ∘ fun (i : ι) ↦ s i)) = sSup (Set.range fun (i : ι) ↦ (↑(s i) : ℝ))

Tactic:
rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
inl : (↑(sInf ∅) : ℝ) = sInf (toReal '' ∅)
inr : ∀ (hs : s.Nonempty), (↑(sInf s) : ℝ) = sInf (toReal '' s)
⊢ (↑(sInf s) : ℝ) = sInf (toReal '' s)

Tactic:
rcases Set.eq_empty_or_nonempty s with rfl | hs

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
inl : Eq (α := ℝ≥0) (sInf ∅) 0
⊢ (↑(sInf ∅) : ℝ) = sInf (toReal '' ∅)

Tactic:
simp only [Set.image_empty, Real.sInf_empty, coe_eq_zero]

Premises used: NNReal.coe_eq_zero, Real.sInf_empty, Set.image_empty
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Eq (α := ℝ≥0) (sInf ∅) 0

Tactic:
@subset_sInf_emptyset ℝ (Set.Ici (0 : ℝ)) _ _ (_)

Premises used: Set.Ici, Set.Mem, subset_sInf_emptyset, NNReal.mk, NNReal, OfNat.ofNat
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Eq (α := ℝ≥0) (sInf ∅) 0

Tactic:
exact @subset_sInf_emptyset ℝ (Set.Ici (0 : ℝ)) _ _ (_)

Premises used: Set.Ici, subset_sInf_emptyset, OfNat.ofNat
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
hs : s.Nonempty
hs₁ : ∀ x ∈ Subtype.val (p := fun (r : ℝ) ↦ 0 ≤ r) '' s, 0 ≤ x
⊢ Membership.mem (γ := Set ℝ) (Set.Ici 0) (sInf (Subtype.val (p := fun (r : ℝ) ↦ 0 ≤ r) '' s))

Tactic:
apply Real.sInf_nonneg

Premises used: Real.sInf_nonneg
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
hs : s.Nonempty
y : { r : ℝ // 0 ≤ r }
⊢ 0 ≤ (↑y : ℝ)

Tactic:
y.2

Premises used: Subtype.property
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
hs : s.Nonempty
y : { r : ℝ // 0 ≤ r }
⊢ 0 ≤ (↑y : ℝ)

Tactic:
exact y.2

Premises used: Subtype.property
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
hs : s.Nonempty
⊢ Membership.mem (γ := Set ℝ) (Set.Ici 0) (sInf (Subtype.val (p := fun (r : ℝ) ↦ 0 ≤ r) '' s))

Tactic:
have A : sInf (Subtype.val '' s) ∈ Set.Ici 0 := by
    apply Real.sInf_nonneg
    rintro - ⟨y, -, rfl⟩
    exact y.2
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
hs : s.Nonempty
A : Membership.mem (γ := Set ℝ) (Set.Ici 0) (sInf (Subtype.val (p := fun (r : ℝ) ↦ 0 ≤ r) '' s))
⊢ (↑(sInf s) : ℝ) = sInf (toReal '' s)

Tactic:
(@subset_sInf_of_within ℝ (Set.Ici (0 : ℝ)) _ _ (_) s hs (OrderBot.bddBelow s) A).symm

Premises used: Set.Ici, Set.Mem, NNReal, subset_sInf_of_within, OrderBot.bddBelow, OfNat.ofNat, Eq.symm, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
hs : s.Nonempty
A : Membership.mem (γ := Set ℝ) (Set.Ici 0) (sInf (Subtype.val (p := fun (r : ℝ) ↦ 0 ≤ r) '' s))
⊢ (↑(sInf s) : ℝ) = sInf (toReal '' s)

Tactic:
exact (@subset_sInf_of_within ℝ (Set.Ici (0 : ℝ)) _ _ (_) s hs (OrderBot.bddBelow s) A).symm

Premises used: Set.Ici, subset_sInf_of_within, OrderBot.bddBelow, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Data.NNReal.Defs
Goal:
rw : (↑(sInf ∅) : ℝ) = 0
rw₁ : sInf (toReal '' ∅) = 0
rw₂ : Eq (α := ℝ) (sInf ∅) 0
rw₃ rw₄ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ≥0) (sInf ∅) 0

Tactic:
rw [← coe_eq_zero, coe_sInf, Set.image_empty, Real.sInf_empty]

Premises used: NNReal.coe_eq_zero, Real.sInf_empty, Set.image_empty, NNReal.coe_sInf
-- Module: Mathlib.Data.NNReal.Defs
Goal:
ι : Sort u_2
s : ι → ℝ≥0
rw : sInf (Set.range.{0, u_2} (ι := ι) (toReal ∘ fun (i : ι) ↦ s i)) = sInf (Set.range fun (i : ι) ↦ (↑(s i) : ℝ))
⊢ (↑(⨅ (i : ι), s i) : ℝ) = ⨅ (i : ι), (↑(s i) : ℝ)

Tactic:
rw [iInf, iInf, coe_sInf, ← Set.range_comp]

Premises used: Set.range_comp, iInf, NNReal.coe_sInf
-- Module: Mathlib.Data.NNReal.Defs
Goal:
ι : Sort u_2
s : ι → ℝ≥0
⊢ sInf (Set.range.{0, u_2} (ι := ι) (toReal ∘ fun (i : ι) ↦ s i)) = sInf (Set.range fun (i : ι) ↦ (↑(s i) : ℝ))

Tactic:
rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ AddLeftMono ℝ≥0

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ AddLeftReflectLT ℝ≥0

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ MulLeftMono ℝ≥0

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
a b : ℝ≥0
h : (↑a : ℝ) < (↑b : ℝ)
q : ℚ
haq : (↑a : ℝ) < (↑q : ℝ)
hqb : (↑q : ℝ) < (↑b : ℝ)
this : LE.le (α := ℝ) 0 (↑q : ℝ)
⊢ a < Real.toNNReal (↑q : ℝ) ∧ Real.toNNReal (↑q : ℝ) < b

Tactic:
simp [Real.coe_toNNReal _ this, NNReal.coe_lt_coe.symm, haq, hqb]

Premises used: Real.coe_toNNReal, NNReal.coe_lt_coe, Iff.symm
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Eq (α := ℝ≥0) ⊥ 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
a b c : ℝ≥0
⊢ a * max b c = max (a * b) (a * c)

Tactic:
mul_max_of_nonneg _ _ zero_le

Premises used: zero_le, mul_max_of_nonneg
-- Module: Mathlib.Data.NNReal.Defs
Goal:
a b c : ℝ≥0
⊢ max a b * c = max (a * c) (b * c)

Tactic:
max_mul_of_nonneg _ _ zero_le

Premises used: zero_le, max_mul_of_nonneg
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ≥0
⊢ (↑(max x y) : ℝ) = max (↑x : ℝ) (↑y : ℝ)

Tactic:
NNReal.coe_mono.map_max

Premises used: Monotone.map_max, NNReal.coe_mono
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ≥0
⊢ (↑(min x y) : ℝ) = min (↑x : ℝ) (↑y : ℝ)

Tactic:
NNReal.coe_mono.map_min

Premises used: Monotone.map_min, NNReal.coe_mono
-- Module: Mathlib.Data.NNReal.Defs
Goal:
q : ℝ≥0
⊢ 0 ≤ (↑q : ℝ)

Tactic:
q.2

Premises used: NNReal.toReal, Subtype.property
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
M : Type u_2
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Module ℝ M
inst_3 : IsStrictOrderedModule ℝ M
⊢ IsStrictOrderedModule ℝ≥0 M

Tactic:
inferInstanceAs <| IsStrictOrderedModule (Subtype _) M

Premises used: _private.0.NNReal.instIsStrictOrderedModule._proof_1
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
⊢ (↑r.toNNReal : ℝ) = max r 0

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ toNNReal 0 = 0

Tactic:
NNReal.eq <| coe_toNNReal _ le_rfl

Premises used: le_rfl, NNReal.eq, Real.coe_toNNReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ toNNReal 1 = 1

Tactic:
NNReal.eq <| coe_toNNReal _ zero_le_one

Premises used: NNReal.eq, zero_le_one, Real.coe_toNNReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
⊢ 0 < r.toNNReal ↔ 0 < r

Tactic:
simp [← NNReal.coe_lt_coe]

Premises used: NNReal.coe_lt_coe
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
⊢ r.toNNReal = 0 ↔ r ≤ 0

Tactic:
simpa [-toNNReal_pos] using not_iff_not.2 (@toNNReal_pos r)

Premises used: not_iff_not, Iff.mpr, Real.toNNReal_pos
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
⊢ r ≤ 0 → r.toNNReal = 0

Tactic:
toNNReal_eq_zero.2

Premises used: Iff.mpr, Real.toNNReal_eq_zero
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
p : ℝ≥0
hp : p ≠ 0
⊢ r.toNNReal = p ↔ r = (↑p : ℝ)

Tactic:
⟨fun h ↦ h ▸ (coe_toNNReal _ <| not_lt.1 fun hlt ↦ hp <| h ▸ toNNReal_of_nonpos hlt.le).symm,
    fun h ↦ h.symm ▸ toNNReal_coe⟩

Premises used: Eq.rec, LT.lt.le, Real.coe_toNNReal, Real.toNNReal_of_nonpos, not_lt, Iff.intro, Iff.mp, Real.toNNReal_coe, Eq.symm
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
⊢ r.toNNReal = 1 ↔ r = 1

Tactic:
toNNReal_eq_iff_eq_coe one_ne_zero

Premises used: Real.toNNReal_eq_iff_eq_coe, one_ne_zero, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
n : ℕ
hn : n ≠ 0
⊢ r.toNNReal = (↑n : ℝ≥0) ↔ r = (↑n : ℝ)

Tactic:
mod_cast toNNReal_eq_iff_eq_coe <| Nat.cast_ne_zero.2 hn

Premises used: Iff.mpr, congrArg, Real.toNNReal_eq_iff_eq_coe, cast, NNReal.coe_natCast, Nat.cast, Iff, Eq, Nat.cast_ne_zero, Real.toNNReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
n : ℕ
inst : n.AtLeastTwo
⊢ r.toNNReal = OfNat.ofNat n ↔ r = OfNat.ofNat n

Tactic:
toNNReal_eq_natCast (NeZero.ne n)

Premises used: Real.toNNReal_eq_natCast, NeZero.ne
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ
hp : 0 ≤ p
⊢ r.toNNReal ≤ p.toNNReal ↔ r ≤ p

Tactic:
simp [← NNReal.coe_le_coe, hp]

Premises used: NNReal.coe_le_coe
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
⊢ r.toNNReal ≤ 1 ↔ r ≤ 1

Tactic:
simpa using toNNReal_le_toNNReal_iff zero_le_one

Premises used: Real.toNNReal_le_toNNReal_iff, zero_le_one
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
⊢ 1 < r.toNNReal ↔ 1 < r

Tactic:
simpa only [not_le] using toNNReal_le_one.not

Premises used: not_le, Real.toNNReal_le_one, Iff.not
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
n : ℕ
⊢ r.toNNReal ≤ (↑n : ℝ≥0) ↔ r ≤ (↑n : ℝ)

Tactic:
simpa using toNNReal_le_toNNReal_iff n.cast_nonneg

Premises used: Nat.cast_nonneg, Real.toNNReal_le_toNNReal_iff
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
n : ℕ
⊢ (↑n : ℝ≥0) < r.toNNReal ↔ (↑n : ℝ) < r

Tactic:
simpa only [not_le] using toNNReal_le_natCast.not

Premises used: not_le, Real.toNNReal_le_natCast, Iff.not
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
n : ℕ
inst : n.AtLeastTwo
⊢ r.toNNReal ≤ OfNat.ofNat n ↔ r ≤ (↑n : ℝ)

Tactic:
toNNReal_le_natCast

Premises used: Real.toNNReal_le_natCast
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
n : ℕ
inst : n.AtLeastTwo
⊢ OfNat.ofNat n < r.toNNReal ↔ (↑n : ℝ) < r

Tactic:
natCast_lt_toNNReal

Premises used: Real.natCast_lt_toNNReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ
hr : 0 ≤ r
hp : 0 ≤ p
⊢ r.toNNReal = p.toNNReal ↔ r = p

Tactic:
simp [← coe_inj, hr, hp]

Premises used: NNReal.coe_inj
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ
⊢ r.toNNReal < p.toNNReal ↔ r < p ∧ 0 < p

Tactic:
NNReal.coe_lt_coe.symm.trans max_lt_max_left_iff

Premises used: max_lt_max_left_iff, NNReal.coe_lt_coe, Iff.trans, Iff.symm
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ
h : 0 < p
⊢ r.toNNReal < p.toNNReal ↔ r < p

Tactic:
toNNReal_lt_toNNReal_iff'.trans (and_iff_left h)

Premises used: and_iff_left, Iff.trans, Real.toNNReal_lt_toNNReal_iff'
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ
h : r.toNNReal < p.toNNReal
⊢ r < p

Tactic:
(Real.toNNReal_lt_toNNReal_iff <| Real.toNNReal_pos.1 (ne_bot_of_gt h).bot_lt).1 h

Premises used: Real.toNNReal_pos, Real.toNNReal_lt_toNNReal_iff, Iff.mp, ne_bot_of_gt, Ne.bot_lt
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ
hr : 0 ≤ r
⊢ r.toNNReal < p.toNNReal ↔ r < p

Tactic:
toNNReal_lt_toNNReal_iff'.trans ⟨And.left, fun h => ⟨h, lt_of_le_of_lt hr h⟩⟩

Premises used: lt_of_le_of_lt, And.left, And.intro, Iff.intro, Iff.trans, Real.toNNReal_lt_toNNReal_iff'
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ
simp_rw : ¬p.toNNReal < r.toNNReal ↔ ¬p < r ∨ ¬0 < r
simp_rw₁ : ¬(p < r ∧ 0 < r) ↔ ¬p < r ∨ ¬0 < r
⊢ r.toNNReal ≤ p.toNNReal ↔ r ≤ p ∨ r ≤ 0

Tactic:
simp_rw [← not_lt, toNNReal_lt_toNNReal_iff', not_and_or]

Premises used: not_lt, not_and_or, Real.toNNReal_lt_toNNReal_iff'
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ
hr : 0 < r
⊢ r.toNNReal ≤ p.toNNReal ↔ r ≤ p

Tactic:
simp [toNNReal_le_toNNReal_iff', hr.not_ge]

Premises used: Real.toNNReal_le_toNNReal_iff', LT.lt.not_ge
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
⊢ 1 ≤ r.toNNReal ↔ 1 ≤ r

Tactic:
simpa using toNNReal_le_toNNReal_iff_of_pos one_pos

Premises used: Real.toNNReal_le_toNNReal_iff_of_pos, one_pos
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
⊢ r.toNNReal < 1 ↔ r < 1

Tactic:
simp only [← not_le, one_le_toNNReal]

Premises used: not_le, Real.one_le_toNNReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
n : ℕ
r : ℝ
⊢ (↑n : ℝ≥0) ≤ r.toNNReal ↔ (↑n : ℝ) ≤ r ∨ n = 0

Tactic:
simpa [n.cast_nonneg.ge_iff_eq'] using toNNReal_le_toNNReal_iff' (r := n)

Premises used: Real.toNNReal_le_toNNReal_iff', Nat.cast_nonneg, LE.le.ge_iff_eq'
-- Module: Mathlib.Data.NNReal.Defs
Goal:
n : ℕ
r : ℝ
⊢ r.toNNReal < (↑n : ℝ≥0) ↔ r < (↑n : ℝ) ∧ n ≠ 0

Tactic:
simpa [pos_iff_ne_zero] using toNNReal_lt_toNNReal_iff' (r := r) (p := n)

Premises used: pos_iff_ne_zero, Real.toNNReal_lt_toNNReal_iff'
-- Module: Mathlib.Data.NNReal.Defs
Goal:
n : ℕ
r : ℝ
hn : n ≠ 0
⊢ (↑n : ℝ≥0) ≤ r.toNNReal ↔ (↑n : ℝ) ≤ r

Tactic:
simp [hn]
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
n : ℕ
hn : n ≠ 0
⊢ r.toNNReal < (↑n : ℝ≥0) ↔ r < (↑n : ℝ)

Tactic:
simp [hn]
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
n : ℕ
inst : n.AtLeastTwo
⊢ r.toNNReal < OfNat.ofNat n ↔ r < OfNat.ofNat n

Tactic:
toNNReal_lt_natCast (NeZero.ne n)

Premises used: Real.toNNReal_lt_natCast, NeZero.ne
-- Module: Mathlib.Data.NNReal.Defs
Goal:
n : ℕ
r : ℝ
inst : n.AtLeastTwo
⊢ OfNat.ofNat n ≤ r.toNNReal ↔ OfNat.ofNat n ≤ r

Tactic:
natCast_le_toNNReal (NeZero.ne n)

Premises used: Real.natCast_le_toNNReal, NeZero.ne
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ
hr : 0 ≤ r
hp : 0 ≤ p
⊢ (↑(r + p).toNNReal : ℝ) = (↑(r.toNNReal + p.toNNReal) : ℝ)

Tactic:
simp [hr, hp, add_nonneg]

Premises used: add_nonneg
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ
hr : 0 ≤ r
hp : 0 ≤ p
⊢ r.toNNReal + p.toNNReal = (r + p).toNNReal

Tactic:
(Real.toNNReal_add hr hp).symm

Premises used: Real.toNNReal_add, Eq.symm
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ
h : r ≤ p
⊢ r.toNNReal ≤ p.toNNReal

Tactic:
Real.toNNReal_mono h

Premises used: Real.toNNReal_mono
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ
⊢ (r + p).toNNReal ≤ r.toNNReal + p.toNNReal

Tactic:
NNReal.coe_le_coe.1 <| max_le (add_le_add (le_max_left _ _) (le_max_left _ _)) NNReal.zero_le_coe

Premises used: add_le_add, max_le, Iff.mp, NNReal.zero_le_coe, le_max_left, NNReal.coe_le_coe
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
p : ℝ≥0
⊢ r.toNNReal ≤ p ↔ r ≤ (↑p : ℝ)

Tactic:
NNReal.gi.gc r p

Premises used: NNReal.gi, GaloisInsertion.gc
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
p : ℝ
hp : 0 ≤ p
rw : (↑r : ℝ) ≤ (↑p.toNNReal : ℝ) ↔ (↑r : ℝ) ≤ p
rw₁ rw₂ : (↑r : ℝ) ≤ p ↔ (↑r : ℝ) ≤ p
⊢ r ≤ p.toNNReal ↔ (↑r : ℝ) ≤ p

Tactic:
rw [← NNReal.coe_le_coe, Real.coe_toNNReal p hp]

Premises used: Real.coe_toNNReal, NNReal.coe_le_coe
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
p : ℝ
hr : 0 < r
hp : p < 0
⊢ r ≤ p.toNNReal ↔ (↑r : ℝ) ≤ p

Tactic:
simp only [(hp.trans_le r.coe_nonneg).not_ge, toNNReal_eq_zero.2 hp.le, hr.not_ge]

Premises used: Iff.mpr, LT.lt.le, Real.toNNReal_eq_zero, LT.lt.trans_le, NNReal.coe_nonneg, LT.lt.not_ge
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
p : ℝ≥0
ha : 0 ≤ r
rw : (↑r.toNNReal : ℝ) < (↑p : ℝ) ↔ r < (↑p : ℝ)
rw₁ rw₂ : r < (↑p : ℝ) ↔ r < (↑p : ℝ)
⊢ r.toNNReal < p ↔ r < (↑p : ℝ)

Tactic:
rw [← NNReal.coe_lt_coe, Real.coe_toNNReal r ha]

Premises used: Real.coe_toNNReal, NNReal.coe_lt_coe
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
p : ℝ
⊢ r < p.toNNReal ↔ (↑r : ℝ) < p

Tactic:
lt_iff_lt_of_le_iff_le toNNReal_le_iff_le_coe

Premises used: Real.toNNReal_le_iff_le_coe, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ
hx : 0 ≤ x
n : ℕ
rw : (↑(x ^ n).toNNReal : ℝ) = (↑(x.toNNReal ^ n) : ℝ)
rw₁ : (↑(x ^ n).toNNReal : ℝ) = (↑x.toNNReal : ℝ) ^ n
rw₂ : x ^ n = (↑x.toNNReal : ℝ) ^ n
rw₃ rw₄ : x ^ n = x ^ n
⊢ (x ^ n).toNNReal = x.toNNReal ^ n

Tactic:
rw [← coe_inj, NNReal.coe_pow, Real.coe_toNNReal _ (pow_nonneg hx _),
    Real.coe_toNNReal x hx]

Premises used: pow_nonneg, Real.coe_toNNReal, NNReal.coe_pow, NNReal.coe_inj
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ
hx : 0 ≤ x
n : ℤ
rw : (↑(x ^ n).toNNReal : ℝ) = (↑(x.toNNReal ^ n) : ℝ)
rw₁ : (↑(x ^ n).toNNReal : ℝ) = (↑x.toNNReal : ℝ) ^ n
rw₂ : x ^ n = (↑x.toNNReal : ℝ) ^ n
rw₃ rw₄ : x ^ n = x ^ n
⊢ (x ^ n).toNNReal = x.toNNReal ^ n

Tactic:
rw [← coe_inj, NNReal.coe_zpow, Real.coe_toNNReal _ (zpow_nonneg hx _), Real.coe_toNNReal x hx]

Premises used: zpow_nonneg, Real.coe_toNNReal, NNReal.coe_zpow, NNReal.coe_inj
-- Module: Mathlib.Data.NNReal.Defs
Goal:
p q : ℝ
hp : 0 ≤ p
⊢ (↑(p * q).toNNReal : ℝ) = (↑(p.toNNReal * q.toNNReal) : ℝ)

Tactic:
simp [mul_max_of_nonneg, hp]

Premises used: mul_max_of_nonneg
-- Module: Mathlib.Data.NNReal.Defs
Goal:
a b c : ℝ≥0
h : a ≠ 0
rw : b = c ∨ a = 0 ↔ b = c
rw₁ rw₂ : b = c ↔ b = c
⊢ a * b = a * c ↔ b = c

Tactic:
rw [mul_eq_mul_left_iff, or_iff_left h]

Premises used: mul_eq_mul_left_iff, or_iff_left
-- Module: Mathlib.Data.NNReal.Defs
Goal:
a : ℝ≥0
m n : ℕ
mn : m ≤ n
a1 : a ≤ 1
⊢ a ^ n ≤ a ^ m

Tactic:
pow_le_pow_of_le_one zero_le a1 mn

Premises used: zero_le, pow_le_pow_of_le_one
-- Module: Mathlib.Data.NNReal.Defs
Goal:
a b : ℝ≥0
ha : 0 < a
hb : b < 1
⊢ ∃ (n : ℕ), b ^ n < a

Tactic:
simpa only [← coe_pow, NNReal.coe_lt_coe] using
    exists_pow_lt_of_lt_one (NNReal.coe_pos.2 ha) (NNReal.coe_lt_coe.2 hb)

Premises used: Iff.mpr, NNReal.exists_pow_lt_of_lt_one, NNReal.coe_pow, NNReal.coe_lt_coe, NNReal.coe_pos
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ≥0
hx : x ≠ 0
hy : 1 < y
⊢ ∃ (n : ℤ), x ∈ Set.Ico (y ^ n) (y ^ (n + 1))

Tactic:
exists_mem_Ico_zpow hx.bot_lt hy

Premises used: Set.Mem, exists_mem_Ico_zpow, Ne.bot_lt
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ≥0
hx : x ≠ 0
hy : 1 < y
⊢ ∃ (n : ℤ), x ∈ Set.Ioc (y ^ n) (y ^ (n + 1))

Tactic:
exists_mem_Ioc_zpow hx.bot_lt hy

Premises used: Set.Mem, exists_mem_Ioc_zpow, Ne.bot_lt
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ≥0
⊢ r - p = ((↑r : ℝ) - (↑p : ℝ)).toNNReal

Tactic:
rfl

Premises used: NNReal.mk, NNReal.toReal, rfl, Nonneg.toNonneg, Real.toNNReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ≥0
⊢ (↑(r - p) : ℝ) = max ((↑r : ℝ) - (↑p : ℝ)) 0

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ OrderedSub ℝ≥0

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
hr : 0 ≤ r
⊢ (NNReal.mk r hr)⁻¹ = NNReal.mk r⁻¹ ⋯

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ≥0
h : r ≠ 0
rw : r * r⁻¹ ≤ r * p ↔ 1 ≤ r * p
rw₁ rw₂ : 1 ≤ r * p ↔ 1 ≤ r * p
⊢ r⁻¹ ≤ p ↔ 1 ≤ r * p

Tactic:
rw [← mul_le_mul_iff_right₀ (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h]

Premises used: Iff.mpr, mul_inv_cancel₀, pos_iff_ne_zero, mul_le_mul_iff_right₀
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ≥0
h : 1 ≤ r * p
pos : r = 0 → r⁻¹ ≤ p
neg : ¬r = 0 → r⁻¹ ≤ p
⊢ r⁻¹ ≤ p

Tactic:
by_cases r = 0
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ≥0
h : 1 ≤ r * p
h_1 : r = 0
⊢ r⁻¹ ≤ p

Tactic:
simp [*, inv_le]

Premises used: NNReal.inv_le
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ≥0
h : 1 ≤ r * p
h_1 : ¬r = 0
⊢ r⁻¹ ≤ p

Tactic:
simp [*, inv_le]

Premises used: NNReal.inv_le
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ≥0
h : p ≠ 0
rw : p * r ≤ p * p⁻¹ ↔ r * p ≤ 1
rw₁ : p * r ≤ 1 ↔ r * p ≤ 1
rw₂ rw₃ : r * p ≤ 1 ↔ r * p ≤ 1
⊢ r ≤ p⁻¹ ↔ r * p ≤ 1

Tactic:
rw [← mul_le_mul_iff_right₀ (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h, mul_comm]

Premises used: Iff.mpr, mul_inv_cancel₀, mul_comm, pos_iff_ne_zero, mul_le_mul_iff_right₀
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r p : ℝ≥0
h : p ≠ 0
rw : p * r < p * p⁻¹ ↔ r * p < 1
rw₁ : p * r < 1 ↔ r * p < 1
rw₂ rw₃ : r * p < 1 ↔ r * p < 1
⊢ r < p⁻¹ ↔ r * p < 1

Tactic:
rw [← mul_lt_mul_iff_right₀ (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h, mul_comm]

Premises used: Iff.mpr, mul_inv_cancel₀, mul_lt_mul_iff_right₀, mul_comm, pos_iff_ne_zero
-- Module: Mathlib.Data.NNReal.Defs
Goal:
a b c : ℝ≥0
h : a ≤ b * c
h0 : c = 0
⊢ a / c ≤ b

Tactic:
simp [h0]
-- Module: Mathlib.Data.NNReal.Defs
Goal:
a b c : ℝ≥0
h : a ≤ b * c
⊢ a / b ≤ c

Tactic:
div_le_of_le_mul <| mul_comm b c ▸ h

Premises used: Eq.rec, NNReal.div_le_of_le_mul, mul_comm
-- Module: Mathlib.Data.NNReal.Defs
Goal:
a b r : ℝ≥0
h : a < b / r
hr : r = 0
⊢ False

Tactic:
simp [hr] at h
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := ha.ne_zero
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
rwa : ¬x⁻¹ = 0
rwa₁ rwa₂ rwa₃ rwa₄ : ¬x = 0
⊢ x⁻¹ ≠ 0

Tactic:
rwa [Ne, inv_eq_zero]

Premises used: inv_eq_zero, Ne
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ x⁻¹ ≠ 0

Tactic:
have hx' : x⁻¹ ≠ 0 := by rwa [Ne, inv_eq_zero]
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
rwa : a < x⁻¹⁻¹
rwa₁ rwa₂ rwa₃ rwa₄ : a < x
⊢ a * x⁻¹ < 1

Tactic:
rwa [← lt_inv_iff_mul_lt hx', inv_inv]

Premises used: NNReal.lt_inv_iff_mul_lt, inv_inv
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a * x⁻¹ < 1

Tactic:
have : a * x⁻¹ < 1 := by rwa [← lt_inv_iff_mul_lt hx', inv_inv]
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this : a * x⁻¹ < 1
⊢ a * x⁻¹ * x ≤ y

Tactic:
have : a * x⁻¹ * x ≤ y := h _ this
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this_1 : a * x⁻¹ < 1
this : a * x⁻¹ * x ≤ y
rwa : ∀ (this : a * (x⁻¹ * x) ≤ y), a ≤ y
rwa₁ : ∀ (this : a * 1 ≤ y), a ≤ y
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : a ≤ y), a ≤ y
⊢ a ≤ y

Tactic:
rwa [mul_assoc, inv_mul_cancel₀ hx, mul_one] at this

Premises used: mul_assoc, mul_one, inv_mul_cancel₀
-- Module: Mathlib.Data.NNReal.Defs
Goal:
a : ℝ≥0
⊢ a / 2 ≤ a

Tactic:
half_le_self bot_le

Premises used: half_le_self, bot_le
-- Module: Mathlib.Data.NNReal.Defs
Goal:
a : ℝ≥0
h : a ≠ 0
⊢ a / 2 < a

Tactic:
half_lt_self h.bot_lt

Premises used: half_lt_self, Ne.bot_lt
-- Module: Mathlib.Data.NNReal.Defs
Goal:
a b : ℝ≥0
h : a < b
rwa : a < 1 * b
rwa₁ rwa₂ rwa₃ rwa₄ : a < b
⊢ a / b < 1

Tactic:
rwa [div_lt_iff₀ h.bot_lt, one_mul]

Premises used: div_lt_iff₀, LT.lt.bot_lt, one_mul
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ
inl : ∀ (hx : 0 ≤ x), x⁻¹.toNNReal = x.toNNReal⁻¹
inr : ∀ (hx : x ≤ 0), x⁻¹.toNNReal = x.toNNReal⁻¹
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹

Tactic:
rcases le_total 0 x with hx | hx

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ
hx : 0 ≤ x
inl : (↑x.toNNReal : ℝ)⁻¹.toNNReal = x.toNNReal⁻¹
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹

Tactic:
nth_rw 1 [← Real.coe_toNNReal x hx]

Premises used: Real.coe_toNNReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ
hx : 0 ≤ x
inl : (↑x.toNNReal⁻¹ : ℝ).toNNReal = x.toNNReal⁻¹
inl₁ inl₂ : x.toNNReal⁻¹ = x.toNNReal⁻¹
⊢ (↑x.toNNReal : ℝ)⁻¹.toNNReal = x.toNNReal⁻¹

Tactic:
rw [← NNReal.coe_inv, Real.toNNReal_coe]

Premises used: NNReal.coe_inv, Real.toNNReal_coe
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ
hx : x ≤ 0
inr : x⁻¹.toNNReal = 0⁻¹
inr₁ : x⁻¹.toNNReal = 0
inr₂ inr₃ : Eq (α := ℝ≥0) 0 0
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹

Tactic:
rw [toNNReal_eq_zero.mpr hx, inv_zero, toNNReal_eq_zero.mpr (inv_nonpos.mpr hx)]

Premises used: Iff.mpr, inv_zero, Real.toNNReal_eq_zero, inv_nonpos