awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.EReal.Basic
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 ⊥ ⊥
⊢ P ⊤ (↑0 : EReal)

Tactic:
top_zero

Premises used: WithBot.some, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
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 : ℝ
hy : 0 < y
⊢ P ⊤ (↑y : EReal)

Tactic:
top_pos y hy
-- Module: Mathlib.Data.EReal.Basic
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 : ℝ
hy : y < 0
⊢ P ⊤ (↑y : EReal)

Tactic:
exacts [top_neg y hy, top_zero, top_pos y hy]
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
symm : ∀ {x y : EReal}, P x y → P y x
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_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_bot : P ⊥ ⊥
⊢ ∀ (x y : EReal), P x y

Tactic:
@induction₂ P top_top top_pos top_zero top_neg top_bot (fun _ h => symm <| top_pos _ h)
    pos_bot (symm top_zero) coe_coe zero_bot (fun _ h => symm <| top_neg _ h) neg_bot (symm top_bot)
    (fun _ h => symm <| pos_bot _ h) (symm zero_bot) (fun _ h => symm <| neg_bot _ h) bot_bot

Premises used: EReal.induction₂
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : EReal
bot : ⊥ * y = y * ⊥
coe : ∀ (a : ℝ), (↑a : EReal) * y = y * (↑a : EReal)
top : ⊤ * y = y * ⊤
⊢ x * y = y * x

Tactic:
induction x
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
bot : HMul.hMul (α := EReal) ⊥ ⊥ = HMul.hMul (α := EReal) ⊥ ⊥
bot₁ : ∀ (a : ℝ), ⊥ * (↑a : EReal) = (↑a : EReal) * ⊥
bot₂ : HMul.hMul (α := EReal) ⊥ ⊤ = HMul.hMul (α := EReal) ⊤ ⊥
⊢ ⊥ * y = y * ⊥

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
a : ℝ
coe : (↑a : EReal) * ⊥ = ⊥ * (↑a : EReal)
coe₁ : ∀ (a_1 : ℝ), (↑a : EReal) * (↑a_1 : EReal) = (↑a_1 : EReal) * (↑a : EReal)
coe₂ : (↑a : EReal) * ⊤ = ⊤ * (↑a : EReal)
⊢ (↑a : EReal) * y = y * (↑a : EReal)

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
top : HMul.hMul (α := EReal) ⊤ ⊥ = HMul.hMul (α := EReal) ⊥ ⊤
top₁ : ∀ (a : ℝ), ⊤ * (↑a : EReal) = (↑a : EReal) * ⊤
top₂ : HMul.hMul (α := EReal) ⊤ ⊤ = HMul.hMul (α := EReal) ⊤ ⊤
⊢ ⊤ * y = y * ⊤

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ HMul.hMul (α := EReal) ⊥ ⊥ = HMul.hMul (α := EReal) ⊥ ⊥

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ HMul.hMul (α := EReal) ⊥ ⊥ = HMul.hMul (α := EReal) ⊥ ⊥

