awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : 0 < b
b_top : b < ⊤
inr : ∀ (a' : EReal) (aa' : a < a') (hc' : a' < c / b), ∃ a' ∈ Ioo a ⊤, a' * b < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
obtain ⟨a', aa', hc'⟩ := exists_between ((lt_div_iff b0 b_top.ne).2 hc)

Premises used: Iff.mpr, EReal.lt_div_iff, exists_between, LT.lt.ne
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : 0 < b
b_top : b < ⊤
a' : EReal
aa' : a < a'
hc' : a' < c / b
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
⟨a', mem_Ioo.2 ⟨aa', lt_top_of_lt hc'⟩, (lt_div_iff b0 b_top.ne).1 hc'⟩

Premises used: Iff.mpr, Set.mem_Ioo, lt_top_of_lt, EReal.lt_div_iff, And.intro, Exists.intro, Iff.mp, LT.lt.ne
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : 0 < b
b_top : b < ⊤
a' : EReal
aa' : a < a'
hc' : a' < c / b
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
exact ⟨a', mem_Ioo.2 ⟨aa', lt_top_of_lt hc'⟩, (lt_div_iff b0 b_top.ne).1 hc'⟩
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ 0
hc : a * b < c
simp_rw : ∀ (hc : b * a < c), ∃ b' ∈ Ioo b ⊤, b' * a < c
⊢ ∃ b' ∈ Ioo b ⊤, a * b' < c

Tactic:
simp_rw [mul_comm a] at hc ⊢

Premises used: mul_comm
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ 0
hc : b * a < c
⊢ ∃ b' ∈ Ioo b ⊤, b' * a < c

Tactic:
exists_mul_left_lt h₂.symm h₁.symm hc

Premises used: _private.0.EReal.exists_mul_left_lt, Or.symm
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ 0
hc : b * a < c
⊢ ∃ b' ∈ Ioo b ⊤, b' * a < c

Tactic:
exact exists_mul_left_lt h₂.symm h₁.symm hc

Premises used: _private.0.EReal.exists_mul_left_lt, Or.symm
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ c ≤ a * b

Tactic:
le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_

Premises used: le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
refine : ∀ (d : EReal) (hd : a * b < d), c ≤ d
⊢ c ≤ a * b

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_

Premises used: le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd : a * b < d
obtain : ∀ (a' : EReal) (aa' : a' ∈ Ioo a ⊤) (hd : a' * b < d), c ≤ d
⊢ c ≤ d

Tactic:
obtain ⟨a', aa', hd⟩ := exists_mul_left_lt (h₁.imp_left ne_of_gt) h₂ hd

Premises used: Or.imp_left, ne_of_gt, _private.0.EReal.exists_mul_left_lt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd_1 : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd : a' * b < d
⊢ 0 < a' ∨ b ≠ ⊤

Tactic:
replace h₁ : 0 < a' ∨ b ≠ ⊤ := h₁.imp_left fun a0 ↦ a0.trans (mem_Ioo.1 aa').1
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd_1 : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd : a' * b < d
h₁ : 0 < a' ∨ b ≠ ⊤
⊢ a' ≠ ⊤ ∨ b ≠ 0

Tactic:
replace h₂ : a' ≠ ⊤ ∨ b ≠ 0 := Or.inl (mem_Ioo.1 aa').2.ne
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd_1 : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd : a' * b < d
h₁ : 0 < a' ∨ b ≠ ⊤
h₂ : a' ≠ ⊤ ∨ b ≠ 0
obtain : ∀ (b' : EReal) (bb' : b' ∈ Ioo b ⊤) (hd : a' * b' < d), c ≤ d
⊢ c ≤ d

Tactic:
obtain ⟨b', bb', hd⟩ := exists_mul_right_lt h₁ h₂ hd

Premises used: _private.0.EReal.exists_mul_right_lt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd_1 : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd_2 : a' * b < d
h₁ : 0 < a' ∨ b ≠ ⊤
h₂ : a' ≠ ⊤ ∨ b ≠ 0
b' : EReal
bb' : b' ∈ Ioo b ⊤
hd : a' * b' < d
⊢ c ≤ d

Tactic:
(h a' (mem_Ioo.1 aa').1 b' (mem_Ioo.1 bb').1).trans hd.le

