awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (hypothesis)
Goal:
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
⊢ (↑(sSup s) : ℝ) = sSup (toReal '' s)
have A : 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
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ (↑(sSup s) : ℝ) = sSup (toReal '' s)
have neg : 0 = sSup (toReal '' s)
Tactic: simp only [csSup_of_not_bddAbove H, csSup_empty, bot_eq_zero', NNReal.coe_zero]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ 0 = sSup (toReal '' s)
have apply : ¬BddAbove (toReal '' s)
Tactic: apply (Real.sSup_of_not_bddAbove ?_).symm
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ ¬BddAbove (toReal '' s)
have contrapose : ∀ (H : BddAbove (toReal '' s)), BddAbove s
Tactic: contrapose H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
ι : Sort u_2
s : ι → ℝ≥0
⊢ (↑(⨆ (i : ι), s i) : ℝ) = ⨆ (i : ι), (↑(s i) : ℝ)
have rw : sSup (Set.range.{0, u_2} (ι := ι) (toReal ∘ fun (i : ι) ↦ s i)) = sSup (Set.range fun (i : ι) ↦ (↑(s i) : ℝ))
Tactic: rw [iSup, iSup, coe_sSup, ← Set.range_comp]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
s : Set ℝ≥0
⊢ (↑(sInf s) : ℝ) = sInf (toReal '' s)
have inl : (↑(sInf ∅) : ℝ) = sInf (toReal '' ∅)
Tactic: rcases Set.eq_empty_or_nonempty s with rfl | hs
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
s : Set ℝ≥0
inl : (↑(sInf ∅) : ℝ) = sInf (toReal '' ∅)
⊢ (↑(sInf s) : ℝ) = sInf (toReal '' s)
have inr : ∀ (hs : s.Nonempty), (↑(sInf s) : ℝ) = sInf (toReal '' s)
Tactic: rcases Set.eq_empty_or_nonempty s with rfl | hs
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
⊢ (↑(sInf ∅) : ℝ) = sInf (toReal '' ∅)
have inl : Eq (α := ℝ≥0) (sInf ∅) 0
Tactic: simp only [Set.image_empty, Real.sInf_empty, coe_eq_zero]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
s : Set ℝ≥0
hs : s.Nonempty
⊢ Membership.mem (γ := Set ℝ) (Set.Ici 0) (sInf (Subtype.val (p := fun (r : ℝ) ↦ 0 ≤ r) '' s))
have hs₁ : ∀ x ∈ Subtype.val (p := fun (r : ℝ) ↦ 0 ≤ r) '' s, 0 ≤ x
Tactic: apply Real.sInf_nonneg
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (hypothesis)
Goal:
s : Set ℝ≥0
hs : s.Nonempty
⊢ (↑(sInf s) : ℝ) = sInf (toReal '' s)
have A : 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
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
⊢ Eq (α := ℝ≥0) (sInf ∅) 0
have rw : (↑(sInf ∅) : ℝ) = 0
Tactic: rw [← coe_eq_zero, coe_sInf, Set.image_empty, Real.sInf_empty]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
rw : (↑(sInf ∅) : ℝ) = 0
⊢ Eq (α := ℝ≥0) (sInf ∅) 0
have rw₁ : sInf (toReal '' ∅) = 0
Tactic: rw [← coe_eq_zero, coe_sInf, Set.image_empty, Real.sInf_empty]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
rw : (↑(sInf ∅) : ℝ) = 0
rw₁ : sInf (toReal '' ∅) = 0
⊢ Eq (α := ℝ≥0) (sInf ∅) 0
have rw₂ : Eq (α := ℝ) (sInf ∅) 0
Tactic: rw [← coe_eq_zero, coe_sInf, Set.image_empty, Real.sInf_empty]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
rw : (↑(sInf ∅) : ℝ) = 0
rw₁ : sInf (toReal '' ∅) = 0
rw₂ : Eq (α := ℝ) (sInf ∅) 0
⊢ Eq (α := ℝ≥0) (sInf ∅) 0
have rw₃ : Eq (α := ℝ) 0 0
Tactic: rw [← coe_eq_zero, coe_sInf, Set.image_empty, Real.sInf_empty]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
ι : Sort u_2
s : ι → ℝ≥0
⊢ (↑(⨅ (i : ι), s i) : ℝ) = ⨅ (i : ι), (↑(s i) : ℝ)
have rw : sInf (Set.range.{0, u_2} (ι := ι) (toReal ∘ fun (i : ι) ↦ s i)) = sInf (Set.range fun (i : ι) ↦ (↑(s i) : ℝ))
Tactic: rw [iInf, iInf, coe_sInf, ← Set.range_comp]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r p : ℝ
⊢ r.toNNReal ≤ p.toNNReal ↔ r ≤ p ∨ r ≤ 0
have simp_rw : ¬p.toNNReal < r.toNNReal ↔ ¬p < r ∨ ¬0 < r
Tactic: simp_rw [← not_lt, toNNReal_lt_toNNReal_iff', not_and_or]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r p : ℝ
simp_rw : ¬p.toNNReal < r.toNNReal ↔ ¬p < r ∨ ¬0 < r
⊢ r.toNNReal ≤ p.toNNReal ↔ r ≤ p ∨ r ≤ 0
have simp_rw₁ : ¬(p < r ∧ 0 < r) ↔ ¬p < r ∨ ¬0 < r
Tactic: simp_rw [← not_lt, toNNReal_lt_toNNReal_iff', not_and_or]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ≥0
p : ℝ
hp : 0 ≤ p
⊢ r ≤ p.toNNReal ↔ (↑r : ℝ) ≤ p
have rw : (↑r : ℝ) ≤ (↑p.toNNReal : ℝ) ↔ (↑r : ℝ) ≤ p
Tactic: rw [← NNReal.coe_le_coe, Real.coe_toNNReal p hp]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ≥0
p : ℝ
hp : 0 ≤ p
rw : (↑r : ℝ) ≤ (↑p.toNNReal : ℝ) ↔ (↑r : ℝ) ≤ p
⊢ r ≤ p.toNNReal ↔ (↑r : ℝ) ≤ p
have rw₁ : (↑r : ℝ) ≤ p ↔ (↑r : ℝ) ≤ p
Tactic: rw [← NNReal.coe_le_coe, Real.coe_toNNReal p hp]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ
p : ℝ≥0
ha : 0 ≤ r
⊢ r.toNNReal < p ↔ r < (↑p : ℝ)
have rw : (↑r.toNNReal : ℝ) < (↑p : ℝ) ↔ r < (↑p : ℝ)
Tactic: rw [← NNReal.coe_lt_coe, Real.coe_toNNReal r ha]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ
p : ℝ≥0
ha : 0 ≤ r
rw : (↑r.toNNReal : ℝ) < (↑p : ℝ) ↔ r < (↑p : ℝ)
⊢ r.toNNReal < p ↔ r < (↑p : ℝ)
have rw₁ : r < (↑p : ℝ) ↔ r < (↑p : ℝ)
Tactic: rw [← NNReal.coe_lt_coe, Real.coe_toNNReal r ha]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ (x ^ n).toNNReal = x.toNNReal ^ n
have rw : (↑(x ^ n).toNNReal : ℝ) = (↑(x.toNNReal ^ n) : ℝ)
Tactic: rw [← coe_inj, NNReal.coe_pow, Real.coe_toNNReal _ (pow_nonneg hx _),
    Real.coe_toNNReal x hx]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
hx : 0 ≤ x
n : ℕ
rw : (↑(x ^ n).toNNReal : ℝ) = (↑(x.toNNReal ^ n) : ℝ)
⊢ (x ^ n).toNNReal = x.toNNReal ^ n
have rw₁ : (↑(x ^ n).toNNReal : ℝ) = (↑x.toNNReal : ℝ) ^ n
Tactic: rw [← coe_inj, NNReal.coe_pow, Real.coe_toNNReal _ (pow_nonneg hx _),
    Real.coe_toNNReal x hx]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
hx : 0 ≤ x
n : ℕ
rw : (↑(x ^ n).toNNReal : ℝ) = (↑(x.toNNReal ^ n) : ℝ)
rw₁ : (↑(x ^ n).toNNReal : ℝ) = (↑x.toNNReal : ℝ) ^ n
⊢ (x ^ n).toNNReal = x.toNNReal ^ n
have rw₂ : x ^ n = (↑x.toNNReal : ℝ) ^ n
Tactic: rw [← coe_inj, NNReal.coe_pow, Real.coe_toNNReal _ (pow_nonneg hx _),
    Real.coe_toNNReal x hx]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
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
⊢ (x ^ n).toNNReal = x.toNNReal ^ n
have rw₃ : x ^ n = x ^ n
Tactic: rw [← coe_inj, NNReal.coe_pow, Real.coe_toNNReal _ (pow_nonneg hx _),
    Real.coe_toNNReal x hx]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
hx : 0 ≤ x
n : ℤ
⊢ (x ^ n).toNNReal = x.toNNReal ^ n
have rw : (↑(x ^ n).toNNReal : ℝ) = (↑(x.toNNReal ^ n) : ℝ)
Tactic: rw [← coe_inj, NNReal.coe_zpow, Real.coe_toNNReal _ (zpow_nonneg hx _), Real.coe_toNNReal x hx]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
hx : 0 ≤ x
n : ℤ
rw : (↑(x ^ n).toNNReal : ℝ) = (↑(x.toNNReal ^ n) : ℝ)
⊢ (x ^ n).toNNReal = x.toNNReal ^ n
have rw₁ : (↑(x ^ n).toNNReal : ℝ) = (↑x.toNNReal : ℝ) ^ n
Tactic: rw [← coe_inj, NNReal.coe_zpow, Real.coe_toNNReal _ (zpow_nonneg hx _), Real.coe_toNNReal x hx]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
hx : 0 ≤ x
n : ℤ
rw : (↑(x ^ n).toNNReal : ℝ) = (↑(x.toNNReal ^ n) : ℝ)
rw₁ : (↑(x ^ n).toNNReal : ℝ) = (↑x.toNNReal : ℝ) ^ n
⊢ (x ^ n).toNNReal = x.toNNReal ^ n
have rw₂ : x ^ n = (↑x.toNNReal : ℝ) ^ n
Tactic: rw [← coe_inj, NNReal.coe_zpow, Real.coe_toNNReal _ (zpow_nonneg hx _), Real.coe_toNNReal x hx]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
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
⊢ (x ^ n).toNNReal = x.toNNReal ^ n
have rw₃ : x ^ n = x ^ n
Tactic: rw [← coe_inj, NNReal.coe_zpow, Real.coe_toNNReal _ (zpow_nonneg hx _), Real.coe_toNNReal x hx]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
a b c : ℝ≥0
h : a ≠ 0
⊢ a * b = a * c ↔ b = c
have rw : b = c ∨ a = 0 ↔ b = c
Tactic: rw [mul_eq_mul_left_iff, or_iff_left h]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
a b c : ℝ≥0
h : a ≠ 0
rw : b = c ∨ a = 0 ↔ b = c
⊢ a * b = a * c ↔ b = c
have rw₁ : b = c ↔ b = c
Tactic: rw [mul_eq_mul_left_iff, or_iff_left h]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r p : ℝ≥0
h : r ≠ 0
⊢ r⁻¹ ≤ p ↔ 1 ≤ r * p
have rw : r * r⁻¹ ≤ r * p ↔ 1 ≤ r * p
Tactic: rw [← mul_le_mul_iff_right₀ (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r p : ℝ≥0
h : r ≠ 0
rw : r * r⁻¹ ≤ r * p ↔ 1 ≤ r * p
⊢ r⁻¹ ≤ p ↔ 1 ≤ r * p
have rw₁ : 1 ≤ r * p ↔ 1 ≤ r * p
Tactic: rw [← mul_le_mul_iff_right₀ (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r p : ℝ≥0
h : 1 ≤ r * p
⊢ r⁻¹ ≤ p
have pos : r = 0 → r⁻¹ ≤ p
Tactic: by_cases r = 0
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r p : ℝ≥0
h : 1 ≤ r * p
pos : r = 0 → r⁻¹ ≤ p
⊢ r⁻¹ ≤ p
have neg : ¬r = 0 → r⁻¹ ≤ p
Tactic: by_cases r = 0
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r p : ℝ≥0
h : p ≠ 0
⊢ r ≤ p⁻¹ ↔ r * p ≤ 1
have rw : p * r ≤ p * p⁻¹ ↔ r * p ≤ 1
Tactic: rw [← mul_le_mul_iff_right₀ (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h, mul_comm]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r p : ℝ≥0
h : p ≠ 0
rw : p * r ≤ p * p⁻¹ ↔ r * p ≤ 1
⊢ r ≤ p⁻¹ ↔ r * p ≤ 1
have rw₁ : p * r ≤ 1 ↔ r * p ≤ 1
Tactic: rw [← mul_le_mul_iff_right₀ (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h, mul_comm]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r p : ℝ≥0
h : p ≠ 0
rw : p * r ≤ p * p⁻¹ ↔ r * p ≤ 1
rw₁ : p * r ≤ 1 ↔ r * p ≤ 1
⊢ r ≤ p⁻¹ ↔ r * p ≤ 1
have rw₂ : r * p ≤ 1 ↔ r * p ≤ 1
Tactic: rw [← mul_le_mul_iff_right₀ (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h, mul_comm]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r p : ℝ≥0
h : p ≠ 0
⊢ r < p⁻¹ ↔ r * p < 1
have rw : p * r < p * p⁻¹ ↔ r * p < 1
Tactic: rw [← mul_lt_mul_iff_right₀ (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h, mul_comm]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r p : ℝ≥0
h : p ≠ 0
rw : p * r < p * p⁻¹ ↔ r * p < 1
⊢ r < p⁻¹ ↔ r * p < 1
have rw₁ : p * r < 1 ↔ r * p < 1
Tactic: rw [← mul_lt_mul_iff_right₀ (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h, mul_comm]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r p : ℝ≥0
h : p ≠ 0
rw : p * r < p * p⁻¹ ↔ r * p < 1
rw₁ : p * r < 1 ↔ r * p < 1
⊢ r < p⁻¹ ↔ r * p < 1
have rw₂ : r * p < 1 ↔ r * p < 1
Tactic: rw [← mul_lt_mul_iff_right₀ (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h, mul_comm]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (hypothesis)
Goal:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
⊢ a ≤ y
have hx : x ≠ 0
Tactic: have hx : x ≠ 0 := ha.ne_zero
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ x⁻¹ ≠ 0
have rwa : ¬x⁻¹ = 0
Tactic: rwa [Ne, inv_eq_zero]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
rwa : ¬x⁻¹ = 0
⊢ x⁻¹ ≠ 0
have rwa₁ : ¬x = 0
Tactic: rwa [Ne, inv_eq_zero]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (hypothesis)
Goal:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ a ≤ y
have hx' : x⁻¹ ≠ 0
Tactic: have hx' : x⁻¹ ≠ 0 := by rwa [Ne, inv_eq_zero]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a * x⁻¹ < 1
have rwa : a < x⁻¹⁻¹
Tactic: rwa [← lt_inv_iff_mul_lt hx', inv_inv]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (hypothesis)
Goal:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a ≤ y
have this : a * x⁻¹ < 1
Tactic: have : a * x⁻¹ < 1 := by rwa [← lt_inv_iff_mul_lt hx', inv_inv]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (hypothesis)
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 ≤ y
have this₁ : a * x⁻¹ * x ≤ y
Tactic: have : a * x⁻¹ * x ≤ y := h _ this
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
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
⊢ a ≤ y
have rwa : ∀ (this : a * (x⁻¹ * x) ≤ y), a ≤ y
Tactic: rwa [mul_assoc, inv_mul_cancel₀ hx, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
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
⊢ a ≤ y
have rwa₁ : ∀ (this : a * 1 ≤ y), a ≤ y
Tactic: rwa [mul_assoc, inv_mul_cancel₀ hx, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
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
⊢ a ≤ y
have rwa₂ : ∀ (this : a ≤ y), a ≤ y
Tactic: rwa [mul_assoc, inv_mul_cancel₀ hx, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
a b : ℝ≥0
h : a < b
⊢ a / b < 1
have rwa : a < 1 * b
Tactic: rwa [div_lt_iff₀ h.bot_lt, one_mul]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹
have inl : ∀ (hx : 0 ≤ x), x⁻¹.toNNReal = x.toNNReal⁻¹
Tactic: rcases le_total 0 x with hx | hx
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
inl : ∀ (hx : 0 ≤ x), x⁻¹.toNNReal = x.toNNReal⁻¹
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹
have inr : ∀ (hx : x ≤ 0), x⁻¹.toNNReal = x.toNNReal⁻¹
Tactic: rcases le_total 0 x with hx | hx
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹
have inl : (↑x.toNNReal : ℝ)⁻¹.toNNReal = x.toNNReal⁻¹
Tactic: nth_rw 1 [← Real.coe_toNNReal x hx]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ (↑x.toNNReal : ℝ)⁻¹.toNNReal = x.toNNReal⁻¹
have inl : (↑x.toNNReal⁻¹ : ℝ).toNNReal = x.toNNReal⁻¹
Tactic: rw [← NNReal.coe_inv, Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
hx : 0 ≤ x
inl : (↑x.toNNReal⁻¹ : ℝ).toNNReal = x.toNNReal⁻¹
⊢ (↑x.toNNReal : ℝ)⁻¹.toNNReal = x.toNNReal⁻¹
have inl₁ : x.toNNReal⁻¹ = x.toNNReal⁻¹
Tactic: rw [← NNReal.coe_inv, Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
hx : x ≤ 0
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹
have inr : x⁻¹.toNNReal = 0⁻¹
Tactic: rw [toNNReal_eq_zero.mpr hx, inv_zero, toNNReal_eq_zero.mpr (inv_nonpos.mpr hx)]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
hx : x ≤ 0
inr : x⁻¹.toNNReal = 0⁻¹
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹
have inr₁ : x⁻¹.toNNReal = 0
Tactic: rw [toNNReal_eq_zero.mpr hx, inv_zero, toNNReal_eq_zero.mpr (inv_nonpos.mpr hx)]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
hx : x ≤ 0
inr : x⁻¹.toNNReal = 0⁻¹
inr₁ : x⁻¹.toNNReal = 0
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹
have inr₂ : Eq (α := ℝ≥0) 0 0
Tactic: rw [toNNReal_eq_zero.mpr hx, inv_zero, toNNReal_eq_zero.mpr (inv_nonpos.mpr hx)]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal
have rw : (x * y⁻¹).toNNReal = x.toNNReal / y.toNNReal
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← Real.toNNReal_inv, ← Real.toNNReal_mul hx]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
rw : (x * y⁻¹).toNNReal = x.toNNReal / y.toNNReal
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal
have rw₁ : (x * y⁻¹).toNNReal = x.toNNReal * y.toNNReal⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← Real.toNNReal_inv, ← Real.toNNReal_mul hx]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
rw : (x * y⁻¹).toNNReal = x.toNNReal / y.toNNReal
rw₁ : (x * y⁻¹).toNNReal = x.toNNReal * y.toNNReal⁻¹
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal
have rw₂ : (x * y⁻¹).toNNReal = x.toNNReal * y⁻¹.toNNReal
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← Real.toNNReal_inv, ← Real.toNNReal_mul hx]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
rw : (x * y⁻¹).toNNReal = x.toNNReal / y.toNNReal
rw₁ : (x * y⁻¹).toNNReal = x.toNNReal * y.toNNReal⁻¹
rw₂ : (x * y⁻¹).toNNReal = x.toNNReal * y⁻¹.toNNReal
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal
have rw₃ : (x * y⁻¹).toNNReal = (x * y⁻¹).toNNReal
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← Real.toNNReal_inv, ← Real.toNNReal_mul hx]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal
have rw : (y⁻¹ * x).toNNReal = x.toNNReal / y.toNNReal
Tactic: rw [div_eq_inv_mul, div_eq_inv_mul, Real.toNNReal_mul (inv_nonneg.2 hy), Real.toNNReal_inv]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (y⁻¹ * x).toNNReal = x.toNNReal / y.toNNReal
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal
have rw₁ : (y⁻¹ * x).toNNReal = y.toNNReal⁻¹ * x.toNNReal
Tactic: rw [div_eq_inv_mul, div_eq_inv_mul, Real.toNNReal_mul (inv_nonneg.2 hy), Real.toNNReal_inv]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (y⁻¹ * x).toNNReal = x.toNNReal / y.toNNReal
rw₁ : (y⁻¹ * x).toNNReal = y.toNNReal⁻¹ * x.toNNReal
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal
have rw₂ : y⁻¹.toNNReal * x.toNNReal = y.toNNReal⁻¹ * x.toNNReal
Tactic: rw [div_eq_inv_mul, div_eq_inv_mul, Real.toNNReal_mul (inv_nonneg.2 hy), Real.toNNReal_inv]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (y⁻¹ * x).toNNReal = x.toNNReal / y.toNNReal
rw₁ : (y⁻¹ * x).toNNReal = y.toNNReal⁻¹ * x.toNNReal
rw₂ : y⁻¹.toNNReal * x.toNNReal = y.toNNReal⁻¹ * x.toNNReal
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal
have rw₃ : y.toNNReal⁻¹ * x.toNNReal = y.toNNReal⁻¹ * x.toNNReal
Tactic: rw [div_eq_inv_mul, div_eq_inv_mul, Real.toNNReal_mul (inv_nonneg.2 hy), Real.toNNReal_inv]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ≥0
hx : x ≠ 0
⊢ x⁻¹ < 1 ↔ 1 < x
have rw : 1 / x < 1 ↔ 1 < x
Tactic: rw [← one_div, div_lt_iff₀ hx.bot_lt, one_mul]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ≥0
hx : x ≠ 0
rw : 1 / x < 1 ↔ 1 < x
⊢ x⁻¹ < 1 ↔ 1 < x
have rw₁ : 1 < 1 * x ↔ 1 < x
Tactic: rw [← one_div, div_lt_iff₀ hx.bot_lt, one_mul]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ≥0
hx : x ≠ 0
rw : 1 / x < 1 ↔ 1 < x
rw₁ : 1 < 1 * x ↔ 1 < x
⊢ x⁻¹ < 1 ↔ 1 < x
have rw₂ : 1 < x ↔ 1 < x
Tactic: rw [← one_div, div_lt_iff₀ hx.bot_lt, one_mul]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
ι : Sort u_1
inst : IsEmpty ι
f : ι → ℝ≥0
⊢ Eq (α := ℝ≥0) (⨅ (i : ι), f i) 0
have rw : Eq (α := ℝ≥0) (sInf ∅) 0
Tactic: rw [_root_.iInf_of_isEmpty, sInf_empty]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
ι : Sort u_1
inst : IsEmpty ι
f : ι → ℝ≥0
rw : Eq (α := ℝ≥0) (sInf ∅) 0
⊢ Eq (α := ℝ≥0) (⨅ (i : ι), f i) 0
have rw₁ : Eq (α := ℝ≥0) 0 0
Tactic: rw [_root_.iInf_of_isEmpty, sInf_empty]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
⊢ Eq (α := ℝ≥0) (⨆ (i : ι), f i) 0 ↔ ∀ (i : ι), f i = 0
have inl : IsEmpty ι → (Eq (α := ℝ≥0) (⨆ (i : ι), f i) 0 ↔ ∀ (i : ι), f i = 0)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
inl : IsEmpty ι → (Eq (α := ℝ≥0) (⨆ (i : ι), f i) 0 ↔ ∀ (i : ι), f i = 0)
⊢ Eq (α := ℝ≥0) (⨆ (i : ι), f i) 0 ↔ ∀ (i : ι), f i = 0
have inr : Nonempty ι → (Eq (α := ℝ≥0) (⨆ (i : ι), f i) 0 ↔ ∀ (i : ι), f i = 0)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
α : Sort u_2
⊢ Eq (α := ℝ≥0) (⨅ (x : α), 0) 0
have rw : ⨅ (i : α), (↑0 : ℝ) = (↑0 : ℝ)
Tactic: rw [← coe_inj, coe_iInf]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
s : Set ℝ
h : s.OrdConnected
⊢ (toNNReal '' s).OrdConnected
have refine : ∀ (x : ℝ) (hx : x ∈ s) (y : ℝ) (hy : y ∈ s) (z : ℝ≥0) (hz : z ∈ Icc x.toNNReal y.toNNReal), z ∈ toNNReal '' s
Tactic: refine ⟨forall_mem_image.2 fun x hx => forall_mem_image.2 fun y hy z hz => ?_⟩
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
⊢ z ∈ toNNReal '' s
have inl : ∀ (hy₀ : y ≤ 0), z ∈ toNNReal '' s
Tactic: rcases le_total y 0 with hy₀ | hy₀
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
inl : ∀ (hy₀ : y ≤ 0), z ∈ toNNReal '' s
⊢ z ∈ toNNReal '' s
have inr : ∀ (hy₀ : 0 ≤ y), z ∈ toNNReal '' s
Tactic: rcases le_total y 0 with hy₀ | hy₀
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (hypothesis)
Goal:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s
have hz₁ : x.toNNReal ≤ z ∧ z = 0
Tactic: rw [mem_Icc, Real.toNNReal_of_nonpos hy₀, nonpos_iff_eq_zero] at hz
Cleared hypotheses: hz, hy₀
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
hy₀ : 0 ≤ y
⊢ z ∈ toNNReal '' s
have inr : ∀ (y : ℝ≥0) (hy : (↑y : ℝ) ∈ s) (hz : z ∈ Icc x.toNNReal (↑y : ℝ).toNNReal), z ∈ toNNReal '' s
Tactic: lift y to ℝ≥0 using hy₀
Cleared hypotheses: y, hy, hz, hy₀
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (hypothesis)
Goal:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : (↑y : ℝ) ∈ s
hz : z ∈ Icc x.toNNReal (↑y : ℝ).toNNReal
⊢ z ∈ toNNReal '' s
have hz₁ : z ∈ Icc x.toNNReal y
Tactic: rw [toNNReal_coe] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
⊢ Eq (α := ℝ≥0) (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |0| ⋯) 0
have simp : Eq (α := ℝ≥0) (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) 0 sorry) 0
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
⊢ Eq (α := ℝ≥0) (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |1| ⋯) 1
have simp : Eq (α := ℝ≥0) (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) 1 sorry) 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x y : ℝ
⊢ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |x * y| ⋯ =
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |x| ⋯ * Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |y| ⋯
have simp : Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (|x| * |y|) sorry =
  Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |x| sorry * Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |y| sorry
Tactic: simp [abs_mul]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
h : 0 ≤ x
⊢ (nnabs : (a : ℝ) → ℝ≥0) x = x.toNNReal
have a : (↑((nnabs : (a : ℝ) → ℝ≥0) x) : ℝ) = (↑x.toNNReal : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
h : 0 ≤ x
⊢ (↑((nnabs : (a : ℝ) → ℝ≥0) x) : ℝ) = (↑x.toNNReal : ℝ)
have a : (↑((nnabs : (a : ℝ) → ℝ≥0) x) : ℝ) = x
Tactic: rw [coe_toNNReal x h, coe_nnabs, abs_of_nonneg h]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
h : 0 ≤ x
a : (↑((nnabs : (a : ℝ) → ℝ≥0) x) : ℝ) = x
⊢ (↑((nnabs : (a : ℝ) → ℝ≥0) x) : ℝ) = (↑x.toNNReal : ℝ)
have a₁ : |x| = x
Tactic: rw [coe_toNNReal x h, coe_nnabs, abs_of_nonneg h]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
x : ℝ
h : 0 ≤ x
a : (↑((nnabs : (a : ℝ) → ℝ≥0) x) : ℝ) = x
a₁ : |x| = x
⊢ (↑((nnabs : (a : ℝ) → ℝ≥0) x) : ℝ) = (↑x.toNNReal : ℝ)
have a₂ : x = x
Tactic: rw [coe_toNNReal x h, coe_nnabs, abs_of_nonneg h]