awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
hx : LE.le (α := EReal) 0 ⊥
bot : (HMul.hMul (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ * toENNReal ⊥
bot₁ : ∀ (a : ℝ), (⊥ * (↑a : EReal)).toENNReal = toENNReal ⊥ * (↑a : EReal).toENNReal
bot₂ : (HMul.hMul (α := EReal) ⊥ ⊤).toENNReal = toENNReal ⊥ * toENNReal ⊤
⊢ (⊥ * y).toENNReal = toENNReal ⊥ * y.toENNReal

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
a : ℝ
hx : 0 ≤ (↑a : EReal)
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
hx : LE.le (α := EReal) 0 ⊤
top : (HMul.hMul (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ * toENNReal ⊥
top₁ : ∀ (a : ℝ), (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal
top₂ : (HMul.hMul (α := EReal) ⊤ ⊤).toENNReal = toENNReal ⊤ * toENNReal ⊤
⊢ (⊤ * y).toENNReal = toENNReal ⊤ * y.toENNReal

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊥
⊢ (HMul.hMul (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ * toENNReal ⊥

Tactic:
simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊥
⊢ (HMul.hMul (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ * toENNReal ⊥

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊥
⊢ (HMul.hMul (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ * toENNReal ⊥

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊥
a : ℝ
⊢ (⊥ * (↑a : EReal)).toENNReal = toENNReal ⊥ * (↑a : EReal).toENNReal

Tactic:
simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊥
a : ℝ
⊢ (⊥ * (↑a : EReal)).toENNReal = toENNReal ⊥ * (↑a : EReal).toENNReal

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊥
a : ℝ
⊢ (⊥ * (↑a : EReal)).toENNReal = toENNReal ⊥ * (↑a : EReal).toENNReal

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊥
⊢ (HMul.hMul (α := EReal) ⊥ ⊤).toENNReal = toENNReal ⊥ * toENNReal ⊤

Tactic:
simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊥
⊢ (HMul.hMul (α := EReal) ⊥ ⊤).toENNReal = toENNReal ⊥ * toENNReal ⊤

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊥
⊢ (HMul.hMul (α := EReal) ⊥ ⊤).toENNReal = toENNReal ⊥ * toENNReal ⊤

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
⊢ ((↑a : EReal) * ⊥).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊥

Tactic:
simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
⊢ ((↑a : EReal) * ⊥).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊥

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
⊢ ((↑a : EReal) * ⊥).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊥

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
a_1 : ℝ
⊢ ((↑a : EReal) * (↑a_1 : EReal)).toENNReal = (↑a : EReal).toENNReal * (↑a_1 : EReal).toENNReal

Tactic:
simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
a_1 : ℝ
⊢ ((↑a : EReal) * (↑a_1 : EReal)).toENNReal = (↑a : EReal).toENNReal * (↑a_1 : EReal).toENNReal

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
a_1 : ℝ
⊢ ((↑a : EReal) * (↑a_1 : EReal)).toENNReal = (↑a : EReal).toENNReal * (↑a_1 : EReal).toENNReal

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
⊢ ((↑a : EReal) * ⊤).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊤

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
⊢ (HMul.hMul (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ * toENNReal ⊥

Tactic:
simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
⊢ (HMul.hMul (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ * toENNReal ⊥

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
⊢ (HMul.hMul (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ * toENNReal ⊥

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
a : ℝ
⊢ (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
⊢ (HMul.hMul (α := EReal) ⊤ ⊤).toENNReal = toENNReal ⊤ * toENNReal ⊤

Tactic:
simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
⊢ (HMul.hMul (α := EReal) ⊤ ⊤).toENNReal = toENNReal ⊤ * toENNReal ⊤

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
⊢ (HMul.hMul (α := EReal) ⊤ ⊤).toENNReal = toENNReal ⊤ * toENNReal ⊤

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Premises used: EReal.mul_nonpos_iff, ENNReal.ofReal_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
coe : ∀ (hx : 0 = (↑a : EReal)), ((↑a : EReal) * ⊤).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊤
coe₁ : ∀ (hx : 0 < (↑a : EReal)), ((↑a : EReal) * ⊤).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊤
⊢ ((↑a : EReal) * ⊤).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊤

Tactic:
rcases eq_or_lt_of_le hx with (hx | hx)

Premises used: eq_or_lt_of_le
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx_1 : 0 ≤ (↑a : EReal)
hx : 0 = (↑a : EReal)
⊢ ((↑a : EReal) * ⊤).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊤

Tactic:
simp [← hx]
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx_1 : 0 ≤ (↑a : EReal)
hx : 0 < (↑a : EReal)
⊢ ((↑a : EReal) * ⊤).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊤

Tactic:
simp_all [mul_top_of_pos hx]

Premises used: EReal.mul_top_of_pos
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
a : ℝ
top : ∀ (ha : a < 0), (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal
top₁ : ∀ (ha : a = 0), (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal
top₂ : ∀ (ha : 0 < a), (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal
⊢ (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal

Tactic:
rcases lt_trichotomy a 0 with (ha | ha | ha)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
a : ℝ
ha : a < 0
⊢ (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal

Tactic:
simp_all [le_of_lt, top_mul_of_neg (EReal.coe_neg'.mpr ha)]

Premises used: Iff.mpr, le_of_lt, EReal.coe_neg', EReal.top_mul_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
a : ℝ
ha : a = 0
⊢ (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal

Tactic:
simp [ha]
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : LE.le (α := EReal) 0 ⊤
a : ℝ
ha : 0 < a
⊢ (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal

Tactic:
simp_all [top_mul_of_pos (EReal.coe_pos.mpr ha)]

Premises used: Iff.mpr, EReal.top_mul_of_pos, EReal.coe_pos
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
hy : 0 ≤ y
rw : (y * x).toENNReal = x.toENNReal * y.toENNReal
rw₁ : y.toENNReal * x.toENNReal = x.toENNReal * y.toENNReal
rw₂ rw₃ : x.toENNReal * y.toENNReal = x.toENNReal * y.toENNReal
⊢ (x * y).toENNReal = x.toENNReal * y.toENNReal

Tactic:
rw [EReal.mul_comm, toENNReal_mul hy, mul_comm]

Premises used: EReal.toENNReal_mul, EReal.mul_comm, mul_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a

Tactic:
ha
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
lift : ∀ (a : ℝ≥0∞), ((↑a : EReal) + b) * c = (↑a : EReal) * c + b * c
⊢ (a + b) * c = a * c + b * c

Tactic:
lift a to ℝ≥0∞ using ha
-- Module: Mathlib.Data.EReal.Operations
Goal:
b c : EReal
hb : 0 ≤ b
a : ℝ≥0∞
⊢ 0 ≤ b

Tactic:
hb
-- Module: Mathlib.Data.EReal.Operations
Goal:
b c : EReal
hb : 0 ≤ b
a : ℝ≥0∞
lift : ∀ (b : ℝ≥0∞), ((↑a : EReal) + (↑b : EReal)) * c = (↑a : EReal) * c + (↑b : EReal) * c
⊢ ((↑a : EReal) + b) * c = (↑a : EReal) * c + b * c

Tactic:
lift b to ℝ≥0∞ using hb
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : ℝ≥0∞
⊢ ((↑a : EReal) + (↑b : EReal)) * (↑c : EReal) = (↑a : EReal) * (↑c : EReal) + (↑b : EReal) * (↑c : EReal)

Tactic:
exact_mod_cast add_mul a b c

Premises used: add_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : ℝ≥0∞
hc : 0 < c
neg_coe : -(↑(a * c + b * c) : EReal) = -(↑(a * c) : EReal) + -(↑(b * c) : EReal)
⊢ ((↑a : EReal) + (↑b : EReal)) * -(↑c : EReal) = (↑a : EReal) * -(↑c : EReal) + (↑b : EReal) * -(↑c : EReal)

Tactic:
simp only [mul_neg, ← coe_ennreal_add, ← coe_ennreal_mul, add_mul]

Premises used: add_mul, EReal.coe_ennreal_add, EReal.coe_ennreal_mul, mul_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : ℝ≥0∞
hc : 0 < c
neg_coe : -((↑(a * c) : EReal) + (↑(b * c) : EReal)) = -(↑(a * c) : EReal) + -(↑(b * c) : EReal)
neg_coe₁ : -(↑(a * c) : EReal) - (↑(b * c) : EReal) = -(↑(a * c) : EReal) + -(↑(b * c) : EReal)
neg_coe₂ neg_coe₃ : -(↑(a * c) : EReal) + -(↑(b * c) : EReal) = -(↑(a * c) : EReal) + -(↑(b * c) : EReal)
⊢ -(↑(a * c + b * c) : EReal) = -(↑(a * c) : EReal) + -(↑(b * c) : EReal)

Tactic:
rw [coe_ennreal_add, EReal.neg_add (.inl (coe_ennreal_ne_bot _)) (.inr (coe_ennreal_ne_bot _)),
      sub_eq_add_neg]

Premises used: EReal.coe_ennreal_add, EReal.coe_ennreal_ne_bot, sub_eq_add_neg, EReal.neg_add, Or.inl, Or.inr
-- Module: Mathlib.Data.EReal.Operations
Goal:
c : EReal
a b : ℝ≥0∞
coe :
  ∀ (c : ℝ≥0∞), ((↑a : EReal) + (↑b : EReal)) * (↑c : EReal) = (↑a : EReal) * (↑c : EReal) + (↑b : EReal) * (↑c : EReal)
neg_coe :
  ∀ (c : ℝ≥0∞) (hc : 0 < c),
    ((↑a : EReal) + (↑b : EReal)) * -(↑c : EReal) = (↑a : EReal) * -(↑c : EReal) + (↑b : EReal) * -(↑c : EReal)
⊢ ((↑a : EReal) + (↑b : EReal)) * c = (↑a : EReal) * c + (↑b : EReal) * c

Tactic:
cases c using recENNReal with
  | coe c => exact_mod_cast add_mul a b c
  | neg_coe c hc =>
    simp only [mul_neg, ← coe_ennreal_add, ← coe_ennreal_mul, add_mul]
    rw [coe_ennreal_add, EReal.neg_add (.inl (coe_ennreal_ne_bot _)) (.inr (coe_ennreal_ne_bot _)),
      sub_eq_add_neg]

Premises used: add_mul, EReal.coe_ennreal_add, EReal.coe_ennreal_ne_bot, sub_eq_add_neg, EReal.neg_add, Or.inl, EReal.coe_ennreal_mul, Or.inr, mul_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
nth_rewrite : (a + b) * c = c * a + c * b
⊢ c * (a + b) = c * a + c * b

Tactic:
nth_rewrite 1 [EReal.mul_comm]

Premises used: EReal.mul_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
nth_rewrite : (a + b) * c = a * c + c * b
⊢ (a + b) * c = c * a + c * b

Tactic:
nth_rewrite 2 [EReal.mul_comm]

Premises used: EReal.mul_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
nth_rewrite : (a + b) * c = a * c + b * c
⊢ (a + b) * c = a * c + c * b

Tactic:
nth_rewrite 3 [EReal.mul_comm]

Premises used: EReal.mul_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = a * c + b * c

Tactic:
right_distrib_of_nonneg ha hb

Premises used: EReal.right_distrib_of_nonneg
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = a * c + b * c

Tactic:
exact right_distrib_of_nonneg ha hb

Premises used: EReal.right_distrib_of_nonneg
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
hx0 : x = 0
⊢ x * (y + z) = x * y + x * z

Tactic:
simp [hx0]
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
hx0 : 0 < x
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
⟨hx_ne_top, hx0.ne_bot⟩

Premises used: And.intro, LT.lt.ne_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
hx0 : 0 < x
inr :
  ∀ (x : ℝ) (hx_nonneg : 0 ≤ (↑x : EReal)) (hx_ne_top : (↑x : EReal) ≠ ⊤) (hx0 : 0 < (↑x : EReal)),
    (↑x : EReal) * (y + z) = (↑x : EReal) * y + (↑x : EReal) * z
⊢ x * (y + z) = x * y + x * z

Tactic:
lift x to ℝ using ⟨hx_ne_top, hx0.ne_bot⟩
-- Module: Mathlib.Data.EReal.Operations
Goal:
y z : EReal
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
inr : (↑x : EReal) * (⊥ + z) = (↑x : EReal) * ⊥ + (↑x : EReal) * z
inr₁ : ∀ (a : ℝ), (↑x : EReal) * ((↑a : EReal) + z) = (↑x : EReal) * (↑a : EReal) + (↑x : EReal) * z
inr₂ : (↑x : EReal) * (⊤ + z) = (↑x : EReal) * ⊤ + (↑x : EReal) * z
⊢ (↑x : EReal) * (y + z) = (↑x : EReal) * y + (↑x : EReal) * z

Tactic:
cases y
-- Module: Mathlib.Data.EReal.Operations
Goal:
z : EReal
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
inr : (↑x : EReal) * HAdd.hAdd (α := EReal) ⊥ ⊥ = (↑x : EReal) * ⊥ + (↑x : EReal) * ⊥
inr₁ : ∀ (a : ℝ), (↑x : EReal) * (⊥ + (↑a : EReal)) = (↑x : EReal) * ⊥ + (↑x : EReal) * (↑a : EReal)
inr₂ : (↑x : EReal) * HAdd.hAdd (α := EReal) ⊥ ⊤ = (↑x : EReal) * ⊥ + (↑x : EReal) * ⊤
⊢ (↑x : EReal) * (⊥ + z) = (↑x : EReal) * ⊥ + (↑x : EReal) * z

Tactic:
cases z
-- Module: Mathlib.Data.EReal.Operations
Goal:
z : EReal
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
a : ℝ
inr : (↑x : EReal) * ((↑a : EReal) + ⊥) = (↑x : EReal) * (↑a : EReal) + (↑x : EReal) * ⊥
inr₁ :
  ∀ (a_1 : ℝ),
    (↑x : EReal) * ((↑a : EReal) + (↑a_1 : EReal)) = (↑x : EReal) * (↑a : EReal) + (↑x : EReal) * (↑a_1 : EReal)
inr₂ : (↑x : EReal) * ((↑a : EReal) + ⊤) = (↑x : EReal) * (↑a : EReal) + (↑x : EReal) * ⊤
⊢ (↑x : EReal) * ((↑a : EReal) + z) = (↑x : EReal) * (↑a : EReal) + (↑x : EReal) * z

Tactic:
cases z
-- Module: Mathlib.Data.EReal.Operations
Goal:
z : EReal
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
inr : (↑x : EReal) * HAdd.hAdd (α := EReal) ⊤ ⊥ = (↑x : EReal) * ⊤ + (↑x : EReal) * ⊥
inr₁ : ∀ (a : ℝ), (↑x : EReal) * (⊤ + (↑a : EReal)) = (↑x : EReal) * ⊤ + (↑x : EReal) * (↑a : EReal)
inr₂ : (↑x : EReal) * HAdd.hAdd (α := EReal) ⊤ ⊤ = (↑x : EReal) * ⊤ + (↑x : EReal) * ⊤
⊢ (↑x : EReal) * (⊤ + z) = (↑x : EReal) * ⊤ + (↑x : EReal) * z

Tactic:
cases z
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
⊢ (↑x : EReal) * HAdd.hAdd (α := EReal) ⊥ ⊥ = (↑x : EReal) * ⊥ + (↑x : EReal) * ⊥

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

Premises used: EReal.mul_top_of_pos, EReal.mul_bot_of_pos, EReal.coe_mul, EReal.coe_add, mul_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
a : ℝ
⊢ (↑x : EReal) * (⊥ + (↑a : EReal)) = (↑x : EReal) * ⊥ + (↑x : EReal) * (↑a : EReal)

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

Premises used: EReal.mul_top_of_pos, EReal.mul_bot_of_pos, EReal.coe_mul, EReal.coe_add, mul_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
⊢ (↑x : EReal) * HAdd.hAdd (α := EReal) ⊥ ⊤ = (↑x : EReal) * ⊥ + (↑x : EReal) * ⊤

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

Premises used: EReal.mul_top_of_pos, EReal.mul_bot_of_pos, EReal.coe_mul, EReal.coe_add, mul_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
a : ℝ
⊢ (↑x : EReal) * ((↑a : EReal) + ⊥) = (↑x : EReal) * (↑a : EReal) + (↑x : EReal) * ⊥

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

Premises used: EReal.mul_top_of_pos, EReal.mul_bot_of_pos, EReal.coe_mul, EReal.coe_add, mul_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
a a_1 : ℝ
⊢ (↑x : EReal) * ((↑a : EReal) + (↑a_1 : EReal)) = (↑x : EReal) * (↑a : EReal) + (↑x : EReal) * (↑a_1 : EReal)

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

Premises used: EReal.mul_top_of_pos, EReal.mul_bot_of_pos, EReal.coe_mul, EReal.coe_add, mul_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
a : ℝ
⊢ (↑x : EReal) * ((↑a : EReal) + ⊤) = (↑x : EReal) * (↑a : EReal) + (↑x : EReal) * ⊤

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

Premises used: EReal.mul_top_of_pos, EReal.mul_bot_of_pos, EReal.coe_mul, EReal.coe_add, mul_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
⊢ (↑x : EReal) * HAdd.hAdd (α := EReal) ⊤ ⊥ = (↑x : EReal) * ⊤ + (↑x : EReal) * ⊥

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

Premises used: EReal.mul_top_of_pos, EReal.mul_bot_of_pos, EReal.coe_mul, EReal.coe_add, mul_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
a : ℝ
⊢ (↑x : EReal) * (⊤ + (↑a : EReal)) = (↑x : EReal) * ⊤ + (↑x : EReal) * (↑a : EReal)

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

Premises used: EReal.mul_top_of_pos, EReal.mul_bot_of_pos, EReal.coe_mul, EReal.coe_add, mul_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
⊢ (↑x : EReal) * HAdd.hAdd (α := EReal) ⊤ ⊤ = (↑x : EReal) * ⊤ + (↑x : EReal) * ⊤

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

Premises used: EReal.mul_top_of_pos, EReal.mul_bot_of_pos, EReal.coe_mul, EReal.coe_add, mul_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
⊢ x = 0 ∨ 0 < x

Tactic:
cases hx_nonneg.eq_or_lt' with
  | inl hx0 => simp [hx0]
  | inr hx0 =>
  lift x to ℝ using ⟨hx_ne_top, hx0.ne_bot⟩
  cases y <;> cases z <;>
    simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

Premises used: EReal.coe_mul, EReal.coe_add, mul_add, LE.le.eq_or_lt'
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
⊢ (y + z) * x = y * x + z * x

Tactic:
simpa only [EReal.mul_comm] using left_distrib_of_nonneg_of_ne_top hx_nonneg hx_ne_top y z

Premises used: EReal.mul_comm, EReal.left_distrib_of_nonneg_of_ne_top
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
zero : 0 = (↑0 : EReal) * x
zero₁ : 0 = 0 * x
zero₂ zero₃ : Eq (α := EReal) 0 0
⊢ HSMul.hSMul (α := ℕ) 0 x = (↑0 : EReal) * x

Tactic:
rw [zero_smul, Nat.cast_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, zero_smul, Nat.cast_zero
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
n : ℕ
ih : n • x = (↑n : EReal) * x
succ : (↑n : EReal) * x + x = HAdd.hAdd (α := EReal) (↑n : EReal) 1 * x
⊢ (n + 1) • x = (↑(n + 1) : EReal) * x

Tactic:
rw [succ_nsmul, ih, Nat.cast_succ]

Premises used: Nat.cast_succ, succ_nsmul
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
n : ℕ
ih : n • x = (↑n : EReal) * x
⊢ (↑n : EReal) * x + 1 * x = HAdd.hAdd (α := EReal) (↑n : EReal) 1 * x

Tactic:
(EReal.right_distrib_of_nonneg _ _).symm

Premises used: EReal.right_distrib_of_nonneg, Eq.symm
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
n : ℕ
ih : n • x = (↑n : EReal) * x
h : x = 1 * x
succ : LE.le (α := EReal) 0 (↑n : EReal)
succ₁ : LE.le (α := EReal) 0 1
⊢ (↑n : EReal) * x + x = HAdd.hAdd (α := EReal) (↑n : EReal) 1 * x

Tactic:
convert! (EReal.right_distrib_of_nonneg _ _).symm

Premises used: EReal.right_distrib_of_nonneg, Eq.symm
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
n : ℕ
ih : n • x = (↑n : EReal) * x
⊢ x = 1 * x

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
n : ℕ
ih : n • x = (↑n : EReal) * x
⊢ LE.le (α := EReal) 0 (↑n : EReal)

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
n : ℕ
ih : n • x = (↑n : EReal) * x
⊢ LE.le (α := EReal) 0 1

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
n : ℕ
x : EReal
zero : HSMul.hSMul (α := ℕ) 0 x = (↑0 : EReal) * x
succ : ∀ (n : ℕ) (ih : n • x = (↑n : EReal) * x), (n + 1) • x = (↑(n + 1) : EReal) * x
⊢ n • x = (↑n : EReal) * x

Tactic:
induction n with
  | zero => rw [zero_smul, Nat.cast_zero, zero_mul]
  | succ n ih =>
    rw [succ_nsmul, ih, Nat.cast_succ]
    convert! (EReal.right_distrib_of_nonneg _ _).symm <;> simp

Premises used: Nat.cast_succ, MulZeroClass.zero_mul, zero_smul, Nat.cast_zero, EReal.right_distrib_of_nonneg, Eq.symm, succ_nsmul
-- Module: Mathlib.Data.Erased
Goal:
p : Prop
a : Erased p
⊢ p

Tactic:
out a

Premises used: Erased.out
-- Module: Mathlib.Data.Erased
Goal:
α : Sort u_1
a : α
h : ∃ (a_1 : α), Eq.{max 1 u_1} (fun (x : α) ↦ a_1 = x) (↑(mk a) : α → Prop) := ⋯
change : Classical.choose (p := fun (x : α) ↦ Eq.{max 1 u_1} (fun (x_1 : α) ↦ x = x_1) (↑(mk a) : α → Prop)) h = a
⊢ (mk a).out = a

Tactic:
change Classical.choose h = a

Premises used: Classical.choose
-- Module: Mathlib.Data.Erased
Goal:
α : Sort u_1
a : α
h : ∃ (a_1 : α), Eq.{max 1 u_1} (fun (x : α) ↦ a_1 = x) (↑(mk a) : α → Prop) := ⋯
⊢ Eq.{max 1 u_1}
    (fun (x : α) ↦
      Classical.choose (p := fun (x : α) ↦ Eq.{max 1 u_1} (fun (x_1 : α) ↦ x = x_1) (↑(mk a) : α → Prop)) h = x)
    (↑(mk a) : α → Prop)

Tactic:
have := Classical.choose_spec h