awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hp : 0 ≤ p
rw : (↑p.toNNReal : ℝ≥0∞) < ENNReal.ofReal q ↔ p < q
rw₁ : (↑p.toNNReal : ℝ≥0∞) < (↑q.toNNReal : ℝ≥0∞) ↔ p < q
rw₂ : p.toNNReal < q.toNNReal ↔ p < q
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
have rw₃ : p < q ↔ p < q
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff_of_nonneg hp]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
r : ℝ
⊢ ENNReal.ofReal r ≠ 0 ↔ 0 < r
have rw : 0 < ENNReal.ofReal r ↔ 0 < r
Tactic: rw [← pos_iff_ne_zero, ENNReal.ofReal_pos]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
r : ℝ
rw : 0 < ENNReal.ofReal r ↔ 0 < r
⊢ ENNReal.ofReal r ≠ 0 ↔ 0 < r
have rw₁ : 0 < r ↔ 0 < r
Tactic: rw [← pos_iff_ne_zero, ENNReal.ofReal_pos]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a : ℝ
b : ℝ≥0∞
hb : b ≠ ∞
⊢ ENNReal.ofReal a ≤ b ↔ a ≤ b.toReal
have lift : ∀ (b : ℝ≥0), ENNReal.ofReal a ≤ (↑b : ℝ≥0∞) ↔ a ≤ (↑b : ℝ≥0∞).toReal
Tactic: lift b to ℝ≥0 using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a : ℝ
b : ℝ≥0∞
ha : 0 ≤ a
hb : b ≠ ∞
⊢ ENNReal.ofReal a < b ↔ a < b.toReal
have lift : ∀ (b : ℝ≥0), ENNReal.ofReal a < (↑b : ℝ≥0∞) ↔ a < (↑b : ℝ≥0∞).toReal
Tactic: lift b to ℝ≥0 using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a : ℝ
b : ℝ≥0
ha : 0 ≤ a
⊢ a < (↑b : ℝ≥0∞).toReal ↔ a < (↑b : ℝ)
have rw : a < (↑b : ℝ) ↔ a < (↑b : ℝ)
Tactic: rw [coe_toReal]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a : ℝ≥0∞
b : ℝ
ha : a ≠ ∞
hb : 0 ≤ b
⊢ a ≤ ENNReal.ofReal b ↔ a.toReal ≤ b
have lift : ∀ (a : ℝ≥0), (↑a : ℝ≥0∞) ≤ ENNReal.ofReal b ↔ (↑a : ℝ≥0∞).toReal ≤ b
Tactic: lift a to ℝ≥0 using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a : ℝ≥0∞
b : ℝ
ha : a ≠ ∞
⊢ a < ENNReal.ofReal b ↔ a.toReal < b
have lift : ∀ (a : ℝ≥0), (↑a : ℝ≥0∞) < ENNReal.ofReal b ↔ (↑a : ℝ≥0∞).toReal < b
Tactic: lift a to ℝ≥0 using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hq : 0 ≤ q
⊢ ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
have rw : ENNReal.ofReal (q * p) = ENNReal.ofReal p * ENNReal.ofReal q
Tactic: rw [mul_comm, ofReal_mul hq, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hq : 0 ≤ q
rw : ENNReal.ofReal (q * p) = ENNReal.ofReal p * ENNReal.ofReal q
⊢ ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
have rw₁ : ENNReal.ofReal q * ENNReal.ofReal p = ENNReal.ofReal p * ENNReal.ofReal q
Tactic: rw [mul_comm, ofReal_mul hq, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ
hq : 0 ≤ q
rw : ENNReal.ofReal (q * p) = ENNReal.ofReal p * ENNReal.ofReal q
rw₁ : ENNReal.ofReal q * ENNReal.ofReal p = ENNReal.ofReal p * ENNReal.ofReal q
⊢ ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
have rw₂ : ENNReal.ofReal p * ENNReal.ofReal q = ENNReal.ofReal p * ENNReal.ofReal q
Tactic: rw [mul_comm, ofReal_mul hq, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p : ℝ
hp : 0 ≤ p
n : ℕ
⊢ ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n
have rw : ENNReal.ofReal (p ^ n) = (↑(NNReal.mk p hp) : ℝ≥0∞) ^ n
Tactic: rw [ofReal_eq_coe_nnreal hp, ← coe_pow, ← ofReal_coe_nnreal, NNReal.coe_pow, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p : ℝ
hp : 0 ≤ p
n : ℕ
rw : ENNReal.ofReal (p ^ n) = (↑(NNReal.mk p hp) : ℝ≥0∞) ^ n
⊢ ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n
have rw₁ : ENNReal.ofReal (p ^ n) = (↑(NNReal.mk p hp ^ n) : ℝ≥0∞)
Tactic: rw [ofReal_eq_coe_nnreal hp, ← coe_pow, ← ofReal_coe_nnreal, NNReal.coe_pow, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p : ℝ
hp : 0 ≤ p
n : ℕ
rw : ENNReal.ofReal (p ^ n) = (↑(NNReal.mk p hp) : ℝ≥0∞) ^ n
rw₁ : ENNReal.ofReal (p ^ n) = (↑(NNReal.mk p hp ^ n) : ℝ≥0∞)
⊢ ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n
have rw₂ : ENNReal.ofReal (p ^ n) = ENNReal.ofReal (↑(NNReal.mk p hp ^ n) : ℝ)
Tactic: rw [ofReal_eq_coe_nnreal hp, ← coe_pow, ← ofReal_coe_nnreal, NNReal.coe_pow, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p : ℝ
hp : 0 ≤ p
n : ℕ
rw : ENNReal.ofReal (p ^ n) = (↑(NNReal.mk p hp) : ℝ≥0∞) ^ n
rw₁ : ENNReal.ofReal (p ^ n) = (↑(NNReal.mk p hp ^ n) : ℝ≥0∞)
rw₂ : ENNReal.ofReal (p ^ n) = ENNReal.ofReal (↑(NNReal.mk p hp ^ n) : ℝ)
⊢ ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n
have rw₃ : ENNReal.ofReal (p ^ n) = ENNReal.ofReal ((↑(NNReal.mk p hp) : ℝ) ^ n)
Tactic: rw [ofReal_eq_coe_nnreal hp, ← coe_pow, ← ofReal_coe_nnreal, NNReal.coe_pow, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p : ℝ
hp : 0 ≤ p
n : ℕ
rw : ENNReal.ofReal (p ^ n) = (↑(NNReal.mk p hp) : ℝ≥0∞) ^ n
rw₁ : ENNReal.ofReal (p ^ n) = (↑(NNReal.mk p hp ^ n) : ℝ≥0∞)
rw₂ : ENNReal.ofReal (p ^ n) = ENNReal.ofReal (↑(NNReal.mk p hp ^ n) : ℝ)
rw₃ : ENNReal.ofReal (p ^ n) = ENNReal.ofReal ((↑(NNReal.mk p hp) : ℝ) ^ n)
⊢ ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n
have rw₄ : ENNReal.ofReal (p ^ n) = ENNReal.ofReal (p ^ n)
Tactic: rw [ofReal_eq_coe_nnreal hp, ← coe_pow, ← ofReal_coe_nnreal, NNReal.coe_pow, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
c : ℝ
a : ℝ≥0∞
h : 0 ≤ c
⊢ (ENNReal.ofReal c * a).toReal = c * a.toReal
have rw : (ENNReal.ofReal c).toReal * a.toReal = c * a.toReal
Tactic: rw [ENNReal.toReal_mul, ENNReal.toReal_ofReal h]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
c : ℝ
a : ℝ≥0∞
h : 0 ≤ c
rw : (ENNReal.ofReal c).toReal * a.toReal = c * a.toReal
⊢ (ENNReal.ofReal c * a).toReal = c * a.toReal
have rw₁ : c * a.toReal = c * a.toReal
Tactic: rw [ENNReal.toReal_mul, ENNReal.toReal_ofReal h]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a : ℝ≥0∞
⊢ (a * ∞).toReal = 0
have rw : a.toReal * ENNReal.toReal ∞ = 0
Tactic: rw [toReal_mul, toReal_top, mul_zero]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a : ℝ≥0∞
rw : a.toReal * ENNReal.toReal ∞ = 0
⊢ (a * ∞).toReal = 0
have rw₁ : a.toReal * 0 = 0
Tactic: rw [toReal_mul, toReal_top, mul_zero]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a : ℝ≥0∞
rw : a.toReal * ENNReal.toReal ∞ = 0
rw₁ : a.toReal * 0 = 0
⊢ (a * ∞).toReal = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [toReal_mul, toReal_top, mul_zero]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
a : ℝ≥0∞
⊢ (∞ * a).toReal = 0
have rw : (a * ∞).toReal = 0
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ≥0∞
hpq : p ≤ q
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
have inl : ∀ (hpq : 0 ≤ q),
  Eq (α := ℝ≥0∞) 0 0 ∧ q = 0 ∨
    Eq (α := ℝ≥0∞) 0 0 ∧ q = ∞ ∨
      Eq (α := ℝ≥0∞) 0 0 ∧ 0 < q.toReal ∨
        Eq (α := ℝ≥0∞) 0 ∞ ∧ q = ∞ ∨
          0 < ENNReal.toReal 0 ∧ q = ∞ ∨ 0 < ENNReal.toReal 0 ∧ 0 < q.toReal ∧ ENNReal.toReal 0 ≤ q.toReal
Tactic: rcases eq_or_lt_of_le (bot_le : 0 ≤ p) with ((rfl : 0 = p) | (hp : 0 < p))
Cleared hypotheses: p, hpq
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ≥0∞
hpq : p ≤ q
inl :
  ∀ (hpq : 0 ≤ q),
    Eq (α := ℝ≥0∞) 0 0 ∧ q = 0 ∨
      Eq (α := ℝ≥0∞) 0 0 ∧ q = ∞ ∨
        Eq (α := ℝ≥0∞) 0 0 ∧ 0 < q.toReal ∨
          Eq (α := ℝ≥0∞) 0 ∞ ∧ q = ∞ ∨
            0 < ENNReal.toReal 0 ∧ q = ∞ ∨ 0 < ENNReal.toReal 0 ∧ 0 < q.toReal ∧ ENNReal.toReal 0 ≤ q.toReal
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
have inr : ∀ (hp : 0 < p),
  p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
Tactic: rcases eq_or_lt_of_le (bot_le : 0 ≤ p) with ((rfl : 0 = p) | (hp : 0 < p))
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
have inr : ∀ (hpq : p ≤ ∞),
  p = 0 ∧ Eq (α := ℝ≥0∞) ∞ 0 ∨
    p = 0 ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨
      p = 0 ∧ 0 < ENNReal.toReal ∞ ∨
        p = ∞ ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨
          0 < p.toReal ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨ 0 < p.toReal ∧ 0 < ENNReal.toReal ∞ ∧ p.toReal ≤ ENNReal.toReal ∞
Tactic: rcases eq_or_lt_of_le (le_top : q ≤ ∞) with (rfl | hq)
Cleared hypotheses: q, hpq
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (goal)
Goal:
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
inr :
  ∀ (hpq : p ≤ ∞),
    p = 0 ∧ Eq (α := ℝ≥0∞) ∞ 0 ∨
      p = 0 ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨
        p = 0 ∧ 0 < ENNReal.toReal ∞ ∨
          p = ∞ ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨
            0 < p.toReal ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨ 0 < p.toReal ∧ 0 < ENNReal.toReal ∞ ∧ p.toReal ≤ ENNReal.toReal ∞
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
have inr₁ : ∀ (hq : q < ∞),
  p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
Tactic: rcases eq_or_lt_of_le (le_top : q ≤ ∞) with (rfl | hq)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (hypothesis)
Goal:
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ∞
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
have hq' : 0 < q
Tactic: have hq' : 0 < q := lt_of_lt_of_le hp hpq
-- Lean 4 proof step from Mathlib.Data.ENNReal.Real (hypothesis)
Goal:
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ∞
hq' : 0 < q
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
have hp' : p < ∞
Tactic: have hp' : p < ∞ := lt_of_le_of_lt hpq hq
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n x : ℕ∞
⊢ @SuccOrder.succ _ instPreorderENat _ x = x + 1
have top : @SuccOrder.succ _ instPreorderENat _ ⊤ = HAdd.hAdd (α := ℕ∞) ⊤ 1
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n x : ℕ∞
top : @SuccOrder.succ _ instPreorderENat _ ⊤ = HAdd.hAdd (α := ℕ∞) ⊤ 1
⊢ @SuccOrder.succ _ instPreorderENat _ x = x + 1
have coe : ∀ (a : ℕ), @SuccOrder.succ _ instPreorderENat _ (↑a : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) 1
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b : ℕ∞
h : a + b < ⊤
⊢ (a + b).lift h = a.lift ⋯ + b.lift ⋯
have apply : Eq (α := ℕ∞) (↑((a + b).lift h) : ℕ∞) (↑(a.lift sorry + b.lift sorry) : ℕ∞)
Tactic: apply coe_inj.1
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
x : ℕ∞
hx : x < ⊤
⊢ x.lift hx = x.toNat
have none : ∀ (hx : LT.lt (α := ℕ∞) none ⊤), lift none hx = toNat none
Tactic: rcases x with ⟨⟩ | x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
x : ℕ∞
hx : x < ⊤
none : ∀ (hx : LT.lt (α := ℕ∞) Option.none ⊤), lift Option.none hx = toNat Option.none
⊢ x.lift hx = x.toNat
have some : ∀ (x : ℕ) (hx : some x < ⊤), lift (some x) hx = toNat (some x)
Tactic: rcases x with ⟨⟩ | x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ∞
m : ℕ
inst : NeZero m
⊢ n.toNat = m ↔ n = (↑m : ℕ∞)
have top : toNat ⊤ = m ↔ Eq (α := ℕ∞) ⊤ (↑m : ℕ∞)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ∞
m : ℕ
inst : NeZero m
top : toNat ⊤ = m ↔ Eq (α := ℕ∞) ⊤ (↑m : ℕ∞)
⊢ n.toNat = m ↔ n = (↑m : ℕ∞)
have coe : ∀ (a : ℕ), toNat (↑a : ℕ∞) = m ↔ Eq (α := ℕ∞) (↑a : ℕ∞) (↑m : ℕ∞)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m n : ℕ∞
hm : m ≠ ⊤
hn : n ≠ ⊤
⊢ (m + n).toNat = m.toNat + n.toNat
have lift : ∀ (m : ℕ), ((↑m : ℕ∞) + n).toNat = toNat (↑m : ℕ∞) + n.toNat
Tactic: lift m to ℕ using hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ∞
hn : n ≠ ⊤
m : ℕ
⊢ ((↑m : ℕ∞) + n).toNat = toNat (↑m : ℕ∞) + n.toNat
have lift : ∀ (n : ℕ), (HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)).toNat = toNat (↑m : ℕ∞) + toNat (↑n : ℕ∞)
Tactic: lift n to ℕ using hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ∞
hn : n ≠ ⊤
m : ℕ∞
⊢ (m - n).toNat = m.toNat - n.toNat
have lift : ∀ (n : ℕ), (m - (↑n : ℕ∞)).toNat = m.toNat - toNat (↑n : ℕ∞)
Tactic: lift n to ℕ using hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m : ℕ∞
n : ℕ
⊢ (m - (↑n : ℕ∞)).toNat = m.toNat - toNat (↑n : ℕ∞)
have top : (HSub.hSub (α := ℕ∞) ⊤ (↑n : ℕ∞)).toNat = toNat ⊤ - toNat (↑n : ℕ∞)
Tactic: induction m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m : ℕ∞
n : ℕ
top : (HSub.hSub (α := ℕ∞) ⊤ (↑n : ℕ∞)).toNat = toNat ⊤ - toNat (↑n : ℕ∞)
⊢ (m - (↑n : ℕ∞)).toNat = m.toNat - toNat (↑n : ℕ∞)
have coe : ∀ (a : ℕ), (HSub.hSub (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞)).toNat = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)
Tactic: induction m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ
⊢ (HSub.hSub (α := ℕ∞) ⊤ (↑n : ℕ∞)).toNat = toNat ⊤ - toNat (↑n : ℕ∞)
have top : toNat ⊤ = toNat ⊤ - toNat (↑n : ℕ∞)
Tactic: rw [top_sub_coe, toNat_top, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ
top : toNat ⊤ = toNat ⊤ - toNat (↑n : ℕ∞)
⊢ (HSub.hSub (α := ℕ∞) ⊤ (↑n : ℕ∞)).toNat = toNat ⊤ - toNat (↑n : ℕ∞)
have top₁ : 0 = 0 - toNat (↑n : ℕ∞)
Tactic: rw [top_sub_coe, toNat_top, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ
top : toNat ⊤ = toNat ⊤ - toNat (↑n : ℕ∞)
top₁ : 0 = 0 - toNat (↑n : ℕ∞)
⊢ (HSub.hSub (α := ℕ∞) ⊤ (↑n : ℕ∞)).toNat = toNat ⊤ - toNat (↑n : ℕ∞)
have top₂ : Eq (α := ℕ) 0 0
Tactic: rw [top_sub_coe, toNat_top, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n a : ℕ
⊢ (HSub.hSub (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞)).toNat = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)
have coe : toNat (↑(a - n) : ℕ∞) = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)
Tactic: rw [← coe_sub, toNat_coe, toNat_coe, toNat_coe]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n a : ℕ
coe : toNat (↑(a - n) : ℕ∞) = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)
⊢ (HSub.hSub (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞)).toNat = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)
have coe₁ : a - n = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)
Tactic: rw [← coe_sub, toNat_coe, toNat_coe, toNat_coe]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n a : ℕ
coe : toNat (↑(a - n) : ℕ∞) = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)
coe₁ : a - n = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)
⊢ (HSub.hSub (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞)).toNat = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)
have coe₂ : a - n = a - toNat (↑n : ℕ∞)
Tactic: rw [← coe_sub, toNat_coe, toNat_coe, toNat_coe]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n a : ℕ
coe : toNat (↑(a - n) : ℕ∞) = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)
coe₁ : a - n = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)
coe₂ : a - n = a - toNat (↑n : ℕ∞)
⊢ (HSub.hSub (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞)).toNat = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)
have coe₃ : a - n = a - n
Tactic: rw [← coe_sub, toNat_coe, toNat_coe, toNat_coe]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b : ℕ∞
⊢ (a * b).toNat = a.toNat * b.toNat
have top : (⊤ * b).toNat = toNat ⊤ * b.toNat
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b : ℕ∞
top : (⊤ * b).toNat = toNat ⊤ * b.toNat
⊢ (a * b).toNat = a.toNat * b.toNat
have coe : ∀ (a : ℕ), ((↑a : ℕ∞) * b).toNat = toNat (↑a : ℕ∞) * b.toNat
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
b : ℕ∞
⊢ (⊤ * b).toNat = toNat ⊤ * b.toNat
have top : (HMul.hMul (α := ℕ∞) ⊤ ⊤).toNat = toNat ⊤ * toNat ⊤
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
b : ℕ∞
top : (HMul.hMul (α := ℕ∞) ⊤ ⊤).toNat = toNat ⊤ * toNat ⊤
⊢ (⊤ * b).toNat = toNat ⊤ * b.toNat
have top₁ : ∀ (a : ℕ), (HMul.hMul (α := ℕ∞) ⊤ (↑a : ℕ∞)).toNat = toNat ⊤ * toNat (↑a : ℕ∞)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
b : ℕ∞
a : ℕ
⊢ ((↑a : ℕ∞) * b).toNat = toNat (↑a : ℕ∞) * b.toNat
have coe : (HMul.hMul (α := ℕ∞) (↑a : ℕ∞) ⊤).toNat = toNat (↑a : ℕ∞) * toNat ⊤
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
b : ℕ∞
a : ℕ
coe : (HMul.hMul (α := ℕ∞) (↑a : ℕ∞) ⊤).toNat = toNat (↑a : ℕ∞) * toNat ⊤
⊢ ((↑a : ℕ∞) * b).toNat = toNat (↑a : ℕ∞) * b.toNat
have coe₁ : ∀ (a_1 : ℕ), (HMul.hMul (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞)).toNat = toNat (↑a : ℕ∞) * toNat (↑a_1 : ℕ∞)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
b : ℕ
⊢ (HMul.hMul (α := ℕ∞) ⊤ (↑b : ℕ∞)).toNat = toNat ⊤ * toNat (↑b : ℕ∞)
have top : (HMul.hMul (α := ℕ∞) ⊤ (↑0 : ℕ∞)).toNat = toNat ⊤ * toNat (↑0 : ℕ∞)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
b : ℕ
top : (HMul.hMul (α := ℕ∞) ⊤ (↑0 : ℕ∞)).toNat = toNat ⊤ * toNat (↑0 : ℕ∞)
⊢ (HMul.hMul (α := ℕ∞) ⊤ (↑b : ℕ∞)).toNat = toNat ⊤ * toNat (↑b : ℕ∞)
have top₁ : ∀ (n : ℕ), (HMul.hMul (α := ℕ∞) ⊤ (↑(n + 1) : ℕ∞)).toNat = toNat ⊤ * toNat (↑(n + 1) : ℕ∞)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a : ℕ
⊢ (HMul.hMul (α := ℕ∞) (↑a : ℕ∞) ⊤).toNat = toNat (↑a : ℕ∞) * toNat ⊤
have coe : (HMul.hMul (α := ℕ∞) (↑0 : ℕ∞) ⊤).toNat = toNat (↑0 : ℕ∞) * toNat ⊤
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a : ℕ
coe : (HMul.hMul (α := ℕ∞) (↑0 : ℕ∞) ⊤).toNat = toNat (↑0 : ℕ∞) * toNat ⊤
⊢ (HMul.hMul (α := ℕ∞) (↑a : ℕ∞) ⊤).toNat = toNat (↑a : ℕ∞) * toNat ⊤
have coe₁ : ∀ (n : ℕ), (HMul.hMul (α := ℕ∞) (↑(n + 1) : ℕ∞) ⊤).toNat = toNat (↑(n + 1) : ℕ∞) * toNat ⊤
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a a_1 : ℕ
⊢ (HMul.hMul (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞)).toNat = toNat (↑a : ℕ∞) * toNat (↑a_1 : ℕ∞)
have coe : (HMul.hMul (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞)).toNat = a * a_1
Tactic: simp only [toNat_coe]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a a_1 : ℕ
⊢ (HMul.hMul (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞)).toNat = a * a_1
have coe : toNat (↑(a * a_1) : ℕ∞) = a * a_1
Tactic: rw [← coe_mul, toNat_coe]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a a_1 : ℕ
coe : toNat (↑(a * a_1) : ℕ∞) = a * a_1
⊢ (HMul.hMul (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞)).toNat = a * a_1
have coe₁ : a * a_1 = a * a_1
Tactic: rw [← coe_mul, toNat_coe]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m : ℕ∞
n : ℕ
hn : n ≠ 0
⊢ m.toNat = n ↔ m = (↑n : ℕ∞)
have top : toNat ⊤ = n ↔ Eq (α := ℕ∞) ⊤ (↑n : ℕ∞)
Tactic: induction m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m : ℕ∞
n : ℕ
hn : n ≠ 0
top : toNat ⊤ = n ↔ Eq (α := ℕ∞) ⊤ (↑n : ℕ∞)
⊢ m.toNat = n ↔ m = (↑n : ℕ∞)
have coe : ∀ (a : ℕ), toNat (↑a : ℕ∞) = n ↔ Eq (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞)
Tactic: induction m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m : ℕ∞
n : ℕ
h : m ≤ (↑n : ℕ∞)
⊢ m.toNat ≤ n
have lift : ∀ (m : ℕ) (h : LE.le (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)), toNat (↑m : ℕ∞) ≤ n
Tactic: lift m to ℕ using ne_top_of_le_ne_top (coe_ne_top n) h
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m n : ℕ∞
hn : n ≠ ⊤
⊢ m + 1 ≤ n ↔ m < n
have inl : HAdd.hAdd (α := ℕ∞) ⊤ 1 ≤ n ↔ ⊤ < n
Tactic: rcases eq_or_ne m ⊤ with rfl | hm
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m n : ℕ∞
hn : n ≠ ⊤
inl : HAdd.hAdd (α := ℕ∞) ⊤ 1 ≤ n ↔ ⊤ < n
⊢ m + 1 ≤ n ↔ m < n
have inr : ∀ (hm : m ≠ ⊤), m + 1 ≤ n ↔ m < n
Tactic: rcases eq_or_ne m ⊤ with rfl | hm
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ∞
h : n = 0 ∨ n = 1
⊢ n ≤ 1
have inl : n = 0 → n ≤ 1
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ∞
h : n = 0 ∨ n = 1
inl : n = 0 → n ≤ 1
⊢ n ≤ 1
have inr : n = 1 → n ≤ 1
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ∞
⊢ n ≤ 1 ↔ n = 0 ∨ n = 1
have refine : ∀ (h : n ≤ 1), n = 0 ∨ n = 1
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by cases h <;> simp_all⟩
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ∞
h : n ≤ 1
⊢ n = 0 ∨ n = 1
have top : ∀ (h : LE.le (α := ℕ∞) ⊤ 1), Eq (α := ℕ∞) ⊤ 0 ∨ Eq (α := ℕ∞) ⊤ 1
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ∞
h : n ≤ 1
top : ∀ (h : LE.le (α := ℕ∞) ⊤ 1), Eq (α := ℕ∞) ⊤ 0 ∨ Eq (α := ℕ∞) ⊤ 1
⊢ n = 0 ∨ n = 1
have coe : ∀ (a : ℕ) (h : LE.le (α := ℕ∞) (↑a : ℕ∞) 1), Eq (α := ℕ∞) (↑a : ℕ∞) 0 ∨ Eq (α := ℕ∞) (↑a : ℕ∞) 1
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a : ℕ
h : LE.le (α := ℕ∞) (↑a : ℕ∞) 1
⊢ Eq (α := ℕ∞) (↑a : ℕ∞) 0 ∨ Eq (α := ℕ∞) (↑a : ℕ∞) 1
have coe : LT.lt (α := ℕ∞) (↑a : ℕ∞) 1 ∨ Eq (α := ℕ∞) (↑a : ℕ∞) 1
Tactic: rwa [← lt_one_iff_eq_zero, ← le_iff_lt_or_eq]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m n : ℕ∞
hm : m ≠ ⊤
⊢ m < n + 1 ↔ m ≤ n
have rw : m + 1 ≤ n + 1 ↔ m ≤ n
Tactic: rw [← add_one_le_iff hm, add_le_add_iff_right one_ne_top]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m n : ℕ∞
hm : m ≠ ⊤
rw : m + 1 ≤ n + 1 ↔ m ≤ n
⊢ m < n + 1 ↔ m ≤ n
have rw₁ : m ≤ n ↔ m ≤ n
Tactic: rw [← add_one_le_iff hm, add_le_add_iff_right one_ne_top]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
motive : ℕ∞ → Prop
a : ℕ∞
zero : motive 0
succ : ∀ (n : ℕ), motive (↑n : ℕ∞) → motive (↑n.succ : ℕ∞)
top : (∀ (n : ℕ), motive (↑n : ℕ∞)) → motive ⊤
⊢ motive a
have have : ∀ (A : ∀ (n : ℕ), motive (↑n : ℕ∞)), motive a
Tactic: have A : ∀ n : ℕ, motive n := fun n => Nat.recOn n zero succ
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
motive : ℕ∞ → Prop
a : ℕ∞
zero : motive 0
succ : ∀ (n : ℕ), motive (↑n : ℕ∞) → motive (↑n.succ : ℕ∞)
top : (∀ (n : ℕ), motive (↑n : ℕ∞)) → motive ⊤
A : ∀ (n : ℕ), motive (↑n : ℕ∞)
⊢ motive a
have top₁ : motive ⊤
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ
⊢ (↑n : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
have rw : n < n + 1
Tactic: rw [← Nat.cast_one, ← Nat.cast_add, coe_lt_coe]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ∞
hn : n ≠ ⊤
⊢ ∃ (m : ℕ), n < (↑m : ℕ∞)
have simp_rw : ∃ (m : ℕ), ¬(↑m : ℕ∞) ≤ n
Tactic: simp_rw [lt_iff_not_ge]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b : ℕ∞
h : a < b
⊢ a ≤ b - 1
have top : ∀ (h : a < ⊤), a ≤ HSub.hSub (α := ℕ∞) ⊤ 1
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b : ℕ∞
h : a < b
top : ∀ (h : a < ⊤), a ≤ HSub.hSub (α := ℕ∞) ⊤ 1
⊢ a ≤ b - 1
have coe : ∀ (a_1 : ℕ) (h : a < (↑a_1 : ℕ∞)), a ≤ HSub.hSub (α := ℕ∞) (↑a_1 : ℕ∞) 1
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ∞
hn : n ≠ ⊤
⊢ Injective (β := ℕ∞) fun (x : ℕ∞) ↦ n + x
have simp_rw : Injective (β := ℕ∞) fun (x : ℕ∞) ↦ x + n
Tactic: simp_rw [add_comm n _]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
c a : ℕ∞
hc : c ≠ 0
⊢ a ≤ a * c
have inl : ⊤ ≤ ⊤ * c
Tactic: obtain rfl | hne := eq_or_ne a ⊤
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
c a : ℕ∞
hc : c ≠ 0
inl : ⊤ ≤ ⊤ * c
⊢ a ≤ a * c
have inr : ∀ (hne : a ≠ ⊤), a ≤ a * c
Tactic: obtain rfl | hne := eq_or_ne a ⊤
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
⊢ a ≤ a * c
have inr : ∀ (hne : Ne (α := ℕ∞) 0 ⊤), 0 ≤ 0 * c
Tactic: obtain rfl | h0 := eq_or_ne a 0
Cleared hypotheses: a, hne