awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
x : ℝ
inl : ∀ (hx : x < 0), P (↑x : EReal) ⊤
⊢ P (↑x : EReal) ⊤
have inr : P (↑0 : EReal) ⊤
Tactic: rcases lt_trichotomy x 0 with (hx | rfl | hx)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
x : ℝ
inl : ∀ (hx : x < 0), P (↑x : EReal) ⊤
inr : P (↑0 : EReal) ⊤
⊢ P (↑x : EReal) ⊤
have inr₁ : ∀ (hx : 0 < x), P (↑x : EReal) ⊤
Tactic: rcases lt_trichotomy x 0 with (hx | rfl | hx)
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
y : ℝ
⊢ P ⊤ (↑y : EReal)
have inl : ∀ (hy : y < 0), P ⊤ (↑y : EReal)
Tactic: rcases lt_trichotomy y 0 with (hy | rfl | hy)
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
y : ℝ
inl : ∀ (hy : y < 0), P ⊤ (↑y : EReal)
⊢ P ⊤ (↑y : EReal)
have inr : P ⊤ (↑0 : EReal)
Tactic: rcases lt_trichotomy y 0 with (hy | rfl | hy)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
y : ℝ
inl : ∀ (hy : y < 0), P ⊤ (↑y : EReal)
inr : P ⊤ (↑0 : EReal)
⊢ P ⊤ (↑y : EReal)
have inr₁ : ∀ (hy : 0 < y), P ⊤ (↑y : EReal)
Tactic: rcases lt_trichotomy y 0 with (hy | rfl | hy)
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : EReal
⊢ x * y = y * x
have bot : ⊥ * y = y * ⊥
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : EReal
bot : ⊥ * y = y * ⊥
⊢ x * y = y * x
have coe : ∀ (a : ℝ), (↑a : EReal) * y = y * (↑a : EReal)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : EReal
bot : ⊥ * y = y * ⊥
coe : ∀ (a : ℝ), (↑a : EReal) * y = y * (↑a : EReal)
⊢ x * y = y * x
have top : ⊤ * y = y * ⊤
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
⊢ ⊥ * y = y * ⊥
have bot : HMul.hMul (α := EReal) ⊥ ⊥ = HMul.hMul (α := EReal) ⊥ ⊥
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
bot : HMul.hMul (α := EReal) ⊥ ⊥ = HMul.hMul (α := EReal) ⊥ ⊥
⊢ ⊥ * y = y * ⊥
have bot₁ : ∀ (a : ℝ), ⊥ * (↑a : EReal) = (↑a : EReal) * ⊥
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
bot : HMul.hMul (α := EReal) ⊥ ⊥ = HMul.hMul (α := EReal) ⊥ ⊥
bot₁ : ∀ (a : ℝ), ⊥ * (↑a : EReal) = (↑a : EReal) * ⊥
⊢ ⊥ * y = y * ⊥
have bot₂ : HMul.hMul (α := EReal) ⊥ ⊤ = HMul.hMul (α := EReal) ⊤ ⊥
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
a : ℝ
⊢ (↑a : EReal) * y = y * (↑a : EReal)
have coe : (↑a : EReal) * ⊥ = ⊥ * (↑a : EReal)
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
a : ℝ
coe : (↑a : EReal) * ⊥ = ⊥ * (↑a : EReal)
⊢ (↑a : EReal) * y = y * (↑a : EReal)
have coe₁ : ∀ (a_1 : ℝ), (↑a : EReal) * (↑a_1 : EReal) = (↑a_1 : EReal) * (↑a : EReal)
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
a : ℝ
coe : (↑a : EReal) * ⊥ = ⊥ * (↑a : EReal)
coe₁ : ∀ (a_1 : ℝ), (↑a : EReal) * (↑a_1 : EReal) = (↑a_1 : EReal) * (↑a : EReal)
⊢ (↑a : EReal) * y = y * (↑a : EReal)
have coe₂ : (↑a : EReal) * ⊤ = ⊤ * (↑a : EReal)
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
⊢ ⊤ * y = y * ⊤
have top : HMul.hMul (α := EReal) ⊤ ⊥ = HMul.hMul (α := EReal) ⊥ ⊤
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
top : HMul.hMul (α := EReal) ⊤ ⊥ = HMul.hMul (α := EReal) ⊥ ⊤
⊢ ⊤ * y = y * ⊤
have top₁ : ∀ (a : ℝ), ⊤ * (↑a : EReal) = (↑a : EReal) * ⊤
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
top : HMul.hMul (α := EReal) ⊤ ⊥ = HMul.hMul (α := EReal) ⊥ ⊤
top₁ : ∀ (a : ℝ), ⊤ * (↑a : EReal) = (↑a : EReal) * ⊤
⊢ ⊤ * y = y * ⊤
have top₂ : HMul.hMul (α := EReal) ⊤ ⊤ = HMul.hMul (α := EReal) ⊤ ⊤
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
a a_1 : ℝ
⊢ (↑a : EReal) * (↑a_1 : EReal) = (↑a_1 : EReal) * (↑a : EReal)
have coe : (↑(a * a_1) : EReal) = (↑a_1 : EReal) * (↑a : EReal)
Tactic: rw [← coe_mul, ← coe_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
a a_1 : ℝ
coe : (↑(a * a_1) : EReal) = (↑a_1 : EReal) * (↑a : EReal)
⊢ (↑a : EReal) * (↑a_1 : EReal) = (↑a_1 : EReal) * (↑a : EReal)
have coe₁ : (↑(a * a_1) : EReal) = (↑(a_1 * a) : EReal)
Tactic: rw [← coe_mul, ← coe_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
a a_1 : ℝ
coe : (↑(a * a_1) : EReal) = (↑a_1 : EReal) * (↑a : EReal)
coe₁ : (↑(a * a_1) : EReal) = (↑(a_1 * a) : EReal)
⊢ (↑a : EReal) * (↑a_1 : EReal) = (↑a_1 : EReal) * (↑a : EReal)
have coe₂ : (↑(a_1 * a) : EReal) = (↑(a_1 * a) : EReal)
Tactic: rw [← coe_mul, ← coe_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
⊢ x * 1 = x
have rw : 1 * x = x
Tactic: rw [EReal.mul_comm, EReal.one_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
rw : 1 * x = x
⊢ x * 1 = x
have rw₁ : x = x
Tactic: rw [EReal.mul_comm, EReal.one_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
⊢ x * 0 = 0
have rw : 0 * x = 0
Tactic: rw [EReal.mul_comm, EReal.zero_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
rw : 0 * x = 0
⊢ x * 0 = 0
have rw₁ : Eq (α := EReal) 0 0
Tactic: rw [EReal.mul_comm, EReal.zero_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : x ≠ ⊤ ∧ x ≠ ⊥
⊢ ∃ (y : ℝ), (↑y : EReal) = x
have bot : ∀ (hx : Ne (α := EReal) ⊥ ⊤ ∧ Ne (α := EReal) ⊥ ⊥), ∃ (y : ℝ), (↑y : EReal) = ⊥
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : x ≠ ⊤ ∧ x ≠ ⊥
bot : ∀ (hx : Ne (α := EReal) ⊥ ⊤ ∧ Ne (α := EReal) ⊥ ⊥), ∃ (y : ℝ), (↑y : EReal) = ⊥
⊢ ∃ (y : ℝ), (↑y : EReal) = x
have coe : ∀ (a : ℝ) (hx : (↑a : EReal) ≠ ⊤ ∧ (↑a : EReal) ≠ ⊥), ∃ (y : ℝ), (↑y : EReal) = (↑a : EReal)
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : x ≠ ⊤ ∧ x ≠ ⊥
bot : ∀ (hx : Ne (α := EReal) ⊥ ⊤ ∧ Ne (α := EReal) ⊥ ⊥), ∃ (y : ℝ), (↑y : EReal) = ⊥
coe : ∀ (a : ℝ) (hx : (↑a : EReal) ≠ ⊤ ∧ (↑a : EReal) ≠ ⊥), ∃ (y : ℝ), (↑y : EReal) = (↑a : EReal)
⊢ ∃ (y : ℝ), (↑y : EReal) = x
have top : ∀ (hx : Ne (α := EReal) ⊤ ⊤ ∧ Ne (α := EReal) ⊤ ⊥), ∃ (y : ℝ), (↑y : EReal) = ⊤
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
⊢ range Real.toEReal = {⊥, ⊤}ᶜ
have h : ∀ (x : EReal), x ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
⊢ x ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x
have h : ⊥ ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ ⊥
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
h : ⊥ ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ ⊥
⊢ x ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x
have h₁ : ∀ (a : ℝ), (↑a : EReal) ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ (↑a : EReal)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
h : ⊥ ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ ⊥
h₁ : ∀ (a : ℝ), (↑a : EReal) ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ (↑a : EReal)
⊢ x ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x
have h₂ : ⊤ ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ ⊤
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
⊢ range Real.toEReal = Ioo ⊥ ⊤
have h : ∀ (x : EReal), x ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
⊢ x ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) x
have h : ⊥ ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) ⊥
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
h : ⊥ ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) ⊥
⊢ x ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) x
have h₁ : ∀ (a : ℝ), (↑a : EReal) ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) (↑a : EReal)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
h : ⊥ ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) ⊥
h₁ : ∀ (a : ℝ), (↑a : EReal) ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) (↑a : EReal)
⊢ x ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) x
have h₂ : ⊤ ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) ⊤
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
⊢ x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥
have bot : toReal ⊥ = 0 ↔ Eq (α := EReal) ⊥ 0 ∨ Eq (α := EReal) ⊥ ⊤ ∨ Eq (α := EReal) ⊥ ⊥
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
bot : toReal ⊥ = 0 ↔ Eq (α := EReal) ⊥ 0 ∨ Eq (α := EReal) ⊥ ⊤ ∨ Eq (α := EReal) ⊥ ⊥
⊢ x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥
have coe : ∀ (a : ℝ), (↑a : EReal).toReal = 0 ↔ (↑a : EReal) = 0 ∨ (↑a : EReal) = ⊤ ∨ (↑a : EReal) = ⊥
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
bot : toReal ⊥ = 0 ↔ Eq (α := EReal) ⊥ 0 ∨ Eq (α := EReal) ⊥ ⊤ ∨ Eq (α := EReal) ⊥ ⊥
coe : ∀ (a : ℝ), (↑a : EReal).toReal = 0 ↔ (↑a : EReal) = 0 ∨ (↑a : EReal) = ⊤ ∨ (↑a : EReal) = ⊥
⊢ x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥
have top : toReal ⊤ = 0 ↔ Eq (α := EReal) ⊤ 0 ∨ Eq (α := EReal) ⊤ ⊤ ∨ Eq (α := EReal) ⊤ ⊥
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : EReal
hx_top : x ≠ ⊤
hx_bot : x ≠ ⊥
hy_top : y ≠ ⊤
hy_bot : y ≠ ⊥
⊢ x.toReal = y.toReal ↔ x = y
have lift : ∀ (x : ℝ) (hx_top : (↑x : EReal) ≠ ⊤) (hx_bot : (↑x : EReal) ≠ ⊥), (↑x : EReal).toReal = y.toReal ↔ (↑x : EReal) = y
Tactic: lift x to ℝ using ⟨hx_top, hx_bot⟩
Cleared hypotheses: x, hx_top, hx_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
hy_top : y ≠ ⊤
hy_bot : y ≠ ⊥
x : ℝ
hx_top : (↑x : EReal) ≠ ⊤
hx_bot : (↑x : EReal) ≠ ⊥
⊢ (↑x : EReal).toReal = y.toReal ↔ (↑x : EReal) = y
have lift : ∀ (y : ℝ) (hy_top : (↑y : EReal) ≠ ⊤) (hy_bot : (↑y : EReal) ≠ ⊥),
  (↑x : EReal).toReal = (↑y : EReal).toReal ↔ (↑x : EReal) = (↑y : EReal)
