awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : (i : ι) → ℝ≥0
⊢ ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i
have pos : ∀ (h : BddAbove (range f)), ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i
Tactic: by_cases h : BddAbove (range f)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : (i : ι) → ℝ≥0
pos : ∀ (h : BddAbove (range f)), ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i
⊢ ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i
have neg : ∀ (h : ¬BddAbove (range f)), ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i
Tactic: by_cases h : BddAbove (range f)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : (i : ι) → ℝ≥0
h : BddAbove (range f)
⊢ ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i
have pos : (↑(iSup f) : ℝ≥0∞).toNNReal = ⨆ (i : ι), f i
Tactic: rw [← coe_iSup h, toNNReal_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : (i : ι) → ℝ≥0
h : BddAbove (range f)
pos : (↑(iSup f) : ℝ≥0∞).toNNReal = ⨆ (i : ι), f i
⊢ ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i
have pos₁ : iSup f = ⨆ (i : ι), f i
Tactic: rw [← coe_iSup h, toNNReal_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : (i : ι) → ℝ≥0
h : ¬BddAbove (range f)
⊢ ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i
have neg : ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = 0
Tactic: rw [NNReal.iSup_of_not_bddAbove h, iSup_coe_eq_top.2 h, toNNReal_top]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : (i : ι) → ℝ≥0
h : ¬BddAbove (range f)
neg : ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = 0
⊢ ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i
have neg₁ : ENNReal.toNNReal ∞ = 0
Tactic: rw [NNReal.iSup_of_not_bddAbove h, iSup_coe_eq_top.2 h, toNNReal_top]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : (i : ι) → ℝ≥0
h : ¬BddAbove (range f)
neg : ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = 0
neg₁ : ENNReal.toNNReal ∞ = 0
⊢ ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i
have neg₂ : Eq (α := ℝ≥0) 0 0
Tactic: rw [NNReal.iSup_of_not_bddAbove h, iSup_coe_eq_top.2 h, toNNReal_top]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (hypothesis)
Goal:
s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ∞
⊢ (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)
have hf : ∀ (i : { x : ℝ≥0∞ // x ∈ s }), (↑i : ℝ≥0∞) ≠ ∞
Tactic: have hf : ∀ i, ((↑) : s → ℝ≥0∞) i ≠ ∞ := fun ⟨r, rs⟩ => hs r rs
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
a : ℝ≥0∞
inst : Nonempty ι
f : ι → ℝ≥0∞
⊢ a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i
have inl : HAdd.hAdd (α := ℝ≥0∞) ∞ (⨆ (i : ι), f i) = ⨆ (i : ι), ∞ + f i
Tactic: obtain rfl | ha := eq_or_ne a ∞
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
a : ℝ≥0∞
inst : Nonempty ι
f : ι → ℝ≥0∞
inl : HAdd.hAdd (α := ℝ≥0∞) ∞ (⨆ (i : ι), f i) = ⨆ (i : ι), ∞ + f i
⊢ a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i
have inr : ∀ (ha : a ≠ ∞), a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i
Tactic: obtain rfl | ha := eq_or_ne a ∞
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
a : ℝ≥0∞
inst : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
i : ι
⊢ a + f i ≤ a + ⨆ (i : ι), f i
have grw : a + f i ≤ a + f i
Tactic: grw [← le_iSup]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
a : ℝ≥0∞
inst : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
⊢ a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i
have inr : a + ⨆ (i : ι), f i ≤ ⨆ (i : ι), a + f i
Tactic: refine le_antisymm ?_ <| iSup_le fun i ↦ by grw [← le_iSup]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
a : ℝ≥0∞
inst : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
⊢ a + ⨆ (i : ι), f i ≤ ⨆ (i : ι), a + f i
have inr : ⨆ (i : ι), f i ≤ (⨆ (i : ι), a + f i) - a
Tactic: refine add_le_of_le_tsub_left_of_le (le_iSup_of_le (Classical.arbitrary _) le_self_add) ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (hypothesis)
Goal:
ι : Sort u_1
a : ℝ≥0∞
p : ι → Prop
h : ∃ (i : ι), p i
f : ι → ℝ≥0∞
⊢ a + ⨆ (i : ι), ⨆ (_ : p i), f i = ⨆ (i : ι), ⨆ (_ : p i), a + f i
have this : Nonempty.{max 1 u_1} { i : ι // p i }
Tactic: haveI : Nonempty {i // p i} := nonempty_subtype.2 h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
s : Set ℝ≥0∞
a : ℝ≥0∞
hs : s.Nonempty
⊢ a + sSup s = ⨆ b ∈ s, a + b
have rw : a + ⨆ a ∈ s, a = ⨆ b ∈ s, a + b
Tactic: rw [sSup_eq_iSup, add_biSup hs]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
s : Set ℝ≥0∞
a : ℝ≥0∞
hs : s.Nonempty
rw : a + ⨆ a ∈ s, a = ⨆ b ∈ s, a + b
⊢ a + sSup s = ⨆ b ∈ s, a + b
have rw₁ : Eq (α := ℝ≥0∞) (⨆ i ∈ s, a + i) (⨆ b ∈ s, a + b)
Tactic: rw [sSup_eq_iSup, add_biSup hs]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
s : Set ℝ≥0∞
a : ℝ≥0∞
hs : s.Nonempty
⊢ sSup s + a = ⨆ b ∈ s, b + a
have rw : (⨆ a ∈ s, a) + a = ⨆ b ∈ s, b + a
Tactic: rw [sSup_eq_iSup, biSup_add hs]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
s : Set ℝ≥0∞
a : ℝ≥0∞
hs : s.Nonempty
rw : (⨆ a ∈ s, a) + a = ⨆ b ∈ s, b + a
⊢ sSup s + a = ⨆ b ∈ s, b + a
have rw₁ : Eq (α := ℝ≥0∞) (⨆ i ∈ s, i + a) (⨆ b ∈ s, b + a)
Tactic: rw [sSup_eq_iSup, biSup_add hs]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
inst_1 : Nonempty κ
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ iSup f + iSup g ≤ a
have simp_rw : ⨆ (i : ι), ⨆ (i_1 : κ), f i + g i_1 ≤ a
Tactic: simp_rw [iSup_add, add_iSup]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
p : ι → Prop
q : κ → Prop
hp : ∃ (i : ι), p i
hq : ∃ (j : κ), q j
g : κ → ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (i : ι), ⨆ (_ : p i), f i) (⨆ (j : κ), ⨆ (_ : q j), g j) ≤ a
have simp_rw : ⨆ (i : ι), ⨆ (_ : p i), ⨆ (i_1 : κ), ⨆ (_ : q i_1), f i + g i_1 ≤ a
Tactic: simp_rw [biSup_add' hp, add_biSup' hq]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
⊢ iSup f + iSup g = ⨆ (i : ι), f i + g i
have inl : IsEmpty ι → iSup f + iSup g = ⨆ (i : ι), f i + g i
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
inl : IsEmpty ι → iSup f + iSup g = ⨆ (i : ι), f i + g i
⊢ iSup f + iSup g = ⨆ (i : ι), f i + g i
have inr : Nonempty ι → iSup f + iSup g = ⨆ (i : ι), f i + g i
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
⊢ iSup f + iSup g = ⨆ (i : ι), f i + g i
have inr : iSup f + iSup g ≤ ⨆ (i : ι), f i + g i
Tactic: refine le_antisymm ?_ (iSup_le fun a => add_le_add (le_iSup _ _) (le_iSup _ _))
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
⊢ iSup f + iSup g ≤ ⨆ (i : ι), f i + g i
have inr : ∀ (i j : ι), f i + g j ≤ ⨆ (i : ι), f i + g i
Tactic: refine iSup_add_iSup_le fun i j => ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
i j : ι
⊢ f i + g j ≤ ⨆ (i : ι), f i + g i
have inr : ∀ (k : ι) (hk : f i + g j ≤ f k + g k), f i + g j ≤ ⨆ (i : ι), f i + g i
Tactic: rcases h i j with ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Type u_3
inst : Preorder ι
inst_1 : IsDirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ f i + g j ≤ f _k + g _k
have h₁ : f i ≤ f _k
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Type u_3
inst : Preorder ι
inst_1 : IsDirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
h₁ : f i ≤ f _k
⊢ f i + g j ≤ f _k + g _k
have h₂ : g j ≤ g _k
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
have inl : ∀ (i : ι) (hi : a < f i), a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
Tactic: obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
inl : ∀ (i : ι) (hi : a < f i), a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
have inr : ∀ (h : ¬∃ (i : ι), a < f i), a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
Tactic: obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
have inl : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ι), a - f i < b
Tactic: rw [tsub_eq_zero_iff_le.2 <| le_iSup_of_le _ hi.le, iInf_eq_bot.2, bot_eq_zero]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (hypothesis)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
h : ¬∃ (i : ι), a < f i
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
have h₁ : ∀ (x : ι), f x ≤ a
Tactic: simp_rw [not_exists, not_lt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
h : ∀ (x : ι), f x ≤ a
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
have inr : ∀ (i : ι), f i ≤ a - ⨅ (i : ι), a - f i
Tactic: refine le_antisymm (le_iInf fun i ↦ tsub_le_tsub_left (le_iSup ..) _) <|
    ENNReal.le_sub_of_add_le_left (ne_top_of_le_ne_top ha <| iSup_le h) <|
    add_le_of_le_tsub_right_of_le (iInf_le_of_le (Classical.arbitrary _) tsub_le_self) <|
    iSup_le fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ f i ≤ a - ⨅ (i : ι), a - f i
have inr : a - (a - f i) ≤ a - ⨅ (i : ι), a - f i
Tactic: rw [← sub_sub_cancel ha (h _)]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a : ℝ≥0∞
⊢ ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b = a
have refine : a ≤ ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b
Tactic: refine le_antisymm (iSup₂_le fun b hb ↦ hb.le) ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a : ℝ≥0∞
⊢ a ≤ ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b
have refine : ∀ (c : ℝ≥0∞) (hca : c < a), c < ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b
Tactic: refine le_of_forall_lt fun c hca ↦ ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a c : ℝ≥0∞
hca : c < a
⊢ c < ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b
have obtain : ∀ (d : ℝ≥0∞) (hcd : c < d) (hdb : d < a), c < ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b
Tactic: obtain ⟨d, hcd, hdb⟩ := exists_between hca
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
x y z : ℝ≥0∞
h : x < y + z
hy : y ≠ 0
hz : z ≠ 0
⊢ ∃ y' < y, ∃ z' < z, x < y' + z'
have contrapose! : ∀ (h : ∀ (y' : ℝ≥0∞) (_ : y' < y) (z' : ℝ≥0∞) (_ : z' < z), y' + z' ≤ x), y + z ≤ x
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
⊢ (a + b).toReal = a.toReal + b.toReal
have lift : ∀ (a : ℝ≥0), ((↑a : ℝ≥0∞) + b).toReal = (↑a : ℝ≥0∞).toReal + b.toReal
Tactic: lift a to ℝ≥0 using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
b : ℝ≥0∞
hb : b ≠ ∞
a : ℝ≥0
⊢ ((↑a : ℝ≥0∞) + b).toReal = (↑a : ℝ≥0∞).toReal + b.toReal
have lift : ∀ (b : ℝ≥0), ((↑a : ℝ≥0∞) + (↑b : ℝ≥0∞)).toReal = (↑a : ℝ≥0∞).toReal + (↑b : ℝ≥0∞).toReal
Tactic: lift b to ℝ≥0 using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q
have rw : (↑(p + q).toNNReal : ℝ≥0∞) = ENNReal.ofReal p + ENNReal.ofReal q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, ENNReal.ofReal, ← coe_add, coe_inj,
    Real.toNNReal_add hp hq]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
rw : (↑(p + q).toNNReal : ℝ≥0∞) = ENNReal.ofReal p + ENNReal.ofReal q
⊢ ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q
have rw₁ : (↑(p + q).toNNReal : ℝ≥0∞) = (↑p.toNNReal : ℝ≥0∞) + ENNReal.ofReal q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, ENNReal.ofReal, ← coe_add, coe_inj,
    Real.toNNReal_add hp hq]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
rw : (↑(p + q).toNNReal : ℝ≥0∞) = ENNReal.ofReal p + ENNReal.ofReal q
rw₁ : (↑(p + q).toNNReal : ℝ≥0∞) = (↑p.toNNReal : ℝ≥0∞) + ENNReal.ofReal q
⊢ ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q
have rw₂ : (↑(p + q).toNNReal : ℝ≥0∞) = (↑p.toNNReal : ℝ≥0∞) + (↑q.toNNReal : ℝ≥0∞)
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, ENNReal.ofReal, ← coe_add, coe_inj,
    Real.toNNReal_add hp hq]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
rw : (↑(p + q).toNNReal : ℝ≥0∞) = ENNReal.ofReal p + ENNReal.ofReal q
rw₁ : (↑(p + q).toNNReal : ℝ≥0∞) = (↑p.toNNReal : ℝ≥0∞) + ENNReal.ofReal q
rw₂ : (↑(p + q).toNNReal : ℝ≥0∞) = (↑p.toNNReal : ℝ≥0∞) + (↑q.toNNReal : ℝ≥0∞)
⊢ ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q
have rw₃ : (↑(p + q).toNNReal : ℝ≥0∞) = (↑(p.toNNReal + q.toNNReal) : ℝ≥0∞)
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, ENNReal.ofReal, ← coe_add, coe_inj,
    Real.toNNReal_add hp hq]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
rw : (↑(p + q).toNNReal : ℝ≥0∞) = ENNReal.ofReal p + ENNReal.ofReal q
rw₁ : (↑(p + q).toNNReal : ℝ≥0∞) = (↑p.toNNReal : ℝ≥0∞) + ENNReal.ofReal q
rw₂ : (↑(p + q).toNNReal : ℝ≥0∞) = (↑p.toNNReal : ℝ≥0∞) + (↑q.toNNReal : ℝ≥0∞)
rw₃ : (↑(p + q).toNNReal : ℝ≥0∞) = (↑(p.toNNReal + q.toNNReal) : ℝ≥0∞)
⊢ ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q
have rw₄ : (p + q).toNNReal = p.toNNReal + q.toNNReal
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, ENNReal.ofReal, ← coe_add, coe_inj,
    Real.toNNReal_add hp hq]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
