awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
⊢ ((↑a : EReal) * ⊤).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊤
have coe : ∀ (hx : 0 = (↑a : EReal)), ((↑a : EReal) * ⊤).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊤
Tactic: rcases eq_or_lt_of_le hx with (hx | hx)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
coe : ∀ (hx : 0 = (↑a : EReal)), ((↑a : EReal) * ⊤).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊤
⊢ ((↑a : EReal) * ⊤).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊤
have coe₁ : ∀ (hx : 0 < (↑a : EReal)), ((↑a : EReal) * ⊤).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊤
Tactic: rcases eq_or_lt_of_le hx with (hx | hx)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
hx : LE.le (α := EReal) 0 ⊤
a : ℝ
⊢ (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal
have top : ∀ (ha : a < 0), (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal
Tactic: rcases lt_trichotomy a 0 with (ha | ha | ha)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
hx : LE.le (α := EReal) 0 ⊤
a : ℝ
top : ∀ (ha : a < 0), (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal
⊢ (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal
have top₁ : ∀ (ha : a = 0), (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal
Tactic: rcases lt_trichotomy a 0 with (ha | ha | ha)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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
⊢ (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal
have top₂ : ∀ (ha : 0 < a), (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal
Tactic: rcases lt_trichotomy a 0 with (ha | ha | ha)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hy : 0 ≤ y
⊢ (x * y).toENNReal = x.toENNReal * y.toENNReal
have rw : (y * x).toENNReal = x.toENNReal * y.toENNReal
Tactic: rw [EReal.mul_comm, toENNReal_mul hy, mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hy : 0 ≤ y
rw : (y * x).toENNReal = x.toENNReal * y.toENNReal
⊢ (x * y).toENNReal = x.toENNReal * y.toENNReal
have rw₁ : y.toENNReal * x.toENNReal = x.toENNReal * y.toENNReal
Tactic: rw [EReal.mul_comm, toENNReal_mul hy, mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hy : 0 ≤ y
rw : (y * x).toENNReal = x.toENNReal * y.toENNReal
rw₁ : y.toENNReal * x.toENNReal = x.toENNReal * y.toENNReal
⊢ (x * y).toENNReal = x.toENNReal * y.toENNReal
have rw₂ : x.toENNReal * y.toENNReal = x.toENNReal * y.toENNReal
Tactic: rw [EReal.mul_comm, toENNReal_mul hy, mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = a * c + b * c
have lift : ∀ (a : ℝ≥0∞), ((↑a : EReal) + b) * c = (↑a : EReal) * c + b * c
Tactic: lift a to ℝ≥0∞ using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
b c : EReal
hb : 0 ≤ b
a : ℝ≥0∞
⊢ ((↑a : EReal) + b) * c = (↑a : EReal) * c + b * c
have lift : ∀ (b : ℝ≥0∞), ((↑a : EReal) + (↑b : EReal)) * c = (↑a : EReal) * c + (↑b : EReal) * c
Tactic: lift b to ℝ≥0∞ using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
hc : 0 < c
⊢ ((↑a : EReal) + (↑b : EReal)) * -(↑c : EReal) = (↑a : EReal) * -(↑c : EReal) + (↑b : EReal) * -(↑c : EReal)
have neg_coe : -(↑(a * c + b * c) : EReal) = -(↑(a * c) : EReal) + -(↑(b * c) : EReal)
Tactic: simp only [mul_neg, ← coe_ennreal_add, ← coe_ennreal_mul, add_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
hc : 0 < c
⊢ -(↑(a * c + b * c) : EReal) = -(↑(a * c) : EReal) + -(↑(b * c) : EReal)
have neg_coe : -((↑(a * c) : EReal) + (↑(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]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
hc : 0 < c
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)
have neg_coe₁ : -(↑(a * c) : EReal) - (↑(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]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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)
⊢ -(↑(a * c + b * c) : EReal) = -(↑(a * c) : EReal) + -(↑(b * c) : EReal)
have neg_coe₂ : -(↑(a * c) : EReal) + -(↑(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]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
c : EReal
a b : ℝ≥0∞
⊢ ((↑a : EReal) + (↑b : EReal)) * c = (↑a : EReal) * c + (↑b : EReal) * c
have coe : ∀ (c : ℝ≥0∞), ((↑a : EReal) + (↑b : EReal)) * (↑c : EReal) = (↑a : EReal) * (↑c : EReal) + (↑b : EReal) * (↑c : EReal)
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]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
c : EReal
a b : ℝ≥0∞
coe :
  ∀ (c : ℝ≥0∞), ((↑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
have neg_coe : ∀ (c : ℝ≥0∞) (hc : 0 < c),
  ((↑a : EReal) + (↑b : EReal)) * -(↑c : EReal) = (↑a : EReal) * -(↑c : EReal) + (↑b : EReal) * -(↑c : EReal)
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]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ c * (a + b) = c * a + c * b
have nth_rewrite : (a + b) * c = c * a + c * b
Tactic: nth_rewrite 1 [EReal.mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = c * a + c * b
have nth_rewrite : (a + b) * c = a * c + c * b
Tactic: nth_rewrite 2 [EReal.mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = a * c + c * b
have nth_rewrite : (a + b) * c = a * c + b * c
Tactic: nth_rewrite 3 [EReal.mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
hx0 : 0 < x
⊢ x * (y + z) = x * y + x * z
have 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
Tactic: lift x to ℝ using ⟨hx_ne_top, hx0.ne_bot⟩
Cleared hypotheses: x, hx_nonneg, hx_ne_top, hx0
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y z : EReal
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
have inr : (↑x : EReal) * (⊥ + z) = (↑x : EReal) * ⊥ + (↑x : EReal) * z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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
⊢ (↑x : EReal) * (y + z) = (↑x : EReal) * y + (↑x : EReal) * z
have inr₁ : ∀ (a : ℝ), (↑x : EReal) * ((↑a : EReal) + z) = (↑x : EReal) * (↑a : EReal) + (↑x : EReal) * z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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
⊢ (↑x : EReal) * (y + z) = (↑x : EReal) * y + (↑x : EReal) * z
have inr₂ : (↑x : EReal) * (⊤ + z) = (↑x : EReal) * ⊤ + (↑x : EReal) * z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
z : EReal
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
⊢ (↑x : EReal) * (⊥ + z) = (↑x : EReal) * ⊥ + (↑x : EReal) * z
have inr : (↑x : EReal) * HAdd.hAdd (α := EReal) ⊥ ⊥ = (↑x : EReal) * ⊥ + (↑x : EReal) * ⊥
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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) * ⊥
⊢ (↑x : EReal) * (⊥ + z) = (↑x : EReal) * ⊥ + (↑x : EReal) * z
have inr₁ : ∀ (a : ℝ), (↑x : EReal) * (⊥ + (↑a : EReal)) = (↑x : EReal) * ⊥ + (↑x : EReal) * (↑a : EReal)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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)
⊢ (↑x : EReal) * (⊥ + z) = (↑x : EReal) * ⊥ + (↑x : EReal) * z
have inr₂ : (↑x : EReal) * HAdd.hAdd (α := EReal) ⊥ ⊤ = (↑x : EReal) * ⊥ + (↑x : EReal) * ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
z : EReal
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
a : ℝ
⊢ (↑x : EReal) * ((↑a : EReal) + z) = (↑x : EReal) * (↑a : EReal) + (↑x : EReal) * z
have inr : (↑x : EReal) * ((↑a : EReal) + ⊥) = (↑x : EReal) * (↑a : EReal) + (↑x : EReal) * ⊥
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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) * ⊥
⊢ (↑x : EReal) * ((↑a : EReal) + z) = (↑x : EReal) * (↑a : EReal) + (↑x : EReal) * z
have inr₁ : ∀ (a_1 : ℝ),
  (↑x : EReal) * ((↑a : EReal) + (↑a_1 : EReal)) = (↑x : EReal) * (↑a : EReal) + (↑x : EReal) * (↑a_1 : EReal)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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)
⊢ (↑x : EReal) * ((↑a : EReal) + z) = (↑x : EReal) * (↑a : EReal) + (↑x : EReal) * z
have inr₂ : (↑x : EReal) * ((↑a : EReal) + ⊤) = (↑x : EReal) * (↑a : EReal) + (↑x : EReal) * ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
z : EReal
x : ℝ
hx_nonneg : 0 ≤ (↑x : EReal)
hx_ne_top : (↑x : EReal) ≠ ⊤
hx0 : 0 < (↑x : EReal)
⊢ (↑x : EReal) * (⊤ + z) = (↑x : EReal) * ⊤ + (↑x : EReal) * z
have inr : (↑x : EReal) * HAdd.hAdd (α := EReal) ⊤ ⊥ = (↑x : EReal) * ⊤ + (↑x : EReal) * ⊥
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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) * ⊥
⊢ (↑x : EReal) * (⊤ + z) = (↑x : EReal) * ⊤ + (↑x : EReal) * z
have inr₁ : ∀ (a : ℝ), (↑x : EReal) * (⊤ + (↑a : EReal)) = (↑x : EReal) * ⊤ + (↑x : EReal) * (↑a : EReal)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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)
⊢ (↑x : EReal) * (⊤ + z) = (↑x : EReal) * ⊤ + (↑x : EReal) * z
have inr₂ : (↑x : EReal) * HAdd.hAdd (α := EReal) ⊤ ⊤ = (↑x : EReal) * ⊤ + (↑x : EReal) * ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (hypothesis)
Goal:
x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
⊢ x * (y + z) = x * y + x * z
have x₁ : 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]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
⊢ HSMul.hSMul (α := ℕ) 0 x = (↑0 : EReal) * x
have zero : 0 = (↑0 : EReal) * x
Tactic: rw [zero_smul, Nat.cast_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
zero : 0 = (↑0 : EReal) * x
⊢ HSMul.hSMul (α := ℕ) 0 x = (↑0 : EReal) * x
have zero₁ : 0 = 0 * x
Tactic: rw [zero_smul, Nat.cast_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
zero : 0 = (↑0 : EReal) * x
zero₁ : 0 = 0 * x
⊢ HSMul.hSMul (α := ℕ) 0 x = (↑0 : EReal) * x
have zero₂ : Eq (α := EReal) 0 0
Tactic: rw [zero_smul, Nat.cast_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
n : ℕ
ih : n • x = (↑n : EReal) * x
⊢ (n + 1) • x = (↑(n + 1) : EReal) * x
have succ : (↑n : EReal) * x + x = HAdd.hAdd (α := EReal) (↑n : EReal) 1 * x
Tactic: rw [succ_nsmul, ih, Nat.cast_succ]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
n : ℕ
ih : n • x = (↑n : EReal) * x
⊢ (↑n : EReal) * x + x = HAdd.hAdd (α := EReal) (↑n : EReal) 1 * x
have h : x = 1 * x
Tactic: convert! (EReal.right_distrib_of_nonneg _ _).symm
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
n : ℕ
ih : n • x = (↑n : EReal) * x
h : x = 1 * x
⊢ (↑n : EReal) * x + x = HAdd.hAdd (α := EReal) (↑n : EReal) 1 * x
have succ : LE.le (α := EReal) 0 (↑n : EReal)
Tactic: convert! (EReal.right_distrib_of_nonneg _ _).symm
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
n : ℕ
ih : n • x = (↑n : EReal) * x
h : x = 1 * x
succ : LE.le (α := EReal) 0 (↑n : EReal)
⊢ (↑n : EReal) * x + x = HAdd.hAdd (α := EReal) (↑n : EReal) 1 * x
have succ₁ : LE.le (α := EReal) 0 1
Tactic: convert! (EReal.right_distrib_of_nonneg _ _).symm
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
n : ℕ
x : EReal
⊢ n • x = (↑n : EReal) * x
have zero : HSMul.hSMul (α := ℕ) 0 x = (↑0 : 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
n : ℕ
x : EReal
zero : HSMul.hSMul (α := ℕ) 0 x = (↑0 : EReal) * x
⊢ n • x = (↑n : EReal) * x
have succ : ∀ (n : ℕ) (ih : n • x = (↑n : EReal) * x), (n + 1) • x = (↑(n + 1) : 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Erased (goal)
Goal:
α : Sort u_1
a : α
h : ∃ (a_1 : α), Eq.{max 1 u_1} (fun (x : α) ↦ a_1 = x) (↑(mk a) : α → Prop) := ⋯
⊢ (mk a).out = a
have change : Classical.choose (p := fun (x : α) ↦ Eq.{max 1 u_1} (fun (x_1 : α) ↦ x = x_1) (↑(mk a) : α → Prop)) h = a
Tactic: change Classical.choose h = a
-- Lean 4 proof step from Mathlib.Data.Erased (hypothesis)
Goal:
α : Sort u_1
a : α
h : ∃ (a_1 : α), Eq.{max 1 u_1} (fun (x : α) ↦ a_1 = x) (↑(mk a) : α → Prop) := ⋯
⊢ Classical.choose (p := fun (x : α) ↦ Eq.{max 1 u_1} (fun (x_1 : α) ↦ x = x_1) (↑(mk a) : α → Prop)) h = a
have this : 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
-- Lean 4 proof step from Mathlib.Data.Erased (goal)
Goal:
α : Sort u_1
s : α → Prop
h : ∃ (a : α), Eq.{max 1 u_1} (fun (x : α) ↦ a = x) s
⊢ Eq.{max 1 u_1}
    (Subtype.mk.{max 1 u_1} (p := fun (s : α → Prop) ↦ ∃ (a : α), Eq.{max 1 u_1} (fun (x : α) ↦ a = x) s)
      (fun (b : α) ↦
        out (Subtype.mk.{max 1 u_1} (p := fun (s : α → Prop) ↦ ∃ (a : α), Eq.{max 1 u_1} (fun (x : α) ↦ a = x) s) s h) =
          b)
      ⋯)
    (Subtype.mk.{max 1 u_1} (p := fun (s : α → Prop) ↦ ∃ (a : α), Eq.{max 1 u_1} (fun (x : α) ↦ a = x) s) s h)
have e_val : Eq.{max 1 u_1}
  (fun (b : α) ↦
    out (Subtype.mk.{max 1 u_1} (p := fun (s : α → Prop) ↦ ∃ (a : α), Eq.{max 1 u_1} (fun (x : α) ↦ a = x) s) s h) = b)
  s
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Erased (goal)
Goal:
α β : Type u_1
⊢ Eq (α := α → Erased β → Erased α) Functor.mapConst (Functor.map ∘ Function.const β)
have h : ∀ (x : α) (x_1 : Erased β), (Functor.mapConst x x_1).out = out ((Functor.map ∘ Function.const β) x x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Erased (goal)
Goal:
α : Type u_1
x : Erased α
⊢ id <$> x = x
have h : (id <$> x).out = x.out
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Erased (goal)
Goal:
α β : Type u_1
x : Erased α
y : Erased β
⊢ x <* y = Function.const β <$> x <*> y
have h : (x <* y).out = (Function.const β <$> x <*> y).out
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Erased (goal)
Goal:
α β : Type u_1
x : Erased α
y : Erased β
⊢ Eq (α := Erased β) (x *> y) (Function.const α id <$> x <*> y)
have h : Eq (α := β) (out (x *> y)) (out (Function.const α id <$> x <*> y))
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Erased (goal)
Goal:
α β : Type u_1
g : α → β
x : Erased α
⊢ pure g <*> x = g <$> x
have h : out (pure g <*> x) = (g <$> x).out
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Erased (goal)
Goal:
α β : Type u_1
f : α → β
x : Erased α
⊢ (do
      let a ← x
      pure (f a)) =
    f <$> x
have h : (out do
    let a ← x
    pure (f a)) =
  (f <$> x).out
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Erased (goal)
Goal:
α β : Type u_1
f : Erased (α → β)
x : Erased α
⊢ (do
      let x_1 ← f
      x_1 <$> x) =
    f <*> x
have h : (out do
    let x_1 ← f
    x_1 <$> x) =
  (f <*> x).out
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Erased (goal)
Goal:
α β : Type u_1
x : α
f : α → Erased β
⊢ pure x >>= f = f x
have h : (pure x >>= f).out = (f x).out
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Erased (goal)
Goal:
α β γ : Type u_1
x : Erased α
f : α → Erased β
g : β → Erased γ
⊢ x >>= f >>= g = x >>= fun (x : α) ↦ f x >>= g
have h : (x >>= f >>= g).out = out (x >>= fun (x : α) ↦ f x >>= g)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.FP.Basic (goal)
Goal:
C : FloatCfg
⊢ emin ≤ emin + (↑prec : ℤ) - 1
have rw : emin ≤ emin + HSub.hSub (α := ℤ) (↑prec : ℤ) 1
Tactic: rw [add_sub_assoc]
-- Lean 4 proof step from Mathlib.Data.FP.Basic (goal)
Goal:
C : FloatCfg
⊢ emin ≤ emin + HSub.hSub (α := ℤ) (↑prec : ℤ) 1
have h : 0 ≤ HSub.hSub (α := ℤ) (↑prec : ℤ) 1
Tactic: apply le_add_of_nonneg_right
-- Lean 4 proof step from Mathlib.Data.FP.Basic (goal)
Goal:
C : FloatCfg
⊢ 0 ≤ HSub.hSub (α := ℤ) (↑prec : ℤ) 1
have h : LE.le (α := ℤ) 1 (↑prec : ℤ)
Tactic: apply sub_nonneg_of_le
-- Lean 4 proof step from Mathlib.Data.FP.Basic (goal)
Goal:
C : FloatCfg
⊢ LE.le (α := ℤ) 1 (↑prec : ℤ)
have h : 1 ≤ prec
Tactic: apply Int.ofNat_le_ofNat_of_le
-- Lean 4 proof step from Mathlib.Data.FP.Basic (hypothesis)
Goal:
C : FloatCfg
this : prec ≤ 2 * emax
⊢ emin + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ)
have this₁ : LE.le (α := ℤ) (↑prec : ℤ) (↑(2 * emax) : ℤ)
Tactic: rw [← Int.ofNat_le] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.FP.Basic (goal)
Goal:
C : FloatCfg
this : LE.le (α := ℤ) (↑prec : ℤ) (↑(2 * emax) : ℤ)
⊢ emin + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ)
have rw : ∀ (this : 0 ≤ HSub.hSub (α := ℤ) (↑(2 * emax) : ℤ) (↑prec : ℤ)), 0 ≤ (↑emax : ℤ) - (emin + (↑prec : ℤ) - 1)
Tactic: rw [← sub_nonneg] at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.FP.Basic (goal)
Goal:
C : FloatCfg
this : 0 ≤ HSub.hSub (α := ℤ) (↑(2 * emax) : ℤ) (↑prec : ℤ)
⊢ 0 ≤ (↑emax : ℤ) - (emin + (↑prec : ℤ) - 1)
have simp : 0 ≤ (↑FloatCfg.emax : ℤ) - (HSub.hSub (α := ℤ) 1 (↑FloatCfg.emax : ℤ) + (↑prec : ℤ) - 1)
Tactic: simp only [emin, emax] at *
-- Lean 4 proof step from Mathlib.Data.FP.Basic (goal)
Goal:
C : FloatCfg
n d : ℕ+
e₁ : ℤ := HSub.hSub (α := ℤ) (↑(↑n : ℕ).size : ℤ) (↑(↑d : ℕ).size : ℤ) - (↑prec : ℤ)
⊢ Float × Bool
have obtain : (d₁ n₁ : ℕ) → Float × Bool
Tactic: obtain ⟨d₁, n₁⟩ := Int.shift2 d.1 n.1 (e₁ + prec)
-- Lean 4 proof step from Mathlib.Data.FP.Basic (goal)
Goal:
C : FloatCfg
n d : ℕ+
e₁ : ℤ := HSub.hSub (α := ℤ) (↑(↑n : ℕ).size : ℤ) (↑(↑d : ℕ).size : ℤ) - (↑prec : ℤ)
d₁ n₁ : ℕ
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
⊢ Float × Bool
have obtain : (d₂ n₂ : ℕ) → Float × Bool
Tactic: obtain ⟨d₂, n₂⟩ := Int.shift2 d.1 n.1 (e₃ + prec)
-- Lean 4 proof step from Mathlib.Data.FP.Basic (goal)
Goal:
C : FloatCfg
n d : ℕ+
e₁ : ℤ := HSub.hSub (α := ℤ) (↑(↑n : ℕ).size : ℤ) (↑(↑d : ℕ).size : ℤ) - (↑prec : ℤ)
d₁ n₁ : ℕ
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
r : ℚ := mkRat (↑n₂ : ℤ) d₂
m : ℤ := r.floor
⊢ Float × Bool
have refine : ValidFinite e₃ m.toNat
Tactic: refine (Float.finite Bool.false e₃ (Int.toNat m) ?_, r.den = 1)
-- Lean 4 proof step from Mathlib.Data.FP.Basic (hypothesis)
Goal:
C : FloatCfg
e : ℤ
m m' : ℕ
v : ValidFinite e m'.succ
h : m = m'.succ
ss : m'.size = m.size
⊢ ValidFinite e m'
have ss₁ : m'.size = m'.succ.size
Tactic: subst h
Cleared hypotheses: m, h, ss
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
α : Sort u_1
k l : ℕ
h : k = l
f : Fin k → α
g : Fin l → α
⊢ f ≍ g ↔ ∀ (i : Fin k), f i = g ⟨(↑i : ℕ), ⋯⟩
have subst : ∀ {g : Fin k → α}, f ≍ g ↔ ∀ (i : Fin k), f i = g ⟨(↑i : ℕ), sorry⟩
Tactic: subst h
Cleared hypotheses: l, h, g
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
α : Sort u_1
k l k' l' : ℕ
h : k = l
h' : k' = l'
f : Fin k → Fin k' → α
g : Fin l → Fin l' → α
⊢ f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨(↑i : ℕ), ⋯⟩ ⟨(↑j : ℕ), ⋯⟩
have subst : ∀ {g : Fin k → Fin l' → α}, f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨(↑i : ℕ), sorry⟩ ⟨(↑j : ℕ), sorry⟩
Tactic: subst h
Cleared hypotheses: l, h, g
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
α : Sort u_1
k k' l' : ℕ
h' : k' = l'
f : Fin k → Fin k' → α
g : Fin k → Fin l' → α
⊢ f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨(↑i : ℕ), ⋯⟩ ⟨(↑j : ℕ), ⋯⟩
have subst : ∀ {g : Fin k → Fin k' → α}, f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨(↑i : ℕ), sorry⟩ ⟨(↑j : ℕ), sorry⟩
Tactic: subst h'
Cleared hypotheses: l', h', g
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
k l : ℕ
h : k = l
i : Fin k
j : Fin l
⊢ i ≍ j ↔ (↑i : ℕ) = (↑j : ℕ)
have subst : ∀ {j : Fin k}, i ≍ j ↔ (↑i : ℕ) = (↑j : ℕ)
Tactic: subst h
Cleared hypotheses: l, h, j
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : Fin n
⊢ 0 < (↑a : ℕ) ↔ 0 < a
have rw : 0 < (↑a : ℕ) ↔ (↑0 : ℕ) < (↑a : ℕ)
Tactic: rw [← val_fin_lt, val_zero]