awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : ℝ
⊢ WithBot.some '' WithTop.some '' Ico x y = Ico (↑x : EReal) (↑y : EReal)
have rw : Ico (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) = Ico (↑x : EReal) (↑y : EReal)
Tactic: rw [WithTop.image_coe_Ico, WithBot.image_coe_Ico]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ
⊢ Real.toEReal '' Ici x = Ico (↑x : EReal) ⊤
have refine : WithBot.some '' WithTop.some '' Ici x = Ico (↑x : EReal) ⊤
Tactic: refine (image_comp WithBot.some WithTop.some _).trans ?_
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ
⊢ WithBot.some '' WithTop.some '' Ici x = Ico (↑x : EReal) ⊤
have rw : Ico (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑⊤ : WithBot (WithTop ℝ)) = Ico (↑x : EReal) ⊤
Tactic: rw [WithTop.image_coe_Ici, WithBot.image_coe_Ico]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : ℝ
⊢ Real.toEReal '' Ioc x y = Ioc (↑x : EReal) (↑y : EReal)
have refine : WithBot.some '' WithTop.some '' Ioc x y = Ioc (↑x : EReal) (↑y : EReal)
Tactic: refine (image_comp WithBot.some WithTop.some _).trans ?_
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : ℝ
⊢ WithBot.some '' WithTop.some '' Ioc x y = Ioc (↑x : EReal) (↑y : EReal)
have rw : Ioc (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) = Ioc (↑x : EReal) (↑y : EReal)
Tactic: rw [WithTop.image_coe_Ioc, WithBot.image_coe_Ioc]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : ℝ
⊢ Real.toEReal '' Ioo x y = Ioo (↑x : EReal) (↑y : EReal)
have refine : WithBot.some '' WithTop.some '' Ioo x y = Ioo (↑x : EReal) (↑y : EReal)
Tactic: refine (image_comp WithBot.some WithTop.some _).trans ?_
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : ℝ
⊢ WithBot.some '' WithTop.some '' Ioo x y = Ioo (↑x : EReal) (↑y : EReal)
have rw : Ioo (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) = Ioo (↑x : EReal) (↑y : EReal)
Tactic: rw [WithTop.image_coe_Ioo, WithBot.image_coe_Ioo]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ
⊢ Real.toEReal '' Ioi x = Ioo (↑x : EReal) ⊤
have refine : WithBot.some '' WithTop.some '' Ioi x = Ioo (↑x : EReal) ⊤
Tactic: refine (image_comp WithBot.some WithTop.some _).trans ?_
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ
⊢ WithBot.some '' WithTop.some '' Ioi x = Ioo (↑x : EReal) ⊤
have rw : Ioo (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑⊤ : WithBot (WithTop ℝ)) = Ioo (↑x : EReal) ⊤
Tactic: rw [WithTop.image_coe_Ioi, WithBot.image_coe_Ioo]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ
⊢ Real.toEReal '' Iic x = Ioc ⊥ (↑x : EReal)
have refine : WithBot.some '' WithTop.some '' Iic x = Ioc ⊥ (↑x : EReal)
Tactic: refine (image_comp WithBot.some WithTop.some _).trans ?_
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ
⊢ WithBot.some '' WithTop.some '' Iic x = Ioc ⊥ (↑x : EReal)
have rw : Ioc ⊥ (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) = Ioc ⊥ (↑x : EReal)
Tactic: rw [WithTop.image_coe_Iic, WithBot.image_coe_Iic]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ
⊢ Real.toEReal '' Iio x = Ioo ⊥ (↑x : EReal)
have refine : WithBot.some '' WithTop.some '' Iio x = Ioo ⊥ (↑x : EReal)
Tactic: refine (image_comp WithBot.some WithTop.some _).trans ?_
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ
⊢ WithBot.some '' WithTop.some '' Iio x = Ioo ⊥ (↑x : EReal)
have rw : Ioo ⊥ (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) = Ioo ⊥ (↑x : EReal)
Tactic: rw [WithTop.image_coe_Iio, WithBot.image_coe_Iio]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0∞
hx : x ≠ ∞
⊢ (↑x.toReal : EReal) = (↑x : EReal)
have lift : ∀ (x : ℝ≥0), (↑(↑x : ℝ≥0∞).toReal : EReal) = (↑(↑x : ℝ≥0∞) : EReal)
Tactic: lift x to ℝ≥0 using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0∞
⊢ (↑x : EReal) = 0 ↔ x = 0
have rw : (↑x : EReal) = 0 ↔ (↑x : EReal) = (↑0 : EReal)
Tactic: rw [← coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0∞
rw : (↑x : EReal) = 0 ↔ (↑x : EReal) = (↑0 : EReal)
⊢ (↑x : EReal) = 0 ↔ x = 0
have rw₁ : (↑x : EReal) = 0 ↔ (↑x : EReal) = 0
Tactic: rw [← coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0∞
⊢ (↑x : EReal) = 1 ↔ x = 1
have rw : (↑x : EReal) = 1 ↔ (↑x : EReal) = (↑1 : EReal)
Tactic: rw [← coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_one]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0∞
rw : (↑x : EReal) = 1 ↔ (↑x : EReal) = (↑1 : EReal)
⊢ (↑x : EReal) = 1 ↔ x = 1
have rw₁ : (↑x : EReal) = 1 ↔ (↑x : EReal) = 1
Tactic: rw [← coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_one]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0∞
⊢ 0 < (↑x : EReal) ↔ 0 < x
have rw : (↑0 : EReal) < (↑x : EReal) ↔ 0 < x
Tactic: rw [← coe_ennreal_zero, coe_ennreal_lt_coe_ennreal_iff]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0∞
rw : (↑0 : EReal) < (↑x : EReal) ↔ 0 < x
⊢ 0 < (↑x : EReal) ↔ 0 < x
have rw₁ : 0 < x ↔ 0 < x
Tactic: rw [← coe_ennreal_zero, coe_ennreal_lt_coe_ennreal_iff]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0∞
⊢ 0 < (↑x : EReal) ↔ x ≠ 0
have rw : 0 < x ↔ x ≠ 0
Tactic: rw [coe_ennreal_pos, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0∞
rw : 0 < x ↔ x ≠ 0
⊢ 0 < (↑x : EReal) ↔ x ≠ 0
have rw₁ : x ≠ 0 ↔ x ≠ 0
Tactic: rw [coe_ennreal_pos, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : ℝ≥0∞
⊢ (↑(x + y) : EReal) = (↑x : EReal) + (↑y : EReal)
have top : (↑(∞ + y) : EReal) = (↑∞ : EReal) + (↑y : EReal)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : ℝ≥0∞
top : (↑(∞ + y) : EReal) = (↑∞ : EReal) + (↑y : EReal)
⊢ (↑(x + y) : EReal) = (↑x : EReal) + (↑y : EReal)
have coe : ∀ (x : ℝ≥0), (↑((↑x : ℝ≥0∞) + y) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) + (↑y : EReal)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : ℝ≥0∞
⊢ (↑(∞ + y) : EReal) = (↑∞ : EReal) + (↑y : EReal)
have top : (↑(HAdd.hAdd (α := ℝ≥0∞) ∞ ∞) : EReal) = (↑∞ : EReal) + (↑∞ : EReal)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : ℝ≥0∞
top : (↑(HAdd.hAdd (α := ℝ≥0∞) ∞ ∞) : EReal) = (↑∞ : EReal) + (↑∞ : EReal)
⊢ (↑(∞ + y) : EReal) = (↑∞ : EReal) + (↑y : EReal)
have top₁ : ∀ (x : ℝ≥0), (↑(∞ + (↑x : ℝ≥0∞)) : EReal) = (↑∞ : EReal) + (↑(↑x : ℝ≥0∞) : EReal)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : ℝ≥0∞
x : ℝ≥0
⊢ (↑((↑x : ℝ≥0∞) + y) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) + (↑y : EReal)
have coe : (↑((↑x : ℝ≥0∞) + ∞) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) + (↑∞ : EReal)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : ℝ≥0∞
x : ℝ≥0
coe : (↑((↑x : ℝ≥0∞) + ∞) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) + (↑∞ : EReal)
⊢ (↑((↑x : ℝ≥0∞) + y) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) + (↑y : EReal)
have coe₁ : ∀ (x_1 : ℝ≥0), (↑((↑x : ℝ≥0∞) + (↑x_1 : ℝ≥0∞)) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) + (↑(↑x_1 : ℝ≥0∞) : EReal)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0
⊢ (↑(∞ * (↑x : ℝ≥0∞)) : EReal) = ⊤ * (↑(↑x : ℝ≥0∞) : EReal)
have inl : (↑(∞ * (↑0 : ℝ≥0∞)) : EReal) = ⊤ * (↑(↑0 : ℝ≥0∞) : EReal)
Tactic: rcases eq_or_ne x 0 with (rfl | h0)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0
inl : (↑(∞ * (↑0 : ℝ≥0∞)) : EReal) = ⊤ * (↑(↑0 : ℝ≥0∞) : EReal)
⊢ (↑(∞ * (↑x : ℝ≥0∞)) : EReal) = ⊤ * (↑(↑x : ℝ≥0∞) : EReal)
have inr : ∀ (h0 : x ≠ 0), (↑(∞ * (↑x : ℝ≥0∞)) : EReal) = ⊤ * (↑(↑x : ℝ≥0∞) : EReal)
Tactic: rcases eq_or_ne x 0 with (rfl | h0)
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0
h0 : x ≠ 0
⊢ (↑(∞ * (↑x : ℝ≥0∞)) : EReal) = ⊤ * (↑(↑x : ℝ≥0∞) : EReal)
have inr : (↑∞ : EReal) = ⊤ * (↑(↑x : ℝ≥0∞) : EReal)
Tactic: rw [ENNReal.top_mul (ENNReal.coe_ne_zero.2 h0)]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0
⊢ (↑((↑x : ℝ≥0∞) * ∞) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
have rw : (↑(∞ * (↑x : ℝ≥0∞)) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
Tactic: rw [mul_comm, coe_ennreal_top_mul, EReal.mul_comm, coe_ennreal_top]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0
rw : (↑(∞ * (↑x : ℝ≥0∞)) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
⊢ (↑((↑x : ℝ≥0∞) * ∞) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
have rw₁ : ⊤ * (↑(↑x : ℝ≥0∞) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
Tactic: rw [mul_comm, coe_ennreal_top_mul, EReal.mul_comm, coe_ennreal_top]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0
rw : (↑(∞ * (↑x : ℝ≥0∞)) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
rw₁ : ⊤ * (↑(↑x : ℝ≥0∞) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
⊢ (↑((↑x : ℝ≥0∞) * ∞) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
have rw₂ : (↑(↑x : ℝ≥0∞) : EReal) * ⊤ = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
Tactic: rw [mul_comm, coe_ennreal_top_mul, EReal.mul_comm, coe_ennreal_top]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0
rw : (↑(∞ * (↑x : ℝ≥0∞)) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
rw₁ : ⊤ * (↑(↑x : ℝ≥0∞) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
rw₂ : (↑(↑x : ℝ≥0∞) : EReal) * ⊤ = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
⊢ (↑((↑x : ℝ≥0∞) * ∞) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) * (↑∞ : EReal)
have rw₃ : (↑(↑x : ℝ≥0∞) : EReal) * ⊤ = (↑(↑x : ℝ≥0∞) : EReal) * ⊤
Tactic: rw [mul_comm, coe_ennreal_top_mul, EReal.mul_comm, coe_ennreal_top]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
⊢ x.toENNReal = ∞ ↔ x = ⊤
have pos : ∀ (h : x = ⊤), x.toENNReal = ∞ ↔ x = ⊤
Tactic: by_cases h : x = ⊤
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
pos : ∀ (h : x = ⊤), x.toENNReal = ∞ ↔ x = ⊤
⊢ x.toENNReal = ∞ ↔ x = ⊤
have neg : ∀ (h : ¬x = ⊤), x.toENNReal = ∞ ↔ x = ⊤
Tactic: by_cases h : x = ⊤
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : x ≤ 0
⊢ x.toENNReal = 0
have rw : ENNReal.ofReal x.toReal = 0
Tactic: rw [toENNReal, if_neg (fun h ↦ ?_)]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : x ≤ 0
rw : ENNReal.ofReal x.toReal = 0
⊢ x.toENNReal = 0
have rw₁ : ∀ (h : x = ⊤), False
Tactic: rw [toENNReal, if_neg (fun h ↦ ?_)]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
⊢ x.toENNReal = 0 ↔ x ≤ 0
have bot : toENNReal ⊥ = 0 ↔ LE.le (α := EReal) ⊥ 0
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
bot : toENNReal ⊥ = 0 ↔ LE.le (α := EReal) ⊥ 0
⊢ x.toENNReal = 0 ↔ x ≤ 0
have coe : ∀ (a : ℝ), (↑a : EReal).toENNReal = 0 ↔ (↑a : EReal) ≤ 0
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
bot : toENNReal ⊥ = 0 ↔ LE.le (α := EReal) ⊥ 0
coe : ∀ (a : ℝ), (↑a : EReal).toENNReal = 0 ↔ (↑a : EReal) ≤ 0
⊢ x.toENNReal = 0 ↔ x ≤ 0
have top : toENNReal ⊤ = 0 ↔ LE.le (α := EReal) ⊤ 0
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
⊢ 0 < x.toENNReal ↔ 0 < x
have rw : x.toENNReal ≠ 0 ↔ 0 < x
Tactic: rw [pos_iff_ne_zero, toENNReal_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
rw : x.toENNReal ≠ 0 ↔ 0 < x
⊢ 0 < x.toENNReal ↔ 0 < x
have rw₁ : 0 < x ↔ 0 < x
Tactic: rw [pos_iff_ne_zero, toENNReal_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : 0 ≤ x
⊢ (↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) : EReal) = x
have pos : ∀ (h_top : x = ⊤), (↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) : EReal) = x
Tactic: by_cases h_top : x = ⊤
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : 0 ≤ x
pos : ∀ (h_top : x = ⊤), (↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) : EReal) = x
⊢ (↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) : EReal) = x
have neg : ∀ (h_top : ¬x = ⊤), (↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) : EReal) = x
Tactic: by_cases h_top : x = ⊤
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : 0 ≤ x
h_top : x = ⊤
⊢ (↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) : EReal) = x
have pos : (↑∞ : EReal) = ⊤
Tactic: rw [if_pos h_top, h_top]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ (↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) : EReal) = x
have neg : (↑(ENNReal.ofReal x.toReal) : EReal) = x
Tactic: rw [if_neg h_top]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ (↑(ENNReal.ofReal x.toReal) : EReal) = x
have neg : (↑x.toReal : EReal) = x
Tactic: simp only [coe_ennreal_ofReal, hx, toReal_nonneg, max_eq_left]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
⊢ (↑x.toENNReal : EReal) = max 0 x
have inl : ∀ (hx : 0 ≤ x), (↑x.toENNReal : EReal) = max 0 x
Tactic: rcases le_total 0 x with (hx | hx)
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
inl : ∀ (hx : 0 ≤ x), (↑x.toENNReal : EReal) = max 0 x
⊢ (↑x.toENNReal : EReal) = max 0 x
have inr : ∀ (hx : x ≤ 0), (↑x.toENNReal : EReal) = max 0 x
Tactic: rcases le_total 0 x with (hx | hx)
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : 0 ≤ x
⊢ (↑x.toENNReal : EReal) = max 0 x
have inl : x = max 0 x
Tactic: rw [coe_toENNReal hx, max_eq_right hx]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : 0 ≤ x
inl : x = max 0 x
⊢ (↑x.toENNReal : EReal) = max 0 x
have inl₁ : x = x
Tactic: rw [coe_toENNReal hx, max_eq_right hx]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : x ≤ 0
⊢ (↑x.toENNReal : EReal) = max 0 x
have inr : (↑0 : EReal) = max 0 x
Tactic: rw [toENNReal_of_nonpos hx, max_eq_left hx, coe_ennreal_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : x ≤ 0
inr : (↑0 : EReal) = max 0 x
⊢ (↑x.toENNReal : EReal) = max 0 x
have inr₁ : (↑0 : EReal) = 0
Tactic: rw [toENNReal_of_nonpos hx, max_eq_left hx, coe_ennreal_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : x ≤ 0
inr : (↑0 : EReal) = max 0 x
inr₁ : (↑0 : EReal) = 0
⊢ (↑x.toENNReal : EReal) = max 0 x
have inr₂ : Eq (α := EReal) 0 0
Tactic: rw [toENNReal_of_nonpos hx, max_eq_left hx, coe_ennreal_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0∞
⊢ (↑x : EReal).toENNReal = x
have pos : ∀ (h_top : x = ∞), (↑x : EReal).toENNReal = x
Tactic: by_cases h_top : x = ⊤
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0∞
pos : ∀ (h_top : x = ∞), (↑x : EReal).toENNReal = x
⊢ (↑x : EReal).toENNReal = x
have neg : ∀ (h_top : ¬x = ∞), (↑x : EReal).toENNReal = x
Tactic: by_cases h_top : x = ⊤
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0∞
h_top : x = ∞
⊢ (↑x : EReal).toENNReal = x
have pos : (↑∞ : EReal).toENNReal = ∞
Tactic: rw [h_top, coe_ennreal_top, toENNReal_top]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0∞
h_top : x = ∞
pos : (↑∞ : EReal).toENNReal = ∞
⊢ (↑x : EReal).toENNReal = x
have pos₁ : toENNReal ⊤ = ∞
Tactic: rw [h_top, coe_ennreal_top, toENNReal_top]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0∞
h_top : x = ∞
pos : (↑∞ : EReal).toENNReal = ∞
pos₁ : toENNReal ⊤ = ∞
⊢ (↑x : EReal).toENNReal = x
have pos₂ : Eq (α := ℝ≥0∞) ∞ ∞
Tactic: rw [h_top, coe_ennreal_top, toENNReal_top]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ≥0∞
h_top : ¬x = ∞
⊢ (↑x : EReal).toENNReal = x
have rwa : ¬(↑x : EReal) = ⊤
Tactic: rwa [toENNReal, if_neg _, toReal_coe_ennreal, ENNReal.ofReal_toReal_eq_iff]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : 0 ≤ x
⊢ x.toENNReal.toReal = x.toReal
have pos : ∀ (h : x = ⊤), x.toENNReal.toReal = x.toReal
Tactic: by_cases h : x = ⊤
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : 0 ≤ x
pos : ∀ (h : x = ⊤), x.toENNReal.toReal = x.toReal
⊢ x.toENNReal.toReal = x.toReal
have neg : ∀ (h : ¬x = ⊤), x.toENNReal.toReal = x.toReal
Tactic: by_cases h : x = ⊤
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : EReal
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x.toENNReal = y.toENNReal ↔ x = y
have bot : ∀ (hx : LE.le (α := EReal) 0 ⊥), toENNReal ⊥ = y.toENNReal ↔ ⊥ = y
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : EReal
hx : 0 ≤ x
hy : 0 ≤ y
bot : ∀ (hx : LE.le (α := EReal) 0 ⊥), toENNReal ⊥ = y.toENNReal ↔ ⊥ = y
⊢ x.toENNReal = y.toENNReal ↔ x = y
have coe : ∀ (a : ℝ) (hx : 0 ≤ (↑a : EReal)), (↑a : EReal).toENNReal = y.toENNReal ↔ (↑a : EReal) = y
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : EReal
hx : 0 ≤ x
hy : 0 ≤ y
bot : ∀ (hx : LE.le (α := EReal) 0 ⊥), toENNReal ⊥ = y.toENNReal ↔ ⊥ = y
coe : ∀ (a : ℝ) (hx : 0 ≤ (↑a : EReal)), (↑a : EReal).toENNReal = y.toENNReal ↔ (↑a : EReal) = y
⊢ x.toENNReal = y.toENNReal ↔ x = y
have top : ∀ (hx : LE.le (α := EReal) 0 ⊤), toENNReal ⊤ = y.toENNReal ↔ ⊤ = y
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊥
⊢ toENNReal ⊥ = y.toENNReal ↔ ⊥ = y
have bot : ∀ (hy : LE.le (α := EReal) 0 ⊥), toENNReal ⊥ = toENNReal ⊥ ↔ Eq (α := EReal) ⊥ ⊥
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊥
bot : ∀ (hy : LE.le (α := EReal) 0 ⊥), toENNReal ⊥ = toENNReal ⊥ ↔ Eq (α := EReal) ⊥ ⊥
⊢ toENNReal ⊥ = y.toENNReal ↔ ⊥ = y
have bot₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), toENNReal ⊥ = (↑a : EReal).toENNReal ↔ ⊥ = (↑a : EReal)
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊥
bot : ∀ (hy : LE.le (α := EReal) 0 ⊥), toENNReal ⊥ = toENNReal ⊥ ↔ Eq (α := EReal) ⊥ ⊥
bot₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), toENNReal ⊥ = (↑a : EReal).toENNReal ↔ ⊥ = (↑a : EReal)
⊢ toENNReal ⊥ = y.toENNReal ↔ ⊥ = y
have bot₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), toENNReal ⊥ = toENNReal ⊤ ↔ Eq (α := EReal) ⊥ ⊤
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
hy : 0 ≤ y
a : ℝ
hx : 0 ≤ (↑a : EReal)
⊢ (↑a : EReal).toENNReal = y.toENNReal ↔ (↑a : EReal) = y
have coe : ∀ (hy : LE.le (α := EReal) 0 ⊥), (↑a : EReal).toENNReal = toENNReal ⊥ ↔ (↑a : EReal) = ⊥
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
hy : 0 ≤ y
a : ℝ
hx : 0 ≤ (↑a : EReal)
coe : ∀ (hy : LE.le (α := EReal) 0 ⊥), (↑a : EReal).toENNReal = toENNReal ⊥ ↔ (↑a : EReal) = ⊥
⊢ (↑a : EReal).toENNReal = y.toENNReal ↔ (↑a : EReal) = y
have coe₁ : ∀ (a_1 : ℝ) (hy : 0 ≤ (↑a_1 : EReal)), (↑a : EReal).toENNReal = (↑a_1 : EReal).toENNReal ↔ (↑a : EReal) = (↑a_1 : EReal)
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
hy : 0 ≤ y
a : ℝ
hx : 0 ≤ (↑a : EReal)
coe : ∀ (hy : LE.le (α := EReal) 0 ⊥), (↑a : EReal).toENNReal = toENNReal ⊥ ↔ (↑a : EReal) = ⊥
coe₁ :
  ∀ (a_1 : ℝ) (hy : 0 ≤ (↑a_1 : EReal)),
    (↑a : EReal).toENNReal = (↑a_1 : EReal).toENNReal ↔ (↑a : EReal) = (↑a_1 : EReal)
⊢ (↑a : EReal).toENNReal = y.toENNReal ↔ (↑a : EReal) = y
have coe₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), (↑a : EReal).toENNReal = toENNReal ⊤ ↔ (↑a : EReal) = ⊤
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊤
⊢ toENNReal ⊤ = y.toENNReal ↔ ⊤ = y
have top : ∀ (hy : LE.le (α := EReal) 0 ⊥), toENNReal ⊤ = toENNReal ⊥ ↔ Eq (α := EReal) ⊤ ⊥
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊤
top : ∀ (hy : LE.le (α := EReal) 0 ⊥), toENNReal ⊤ = toENNReal ⊥ ↔ Eq (α := EReal) ⊤ ⊥
⊢ toENNReal ⊤ = y.toENNReal ↔ ⊤ = y
have top₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), toENNReal ⊤ = (↑a : EReal).toENNReal ↔ ⊤ = (↑a : EReal)
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊤
top : ∀ (hy : LE.le (α := EReal) 0 ⊥), toENNReal ⊤ = toENNReal ⊥ ↔ Eq (α := EReal) ⊤ ⊥
top₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), toENNReal ⊤ = (↑a : EReal).toENNReal ↔ ⊤ = (↑a : EReal)
⊢ toENNReal ⊤ = y.toENNReal ↔ ⊤ = y
have top₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), toENNReal ⊤ = toENNReal ⊤ ↔ Eq (α := EReal) ⊤ ⊤
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : EReal
h : x ≤ y
⊢ x.toENNReal ≤ y.toENNReal
have bot : ∀ (h : ⊥ ≤ y), toENNReal ⊥ ≤ y.toENNReal
Tactic: induction x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : EReal
h : x ≤ y
bot : ∀ (h : ⊥ ≤ y), toENNReal ⊥ ≤ y.toENNReal
⊢ x.toENNReal ≤ y.toENNReal
have coe : ∀ (a : ℝ) (h : (↑a : EReal) ≤ y), (↑a : EReal).toENNReal ≤ y.toENNReal
Tactic: induction x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : EReal
h : x ≤ y
bot : ∀ (h : ⊥ ≤ y), toENNReal ⊥ ≤ y.toENNReal
coe : ∀ (a : ℝ) (h : (↑a : EReal) ≤ y), (↑a : EReal).toENNReal ≤ y.toENNReal
⊢ x.toENNReal ≤ y.toENNReal
have top : ∀ (h : ⊤ ≤ y), toENNReal ⊤ ≤ y.toENNReal
Tactic: induction x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
a : ℝ
h : (↑a : EReal) ≤ y
⊢ (↑a : EReal).toENNReal ≤ y.toENNReal
have pos : ∀ (hy_top : y = ⊤), (↑a : EReal).toENNReal ≤ y.toENNReal
Tactic: by_cases hy_top : y = ⊤
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
a : ℝ
h : (↑a : EReal) ≤ y
pos : ∀ (hy_top : y = ⊤), (↑a : EReal).toENNReal ≤ y.toENNReal
⊢ (↑a : EReal).toENNReal ≤ y.toENNReal
have neg : ∀ (hy_top : ¬y = ⊤), (↑a : EReal).toENNReal ≤ y.toENNReal
Tactic: by_cases hy_top : y = ⊤
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
a : ℝ
h : (↑a : EReal) ≤ y
hy_top : ¬y = ⊤
⊢ (↑a : EReal).toENNReal ≤ y.toENNReal
have neg : ENNReal.ofReal a ≤ ENNReal.ofReal y.toReal
Tactic: simp only [toENNReal, coe_ne_top, ↓reduceIte, toReal_coe, hy_top]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
⊢ Eq (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m = n
have rw : (↑m : EReal) = (↑(↑n : ℝ) : EReal) ↔ m = n
Tactic: rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_eq_coe_iff, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
rw : (↑m : EReal) = (↑(↑n : ℝ) : EReal) ↔ m = n
⊢ Eq (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m = n
have rw₁ : (↑(↑m : ℝ) : EReal) = (↑(↑n : ℝ) : EReal) ↔ m = n
Tactic: rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_eq_coe_iff, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
rw : (↑m : EReal) = (↑(↑n : ℝ) : EReal) ↔ m = n
rw₁ : (↑(↑m : ℝ) : EReal) = (↑(↑n : ℝ) : EReal) ↔ m = n
⊢ Eq (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m = n
have rw₂ : Eq (α := ℝ) (↑m : ℝ) (↑n : ℝ) ↔ m = n
Tactic: rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_eq_coe_iff, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
rw : (↑m : EReal) = (↑(↑n : ℝ) : EReal) ↔ m = n
rw₁ : (↑(↑m : ℝ) : EReal) = (↑(↑n : ℝ) : EReal) ↔ m = n
rw₂ : Eq (α := ℝ) (↑m : ℝ) (↑n : ℝ) ↔ m = n
⊢ Eq (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m = n
have rw₃ : m = n ↔ m = n
Tactic: rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_eq_coe_iff, Nat.cast_inj]