rw : (↑(p + q).toNNReal : ℝ≥0∞) = ENNReal.ofReal p + ENNReal.ofReal q
rw₁ : (↑(p + q).toNNReal : ℝ≥0∞) = (↑p.toNNReal : ℝ≥0∞) + ENNReal.ofReal q
rw₂ : (↑(p + q).toNNReal : ℝ≥0∞) = (↑p.toNNReal : ℝ≥0∞) + (↑q.toNNReal : ℝ≥0∞)
rw₃ : (↑(p + q).toNNReal : ℝ≥0∞) = (↑(p.toNNReal + q.toNNReal) : ℝ≥0∞)
rw₄ : (p + q).toNNReal = p.toNNReal + q.toNNReal
⊢ ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q
have rw₅ : p.toNNReal + q.toNNReal = p.toNNReal + q.toNNReal
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, ENNReal.ofReal, ← coe_add, coe_inj,
    Real.toNNReal_add hp hq]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
⊢ a.toReal ≤ b.toReal ↔ a ≤ b
have lift : ∀ (a : ℝ≥0), (↑a : ℝ≥0∞).toReal ≤ b.toReal ↔ (↑a : ℝ≥0∞) ≤ b
Tactic: lift a to ℝ≥0 using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
b : ℝ≥0∞
hb : b ≠ ∞
a : ℝ≥0
⊢ (↑a : ℝ≥0∞).toReal ≤ b.toReal ↔ (↑a : ℝ≥0∞) ≤ b
have lift : ∀ (b : ℝ≥0), (↑a : ℝ≥0∞).toReal ≤ (↑b : ℝ≥0∞).toReal ↔ (↑a : ℝ≥0∞) ≤ (↑b : ℝ≥0∞)
Tactic: lift b to ℝ≥0 using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a b : ℝ≥0
⊢ (↑a : ℝ≥0∞).toReal ≤ (↑b : ℝ≥0∞).toReal ↔ (↑a : ℝ≥0∞) ≤ (↑b : ℝ≥0∞)
have norm_cast : (↑a : ℝ≥0∞).toReal ≤ (↑b : ℝ≥0∞).toReal ↔ a ≤ b
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a b : ℝ≥0∞
h : a ≤ b
ht : b = ∞ → a = ∞
⊢ a.toReal ≤ b.toReal
have inl : ∀ (h : ∞ ≤ b) (ht : b = ∞ → Eq (α := ℝ≥0∞) ∞ ∞), ENNReal.toReal ∞ ≤ b.toReal
Tactic: rcases eq_or_ne a ∞ with rfl | ha
Cleared hypotheses: a, h, ht
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a b : ℝ≥0∞
h : a ≤ b
ht : b = ∞ → a = ∞
inl : ∀ (h : ∞ ≤ b) (ht : b = ∞ → Eq (α := ℝ≥0∞) ∞ ∞), ENNReal.toReal ∞ ≤ b.toReal
⊢ a.toReal ≤ b.toReal
have inr : ∀ (ha : a ≠ ∞), a.toReal ≤ b.toReal
Tactic: rcases eq_or_ne a ∞ with rfl | ha
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
⊢ a.toReal < b.toReal ↔ a < b
have lift : ∀ (a : ℝ≥0), (↑a : ℝ≥0∞).toReal < b.toReal ↔ (↑a : ℝ≥0∞) < b
Tactic: lift a to ℝ≥0 using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
b : ℝ≥0∞
hb : b ≠ ∞
a : ℝ≥0
⊢ (↑a : ℝ≥0∞).toReal < b.toReal ↔ (↑a : ℝ≥0∞) < b
have lift : ∀ (b : ℝ≥0), (↑a : ℝ≥0∞).toReal < (↑b : ℝ≥0∞).toReal ↔ (↑a : ℝ≥0∞) < (↑b : ℝ≥0∞)
Tactic: lift b to ℝ≥0 using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a b : ℝ≥0
⊢ (↑a : ℝ≥0∞).toReal < (↑b : ℝ≥0∞).toReal ↔ (↑a : ℝ≥0∞) < (↑b : ℝ≥0∞)
have norm_cast : (↑a : ℝ≥0∞).toReal < (↑b : ℝ≥0∞).toReal ↔ a < b
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal ≤ b.toNNReal
⊢ a ≤ b
have rwa : (↑a.toNNReal : ℝ≥0∞) ≤ b
Tactic: rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_le_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal ≤ b.toNNReal
rwa : (↑a.toNNReal : ℝ≥0∞) ≤ b
⊢ a ≤ b
have rwa₁ : (↑a.toNNReal : ℝ≥0∞) ≤ (↑b.toNNReal : ℝ≥0∞)
Tactic: rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_le_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal < b.toNNReal
⊢ a < b
have rwa : (↑a.toNNReal : ℝ≥0∞) < b
Tactic: rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_lt_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal < b.toNNReal
rwa : (↑a.toNNReal : ℝ≥0∞) < b
⊢ a < b
have rwa₁ : (↑a.toNNReal : ℝ≥0∞) < (↑b.toNNReal : ℝ≥0∞)
Tactic: rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_lt_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a : ℝ≥0∞
⊢ 0 < a.toNNReal ↔ 0 < a ∧ a < ∞
have top : 0 < ENNReal.toNNReal ∞ ↔ LT.lt (α := ℝ≥0∞) 0 ∞ ∧ LT.lt (α := ℝ≥0∞) ∞ ∞
Tactic: induction a
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a : ℝ≥0∞
top : 0 < ENNReal.toNNReal ∞ ↔ LT.lt (α := ℝ≥0∞) 0 ∞ ∧ LT.lt (α := ℝ≥0∞) ∞ ∞
⊢ 0 < a.toNNReal ↔ 0 < a ∧ a < ∞
have coe : ∀ (x : ℝ≥0), 0 < (↑x : ℝ≥0∞).toNNReal ↔ 0 < (↑x : ℝ≥0∞) ∧ (↑x : ℝ≥0∞) < ∞
Tactic: induction a
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
h : 0 ≤ q
⊢ ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q
have rw : (↑p.toNNReal : ℝ≥0∞) ≤ ENNReal.ofReal q ↔ p ≤ q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_le_coe, Real.toNNReal_le_toNNReal_iff h]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
h : 0 ≤ q
rw : (↑p.toNNReal : ℝ≥0∞) ≤ ENNReal.ofReal q ↔ p ≤ q
⊢ ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q
have rw₁ : (↑p.toNNReal : ℝ≥0∞) ≤ (↑q.toNNReal : ℝ≥0∞) ↔ p ≤ q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_le_coe, Real.toNNReal_le_toNNReal_iff h]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
h : 0 ≤ q
rw : (↑p.toNNReal : ℝ≥0∞) ≤ ENNReal.ofReal q ↔ p ≤ q
rw₁ : (↑p.toNNReal : ℝ≥0∞) ≤ (↑q.toNNReal : ℝ≥0∞) ↔ p ≤ q
⊢ ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q
have rw₂ : p.toNNReal ≤ q.toNNReal ↔ p ≤ q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_le_coe, Real.toNNReal_le_toNNReal_iff h]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
h : 0 ≤ q
rw : (↑p.toNNReal : ℝ≥0∞) ≤ ENNReal.ofReal q ↔ p ≤ q
rw₁ : (↑p.toNNReal : ℝ≥0∞) ≤ (↑q.toNNReal : ℝ≥0∞) ↔ p ≤ q
rw₂ : p.toNNReal ≤ q.toNNReal ↔ p ≤ q
⊢ ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q
have rw₃ : p ≤ q ↔ p ≤ q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_le_coe, Real.toNNReal_le_toNNReal_iff h]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q
have rw : (↑p.toNNReal : ℝ≥0∞) = ENNReal.ofReal q ↔ p = q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_inj, Real.toNNReal_eq_toNNReal_iff hp hq]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
rw : (↑p.toNNReal : ℝ≥0∞) = ENNReal.ofReal q ↔ p = q
⊢ ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q
have rw₁ : (↑p.toNNReal : ℝ≥0∞) = (↑q.toNNReal : ℝ≥0∞) ↔ p = q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_inj, Real.toNNReal_eq_toNNReal_iff hp hq]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
rw : (↑p.toNNReal : ℝ≥0∞) = ENNReal.ofReal q ↔ p = q
rw₁ : (↑p.toNNReal : ℝ≥0∞) = (↑q.toNNReal : ℝ≥0∞) ↔ p = q
⊢ ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q
have rw₂ : p.toNNReal = q.toNNReal ↔ p = q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_inj, Real.toNNReal_eq_toNNReal_iff hp hq]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
rw : (↑p.toNNReal : ℝ≥0∞) = ENNReal.ofReal q ↔ p = q
rw₁ : (↑p.toNNReal : ℝ≥0∞) = (↑q.toNNReal : ℝ≥0∞) ↔ p = q
rw₂ : p.toNNReal = q.toNNReal ↔ p = q
⊢ ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q
have rw₃ : p = q ↔ p = q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_inj, Real.toNNReal_eq_toNNReal_iff hp hq]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
h : 0 < q
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
have rw : (↑p.toNNReal : ℝ≥0∞) < ENNReal.ofReal q ↔ p < q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff h]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
h : 0 < q
rw : (↑p.toNNReal : ℝ≥0∞) < ENNReal.ofReal q ↔ p < q
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
have rw₁ : (↑p.toNNReal : ℝ≥0∞) < (↑q.toNNReal : ℝ≥0∞) ↔ p < q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff h]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
h : 0 < q
rw : (↑p.toNNReal : ℝ≥0∞) < ENNReal.ofReal q ↔ p < q
rw₁ : (↑p.toNNReal : ℝ≥0∞) < (↑q.toNNReal : ℝ≥0∞) ↔ p < q
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
have rw₂ : p.toNNReal < q.toNNReal ↔ p < q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff h]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
h : 0 < q
rw : (↑p.toNNReal : ℝ≥0∞) < ENNReal.ofReal q ↔ p < q
rw₁ : (↑p.toNNReal : ℝ≥0∞) < (↑q.toNNReal : ℝ≥0∞) ↔ p < q
rw₂ : p.toNNReal < q.toNNReal ↔ p < q
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
have rw₃ : p < q ↔ p < q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff h]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hp : 0 ≤ p
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
have rw : (↑p.toNNReal : ℝ≥0∞) < ENNReal.ofReal q ↔ p < q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff_of_nonneg hp]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hp : 0 ≤ p
rw : (↑p.toNNReal : ℝ≥0∞) < ENNReal.ofReal q ↔ p < q
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
have rw₁ : (↑p.toNNReal : ℝ≥0∞) < (↑q.toNNReal : ℝ≥0∞) ↔ p < q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff_of_nonneg hp]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hp : 0 ≤ p
rw : (↑p.toNNReal : ℝ≥0∞) < ENNReal.ofReal q ↔ p < q
rw₁ : (↑p.toNNReal : ℝ≥0∞) < (↑q.toNNReal : ℝ≥0∞) ↔ p < q
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
have rw₂ : p.toNNReal < q.toNNReal ↔ p < q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff_of_nonneg hp]