awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), g i * h ≤ a
⊢ ⨆ (i : ι), g i * h ≤ a

Tactic:
exact ciSup_le' H

Premises used: ciSup_le'
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
a : ℝ≥0
g h : ι → ℝ≥0
H : ∀ (i j : ι), g i * h j ≤ a
⊢ iSup g * iSup h ≤ a

Tactic:
iSup_mul_le fun _ => mul_iSup_le <| H _

Premises used: NNReal.mul_iSup_le, NNReal.iSup_mul_le
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
inst : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
rw : a ≤ ⨅ (i : ι), g * h i
⊢ a ≤ g * iInf h

Tactic:
rw [mul_iInf]

Premises used: NNReal.mul_iInf
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
inst : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ ⨅ (i : ι), g * h i

Tactic:
le_ciInf H

Premises used: le_ciInf
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
inst : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ ⨅ (i : ι), g * h i

Tactic:
exact le_ciInf H

Premises used: le_ciInf
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
inst : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
rw : a ≤ ⨅ (i : ι), g i * h
⊢ a ≤ iInf g * h

Tactic:
rw [iInf_mul]

Premises used: NNReal.iInf_mul
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
inst : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ ⨅ (i : ι), g i * h

Tactic:
le_ciInf H

Premises used: le_ciInf
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
inst : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ ⨅ (i : ι), g i * h

Tactic:
exact le_ciInf H

Premises used: le_ciInf
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
inst : Nonempty ι
a : ℝ≥0
g h : ι → ℝ≥0
H : ∀ (i j : ι), a ≤ g i * h j
⊢ a ≤ iInf g * iInf h

Tactic:
le_iInf_mul fun i => le_mul_iInf <| H i

Premises used: NNReal.le_mul_iInf, NNReal.le_iInf_mul
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_3
f : ι → ℕ
pos : ∀ (h : BddAbove (range f)), Eq (α := ℝ≥0) (↑(⨆ (i : ι), f i) : ℝ≥0) (⨆ (i : ι), (↑(f i) : ℝ≥0))
neg : ∀ (h : ¬BddAbove (range f)), Eq (α := ℝ≥0) (↑(⨆ (i : ι), f i) : ℝ≥0) (⨆ (i : ι), (↑(f i) : ℝ≥0))
⊢ Eq (α := ℝ≥0) (↑(⨆ (i : ι), f i) : ℝ≥0) (⨆ (i : ι), (↑(f i) : ℝ≥0))

Tactic:
by_cases h : BddAbove (Set.range f)

Premises used: BddAbove, Set.range
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_3
f : ι → ℕ
h : BddAbove (range f)
pos : ∀ (c : ℝ≥0), (↑(⨆ (i : ι), f i) : ℝ≥0) ≤ c ↔ ⨆ (i : ι), (↑(f i) : ℝ≥0) ≤ c
⊢ Eq (α := ℝ≥0) (↑(⨆ (i : ι), f i) : ℝ≥0) (⨆ (i : ι), (↑(f i) : ℝ≥0))

Tactic:
apply eq_of_forall_ge_iff

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_3
f : ι → ℕ
h : BddAbove (range f)
⊢ ∀ (c : ℝ≥0), (↑(⨆ (i : ι), f i) : ℝ≥0) ≤ c ↔ ⨆ (i : ι), (↑(f i) : ℝ≥0) ≤ c

