awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
h : x ≠ ⊥
pos : ∀ (h' : x = ⊤), (↑x.toReal : EReal) ≤ x
neg : ∀ (h' : ¬x = ⊤), (↑x.toReal : EReal) ≤ x
⊢ (↑x.toReal : EReal) ≤ x

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

Tactic:
simp only [h', le_top]

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

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

Premises used: le_refl, EReal.coe_toReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
mp : x = ⊤ → ∀ (y : ℝ), (↑y : EReal) < x
mpr : (∀ (y : ℝ), (↑y : EReal) < x) → x = ⊤
⊢ x = ⊤ ↔ ∀ (y : ℝ), (↑y : EReal) < x

Tactic:
constructor
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ ∀ (y : ℝ), (↑y : EReal) < ⊤

Tactic:
EReal.coe_lt_top

Premises used: EReal.coe_lt_top
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ ∀ (y : ℝ), (↑y : EReal) < ⊤

Tactic:
exact EReal.coe_lt_top

Premises used: EReal.coe_lt_top
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
mpr : x ≠ ⊤ → ∃ (y : ℝ), x ≤ (↑y : EReal)
⊢ (∀ (y : ℝ), (↑y : EReal) < x) → x = ⊤

Tactic:
contrapose!
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
h : x ≠ ⊤
⊢ ∃ (y : ℝ), x ≤ (↑y : EReal)

Tactic:
⟨x.toReal, le_coe_toReal h⟩

Premises used: EReal.le_coe_toReal, EReal.toReal, Exists.intro
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
h : x ≠ ⊤
⊢ ∃ (y : ℝ), x ≤ (↑y : EReal)

Tactic:
exact ⟨x.toReal, le_coe_toReal h⟩
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
mp : x = ⊥ → ∀ (y : ℝ), x < (↑y : EReal)
mpr : (∀ (y : ℝ), x < (↑y : EReal)) → x = ⊥
⊢ x = ⊥ ↔ ∀ (y : ℝ), x < (↑y : EReal)

Tactic:
constructor
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ ∀ (y : ℝ), ⊥ < (↑y : EReal)

Tactic:
bot_lt_coe

Premises used: EReal.bot_lt_coe
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ ∀ (y : ℝ), ⊥ < (↑y : EReal)

Tactic:
exact bot_lt_coe

Premises used: EReal.bot_lt_coe
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
mpr : x ≠ ⊥ → ∃ (y : ℝ), (↑y : EReal) ≤ x
⊢ (∀ (y : ℝ), x < (↑y : EReal)) → x = ⊥

Tactic:
contrapose!
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
h : x ≠ ⊥
⊢ ∃ (y : ℝ), (↑y : EReal) ≤ x

Tactic:
⟨x.toReal, coe_toReal_le h⟩

Premises used: EReal.toReal, Exists.intro, EReal.coe_toReal_le
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : EReal
h : x ≠ ⊥
⊢ ∃ (y : ℝ), (↑y : EReal) ≤ x

Tactic:
exact ⟨x.toReal, coe_toReal_le h⟩
-- Module: Mathlib.Data.EReal.Basic
Goal:
x z : EReal
h : x < z
obtain : ∀ (a : EReal) (ha₁ : x < a) (ha₂ : a < z), ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z
⊢ ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z

Tactic:
obtain ⟨a, ha₁, ha₂⟩ := exists_between h

Premises used: exists_between
-- Module: Mathlib.Data.EReal.Basic
Goal:
x z : EReal
h : x < z
ha₁ : x < ⊥
ha₂ : ⊥ < z
⊢ ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z

Tactic:
(not_lt_bot ha₁).elim

Premises used: False.elim, not_lt_bot
-- Module: Mathlib.Data.EReal.Basic
Goal:
x z : EReal
h : x < z
ha₁ : x < ⊥
ha₂ : ⊥ < z
⊢ ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z

Tactic:
exact (not_lt_bot ha₁).elim

Premises used: False.elim, not_lt_bot
-- Module: Mathlib.Data.EReal.Basic
Goal:
x z : EReal
h : x < z
a₀ : ℝ
ha₁ : x < (↑a₀ : EReal)
ha₂ : (↑a₀ : EReal) < z
⊢ ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z

Tactic:
⟨a₀, ha₁, ha₂⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.EReal.Basic
Goal:
x z : EReal
h : x < z
a₀ : ℝ
ha₁ : x < (↑a₀ : EReal)
ha₂ : (↑a₀ : EReal) < z
⊢ ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z

Tactic:
exact ⟨a₀, ha₁, ha₂⟩
-- Module: Mathlib.Data.EReal.Basic
Goal:
x z : EReal
h : x < z
ha₁ : x < ⊤
ha₂ : ⊤ < z
⊢ ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z

Tactic:
(not_top_lt ha₂).elim

Premises used: False.elim, not_top_lt
-- Module: Mathlib.Data.EReal.Basic
Goal:
x z : EReal
h : x < z
ha₁ : x < ⊤
ha₂ : ⊤ < z
⊢ ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : EReal) < z

Tactic:
exact (not_top_lt ha₂).elim

Premises used: False.elim, not_top_lt
-- Module: Mathlib.Data.EReal.Basic
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
top : ∀ (ha₁ : x < ⊤) (ha₂ : ⊤ < z), ∃ (y : ℝ), x < (↑y : EReal) ∧ (↑y : 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

Premises used: False.elim, not_top_lt, not_lt_bot
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ Real.toEReal '' Icc x y = Icc (↑x : EReal) (↑y : EReal)

Tactic:
(image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, EReal, WithTop.some, Set.image_comp, Eq.trans, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
refine : WithBot.some '' WithTop.some '' Icc x y = Icc (↑x : EReal) (↑y : EReal)
⊢ Real.toEReal '' Icc x y = Icc (↑x : EReal) (↑y : EReal)

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, WithTop.some, Set.image_comp, Eq.trans
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
rw :
  Icc (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) =
    Icc (↑x : EReal) (↑y : EReal)
⊢ WithBot.some '' WithTop.some '' Icc x y = Icc (↑x : EReal) (↑y : EReal)

Tactic:
rw [WithTop.image_coe_Icc, WithBot.image_coe_Icc]

Premises used: WithTop.image_coe_Icc, WithBot.image_coe_Icc
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ Icc (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) =
    Icc (↑x : EReal) (↑y : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ Real.toEReal '' Ico x y = Ico (↑x : EReal) (↑y : EReal)

Tactic:
(image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, EReal, WithTop.some, Set.image_comp, Eq.trans, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
refine : WithBot.some '' WithTop.some '' Ico x y = Ico (↑x : EReal) (↑y : EReal)
⊢ Real.toEReal '' Ico x y = Ico (↑x : EReal) (↑y : EReal)

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, WithTop.some, Set.image_comp, Eq.trans
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
rw :
  Ico (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) =
    Ico (↑x : EReal) (↑y : EReal)
⊢ WithBot.some '' WithTop.some '' Ico x y = Ico (↑x : EReal) (↑y : EReal)

Tactic:
rw [WithTop.image_coe_Ico, WithBot.image_coe_Ico]

Premises used: WithTop.image_coe_Ico, WithBot.image_coe_Ico
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ Ico (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) =
    Ico (↑x : EReal) (↑y : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ Real.toEReal '' Ici x = Ico (↑x : EReal) ⊤

Tactic:
(image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, EReal, WithTop.some, Set.image_comp, Eq.trans, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
refine : WithBot.some '' WithTop.some '' Ici x = Ico (↑x : EReal) ⊤
⊢ Real.toEReal '' Ici x = Ico (↑x : EReal) ⊤

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, WithTop.some, Set.image_comp, Eq.trans
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
rw : Ico (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑⊤ : WithBot (WithTop ℝ)) = Ico (↑x : EReal) ⊤
⊢ WithBot.some '' WithTop.some '' Ici x = Ico (↑x : EReal) ⊤

Tactic:
rw [WithTop.image_coe_Ici, WithBot.image_coe_Ico]

Premises used: WithBot.image_coe_Ico, WithTop.image_coe_Ici
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ Ico (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑⊤ : WithBot (WithTop ℝ)) = Ico (↑x : EReal) ⊤

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ Real.toEReal '' Ioc x y = Ioc (↑x : EReal) (↑y : EReal)

Tactic:
(image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, EReal, WithTop.some, Set.image_comp, Eq.trans, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
refine : WithBot.some '' WithTop.some '' Ioc x y = Ioc (↑x : EReal) (↑y : EReal)
⊢ Real.toEReal '' Ioc x y = Ioc (↑x : EReal) (↑y : EReal)

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, WithTop.some, Set.image_comp, Eq.trans
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
rw :
  Ioc (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) =
    Ioc (↑x : EReal) (↑y : EReal)
⊢ WithBot.some '' WithTop.some '' Ioc x y = Ioc (↑x : EReal) (↑y : EReal)

Tactic:
rw [WithTop.image_coe_Ioc, WithBot.image_coe_Ioc]

Premises used: WithTop.image_coe_Ioc, WithBot.image_coe_Ioc
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ Ioc (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) =
    Ioc (↑x : EReal) (↑y : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ Real.toEReal '' Ioo x y = Ioo (↑x : EReal) (↑y : EReal)

Tactic:
(image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, EReal, WithTop.some, Set.image_comp, Eq.trans, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
refine : WithBot.some '' WithTop.some '' Ioo x y = Ioo (↑x : EReal) (↑y : EReal)
⊢ Real.toEReal '' Ioo x y = Ioo (↑x : EReal) (↑y : EReal)

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, WithTop.some, Set.image_comp, Eq.trans
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
rw :
  Ioo (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) =
    Ioo (↑x : EReal) (↑y : EReal)
⊢ WithBot.some '' WithTop.some '' Ioo x y = Ioo (↑x : EReal) (↑y : EReal)

Tactic:
rw [WithTop.image_coe_Ioo, WithBot.image_coe_Ioo]

Premises used: WithBot.image_coe_Ioo, WithTop.image_coe_Ioo
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ Ioo (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) =
    Ioo (↑x : EReal) (↑y : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ Real.toEReal '' Ioi x = Ioo (↑x : EReal) ⊤

Tactic:
(image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, EReal, WithTop.some, Set.image_comp, Eq.trans, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
refine : WithBot.some '' WithTop.some '' Ioi x = Ioo (↑x : EReal) ⊤
⊢ Real.toEReal '' Ioi x = Ioo (↑x : EReal) ⊤

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, WithTop.some, Set.image_comp, Eq.trans
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
rw : Ioo (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑⊤ : WithBot (WithTop ℝ)) = Ioo (↑x : EReal) ⊤
⊢ WithBot.some '' WithTop.some '' Ioi x = Ioo (↑x : EReal) ⊤

Tactic:
rw [WithTop.image_coe_Ioi, WithBot.image_coe_Ioo]

Premises used: WithBot.image_coe_Ioo, WithTop.image_coe_Ioi
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ Ioo (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) (↑⊤ : WithBot (WithTop ℝ)) = Ioo (↑x : EReal) ⊤

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ Real.toEReal '' Iic x = Ioc ⊥ (↑x : EReal)

Tactic:
(image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, EReal, WithTop.some, Set.image_comp, Eq.trans, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
refine : WithBot.some '' WithTop.some '' Iic x = Ioc ⊥ (↑x : EReal)
⊢ Real.toEReal '' Iic x = Ioc ⊥ (↑x : EReal)

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, WithTop.some, Set.image_comp, Eq.trans
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
rw : Ioc ⊥ (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) = Ioc ⊥ (↑x : EReal)
⊢ WithBot.some '' WithTop.some '' Iic x = Ioc ⊥ (↑x : EReal)

Tactic:
rw [WithTop.image_coe_Iic, WithBot.image_coe_Iic]

Premises used: WithTop.image_coe_Iic, WithBot.image_coe_Iic
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ Ioc ⊥ (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) = Ioc ⊥ (↑x : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ Real.toEReal '' Iio x = Ioo ⊥ (↑x : EReal)

Tactic:
(image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, EReal, WithTop.some, Set.image_comp, Eq.trans, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
refine : WithBot.some '' WithTop.some '' Iio x = Ioo ⊥ (↑x : EReal)
⊢ Real.toEReal '' Iio x = Ioo ⊥ (↑x : EReal)

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Premises used: WithBot.some, WithTop.some, Set.image_comp, Eq.trans
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
rw : Ioo ⊥ (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) = Ioo ⊥ (↑x : EReal)
⊢ WithBot.some '' WithTop.some '' Iio x = Ioo ⊥ (↑x : EReal)

Tactic:
rw [WithTop.image_coe_Iio, WithBot.image_coe_Iio]

Premises used: WithBot.image_coe_Iio, WithTop.image_coe_Iio
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ Ioo ⊥ (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) = Ioo ⊥ (↑x : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ WithBot.some ∘ WithTop.some ⁻¹' Ici (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) = Ici x

Tactic:
preimage_comp.trans ?_

Premises used: Set.preimage_comp, Eq.trans
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ WithTop.some ⁻¹' WithBot.some ⁻¹' Ici (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) = Ici x

Tactic:
simp only [WithBot.preimage_coe_Ici, WithTop.preimage_coe_Ici]

Premises used: WithTop.preimage_coe_Ici, WithBot.preimage_coe_Ici
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ WithBot.some ∘ WithTop.some ⁻¹' Ioi (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) = Ioi x

Tactic:
preimage_comp.trans ?_

Premises used: Set.preimage_comp, Eq.trans
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ WithTop.some ⁻¹' WithBot.some ⁻¹' Ioi (↑(↑x : WithTop ℝ) : WithBot (WithTop ℝ)) = Ioi x

Tactic:
simp only [WithBot.preimage_coe_Ioi, WithTop.preimage_coe_Ioi]

Premises used: WithBot.preimage_coe_Ioi, WithTop.preimage_coe_Ioi
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ Eq (α := Set ℝ) (WithBot.some ∘ WithTop.some ⁻¹' Ioi ⊥) univ

Tactic:
preimage_comp.trans ?_

Premises used: Set.preimage_comp, Eq.trans
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ Eq (α := Set ℝ) (WithTop.some ⁻¹' WithBot.some ⁻¹' Ioi ⊥) univ

Tactic:
simp only [WithBot.preimage_coe_Ioi_bot, preimage_univ]

Premises used: Set.preimage_univ, WithBot.preimage_coe_Ioi_bot
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : ℝ
⊢ WithBot.some ∘ WithTop.some ⁻¹' Iic (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) = Iic y

Tactic:
preimage_comp.trans ?_

Premises used: Set.preimage_comp, Eq.trans
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : ℝ
⊢ WithTop.some ⁻¹' WithBot.some ⁻¹' Iic (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) = Iic y

Tactic:
simp only [WithBot.preimage_coe_Iic, WithTop.preimage_coe_Iic]

Premises used: WithTop.preimage_coe_Iic, WithBot.preimage_coe_Iic
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : ℝ
⊢ WithBot.some ∘ WithTop.some ⁻¹' Iio (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) = Iio y

Tactic:
preimage_comp.trans ?_

Premises used: Set.preimage_comp, Eq.trans
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : ℝ
⊢ WithTop.some ⁻¹' WithBot.some ⁻¹' Iio (↑(↑y : WithTop ℝ) : WithBot (WithTop ℝ)) = Iio y

Tactic:
simp only [WithBot.preimage_coe_Iio, WithTop.preimage_coe_Iio]

Premises used: WithTop.preimage_coe_Iio, WithBot.preimage_coe_Iio
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ Eq (α := Set ℝ) (WithBot.some ∘ WithTop.some ⁻¹' Iio (↑⊤ : WithBot (WithTop ℝ))) univ

Tactic:
preimage_comp.trans ?_

Premises used: Set.preimage_comp, Eq.trans
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ Eq (α := Set ℝ) (WithTop.some ⁻¹' WithBot.some ⁻¹' Iio (↑⊤ : WithBot (WithTop ℝ))) univ

Tactic:
simp only [WithBot.preimage_coe_Iio, WithTop.preimage_coe_Iio_top]

Premises used: WithTop.preimage_coe_Iio_top, WithBot.preimage_coe_Iio
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ Real.toEReal ⁻¹' (Ici (↑x : EReal) ∩ Iic (↑y : EReal)) = Ici x ∩ Iic y

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ Real.toEReal ⁻¹' (Ici (↑x : EReal) ∩ Iio (↑y : EReal)) = Ici x ∩ Iio y

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi (↑x : EReal) ∩ Iic (↑y : EReal)) = Ioi x ∩ Iic y

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi (↑x : EReal) ∩ Iio (↑y : EReal)) = Ioi x ∩ Iio y

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ Real.toEReal ⁻¹' (Ici (↑x : EReal) ∩ Iio ⊤) = Ici x

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ Real.toEReal ⁻¹' (Ioi (↑x : EReal) ∩ Iio ⊤) = Ioi x

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iic (↑y : EReal)) = Iic y

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iio (↑y : EReal)) = Iio y

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iio ⊤) = univ

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ
⊢ (↑(ENNReal.ofReal x) : EReal) = (↑(max x 0) : EReal)

Tactic:
rfl

Premises used: ENNReal.toEReal, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
hx : x ≠ ∞
⊢ x ≠ ∞

Tactic:
hx
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
hx : x ≠ ∞
lift : ∀ (x : ℝ≥0), (↑(↑x : ℝ≥0∞).toReal : EReal) = (↑(↑x : ℝ≥0∞) : EReal)
⊢ (↑x.toReal : EReal) = (↑x : EReal)

Tactic:
lift x to ℝ≥0 using hx
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0
⊢ (↑(↑x : ℝ≥0∞).toReal : EReal) = (↑(↑x : ℝ≥0∞) : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0
⊢ (↑(↑x : ℝ≥0∞) : EReal) = (↑(↑x : ℝ) : EReal)

Tactic:
rfl

Premises used: ENNReal.toEReal, NNReal.toReal, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ (↑0 : EReal) = 0

Tactic:
rfl

Premises used: WithBot.some, ENNReal.toEReal, rfl, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ (↑1 : EReal) = 1

Tactic:
rfl

Premises used: WithBot.some, ENNReal.toEReal, rfl, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ (↑∞ : EReal) = ⊤

Tactic:
rfl

Premises used: ENNReal.toEReal, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ StrictMono toEReal

Tactic:
WithTop.strictMono_iff.2 ⟨fun _ _ => EReal.coe_lt_coe_iff.2, fun _ => coe_lt_top _⟩

Premises used: Iff.mpr, And.intro, ENNReal, WithTop.strictMono_iff, Subtype.val, EReal.coe_lt_coe_iff, EReal.coe_lt_top
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ Injective toEReal

Tactic:
coe_ennreal_strictMono.injective

Premises used: StrictMono.injective, EReal.coe_ennreal_strictMono
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
⊢ (↑x : EReal) = ⊤ ↔ x = ∞

Tactic:
coe_ennreal_injective.eq_iff' rfl

Premises used: Function.Injective.eq_iff', EReal.coe_ennreal_injective, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0
⊢ (↑(↑x : ℝ≥0∞) : EReal) ≠ ⊤

Tactic:
coe_ne_top x

Premises used: ENNReal.toEReal, EReal.coe_ne_top, NNReal.toReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0
⊢ (↑(↑x : ℝ≥0∞) : EReal) < ⊤

Tactic:
coe_lt_top x

Premises used: ENNReal.toEReal, NNReal.toReal, EReal.coe_lt_top
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ≥0∞
⊢ (↑x : EReal) ≤ (↑y : EReal) ↔ x ≤ y

Tactic:
coe_ennreal_strictMono.le_iff_le

Premises used: EReal.coe_ennreal_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ≥0∞
⊢ (↑x : EReal) < (↑y : EReal) ↔ x < y

Tactic:
coe_ennreal_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, EReal.coe_ennreal_strictMono
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ≥0∞
⊢ (↑x : EReal) = (↑y : EReal) ↔ x = y

Tactic:
coe_ennreal_injective.eq_iff

Premises used: Function.Injective.eq_iff, EReal.coe_ennreal_injective
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ≥0∞
⊢ (↑x : EReal) ≠ (↑y : EReal) ↔ x ≠ y

Tactic:
coe_ennreal_injective.ne_iff

Premises used: Function.Injective.ne_iff, EReal.coe_ennreal_injective
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
rw : (↑x : EReal) = 0 ↔ (↑x : EReal) = (↑0 : EReal)
rw₁ rw₂ : (↑x : EReal) = 0 ↔ (↑x : EReal) = 0
⊢ (↑x : EReal) = 0 ↔ x = 0

Tactic:
rw [← coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_zero]

Premises used: EReal.coe_ennreal_eq_coe_ennreal_iff, EReal.coe_ennreal_zero
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
rw : (↑x : EReal) = 1 ↔ (↑x : EReal) = (↑1 : EReal)
rw₁ rw₂ : (↑x : EReal) = 1 ↔ (↑x : EReal) = 1
⊢ (↑x : EReal) = 1 ↔ x = 1

Tactic:
rw [← coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_one]

Premises used: EReal.coe_ennreal_eq_coe_ennreal_iff, EReal.coe_ennreal_one
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
⊢ (↑x : EReal) ≠ 0 ↔ x ≠ 0

Tactic:
coe_ennreal_eq_zero.not

Premises used: Iff.not, EReal.coe_ennreal_eq_zero
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
⊢ (↑x : EReal) ≠ 1 ↔ x ≠ 1

Tactic:
coe_ennreal_eq_one.not

Premises used: Iff.not, EReal.coe_ennreal_eq_one
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
⊢ 0 ≤ (↑x : EReal)

Tactic:
coe_ennreal_le_coe_ennreal_iff.2 zero_le

Premises used: Iff.mpr, zero_le, EReal.coe_ennreal_le_coe_ennreal_iff, WithBot.some, ENNReal.toEReal, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ range toEReal = Ici 0

Tactic:
Subset.antisymm (range_subset_iff.2 coe_ennreal_nonneg) fun x => match x with
    | ⊥ => fun h => absurd h bot_lt_zero.not_ge
    | ⊤ => fun _ => ⟨⊤, rfl⟩
    | (x : ℝ) => fun h => ⟨.some ⟨x, EReal.coe_nonneg.1 h⟩, rfl⟩

Premises used: Set.Subset.antisymm, Iff.mpr, EReal.bot_lt_zero, WithTop.some, Subtype.mk, EReal.coe_nonneg, absurd, _private.0.EReal.range_coe_ennreal.match_1, Exists.intro, Iff.mp, LT.lt.not_ge, Set.range_subset_iff, Top.top, EReal.coe_ennreal_nonneg, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ CanLift EReal ℝ≥0∞ toEReal fun (x : EReal) ↦ 0 ≤ x

Tactic:
⟨range_coe_ennreal.ge⟩

Premises used: Eq.ge, EReal.range_coe_ennreal, CanLift.mk
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
rw : (↑0 : EReal) < (↑x : EReal) ↔ 0 < x
rw₁ rw₂ : 0 < x ↔ 0 < x
⊢ 0 < (↑x : EReal) ↔ 0 < x

Tactic:
rw [← coe_ennreal_zero, coe_ennreal_lt_coe_ennreal_iff]

Premises used: EReal.coe_ennreal_zero, EReal.coe_ennreal_lt_coe_ennreal_iff
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
rw : 0 < x ↔ x ≠ 0
rw₁ rw₂ : x ≠ 0 ↔ x ≠ 0
⊢ 0 < (↑x : EReal) ↔ x ≠ 0

Tactic:
rw [coe_ennreal_pos, pos_iff_ne_zero]

Premises used: pos_iff_ne_zero, EReal.coe_ennreal_pos
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
⊢ ⊥ < (↑x : EReal)

Tactic:
(bot_lt_coe 0).trans_le (coe_ennreal_nonneg _)

Premises used: EReal.bot_lt_coe, LT.lt.trans_le, OfNat.ofNat, EReal.coe_ennreal_nonneg
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0∞
⊢ (↑x : EReal) ≠ ⊥

Tactic:
(bot_lt_coe_ennreal x).ne'

Premises used: LT.lt.ne', EReal.bot_lt_coe_ennreal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ≥0∞
top : (↑(∞ + y) : EReal) = (↑∞ : EReal) + (↑y : EReal)
coe : ∀ (x : ℝ≥0), (↑((↑x : ℝ≥0∞) + y) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) + (↑y : EReal)
⊢ (↑(x + y) : EReal) = (↑x : EReal) + (↑y : EReal)

Tactic:
cases x
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : ℝ≥0∞
top : (↑(HAdd.hAdd (α := ℝ≥0∞) ∞ ∞) : EReal) = (↑∞ : EReal) + (↑∞ : EReal)
top₁ : ∀ (x : ℝ≥0), (↑(∞ + (↑x : ℝ≥0∞)) : EReal) = (↑∞ : EReal) + (↑(↑x : ℝ≥0∞) : EReal)
⊢ (↑(∞ + y) : EReal) = (↑∞ : EReal) + (↑y : EReal)

Tactic:
cases y
-- Module: Mathlib.Data.EReal.Basic
Goal:
y : ℝ≥0∞
x : ℝ≥0
coe : (↑((↑x : ℝ≥0∞) + ∞) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) + (↑∞ : EReal)
coe₁ : ∀ (x_1 : ℝ≥0), (↑((↑x : ℝ≥0∞) + (↑x_1 : ℝ≥0∞)) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) + (↑(↑x_1 : ℝ≥0∞) : EReal)
⊢ (↑((↑x : ℝ≥0∞) + y) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) + (↑y : EReal)

Tactic:
cases y
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ (↑(HAdd.hAdd (α := ℝ≥0∞) ∞ ∞) : EReal) = (↑∞ : EReal) + (↑∞ : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0
⊢ (↑(∞ + (↑x : ℝ≥0∞)) : EReal) = (↑∞ : EReal) + (↑(↑x : ℝ≥0∞) : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x : ℝ≥0
⊢ (↑((↑x : ℝ≥0∞) + ∞) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) + (↑∞ : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
x x_1 : ℝ≥0
⊢ (↑((↑x : ℝ≥0∞) + (↑x_1 : ℝ≥0∞)) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) + (↑(↑x_1 : ℝ≥0∞) : EReal)

Tactic:
rfl