Tactic:
{ rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ HMul.hMul (α := EReal) ⊥ ⊥ = HMul.hMul (α := EReal) ⊥ ⊥

Tactic:
try { rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ ⊥ * (↑a : EReal) = (↑a : EReal) * ⊥

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ ⊥ * (↑a : EReal) = (↑a : EReal) * ⊥

Tactic:
{ rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ ⊥ * (↑a : EReal) = (↑a : EReal) * ⊥

Tactic:
try { rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ HMul.hMul (α := EReal) ⊥ ⊤ = HMul.hMul (α := EReal) ⊤ ⊥

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ HMul.hMul (α := EReal) ⊥ ⊤ = HMul.hMul (α := EReal) ⊤ ⊥

Tactic:
{ rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ HMul.hMul (α := EReal) ⊥ ⊤ = HMul.hMul (α := EReal) ⊤ ⊥

Tactic:
try { rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ (↑a : EReal) * ⊥ = ⊥ * (↑a : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ (↑a : EReal) * ⊥ = ⊥ * (↑a : EReal)

Tactic:
{ rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ (↑a : EReal) * ⊥ = ⊥ * (↑a : EReal)

Tactic:
try { rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ (↑a : EReal) * ⊤ = ⊤ * (↑a : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ (↑a : EReal) * ⊤ = ⊤ * (↑a : EReal)

Tactic:
{ rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ (↑a : EReal) * ⊤ = ⊤ * (↑a : EReal)

Tactic:
try { rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ HMul.hMul (α := EReal) ⊤ ⊥ = HMul.hMul (α := EReal) ⊥ ⊤

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ HMul.hMul (α := EReal) ⊤ ⊥ = HMul.hMul (α := EReal) ⊥ ⊤

Tactic:
{ rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ HMul.hMul (α := EReal) ⊤ ⊥ = HMul.hMul (α := EReal) ⊥ ⊤

Tactic:
try { rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ ⊤ * (↑a : EReal) = (↑a : EReal) * ⊤

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ ⊤ * (↑a : EReal) = (↑a : EReal) * ⊤

Tactic:
{ rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ ⊤ * (↑a : EReal) = (↑a : EReal) * ⊤

Tactic:
try { rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ HMul.hMul (α := EReal) ⊤ ⊤ = HMul.hMul (α := EReal) ⊤ ⊤

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ HMul.hMul (α := EReal) ⊤ ⊤ = HMul.hMul (α := EReal) ⊤ ⊤

Tactic:
{ rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ HMul.hMul (α := EReal) ⊤ ⊤ = HMul.hMul (α := EReal) ⊤ ⊤

Tactic:
try { rfl }
-- Module: Mathlib.Data.EReal.Basic
Goal:
a a_1 : ℝ
coe : (↑(a * a_1) : EReal) = (↑a_1 : EReal) * (↑a : EReal)
coe₁ : (↑(a * a_1) : EReal) = (↑(a_1 * a) : EReal)
coe₂ coe₃ : (↑(a_1 * a) : EReal) = (↑(a_1 * a) : EReal)
⊢ (↑a : EReal) * (↑a_1 : EReal) = (↑a_1 : EReal) * (↑a : EReal)

Tactic:
rw [← coe_mul, ← coe_mul, mul_comm]

Premises used: mul_comm, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
rw : 1 * x = x
rw₁ rw₂ : x = x
⊢ x * 1 = x

Tactic:
rw [EReal.mul_comm, EReal.one_mul]

Premises used: EReal.one_mul, EReal.mul_comm
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
rw : 0 * x = 0
rw₁ rw₂ : Eq (α := EReal) 0 0
⊢ x * 0 = 0

Tactic:
rw [EReal.mul_comm, EReal.zero_mul]

Premises used: EReal.mul_comm, EReal.zero_mul
-- Module: Mathlib.Data.EReal.Basic
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)
top : ∀ (hx : Ne (α := EReal) ⊤ ⊤ ∧ Ne (α := EReal) ⊤ ⊥), ∃ (y : ℝ), (↑y : EReal) = ⊤
⊢ ∃ (y : ℝ), (↑y : EReal) = x

Tactic:
induction x
-- Module: Mathlib.Data.EReal.Basic
Goal:
hx : Ne (α := EReal) ⊥ ⊤ ∧ Ne (α := EReal) ⊥ ⊥
⊢ ∃ (y : ℝ), (↑y : EReal) = ⊥

Tactic:
simp at hx
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
hx : (↑a : EReal) ≠ ⊤ ∧ (↑a : EReal) ≠ ⊥
⊢ ∃ (y : ℝ), (↑y : EReal) = (↑a : EReal)

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
hx : Ne (α := EReal) ⊤ ⊤ ∧ Ne (α := EReal) ⊤ ⊥
⊢ ∃ (y : ℝ), (↑y : EReal) = ⊤

Tactic:
simp at hx
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ toReal ⊤ = 0

Tactic:
rfl

Premises used: EReal.toReal, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ toReal ⊥ = 0

Tactic:
rfl

Premises used: EReal.toReal, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ toReal 0 = 0

Tactic:
rfl

Premises used: EReal.toReal, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ toReal 1 = 1

Tactic:
rfl

Premises used: EReal.toReal, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ (↑x : EReal).toReal = x

Tactic:
rfl

Premises used: EReal.toReal, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ ⊥ < (↑x : EReal)

Tactic:
WithBot.bot_lt_coe _

Premises used: WithBot.bot_lt_coe, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ (↑x : EReal) ≠ ⊥

Tactic:
(bot_lt_coe x).ne'

Premises used: EReal.bot_lt_coe, LT.lt.ne'
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ ⊥ ≠ (↑x : EReal)

Tactic:
(bot_lt_coe x).ne

Premises used: EReal.bot_lt_coe, LT.lt.ne
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ (↑x : EReal) < ⊤

Tactic:
WithBot.coe_lt_coe.2 <| WithTop.coe_lt_top _

Premises used: Iff.mpr, WithBot.some, WithTop.coe_lt_top, WithBot.coe_lt_coe, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ (↑x : EReal) ≠ ⊤

Tactic:
(coe_lt_top x).ne

Premises used: LT.lt.ne, EReal.coe_lt_top
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ ⊤ ≠ (↑x : EReal)

Tactic:
(coe_lt_top x).ne'

Premises used: LT.lt.ne', EReal.coe_lt_top
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ LT.lt (α := EReal) ⊥ 0

Tactic:
bot_lt_coe 0

Premises used: WithBot.some, EReal.bot_lt_coe, OfNat.ofNat, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ Ne (α := EReal) ⊥ 0

Tactic:
(coe_ne_bot 0).symm

Premises used: WithBot.some, EReal.coe_ne_bot, Ne.symm, OfNat.ofNat, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ Ne (α := EReal) 0 ⊥

Tactic:
coe_ne_bot 0

Premises used: WithBot.some, EReal.coe_ne_bot, OfNat.ofNat, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ LT.lt (α := EReal) 0 ⊤

Tactic:
coe_lt_top 0

Premises used: WithBot.some, OfNat.ofNat, Real.toEReal, EReal.coe_lt_top
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ Ne (α := EReal) 0 ⊤

Tactic:
coe_ne_top 0

Premises used: WithBot.some, EReal.coe_ne_top, OfNat.ofNat, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ Ne (α := EReal) ⊤ 0

Tactic:
(coe_ne_top 0).symm

Premises used: WithBot.some, Ne.symm, EReal.coe_ne_top, OfNat.ofNat, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
h : ∀ (x : EReal), x ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x
⊢ range Real.toEReal = {⊥, ⊤}ᶜ

Tactic:
ext x
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
h : ⊥ ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ ⊥
h₁ : ∀ (a : ℝ), (↑a : EReal) ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ (↑a : EReal)
h₂ : ⊤ ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ ⊤
⊢ x ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x

Tactic:
induction x
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ ⊥ ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ ⊥

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ (↑a : EReal) ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ (↑a : EReal)

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ ⊤ ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ ⊤

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
h : ∀ (x : EReal), x ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) x
⊢ range Real.toEReal = Ioo ⊥ ⊤

Tactic:
ext x
-- Module: Mathlib.Data.EReal.Basic
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)
h₂ : ⊤ ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) ⊤
⊢ x ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) x

Tactic:
induction x
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ ⊥ ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) ⊥

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ (↑a : EReal) ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) (↑a : EReal)

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ ⊤ ∈ range Real.toEReal ↔ Membership.mem (γ := Set EReal) (Ioo ⊥ ⊤) ⊤

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ (↑(x + y) : EReal) = (↑x : EReal) + (↑y : EReal)

Tactic:
rfl

Premises used: WithBot.some, WithTop.map₂, WithTop.some, WithBot.map₂, rfl, Real.toEReal, Option.map₂
-- Module: Mathlib.Data.EReal.Basic
Goal:
n : ℕ
x : ℝ
⊢ (↑(n • x) : EReal) = n • (↑x : EReal)

Tactic:
map_nsmul (⟨⟨Real.toEReal, coe_zero⟩, coe_add⟩ : ℝ →+ EReal) _ _

Premises used: WithBot.some, AddMonoidHom.mk, EReal.coe_zero, ZeroHom.mk, EReal.coe_add, map_nsmul, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ (↑x : EReal) = 0 ↔ x = 0

Tactic:
EReal.coe_eq_coe_iff

Premises used: WithBot.some, EReal.coe_eq_coe_iff, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ (↑x : EReal) = 1 ↔ x = 1

Tactic:
EReal.coe_eq_coe_iff

Premises used: WithBot.some, EReal.coe_eq_coe_iff, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ (↑x : EReal) ≠ 0 ↔ x ≠ 0

Tactic:
EReal.coe_ne_coe_iff

Premises used: WithBot.some, EReal.coe_ne_coe_iff, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ (↑x : EReal) ≠ 1 ↔ x ≠ 1

Tactic:
EReal.coe_ne_coe_iff

Premises used: WithBot.some, EReal.coe_ne_coe_iff, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ 0 ≤ (↑x : EReal) ↔ 0 ≤ x

Tactic:
EReal.coe_le_coe_iff

Premises used: EReal.coe_le_coe_iff, WithBot.some, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ (↑x : EReal) ≤ 0 ↔ x ≤ 0

Tactic:
EReal.coe_le_coe_iff

Premises used: EReal.coe_le_coe_iff, WithBot.some, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ 0 < (↑x : EReal) ↔ 0 < x

Tactic:
EReal.coe_lt_coe_iff

Premises used: WithBot.some, Real.toEReal, EReal.coe_lt_coe_iff
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ (↑x : EReal) < 0 ↔ x < 0

Tactic:
EReal.coe_lt_coe_iff

Premises used: WithBot.some, Real.toEReal, EReal.coe_lt_coe_iff
-- Module: Mathlib.Data.EReal.Basic
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) = ⊥
top : toReal ⊤ = 0 ↔ Eq (α := EReal) ⊤ 0 ∨ Eq (α := EReal) ⊤ ⊤ ∨ Eq (α := EReal) ⊤ ⊥
⊢ x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥

Tactic:
cases x
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ toReal ⊥ = 0 ↔ Eq (α := EReal) ⊥ 0 ∨ Eq (α := EReal) ⊥ ⊤ ∨ Eq (α := EReal) ⊥ ⊥

Tactic:
norm_num
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
⊢ (↑a : EReal).toReal = 0 ↔ (↑a : EReal) = 0 ∨ (↑a : EReal) = ⊤ ∨ (↑a : EReal) = ⊥

Tactic:
norm_num
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ toReal ⊤ = 0 ↔ Eq (α := EReal) ⊤ 0 ∨ Eq (α := EReal) ⊤ ⊤ ∨ Eq (α := EReal) ⊤ ⊥

Tactic:
norm_num
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
⊢ x.toReal ≠ 0 ↔ x ≠ 0 ∧ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
simp only [ne_eq, toReal_eq_zero_iff, not_or]

Premises used: ne_eq, not_or, EReal.toReal_eq_zero_iff
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : EReal
hx_top : x ≠ ⊤
hx_bot : x ≠ ⊥
hy_top : y ≠ ⊤
hy_bot : y ≠ ⊥
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
⟨hx_top, hx_bot⟩

Premises used: And.intro
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : EReal
hx_top : x ≠ ⊤
hx_bot : x ≠ ⊥
hy_top : y ≠ ⊤
hy_bot : y ≠ ⊥
lift :
  ∀ (x : ℝ) (hx_top : (↑x : EReal) ≠ ⊤) (hx_bot : (↑x : EReal) ≠ ⊥), (↑x : EReal).toReal = y.toReal ↔ (↑x : EReal) = y
⊢ x.toReal = y.toReal ↔ x = y

Tactic:
lift x to ℝ using ⟨hx_top, hx_bot⟩
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
hy_top : y ≠ ⊤
hy_bot : y ≠ ⊥
x : ℝ
hx_top : (↑x : EReal) ≠ ⊤
hx_bot : (↑x : EReal) ≠ ⊥
⊢ y ≠ ⊤ ∧ y ≠ ⊥

Tactic:
⟨hy_top, hy_bot⟩

Premises used: And.intro
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
hy_top : y ≠ ⊤
hy_bot : y ≠ ⊥
x : ℝ
hx_top : (↑x : EReal) ≠ ⊤
hx_bot : (↑x : EReal) ≠ ⊥
lift :
  ∀ (y : ℝ) (hy_top : (↑y : EReal) ≠ ⊤) (hy_bot : (↑y : EReal) ≠ ⊥),
    (↑x : EReal).toReal = (↑y : EReal).toReal ↔ (↑x : EReal) = (↑y : EReal)
⊢ (↑x : EReal).toReal = y.toReal ↔ (↑x : EReal) = y

Tactic:
lift y to ℝ using ⟨hy_top, hy_bot⟩
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
hx_top : (↑x : EReal) ≠ ⊤
hx_bot : (↑x : EReal) ≠ ⊥
y : ℝ
hy_top : (↑y : EReal) ≠ ⊤
hy_bot : (↑y : EReal) ≠ ⊥
⊢ (↑x : EReal).toReal = (↑y : EReal).toReal ↔ (↑x : EReal) = (↑y : EReal)

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : 0 ≤ x
bot : ∀ (hx : LE.le (α := EReal) 0 ⊥), 0 ≤ toReal ⊥
coe : ∀ (a : ℝ) (hx : 0 ≤ (↑a : EReal)), 0 ≤ (↑a : EReal).toReal
top : ∀ (hx : LE.le (α := EReal) 0 ⊤), 0 ≤ toReal ⊤
⊢ 0 ≤ x.toReal

Tactic:
cases x
-- Module: Mathlib.Data.EReal.Basic
Goal:
hx : LE.le (α := EReal) 0 ⊥
⊢ 0 ≤ toReal ⊥

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
⊢ 0 ≤ (↑a : EReal).toReal

Tactic:
toReal_coe _ ▸ EReal.coe_nonneg.mp hx

Premises used: Eq.rec, EReal.coe_nonneg, EReal.toReal_coe, Iff.mp, Eq.symm
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
⊢ 0 ≤ (↑a : EReal).toReal

Tactic:
exact toReal_coe _ ▸ EReal.coe_nonneg.mp hx
-- Module: Mathlib.Data.EReal.Basic
Goal:
hx : LE.le (α := EReal) 0 ⊤
⊢ 0 ≤ toReal ⊤

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : x ≤ 0
bot : ∀ (hx : LE.le (α := EReal) ⊥ 0), toReal ⊥ ≤ 0
coe : ∀ (a : ℝ) (hx : (↑a : EReal) ≤ 0), (↑a : EReal).toReal ≤ 0
top : ∀ (hx : LE.le (α := EReal) ⊤ 0), toReal ⊤ ≤ 0
⊢ x.toReal ≤ 0

Tactic:
cases x
-- Module: Mathlib.Data.EReal.Basic
Goal:
hx : LE.le (α := EReal) ⊥ 0
⊢ toReal ⊥ ≤ 0

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
hx : (↑a : EReal) ≤ 0
⊢ (↑a : EReal).toReal ≤ 0

Tactic:
toReal_coe _ ▸ EReal.coe_nonpos.mp hx

Premises used: EReal.coe_nonpos, Eq.rec, EReal.toReal_coe, Iff.mp, Eq.symm
-- Module: Mathlib.Data.EReal.Basic
Goal:
a : ℝ
hx : (↑a : EReal) ≤ 0
⊢ (↑a : EReal).toReal ≤ 0

Tactic:
exact toReal_coe _ ▸ EReal.coe_nonpos.mp hx
-- Module: Mathlib.Data.EReal.Basic
Goal:
hx : LE.le (α := EReal) ⊤ 0
⊢ toReal ⊤ ≤ 0

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : 0 < x
h'x : x ≠ ⊤
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
aesop
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : 0 < x
h'x : x ≠ ⊤
lift : ∀ (x : ℝ) (hx : 0 < (↑x : EReal)) (h'x : (↑x : EReal) ≠ ⊤), 0 < (↑x : EReal).toReal
⊢ 0 < x.toReal

Tactic:
lift x to ℝ using by aesop
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
hx : 0 < (↑x : EReal)
h'x : (↑x : EReal) ≠ ⊤
⊢ 0 < (↑x : EReal).toReal

Tactic:
simpa using hx
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : x < 0
h'x : x ≠ ⊥
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
aesop
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : x < 0
h'x : x ≠ ⊥
lift : ∀ (x : ℝ) (hx : (↑x : EReal) < 0) (h'x : (↑x : EReal) ≠ ⊥), (↑x : EReal).toReal < 0
⊢ x.toReal < 0

Tactic:
lift x to ℝ using by aesop
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
hx : (↑x : EReal) < 0
h'x : (↑x : EReal) ≠ ⊥
⊢ (↑x : EReal).toReal < 0

Tactic:
simpa using hx
-- Module: Mathlib.Data.EReal.Basic
Goal:
h : ∀ (x : ℝ), x ∈ toReal '' Ioo 0 ⊤ ↔ Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ toReal '' Ioo 0 ⊤ = Ioi 0

Tactic:
ext x
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
h : x ∈ toReal '' Ioo 0 ⊤ → Membership.mem (γ := Set ℝ) (Ioi 0) x
h₁ : Membership.mem (γ := Set ℝ) (Ioi 0) x → x ∈ toReal '' Ioo 0 ⊤
⊢ x ∈ toReal '' Ioo 0 ⊤ ↔ Membership.mem (γ := Set ℝ) (Ioi 0) x

Tactic:
constructor
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
hy0 : 0 < y
right : y < ⊤
⊢ y ≠ ⊤ ∧ y ≠ ⊥

Tactic:
aesop
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
hy0 : 0 < y
right : y < ⊤
h : ∀ (y : ℝ) (hy0 : 0 < (↑y : EReal)), (↑y : EReal) < ⊤ → Membership.mem (γ := Set ℝ) (Ioi 0) (↑y : EReal).toReal
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) y.toReal

Tactic:
lift y to ℝ using by aesop
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : ℝ
hy0 : 0 < (↑y : EReal)
right : (↑y : EReal) < ⊤
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) (↑y : EReal).toReal

Tactic:
simpa using hy0
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
h : Membership.mem (γ := Set EReal) (Ioo 0 ⊤) (↑x : EReal) ∧ (↑x : EReal).toReal = x
⊢ x ∈ toReal '' Ioo 0 ⊤

Tactic:
use (x : EReal)

Premises used: Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ Membership.mem (γ := Set EReal) (Ioo 0 ⊤) (↑x : EReal) ∧ (↑x : EReal).toReal = x

Tactic:
simpa using hx
-- Module: Mathlib.Data.EReal.Basic
Goal:
h : ∀ (x : ℝ), x ∈ toReal '' Ioo ⊥ 0 ↔ Membership.mem (γ := Set ℝ) (Iio 0) x
⊢ toReal '' Ioo ⊥ 0 = Iio 0

Tactic:
ext x
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
h : x ∈ toReal '' Ioo ⊥ 0 → Membership.mem (γ := Set ℝ) (Iio 0) x
h₁ : Membership.mem (γ := Set ℝ) (Iio 0) x → x ∈ toReal '' Ioo ⊥ 0
⊢ x ∈ toReal '' Ioo ⊥ 0 ↔ Membership.mem (γ := Set ℝ) (Iio 0) x

Tactic:
constructor
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
left : ⊥ < y
hy0 : y < 0
⊢ y ≠ ⊤ ∧ y ≠ ⊥

Tactic:
aesop
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
left : ⊥ < y
hy0 : y < 0
h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → ∀ (hy0 : (↑y : EReal) < 0), Membership.mem (γ := Set ℝ) (Iio 0) (↑y : EReal).toReal
⊢ Membership.mem (γ := Set ℝ) (Iio 0) y.toReal

Tactic:
lift y to ℝ using by aesop
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : ℝ
left : ⊥ < (↑y : EReal)
hy0 : (↑y : EReal) < 0
⊢ Membership.mem (γ := Set ℝ) (Iio 0) (↑y : EReal).toReal

Tactic:
simpa using hy0
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Iio 0) x
h : Membership.mem (γ := Set EReal) (Ioo ⊥ 0) (↑x : EReal) ∧ (↑x : EReal).toReal = x
⊢ x ∈ toReal '' Ioo ⊥ 0

Tactic:
use (x : EReal)

Premises used: Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Iio 0) x
⊢ Membership.mem (γ := Set EReal) (Ioo ⊥ 0) (↑x : EReal) ∧ (↑x : EReal).toReal = x

Tactic:
simpa using hx
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : EReal
h : x ≤ y
hx : x ≠ ⊥
hy : y ≠ ⊤
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
⟨ne_top_of_le_ne_top hy h, hx⟩

Premises used: ne_top_of_le_ne_top, And.intro
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : EReal
h : x ≤ y
hx : x ≠ ⊥
hy : y ≠ ⊤
lift : ∀ (x : ℝ) (h : (↑x : EReal) ≤ y) (hx : (↑x : EReal) ≠ ⊥), (↑x : EReal).toReal ≤ y.toReal
⊢ x.toReal ≤ y.toReal

Tactic:
lift x to ℝ using ⟨ne_top_of_le_ne_top hy h, hx⟩
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
hy : y ≠ ⊤
x : ℝ
h : (↑x : EReal) ≤ y
hx : (↑x : EReal) ≠ ⊥
⊢ y ≠ ⊤ ∧ y ≠ ⊥

Tactic:
⟨hy, ne_bot_of_le_ne_bot hx h⟩

Premises used: ne_bot_of_le_ne_bot, And.intro
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : EReal
hy : y ≠ ⊤
x : ℝ
h : (↑x : EReal) ≤ y
hx : (↑x : EReal) ≠ ⊥
lift : ∀ (y : ℝ) (hy : (↑y : EReal) ≠ ⊤) (h : (↑x : EReal) ≤ (↑y : EReal)), (↑x : EReal).toReal ≤ (↑y : EReal).toReal
⊢ (↑x : EReal).toReal ≤ y.toReal

Tactic:
lift y to ℝ using ⟨hy, ne_bot_of_le_ne_bot hx h⟩
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
hx : (↑x : EReal) ≠ ⊥
y : ℝ
hy : (↑y : EReal) ≠ ⊤
h : (↑x : EReal) ≤ (↑y : EReal)
⊢ (↑x : EReal).toReal ≤ (↑y : EReal).toReal

Tactic:
simpa using h
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
⟨hx, h'x⟩

Premises used: And.intro
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
lift : ∀ (x : ℝ) (hx : (↑x : EReal) ≠ ⊤) (h'x : (↑x : EReal) ≠ ⊥), (↑(↑x : EReal).toReal : EReal) = (↑x : EReal)
⊢ (↑x.toReal : EReal) = x

Tactic:
lift x to ℝ using ⟨hx, h'x⟩
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
hx : (↑x : EReal) ≠ ⊤
h'x : (↑x : EReal) ≠ ⊥
⊢ (↑(↑x : EReal).toReal : EReal) = (↑x : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
h : x ≠ ⊤
pos : ∀ (h' : x = ⊥), x ≤ (↑x.toReal : EReal)
neg : ∀ (h' : ¬x = ⊥), x ≤ (↑x.toReal : EReal)
⊢ x ≤ (↑x.toReal : EReal)

Tactic:
by_cases h' : x = ⊥
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
h : x ≠ ⊤
h' : x = ⊥
⊢ x ≤ (↑x.toReal : EReal)

Tactic:
simp only [h', bot_le]

Premises used: bot_le
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
h : x ≠ ⊤
h' : ¬x = ⊥
⊢ x ≤ (↑x.toReal : EReal)

Tactic:
simp only [le_refl, coe_toReal h h']

Premises used: le_refl, EReal.coe_toReal