Premises used: Set.mem_Ioo, LT.lt.le, And.left, Iff.mp, LE.le.trans
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd_1 : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd_2 : a' * b < d
h₁ : 0 < a' ∨ b ≠ ⊤
h₂ : a' ≠ ⊤ ∨ b ≠ 0
b' : EReal
bb' : b' ∈ Ioo b ⊤
hd : a' * b' < d
⊢ c ≤ d

Tactic:
exact (h a' (mem_Ioo.1 aa').1 b' (mem_Ioo.1 bb').1).trans hd.le

Premises used: Set.mem_Ioo, LT.lt.le, And.left, Iff.mp, LE.le.trans
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
le_of_forall_lt_imp_le_of_dense fun d dab ↦ ?_

Premises used: le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
refine : ∀ (d : EReal) (dab : d < a * b), d ≤ c
⊢ a * b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d dab ↦ ?_

Premises used: le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
inl : ∀ (d0 : d < 0), d ≤ c
inr : ∀ (d0 : 0 ≤ d), d ≤ c
⊢ d ≤ c

Tactic:
rcases lt_or_ge d 0 with d0 | d0

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
d0 : d < 0
⊢ d ≤ c

Tactic:
d0.le.trans hc

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
d0 : d < 0
⊢ d ≤ c

Tactic:
exact d0.le.trans hc

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
d0 : 0 ≤ d
inr : ∀ (a' : EReal) (aa' : a' ∈ Ioo 0 a) (dab : d < a' * b), d ≤ c
⊢ d ≤ c

Tactic:
obtain ⟨a', aa', dab⟩ := exists_lt_mul_left_of_nonneg ha d0 dab