Tactic:
simp [ciSup_le_iff', ← Nat.le_floor_iff, *]

Premises used: ciSup_le_iff', Nat.le_floor_iff
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_3
f : ι → ℕ
h : ¬BddAbove (range f)
⊢ Eq (α := ℝ≥0) (↑(⨆ (i : ι), f i) : ℝ≥0) (⨆ (i : ι), (↑(f i) : ℝ≥0))

Tactic:
simp [*]
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_3
f : ι → ℕ
inl : ∀ (hι : IsEmpty ι), Eq (α := ℝ≥0) (↑(⨅ (i : ι), f i) : ℝ≥0) (⨅ (i : ι), (↑(f i) : ℝ≥0))
inr : ∀ (hι : Nonempty ι), Eq (α := ℝ≥0) (↑(⨅ (i : ι), f i) : ℝ≥0) (⨅ (i : ι), (↑(f i) : ℝ≥0))
⊢ Eq (α := ℝ≥0) (↑(⨅ (i : ι), f i) : ℝ≥0) (⨅ (i : ι), (↑(f i) : ℝ≥0))

Tactic:
obtain hι | hι := isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_3
f : ι → ℕ
hι : IsEmpty ι
⊢ Eq (α := ℝ≥0) (↑(⨅ (i : ι), f i) : ℝ≥0) (⨅ (i : ι), (↑(f i) : ℝ≥0))

Tactic:
simp [iInf_empty]

Premises used: NNReal.iInf_empty
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_3
f : ι → ℕ
hι : Nonempty ι
inr : ∀ (c : ℝ≥0), c ≤ (↑(⨅ (i : ι), f i) : ℝ≥0) ↔ c ≤ ⨅ (i : ι), (↑(f i) : ℝ≥0)
⊢ Eq (α := ℝ≥0) (↑(⨅ (i : ι), f i) : ℝ≥0) (⨅ (i : ι), (↑(f i) : ℝ≥0))

Tactic:
apply eq_of_forall_le_iff

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_3
f : ι → ℕ
hι : Nonempty ι
⊢ ∀ (c : ℝ≥0), c ≤ (↑(⨅ (i : ι), f i) : ℝ≥0) ↔ c ≤ ⨅ (i : ι), (↑(f i) : ℝ≥0)

Tactic:
simp [le_ciInf_iff, ← Nat.ceil_le]

Premises used: le_ciInf_iff, Nat.ceil_le
-- Module: Mathlib.Data.NNReal.Basic
Goal:
a b : ℝ≥0
⊢ a = b ↔ (↑a : ℝ) = (↑b : ℝ)

Tactic:
simp
-- Module: Mathlib.Data.NNReal.Basic
Goal:
a b : ℝ≥0
⊢ a ≤ b ↔ (↑a : ℝ) ≤ (↑b : ℝ)

Tactic:
simp
-- Module: Mathlib.Data.NNReal.Basic
Goal:
a b : ℝ≥0
⊢ a < b ↔ (↑a : ℝ) < (↑b : ℝ)

Tactic:
simp
-- Module: Mathlib.Data.NNReal.Basic
Goal:
a b : ℝ≥0
⊢ a ≠ b ↔ (↑a : ℝ) ≠ (↑b : ℝ)

Tactic:
simp
-- Module: Mathlib.Data.NNReal.Basic
Goal:
⊢ range toReal = Ici 0

Tactic:
Subtype.range_coe

Premises used: Set.Ici, Set.Mem, setOf, NNReal, Subtype.range_coe, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
x : ℝ≥0
⊢ toReal '' Ici x = Ici (↑x : ℝ)

Tactic:
image_subtype_val_Ici_Ici ..

Premises used: Set.image_subtype_val_Ici_Ici, Set.Ici, Set.Mem, NNReal, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
x : ℝ≥0
⊢ toReal '' Iic x = Icc 0 (↑x : ℝ)

Tactic:
image_subtype_val_Ici_Iic ..

Premises used: Set.Ici, Set.Mem, NNReal, Set.image_subtype_val_Ici_Iic, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
x : ℝ≥0
⊢ toReal '' Ioi x = Ioi (↑x : ℝ)

Tactic:
image_subtype_val_Ici_Ioi ..

Premises used: Set.Ici, Set.Mem, NNReal, NNReal.toReal, Set.image_subtype_val_Ici_Ioi
-- Module: Mathlib.Data.NNReal.Basic
Goal:
x : ℝ≥0
⊢ toReal '' Iio x = Ico 0 (↑x : ℝ)

Tactic:
image_subtype_val_Ici_Iio ..

Premises used: Set.Ici, Set.Mem, Set.image_subtype_val_Ici_Iio, NNReal, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
x y : ℝ≥0
⊢ toReal '' Icc x y = Icc (↑x : ℝ) (↑y : ℝ)

Tactic:
image_subtype_val_Icc (s := Ici 0) ..

Premises used: Set.Ici, Set.Mem, NNReal, NNReal.toReal, Set.image_subtype_val_Icc
-- Module: Mathlib.Data.NNReal.Basic
Goal:
x y : ℝ≥0
⊢ toReal '' Ioc x y = Ioc (↑x : ℝ) (↑y : ℝ)

Tactic:
image_subtype_val_Ioc (s := Ici 0) ..

Premises used: Set.Ici, Set.Mem, NNReal, Set.image_subtype_val_Ioc, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
x y : ℝ≥0
⊢ toReal '' Ico x y = Ico (↑x : ℝ) (↑y : ℝ)

Tactic:
image_subtype_val_Ico (s := Ici 0) ..

Premises used: Set.Ici, Set.Mem, Set.image_subtype_val_Ico, NNReal, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
x y : ℝ≥0
⊢ toReal '' Ioo x y = Ioo (↑x : ℝ) (↑y : ℝ)

Tactic:
image_subtype_val_Ioo (s := Ici 0) ..

Premises used: Set.Ici, Set.Mem, NNReal, Set.image_subtype_val_Ioo, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
x y : ℝ≥0
⊢ toReal '' uIcc x y = uIcc (↑x : ℝ) (↑y : ℝ)

Tactic:
image_subtype_val_uIcc (s := Ici 0) ..

Premises used: Set.Ici, Set.Mem, NNReal, NNReal.toReal, Set.image_subtype_val_uIcc
-- Module: Mathlib.Data.NNReal.Basic
Goal:
x y : ℝ≥0
⊢ toReal '' uIoc x y = uIoc (↑x : ℝ) (↑y : ℝ)

Tactic:
image_subtype_val_uIoc (s := Ici 0) ..

Premises used: NNReal.instLinearOrder._aux_8, Set.Ici, Set.Mem, NNReal.instLinearOrder._aux_4, NNReal, Set.image_subtype_val_uIoc, NNReal.instLinearOrder._aux_6, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
x y : ℝ≥0
⊢ toReal '' uIoo x y = uIoo (↑x : ℝ) (↑y : ℝ)

Tactic:
image_subtype_val_uIoo (s := Ici 0) ..

Premises used: NNReal.instLinearOrder._aux_8, Set.Ici, Set.Mem, NNReal.instLinearOrder._aux_4, Set.image_subtype_val_uIoo, NNReal, NNReal.instLinearOrder._aux_6, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Eq (α := ℝ≥0) 0 ⊥

Tactic:
rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Eq (α := ℝ≥0) 0 ⊥

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℚ≥0
y : ℝ≥0
⊢ 0 ≤ (↑x : ℝ) * (↑y : ℝ)

Tactic:
mul_nonneg x.cast_nonneg y.2

Premises used: mul_nonneg, NNRat.cast_nonneg, Subtype.property
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℚ≥0
y : ℝ≥0
⊢ 0 ≤ (↑x : ℝ) * (↑y : ℝ)

Tactic:
exact mul_nonneg x.cast_nonneg y.2

Premises used: mul_nonneg, NNRat.cast_nonneg, Subtype.property
-- Module: Mathlib.Data.NNReal.Defs
Goal:
p q : ℝ≥0
h1p : 0 < p
h2p : p ≤ q
⊢ q⁻¹ ≤ p⁻¹

Tactic:
inv_anti₀ h1p h2p

Premises used: inv_anti₀
-- Module: Mathlib.Data.NNReal.Defs
Goal:
p q : ℝ≥0
h1p : 0 < p
h2p : p ≤ q
⊢ q⁻¹ ≤ p⁻¹

Tactic:
exact inv_anti₀ h1p h2p

Premises used: inv_anti₀
-- Module: Mathlib.Data.NNReal.Defs
Goal:
p q : ℝ≥0
h1p : 0 < p
h2p : p ≤ q
⊢ q⁻¹ ≤ p⁻¹

Tactic:
with_reducible_and_instances exact inv_anti₀ h1p h2p

Premises used: inv_anti₀
-- Module: Mathlib.Data.NNReal.Defs
Goal:
n : ℝ≥0
⊢ (↑n : ℝ) = (↑n : ℝ)

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ CanLift ℝ ℝ≥0 toReal fun (r : ℝ) ↦ 0 ≤ r

Tactic:
Subtype.canLift _

Premises used: NNReal, Subtype.canLift, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
n m : ℝ≥0
⊢ (↑n : ℝ) = (↑m : ℝ) → n = m

Tactic:
Subtype.ext

Premises used: NNReal, NNReal.toReal, Subtype.ext
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ≥0
⊢ (↑x : ℝ) ≠ (↑y : ℝ) ↔ x ≠ y

Tactic:
not_congr <| NNReal.eq_iff.symm

Premises used: NNReal.eq_iff, Iff.symm, not_congr
-- Module: Mathlib.Data.NNReal.Defs
Goal:
p : ℝ≥0 → Prop
⊢ (∀ (x : ℝ≥0), p x) ↔ ∀ (x : ℝ) (hx : 0 ≤ x), p (NNReal.mk x hx)

Tactic:
Subtype.forall

Premises used: Subtype.forall, NNReal.mk, NNReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
p : ℝ≥0 → Prop
⊢ (∃ (x : ℝ≥0), p x) ↔ ∃ (x : ℝ) (hx : 0 ≤ x), p (NNReal.mk x hx)

Tactic:
Subtype.exists

Premises used: Subtype.exists, NNReal.mk, NNReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
hr : 0 ≤ r
⊢ (↑r.toNNReal : ℝ) = r

Tactic:
max_eq_left hr

Premises used: max_eq_left, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
⊢ r ≤ (↑r.toNNReal : ℝ)

Tactic:
le_max_left r 0

Premises used: OfNat.ofNat, le_max_left, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
⊢ 0 ≤ (↑r : ℝ)

Tactic:
r.2

Premises used: NNReal.toReal, Subtype.property
-- Module: Mathlib.Data.NNReal.Defs
Goal:
a : ℝ
ha : 0 ≤ a
⊢ (↑(NNReal.mk a ha) : ℝ) = a

Tactic:
rfl

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

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ One ℝ≥0

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Add ℝ≥0

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Sub ℝ≥0

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Mul ℝ≥0

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Inv ℝ≥0

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Div ℝ≥0

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ LE ℝ≥0

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Bot ℝ≥0

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Inhabited ℝ≥0

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Nontrivial ℝ≥0

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Injective toReal

Tactic:
Subtype.coe_injective

Premises used: NNReal, Subtype.coe_injective, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r₁ r₂ : ℝ≥0
⊢ (↑r₁ : ℝ) = (↑r₂ : ℝ) ↔ r₁ = r₂

Tactic:
NNReal.coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, NNReal.coe_injective
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ (↑0 : ℝ) = 0

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ (↑1 : ℝ) = 1

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ NNReal.mk 1 ⋯ = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r₁ r₂ : ℝ≥0
⊢ (↑(r₁ + r₂) : ℝ) = (↑r₁ : ℝ) + (↑r₂ : ℝ)

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r₁ r₂ : ℝ≥0
⊢ (↑(r₁ * r₂) : ℝ) = (↑r₁ : ℝ) * (↑r₂ : ℝ)

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
⊢ (↑r⁻¹ : ℝ) = (↑r : ℝ)⁻¹

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r₁ r₂ : ℝ≥0
⊢ (↑(r₁ / r₂) : ℝ) = (↑r₁ : ℝ) / (↑r₂ : ℝ)

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ (↑2 : ℝ) = 2

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r₁ r₂ : ℝ≥0
h : r₂ ≤ r₁
⊢ (↑r₂ : ℝ) ≤ (↑r₁ : ℝ) - 0

Tactic:
simp [show (r₂ : ℝ) ≤ r₁ from h]
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
rw : (↑r : ℝ) = (↑0 : ℝ) ↔ r = 0
rw₁ rw₂ : r = 0 ↔ r = 0
⊢ (↑r : ℝ) = 0 ↔ r = 0

Tactic:
rw [← coe_zero, coe_inj]

Premises used: NNReal.coe_zero, NNReal.coe_inj
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
rw : (↑r : ℝ) = (↑1 : ℝ) ↔ r = 1
rw₁ rw₂ : r = 1 ↔ r = 1
⊢ (↑r : ℝ) = 1 ↔ r = 1

Tactic:
rw [← coe_one, coe_inj]

Premises used: NNReal.coe_one, NNReal.coe_inj
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
⊢ (↑r : ℝ) ≠ 0 ↔ r ≠ 0

Tactic:
coe_eq_zero.not

Premises used: NNReal.coe_eq_zero, Iff.not
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
⊢ (↑r : ℝ) ≠ 1 ↔ r ≠ 1

Tactic:
coe_eq_one.not

Premises used: Iff.not, NNReal.coe_eq_one
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ CommSemiring ℝ≥0

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ (⇑toRealHom : (a : ℝ≥0) → ℝ) = toReal

Tactic:
rfl

Premises used: NNReal, NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
M : Type u_1
inst : SMul ℝ M
c : ℝ≥0
x : M
⊢ c • x = (↑c : ℝ) • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r_1 r₁ r₂ : ℝ≥0
x_1 y : ℝ
A : Type u_1
inst : Semiring A
inst_1 : Algebra ℝ A
r : ℝ≥0
x : A
⊢ HMul.hMul (α := A) ((RingHom.comp (algebraMap ℝ A) toRealHom : (a : ℝ≥0) → A) r : A) x =
    HMul.hMul (β := A) x ((RingHom.comp (algebraMap ℝ A) toRealHom : (a : ℝ≥0) → A) r : A)

Tactic:
simp [Algebra.commutes]

Premises used: Algebra.commutes
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r_1 r₁ r₂ : ℝ≥0
x_1 y : ℝ
A : Type u_1
inst : Semiring A
inst_1 : Algebra ℝ A
r : ℝ≥0
x : A
⊢ r • x = HMul.hMul (α := A) ((RingHom.comp (algebraMap ℝ A) toRealHom : (a : ℝ≥0) → A) r : A) x

Tactic:
simp [← Algebra.smul_def (r : ℝ) x, smul_def]

Premises used: NNReal.smul_def, Algebra.smul_def, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ Algebra ℝ≥0 ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ DistribMulAction ℝ≥0ˣ ℝ

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ MonoidWithZero ℝ≥0

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ CommMonoidWithZero ℝ≥0

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ CommGroupWithZero ℝ≥0

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
n : ℕ
⊢ (↑(r ^ n) : ℝ) = (↑r : ℝ) ^ n

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
n : ℤ
⊢ (↑(r ^ n) : ℝ) = (↑r : ℝ) ^ n

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
n : ℕ
⊢ (↑(n • r) : ℝ) = n • (↑r : ℝ)

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
q : ℚ≥0
x : ℝ≥0
⊢ (↑(q • x) : ℝ) = q • (↑x : ℝ)

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
n : ℕ
⊢ (↑(↑n : ℝ≥0) : ℝ) = (↑n : ℝ)

Tactic:
map_natCast toRealHom n

Premises used: NNReal.toRealHom, map_natCast, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ (↑(OfNat.ofNat n) : ℝ) = OfNat.ofNat n

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
m : ℕ
s : Bool
e : ℕ
⊢ (↑(OfScientific.ofScientific m s e) : ℝ) = OfScientific.ofScientific m s e

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ (⇑(algebraMap ℝ≥0 ℝ) : (a : ℝ≥0) → ℝ) = toReal

Tactic:
rfl

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

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r₁ r₂ : ℝ≥0
⊢ (↑r₁ : ℝ) ≤ (↑r₂ : ℝ) ↔ r₁ ≤ r₂

Tactic:
Iff.rfl

Premises used: Iff.rfl, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r₁ r₂ : ℝ≥0
⊢ (↑r₁ : ℝ) < (↑r₂ : ℝ) ↔ r₁ < r₂

Tactic:
Iff.rfl

Premises used: Iff.rfl, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
⊢ 0 < (↑r : ℝ) ↔ 0 < r

Tactic:
Iff.rfl

Premises used: Iff.rfl, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
rw : 1 ≤ (↑r : ℝ) ↔ (↑1 : ℝ) ≤ (↑r : ℝ)
rw₁ rw₂ : 1 ≤ (↑r : ℝ) ↔ 1 ≤ (↑r : ℝ)
⊢ 1 ≤ (↑r : ℝ) ↔ 1 ≤ r

Tactic:
rw [← coe_le_coe, coe_one]

Premises used: NNReal.coe_one, NNReal.coe_le_coe
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
rw : 1 < (↑r : ℝ) ↔ (↑1 : ℝ) < (↑r : ℝ)
rw₁ rw₂ : 1 < (↑r : ℝ) ↔ 1 < (↑r : ℝ)
⊢ 1 < (↑r : ℝ) ↔ 1 < r

Tactic:
rw [← coe_lt_coe, coe_one]

Premises used: NNReal.coe_lt_coe, NNReal.coe_one
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
rw : (↑r : ℝ) ≤ 1 ↔ (↑r : ℝ) ≤ (↑1 : ℝ)
rw₁ rw₂ : (↑r : ℝ) ≤ 1 ↔ (↑r : ℝ) ≤ 1
⊢ (↑r : ℝ) ≤ 1 ↔ r ≤ 1

Tactic:
rw [← coe_le_coe, coe_one]

Premises used: NNReal.coe_one, NNReal.coe_le_coe
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
rw : (↑r : ℝ) < 1 ↔ (↑r : ℝ) < (↑1 : ℝ)
rw₁ rw₂ : (↑r : ℝ) < 1 ↔ (↑r : ℝ) < 1
⊢ (↑r : ℝ) < 1 ↔ r < 1

Tactic:
rw [← coe_lt_coe, coe_one]

Premises used: NNReal.coe_lt_coe, NNReal.coe_one
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Monotone toReal

Tactic:
fun _ _ => NNReal.coe_le_coe.2

Premises used: Iff.mpr, Monotone, NNReal.coe_le_coe
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Monotone Real.toNNReal

Tactic:
fun _ _ h =>
  max_le_max_right _ h

Premises used: Monotone, OfNat.ofNat, max_le_max_right
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r₁ r₂ : ℝ
h : r₁ ≤ r₂
⊢ r₁.toNNReal ≤ r₂.toNNReal

Tactic:
Real.toNNReal_monotone h

Premises used: Real.toNNReal_monotone
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ≥0
⊢ (↑r : ℝ).toNNReal = r

Tactic:
NNReal.eq <| max_eq_left r.2

Premises used: NNReal.eq, max_eq_left, Subtype.property
-- Module: Mathlib.Data.NNReal.Defs
Goal:
n : ℕ
⊢ NNReal.mk (↑n : ℝ) ⋯ = (↑n : ℝ≥0)

Tactic:
NNReal.eq (NNReal.coe_natCast n).symm

Premises used: NNReal.eq, NNReal.coe_natCast, Eq.symm
-- Module: Mathlib.Data.NNReal.Defs
Goal:
n : ℕ
⊢ (↑(Real.toNNReal (↑n : ℝ)) : ℝ) = (↑(↑n : ℝ≥0) : ℝ)

Tactic:
simp [Real.coe_toNNReal]

Premises used: Real.coe_toNNReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ Real.toNNReal (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
Real.toNNReal_natCast n

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

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

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

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

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

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

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

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

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

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

Tactic:
instLinearOrderedCommGroupWithZero.toIsOrderedMonoid

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

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

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

Tactic:
infer_instance
-- Module: Mathlib.Data.NNReal.Defs
Goal:
a : ℝ≥0
b : (↑(Set.Icc 0 (↑a : ℝ)) : Type)
⊢ (↑(↑((a.orderIsoIccZeroCoe : (a_1 : (↑(Set.Icc 0 (↑a : ℝ)) : Type)) → (↑(Set.Iic a) : Type)) b) : ℝ≥0) : ℝ) = (↑b : ℝ)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Icc, NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
a : ℝ≥0
b : (↑(Set.Iic a) : Type)
⊢ (↑((a.orderIsoIccZeroCoe.symm : (a_1 : (↑(Set.Iic a) : Type)) → (↑(Set.Icc 0 (↑a : ℝ)) : Type)) b) : ℝ) =
    (↑(↑b : ℝ≥0) : ℝ)

Tactic:
rfl

Premises used: NNReal, NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
⊢ toReal '' s = {x : ℝ | ∃ (h : 0 ≤ x), NNReal.mk x h ∈ s}

Tactic:
Subtype.coe_image

Premises used: Subtype.coe_image, Set.Mem, setOf, NNReal.mk, NNReal, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
⊢ BddAbove (toReal '' s) ↔ BddAbove s

Tactic:
Iff.intro
    (fun ⟨b, hb⟩ =>
      ⟨Real.toNNReal b, fun ⟨y, _⟩ hys =>
        show y ≤ max b 0 from le_max_of_le_left <| hb <| Set.mem_image_of_mem _ hys⟩)
    fun ⟨b, hb⟩ => ⟨b, fun _ ⟨_, hx, eq⟩ => eq ▸ hb hx⟩

Premises used: Eq.rec, LE.le, _private.0.NNReal.bddAbove_coe.match_2, BddAbove, _private.0.NNReal.bddAbove_coe.match_3, Set.mem_image_of_mem, le_max_of_le_left, Iff.intro, _private.0.NNReal.bddAbove_coe.match_4, Exists.intro, _private.0.NNReal.bddAbove_coe.match_1, Set.image, NNReal.toReal, Real.toNNReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
⊢ BddBelow (toReal '' s)

Tactic:
⟨0, fun _ ⟨q, _, eq⟩ => eq ▸ q.2⟩

Premises used: _private.0.NNReal.bddBelow_coe.match_1, Eq.rec, LE.le, Set.Nonempty, BddBelow, Exists.intro, OfNat.ofNat, Subtype.property
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
inl : (↑(sSup ∅) : ℝ) = sSup (toReal '' ∅)
inr : ∀ (hs : s.Nonempty), (↑(sSup s) : ℝ) = sSup (toReal '' s)
⊢ (↑(sSup s) : ℝ) = sSup (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:
⊢ (↑(sSup ∅) : ℝ) = sSup (toReal '' ∅)

Tactic:
simp
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
hs : s.Nonempty
pos : ∀ (H : BddAbove s), (↑(sSup s) : ℝ) = sSup (toReal '' s)
neg : ∀ (H : ¬BddAbove s), (↑(sSup s) : ℝ) = sSup (toReal '' s)
⊢ (↑(sSup s) : ℝ) = sSup (toReal '' s)

Tactic:
by_cases H : BddAbove s

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

Tactic:
apply Real.sSup_nonneg

Premises used: Real.sSup_nonneg
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
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
H : BddAbove s
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
H : BddAbove s
⊢ Membership.mem (γ := Set ℝ) (Set.Ici 0) (sSup (Subtype.val (p := fun (r : ℝ) ↦ 0 ≤ r) '' s))

Tactic:
have A : sSup (Subtype.val '' s) ∈ Set.Ici 0 := by
      apply Real.sSup_nonneg
      rintro - ⟨y, -, rfl⟩
      exact y.2
-- 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:
(@subset_sSup_of_within ℝ (Set.Ici (0 : ℝ)) _ _ (_) s hs H A).symm

Premises used: Set.Ici, Set.Mem, subset_sSup_of_within, NNReal, OfNat.ofNat, Eq.symm, NNReal.toReal