Tactic: lift y to ℝ using ⟨hy_top, hy_bot⟩
Cleared hypotheses: y, hy_top, hy_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : 0 ≤ x
⊢ 0 ≤ x.toReal
have bot : ∀ (hx : LE.le (α := EReal) 0 ⊥), 0 ≤ toReal ⊥
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : 0 ≤ x
bot : ∀ (hx : LE.le (α := EReal) 0 ⊥), 0 ≤ toReal ⊥
⊢ 0 ≤ x.toReal
have coe : ∀ (a : ℝ) (hx : 0 ≤ (↑a : EReal)), 0 ≤ (↑a : EReal).toReal
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : 0 ≤ x
bot : ∀ (hx : LE.le (α := EReal) 0 ⊥), 0 ≤ toReal ⊥
coe : ∀ (a : ℝ) (hx : 0 ≤ (↑a : EReal)), 0 ≤ (↑a : EReal).toReal
⊢ 0 ≤ x.toReal
have top : ∀ (hx : LE.le (α := EReal) 0 ⊤), 0 ≤ toReal ⊤
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : x ≤ 0
⊢ x.toReal ≤ 0
have bot : ∀ (hx : LE.le (α := EReal) ⊥ 0), toReal ⊥ ≤ 0
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : x ≤ 0
bot : ∀ (hx : LE.le (α := EReal) ⊥ 0), toReal ⊥ ≤ 0
⊢ x.toReal ≤ 0
have coe : ∀ (a : ℝ) (hx : (↑a : EReal) ≤ 0), (↑a : EReal).toReal ≤ 0
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : x ≤ 0
bot : ∀ (hx : LE.le (α := EReal) ⊥ 0), toReal ⊥ ≤ 0
coe : ∀ (a : ℝ) (hx : (↑a : EReal) ≤ 0), (↑a : EReal).toReal ≤ 0
⊢ x.toReal ≤ 0
have top : ∀ (hx : LE.le (α := EReal) ⊤ 0), toReal ⊤ ≤ 0
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : 0 < x
h'x : x ≠ ⊤
⊢ 0 < x.toReal
have lift : ∀ (x : ℝ) (hx : 0 < (↑x : EReal)) (h'x : (↑x : EReal) ≠ ⊤), 0 < (↑x : EReal).toReal
Tactic: lift x to ℝ using by aesop
Cleared hypotheses: x, hx, h'x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : x < 0
h'x : x ≠ ⊥
⊢ x.toReal < 0
have lift : ∀ (x : ℝ) (hx : (↑x : EReal) < 0) (h'x : (↑x : EReal) ≠ ⊥), (↑x : EReal).toReal < 0
Tactic: lift x to ℝ using by aesop
Cleared hypotheses: x, hx, h'x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
⊢ toReal '' Ioo 0 ⊤ = Ioi 0
have h : ∀ (x : ℝ), x ∈ toReal '' Ioo 0 ⊤ ↔ Membership.mem (γ := Set ℝ) (Ioi 0) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ
⊢ x ∈ toReal '' Ioo 0 ⊤ ↔ Membership.mem (γ := Set ℝ) (Ioi 0) x
have h : x ∈ toReal '' Ioo 0 ⊤ → Membership.mem (γ := Set ℝ) (Ioi 0) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ
h : x ∈ toReal '' Ioo 0 ⊤ → Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ x ∈ toReal '' Ioo 0 ⊤ ↔ Membership.mem (γ := Set ℝ) (Ioi 0) x
have h₁ : Membership.mem (γ := Set ℝ) (Ioi 0) x → x ∈ toReal '' Ioo 0 ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
hy0 : 0 < y
right : y < ⊤
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) y.toReal
have h : ∀ (y : ℝ) (hy0 : 0 < (↑y : EReal)), (↑y : EReal) < ⊤ → Membership.mem (γ := Set ℝ) (Ioi 0) (↑y : EReal).toReal
Tactic: lift y to ℝ using by aesop
Cleared hypotheses: y, hy0, right
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ x ∈ toReal '' Ioo 0 ⊤
have h : Membership.mem (γ := Set EReal) (Ioo 0 ⊤) (↑x : EReal) ∧ (↑x : EReal).toReal = x
Tactic: use (x : EReal)
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
⊢ toReal '' Ioo ⊥ 0 = Iio 0
have h : ∀ (x : ℝ), x ∈ toReal '' Ioo ⊥ 0 ↔ Membership.mem (γ := Set ℝ) (Iio 0) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ
⊢ x ∈ toReal '' Ioo ⊥ 0 ↔ Membership.mem (γ := Set ℝ) (Iio 0) x
have h : x ∈ toReal '' Ioo ⊥ 0 → Membership.mem (γ := Set ℝ) (Iio 0) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ
h : x ∈ toReal '' Ioo ⊥ 0 → Membership.mem (γ := Set ℝ) (Iio 0) x
⊢ x ∈ toReal '' Ioo ⊥ 0 ↔ Membership.mem (γ := Set ℝ) (Iio 0) x
have h₁ : Membership.mem (γ := Set ℝ) (Iio 0) x → x ∈ toReal '' Ioo ⊥ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
left : ⊥ < y
hy0 : y < 0
⊢ Membership.mem (γ := Set ℝ) (Iio 0) y.toReal
have h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → ∀ (hy0 : (↑y : EReal) < 0), Membership.mem (γ := Set ℝ) (Iio 0) (↑y : EReal).toReal
Tactic: lift y to ℝ using by aesop
Cleared hypotheses: y, left, hy0
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Iio 0) x
⊢ x ∈ toReal '' Ioo ⊥ 0
have h : Membership.mem (γ := Set EReal) (Ioo ⊥ 0) (↑x : EReal) ∧ (↑x : EReal).toReal = x
Tactic: use (x : EReal)
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : EReal
h : x ≤ y
hx : x ≠ ⊥
hy : y ≠ ⊤
⊢ x.toReal ≤ y.toReal
have lift : ∀ (x : ℝ) (h : (↑x : EReal) ≤ y) (hx : (↑x : EReal) ≠ ⊥), (↑x : EReal).toReal ≤ y.toReal
Tactic: lift x to ℝ using ⟨ne_top_of_le_ne_top hy h, hx⟩
Cleared hypotheses: x, h, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
y : EReal
hy : y ≠ ⊤
x : ℝ
h : (↑x : EReal) ≤ y
hx : (↑x : EReal) ≠ ⊥
⊢ (↑x : EReal).toReal ≤ y.toReal
have lift : ∀ (y : ℝ) (hy : (↑y : EReal) ≠ ⊤) (h : (↑x : EReal) ≤ (↑y : EReal)), (↑x : EReal).toReal ≤ (↑y : EReal).toReal
Tactic: lift y to ℝ using ⟨hy, ne_bot_of_le_ne_bot hx h⟩
Cleared hypotheses: y, hy, h
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
⊢ (↑x.toReal : EReal) = x
have lift : ∀ (x : ℝ) (hx : (↑x : EReal) ≠ ⊤) (h'x : (↑x : EReal) ≠ ⊥), (↑(↑x : EReal).toReal : EReal) = (↑x : EReal)
Tactic: lift x to ℝ using ⟨hx, h'x⟩
Cleared hypotheses: x, hx, h'x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
h : x ≠ ⊤
⊢ x ≤ (↑x.toReal : EReal)
have pos : ∀ (h' : x = ⊥), x ≤ (↑x.toReal : EReal)
Tactic: by_cases h' : x = ⊥
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
h : x ≠ ⊤
pos : ∀ (h' : x = ⊥), x ≤ (↑x.toReal : EReal)
⊢ x ≤ (↑x.toReal : EReal)
have neg : ∀ (h' : ¬x = ⊥), x ≤ (↑x.toReal : EReal)
Tactic: by_cases h' : x = ⊥
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
h : x ≠ ⊥
⊢ (↑x.toReal : EReal) ≤ x
have pos : ∀ (h' : x = ⊤), (↑x.toReal : EReal) ≤ x
Tactic: by_cases h' : x = ⊤
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
h : x ≠ ⊥
pos : ∀ (h' : x = ⊤), (↑x.toReal : EReal) ≤ x
⊢ (↑x.toReal : EReal) ≤ x
have neg : ∀ (h' : ¬x = ⊤), (↑x.toReal : EReal) ≤ x
Tactic: by_cases h' : x = ⊤
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
⊢ x = ⊤ ↔ ∀ (y : ℝ), (↑y : EReal) < x
have mp : x = ⊤ → ∀ (y : ℝ), (↑y : EReal) < x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
mp : x = ⊤ → ∀ (y : ℝ), (↑y : EReal) < x
⊢ x = ⊤ ↔ ∀ (y : ℝ), (↑y : EReal) < x
have mpr : (∀ (y : ℝ), (↑y : EReal) < x) → x = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
⊢ (∀ (y : ℝ), (↑y : EReal) < x) → x = ⊤
have mpr : x ≠ ⊤ → ∃ (y : ℝ), x ≤ (↑y : EReal)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
⊢ x = ⊥ ↔ ∀ (y : ℝ), x < (↑y : EReal)
have mp : x = ⊥ → ∀ (y : ℝ), x < (↑y : EReal)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
mp : x = ⊥ → ∀ (y : ℝ), x < (↑y : EReal)
⊢ x = ⊥ ↔ ∀ (y : ℝ), x < (↑y : EReal)
have mpr : (∀ (y : ℝ), x < (↑y : EReal)) → x = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x : EReal
⊢ (∀ (y : ℝ), x < (↑y : EReal)) → x = ⊥
have mpr : x ≠ ⊥ → ∃ (y : ℝ), (↑y : EReal) ≤ x
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x z : EReal
h : x < z
⊢ ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z
have obtain : ∀ (a : EReal) (ha₁ : x < a) (ha₂ : a < z), ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z
Tactic: obtain ⟨a, ha₁, ha₂⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x z : EReal
h : x < z
a : EReal
ha₁ : x < a
ha₂ : a < z
⊢ ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z
have bot : ∀ (ha₁ : x < ⊥) (ha₂ : ⊥ < z), ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z
Tactic: induction a with
  | bot => exact (not_lt_bot ha₁).elim
  | coe a₀ => exact ⟨a₀, ha₁, ha₂⟩
  | top => exact (not_top_lt ha₂).elim
Cleared hypotheses: a, ha₁, ha₂
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x z : EReal
h : x < z
a : EReal
ha₁ : x < a
ha₂ : a < z
bot : ∀ (ha₁ : x < ⊥) (ha₂ : ⊥ < z), ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z
⊢ ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z
have coe : ∀ (a₀ : ℝ) (ha₁ : x < (↑a₀ : EReal)) (ha₂ : (↑a₀ : EReal) < z), ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z
Tactic: induction a with
  | bot => exact (not_lt_bot ha₁).elim
  | coe a₀ => exact ⟨a₀, ha₁, ha₂⟩
  | top => exact (not_top_lt ha₂).elim
Cleared hypotheses: a, ha₁, ha₂
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x z : EReal
h : x < z
a : EReal
ha₁ : x < a
ha₂ : a < z
bot : ∀ (ha₁ : x < ⊥) (ha₂ : ⊥ < z), ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z
coe : ∀ (a₀ : ℝ) (ha₁ : x < (↑a₀ : EReal)) (ha₂ : (↑a₀ : EReal) < z), ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z
⊢ ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z
have top : ∀ (ha₁ : x < ⊤) (ha₂ : ⊤ < z), ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z
Tactic: induction a with
  | bot => exact (not_lt_bot ha₁).elim
  | coe a₀ => exact ⟨a₀, ha₁, ha₂⟩
  | top => exact (not_top_lt ha₂).elim
Cleared hypotheses: a, ha₁, ha₂
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : ℝ
⊢ Real.toEReal '' Icc x y = Icc (↑x : EReal) (↑y : EReal)
have refine : WithBot.some '' WithTop.some '' Icc x y = Icc (↑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 '' Icc x y = Icc (↑x : EReal) (↑y : EReal)
have rw : Icc (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) = Icc (↑x : EReal) (↑y : EReal)
Tactic: rw [WithTop.image_coe_Icc, WithBot.image_coe_Icc]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x y : ℝ
⊢ Real.toEReal '' Ico x y = Ico (↑x : EReal) (↑y : EReal)
have refine : WithBot.some '' WithTop.some '' Ico x y = Ico (↑x : EReal) (↑y : EReal)
Tactic: refine (image_comp WithBot.some WithTop.some _).trans ?_