Premises used: _private.0.EReal.exists_lt_mul_left_of_nonneg
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab_1 : d < a * b
d0 : 0 ≤ d
a' : EReal
aa' : a' ∈ Ioo 0 a
dab : d < a' * b
inr : ∀ (b' : EReal) (bb' : b' ∈ Ioo 0 b) (dab : d < a' * b'), d ≤ c
⊢ d ≤ c

Tactic:
obtain ⟨b', bb', dab⟩ := exists_lt_mul_right_of_nonneg aa'.1.le d0 dab

Premises used: LT.lt.le, And.left, _private.0.EReal.exists_lt_mul_right_of_nonneg
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab_1 : d < a * b
d0 : 0 ≤ d
a' : EReal
aa' : a' ∈ Ioo 0 a
dab_2 : d < a' * b
b' : EReal
bb' : b' ∈ Ioo 0 b
dab : d < a' * b'
⊢ d ≤ c

Tactic:
dab.le.trans (h a' aa' b' bb')

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab_1 : d < a * b
d0 : 0 ≤ d
a' : EReal
aa' : a' ∈ Ioo 0 a
dab_2 : d < a' * b
b' : EReal
bb' : b' ∈ Ioo 0 b
dab : d < a' * b'
⊢ d ≤ c

Tactic:
exact dab.le.trans (h a' aa' b' bb')

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : 0 ≤ a
h' : 0 ≤ b
⊢ (a + b) / c = a / c + b / c

Tactic:
EReal.right_distrib_of_nonneg h h'

Premises used: DivInvMonoid.div', EReal.mul, EReal.right_distrib_of_nonneg
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : 0 ≤ c
⊢ (a + b) / c = a / c + b / c

Tactic:
apply right_distrib_of_nonneg_of_ne_top (inv_nonneg_of_nonneg h) (inv_lt_top c).ne

Premises used: EReal.inv_nonneg_of_nonneg, EReal.right_distrib_of_nonneg_of_ne_top, EReal.inv_lt_top, LT.lt.ne
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
⊢ x + ⊥ = ⊥

Tactic:
WithBot.add_bot _

Premises used: EReal, WithBot.add_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
⊢ ⊥ + x = ⊥

Tactic:
WithBot.bot_add _

Premises used: EReal, WithBot.bot_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
⊢ x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥

Tactic:
WithBot.add_eq_bot

Premises used: EReal, WithBot.add_eq_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
⊢ x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥

Tactic:
WithBot.add_ne_bot

Premises used: EReal, WithBot.add_ne_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
⊢ ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y

Tactic:
simp [bot_lt_iff_ne_bot]

Premises used: bot_lt_iff_ne_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HAdd.hAdd (α := EReal) ⊤ ⊤ = ⊤

Tactic:
rfl

Premises used: WithBot.some, WithTop.map₂, WithBot.map₂, rfl, Option.map₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
⊢ ⊤ + (↑x : EReal) = ⊤

Tactic:
rfl

Premises used: WithBot.some, WithTop.map₂, WithBot.map₂, rfl, Option.map₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : x ≠ ⊥
bot : ∀ (h : Ne (α := EReal) ⊥ ⊥), HAdd.hAdd (α := EReal) ⊤ ⊥ = ⊤
coe : ∀ (a : ℝ) (h : (↑a : EReal) ≠ ⊥), ⊤ + (↑a : EReal) = ⊤
top : ∀ (h : Ne (α := EReal) ⊤ ⊥), HAdd.hAdd (α := EReal) ⊤ ⊤ = ⊤
⊢ ⊤ + x = ⊤

Tactic:
induction x
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊥ ⊥
bot : False
⊢ HAdd.hAdd (α := EReal) ⊤ ⊥ = ⊤

Tactic:
exfalso
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊥ ⊥
⊢ False

Tactic:
h (Eq.refl ⊥)

Premises used: Bot.bot, Eq.refl
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊥ ⊥
⊢ False

Tactic:
exact h (Eq.refl ⊥)

Premises used: Bot.bot, Eq.refl
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h : (↑a : EReal) ≠ ⊥
⊢ ⊤ + (↑a : EReal) = ⊤

Tactic:
top_add_coe _

Premises used: EReal.top_add_coe
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h : (↑a : EReal) ≠ ⊥
⊢ ⊤ + (↑a : EReal) = ⊤

Tactic:
exact top_add_coe _

Premises used: EReal.top_add_coe
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊤ ⊥
⊢ HAdd.hAdd (α := EReal) ⊤ ⊤ = ⊤

Tactic:
top_add_top

Premises used: EReal.top_add_top
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊤ ⊥
⊢ HAdd.hAdd (α := EReal) ⊤ ⊤ = ⊤

Tactic:
exact top_add_top

Premises used: EReal.top_add_top
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
mp : ⊤ + x = ⊤ → x ≠ ⊥
mpr : x ≠ ⊥ → ⊤ + x = ⊤
⊢ ⊤ + x = ⊤ ↔ x ≠ ⊥

Tactic:
constructor
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : HAdd.hAdd (α := EReal) ⊤ ⊥ = ⊤
⊢ Eq (α := EReal) ⊥ ⊤

Tactic:
rw [add_bot] at h

Premises used: EReal.add_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Eq (α := EReal) ⊥ ⊤
⊢ False

Tactic:
bot_ne_top h

Premises used: bot_ne_top
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Eq (α := EReal) ⊥ ⊤
⊢ False

Tactic:
exact bot_ne_top h

Premises used: bot_ne_top
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊥ ⊥
⊢ HAdd.hAdd (α := EReal) ⊤ ⊥ = ⊤

Tactic:
contradiction
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊤ ⊥
⊢ HAdd.hAdd (α := EReal) ⊤ ⊤ = ⊤

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
r : ℝ
h : (↑r : EReal) ≠ ⊥
⊢ ⊤ + (↑r : EReal) = ⊤

Tactic:
top_add_of_ne_bot h

Premises used: EReal.top_add_of_ne_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
r : ℝ
h : (↑r : EReal) ≠ ⊥
⊢ ⊤ + (↑r : EReal) = ⊤

Tactic:
exact top_add_of_ne_bot h

Premises used: EReal.top_add_of_ne_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : x ≠ ⊥
mpr : ∀ (h : Ne (α := EReal) ⊥ ⊥), HAdd.hAdd (α := EReal) ⊤ ⊥ = ⊤
mpr₁ : ∀ (h : Ne (α := EReal) ⊤ ⊥), HAdd.hAdd (α := EReal) ⊤ ⊤ = ⊤
mpr₂ : ∀ (r : ℝ) (h : (↑r : EReal) ≠ ⊥), ⊤ + (↑r : EReal) = ⊤
⊢ ⊤ + x = ⊤

Tactic:
cases x with
    | bot => contradiction
    | top => rfl
    | coe r => exact top_add_of_ne_bot h

Premises used: EReal.top_add_of_ne_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : x ≠ ⊥
rw : ⊤ + x = ⊤
rw₁ rw₂ : Eq (α := EReal) ⊤ ⊤
⊢ x + ⊤ = ⊤

Tactic:
rw [add_comm, top_add_of_ne_bot h]

Premises used: EReal.top_add_of_ne_bot, add_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
rw : ⊤ + x = ⊤ ↔ x ≠ ⊥
rw₁ rw₂ : x ≠ ⊥ ↔ x ≠ ⊥
⊢ x + ⊤ = ⊤ ↔ x ≠ ⊥

Tactic:
rw [add_comm, top_add_iff_ne_bot]

Premises used: EReal.top_add_iff_ne_bot, add_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
ha : 0 < a
hb : 0 ≤ b
⊢ 0 < a + b

Tactic:
add_comm a b ▸ Right.add_pos_of_nonneg_of_pos hb ha

Premises used: Eq.rec, add_comm, Right.add_pos_of_nonneg_of_pos, Eq.symm
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
ha : 0 < a
hb : 0 < b
⊢ 0 < a + b

Tactic:
Right.add_pos_of_nonneg_of_pos ha.le hb

Premises used: LT.lt.le, Right.add_pos_of_nonneg_of_pos
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
⊢ (↑x : EReal) + ⊤ = ⊤

Tactic:
rfl

Premises used: WithBot.some, WithTop.map₂, WithBot.map₂, rfl, Option.map₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
hy : y ≠ ⊤
h'y : y ≠ ⊥
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
⟨hx, h'x⟩

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

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

Tactic:
⟨hy, h'y⟩

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

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

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
hx : 0 ≤ x
hy : 0 ≤ y
bot : ∀ (hx : LE.le (α := EReal) 0 ⊥), (⊥ + y).toENNReal = toENNReal ⊥ + y.toENNReal
coe : ∀ (a : ℝ) (hx : 0 ≤ (↑a : EReal)), ((↑a : EReal) + y).toENNReal = (↑a : EReal).toENNReal + y.toENNReal
top : ∀ (hx : LE.le (α := EReal) 0 ⊤), (⊤ + y).toENNReal = toENNReal ⊤ + y.toENNReal
⊢ (x + y).toENNReal = x.toENNReal + y.toENNReal

Tactic:
induction x
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊥
bot : ∀ (hy : LE.le (α := EReal) 0 ⊥), (HAdd.hAdd (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ + toENNReal ⊥
bot₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), (⊥ + (↑a : EReal)).toENNReal = toENNReal ⊥ + (↑a : EReal).toENNReal
bot₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), (HAdd.hAdd (α := EReal) ⊥ ⊤).toENNReal = toENNReal ⊥ + toENNReal ⊤
⊢ (⊥ + y).toENNReal = toENNReal ⊥ + y.toENNReal

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
hy : 0 ≤ y
a : ℝ
hx : 0 ≤ (↑a : EReal)
coe : ∀ (hy : LE.le (α := EReal) 0 ⊥), ((↑a : EReal) + ⊥).toENNReal = (↑a : EReal).toENNReal + toENNReal ⊥
coe₁ :
  ∀ (a_1 : ℝ) (hy : 0 ≤ (↑a_1 : EReal)),
    ((↑a : EReal) + (↑a_1 : EReal)).toENNReal = (↑a : EReal).toENNReal + (↑a_1 : EReal).toENNReal
coe₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), ((↑a : EReal) + ⊤).toENNReal = (↑a : EReal).toENNReal + toENNReal ⊤
⊢ ((↑a : EReal) + y).toENNReal = (↑a : EReal).toENNReal + y.toENNReal

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊤
top : ∀ (hy : LE.le (α := EReal) 0 ⊥), (HAdd.hAdd (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ + toENNReal ⊥
top₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), (⊤ + (↑a : EReal)).toENNReal = toENNReal ⊤ + (↑a : EReal).toENNReal
top₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), (HAdd.hAdd (α := EReal) ⊤ ⊤).toENNReal = toENNReal ⊤ + toENNReal ⊤
⊢ (⊤ + y).toENNReal = toENNReal ⊤ + y.toENNReal

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx hy : LE.le (α := EReal) 0 ⊥
⊢ (HAdd.hAdd (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ + toENNReal ⊥

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx hy : LE.le (α := EReal) 0 ⊥
⊢ (HAdd.hAdd (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ + toENNReal ⊥

Tactic:
{· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx hy : LE.le (α := EReal) 0 ⊥
⊢ (HAdd.hAdd (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ + toENNReal ⊥

Tactic:
try {· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊥
a : ℝ
hy : 0 ≤ (↑a : EReal)
⊢ (⊥ + (↑a : EReal)).toENNReal = toENNReal ⊥ + (↑a : EReal).toENNReal

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊥
a : ℝ
hy : 0 ≤ (↑a : EReal)
⊢ (⊥ + (↑a : EReal)).toENNReal = toENNReal ⊥ + (↑a : EReal).toENNReal

Tactic:
{· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊥
a : ℝ
hy : 0 ≤ (↑a : EReal)
⊢ (⊥ + (↑a : EReal)).toENNReal = toENNReal ⊥ + (↑a : EReal).toENNReal

Tactic:
try {· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊥
hy : LE.le (α := EReal) 0 ⊤
⊢ (HAdd.hAdd (α := EReal) ⊥ ⊤).toENNReal = toENNReal ⊥ + toENNReal ⊤

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊥
hy : LE.le (α := EReal) 0 ⊤
⊢ (HAdd.hAdd (α := EReal) ⊥ ⊤).toENNReal = toENNReal ⊥ + toENNReal ⊤

Tactic:
{· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊥
hy : LE.le (α := EReal) 0 ⊤
⊢ (HAdd.hAdd (α := EReal) ⊥ ⊤).toENNReal = toENNReal ⊥ + toENNReal ⊤

Tactic:
try {· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
hy : LE.le (α := EReal) 0 ⊥
⊢ ((↑a : EReal) + ⊥).toENNReal = (↑a : EReal).toENNReal + toENNReal ⊥

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
hy : LE.le (α := EReal) 0 ⊥
⊢ ((↑a : EReal) + ⊥).toENNReal = (↑a : EReal).toENNReal + toENNReal ⊥

Tactic:
{· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
hy : LE.le (α := EReal) 0 ⊥
⊢ ((↑a : EReal) + ⊥).toENNReal = (↑a : EReal).toENNReal + toENNReal ⊥

Tactic:
try {· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
a_1 : ℝ
hy : 0 ≤ (↑a_1 : EReal)
⊢ ((↑a : EReal) + (↑a_1 : EReal)).toENNReal = (↑a : EReal).toENNReal + (↑a_1 : EReal).toENNReal

Tactic:
{· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
hy : LE.le (α := EReal) 0 ⊤
⊢ ((↑a : EReal) + ⊤).toENNReal = (↑a : EReal).toENNReal + toENNReal ⊤

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
hy : LE.le (α := EReal) 0 ⊤
⊢ ((↑a : EReal) + ⊤).toENNReal = (↑a : EReal).toENNReal + toENNReal ⊤

Tactic:
{· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
hy : LE.le (α := EReal) 0 ⊤
⊢ ((↑a : EReal) + ⊤).toENNReal = (↑a : EReal).toENNReal + toENNReal ⊤

Tactic:
try {· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
hy : LE.le (α := EReal) 0 ⊥
⊢ (HAdd.hAdd (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ + toENNReal ⊥

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
hy : LE.le (α := EReal) 0 ⊥
⊢ (HAdd.hAdd (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ + toENNReal ⊥

Tactic:
{· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
hy : LE.le (α := EReal) 0 ⊥
⊢ (HAdd.hAdd (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ + toENNReal ⊥

Tactic:
try {· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
a : ℝ
hy : 0 ≤ (↑a : EReal)
⊢ (⊤ + (↑a : EReal)).toENNReal = toENNReal ⊤ + (↑a : EReal).toENNReal

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
a : ℝ
hy : 0 ≤ (↑a : EReal)
⊢ (⊤ + (↑a : EReal)).toENNReal = toENNReal ⊤ + (↑a : EReal).toENNReal

Tactic:
{· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
a : ℝ
hy : 0 ≤ (↑a : EReal)
⊢ (⊤ + (↑a : EReal)).toENNReal = toENNReal ⊤ + (↑a : EReal).toENNReal

Tactic:
try {· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx hy : LE.le (α := EReal) 0 ⊤
⊢ (HAdd.hAdd (α := EReal) ⊤ ⊤).toENNReal = toENNReal ⊤ + toENNReal ⊤

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx hy : LE.le (α := EReal) 0 ⊤
⊢ (HAdd.hAdd (α := EReal) ⊤ ⊤).toENNReal = toENNReal ⊤ + toENNReal ⊤

Tactic:
{· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx hy : LE.le (α := EReal) 0 ⊤
⊢ (HAdd.hAdd (α := EReal) ⊤ ⊤).toENNReal = toENNReal ⊤ + toENNReal ⊤

Tactic:
try {· simp_all}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
a_1 : ℝ
hy : 0 ≤ (↑a_1 : EReal)
coe : ENNReal.ofReal (a + a_1) = ENNReal.ofReal a + ENNReal.ofReal a_1
⊢ (↑(a + a_1) : EReal).toENNReal = (↑a : EReal).toENNReal + (↑a_1 : EReal).toENNReal

Tactic:
simp_rw [real_coe_toENNReal]

Premises used: EReal.real_coe_toENNReal
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
a_1 : ℝ
hy : 0 ≤ (↑a_1 : EReal)
⊢ ENNReal.ofReal (a + a_1) = ENNReal.ofReal a + ENNReal.ofReal a_1

Tactic:
simp_all [ENNReal.ofReal_add]

Premises used: ENNReal.ofReal_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
bot : (⊥ + y).toENNReal ≤ toENNReal ⊥ + y.toENNReal
coe : ∀ (a : ℝ), ((↑a : EReal) + y).toENNReal ≤ (↑a : EReal).toENNReal + y.toENNReal
top : (⊤ + y).toENNReal ≤ toENNReal ⊤ + y.toENNReal
⊢ (x + y).toENNReal ≤ x.toENNReal + y.toENNReal

Tactic:
induction x
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
bot : (HAdd.hAdd (α := EReal) ⊥ ⊥).toENNReal ≤ toENNReal ⊥ + toENNReal ⊥
bot₁ : ∀ (a : ℝ), (⊥ + (↑a : EReal)).toENNReal ≤ toENNReal ⊥ + (↑a : EReal).toENNReal
bot₂ : (HAdd.hAdd (α := EReal) ⊥ ⊤).toENNReal ≤ toENNReal ⊥ + toENNReal ⊤
⊢ (⊥ + y).toENNReal ≤ toENNReal ⊥ + y.toENNReal

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
a : ℝ
coe : ((↑a : EReal) + ⊥).toENNReal ≤ (↑a : EReal).toENNReal + toENNReal ⊥
coe₁ : ∀ (a_1 : ℝ), ((↑a : EReal) + (↑a_1 : EReal)).toENNReal ≤ (↑a : EReal).toENNReal + (↑a_1 : EReal).toENNReal
coe₂ : ((↑a : EReal) + ⊤).toENNReal ≤ (↑a : EReal).toENNReal + toENNReal ⊤
⊢ ((↑a : EReal) + y).toENNReal ≤ (↑a : EReal).toENNReal + y.toENNReal

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
top : (HAdd.hAdd (α := EReal) ⊤ ⊥).toENNReal ≤ toENNReal ⊤ + toENNReal ⊥
top₁ : ∀ (a : ℝ), (⊤ + (↑a : EReal)).toENNReal ≤ toENNReal ⊤ + (↑a : EReal).toENNReal
top₂ : (HAdd.hAdd (α := EReal) ⊤ ⊤).toENNReal ≤ toENNReal ⊤ + toENNReal ⊤
⊢ (⊤ + y).toENNReal ≤ toENNReal ⊤ + y.toENNReal

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HAdd.hAdd (α := EReal) ⊥ ⊥).toENNReal ≤ toENNReal ⊥ + toENNReal ⊥

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HAdd.hAdd (α := EReal) ⊥ ⊥).toENNReal ≤ toENNReal ⊥ + toENNReal ⊥

Tactic:
{· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HAdd.hAdd (α := EReal) ⊥ ⊥).toENNReal ≤ toENNReal ⊥ + toENNReal ⊥

Tactic:
try {· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ (⊥ + (↑a : EReal)).toENNReal ≤ toENNReal ⊥ + (↑a : EReal).toENNReal

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ (⊥ + (↑a : EReal)).toENNReal ≤ toENNReal ⊥ + (↑a : EReal).toENNReal

Tactic:
{· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ (⊥ + (↑a : EReal)).toENNReal ≤ toENNReal ⊥ + (↑a : EReal).toENNReal

Tactic:
try {· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HAdd.hAdd (α := EReal) ⊥ ⊤).toENNReal ≤ toENNReal ⊥ + toENNReal ⊤

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HAdd.hAdd (α := EReal) ⊥ ⊤).toENNReal ≤ toENNReal ⊥ + toENNReal ⊤

Tactic:
{· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HAdd.hAdd (α := EReal) ⊥ ⊤).toENNReal ≤ toENNReal ⊥ + toENNReal ⊤

Tactic:
try {· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ ((↑a : EReal) + ⊥).toENNReal ≤ (↑a : EReal).toENNReal + toENNReal ⊥

Tactic:
simp