awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENNReal.Real
Goal:
x : ℝ
n : ℕ
⊢ ENNReal.ofReal (n • x) = n • ENNReal.ofReal x

Tactic:
simp only [nsmul_eq_mul, ← ofReal_natCast n, ← ofReal_mul n.cast_nonneg]

Premises used: Nat.cast_nonneg, ENNReal.ofReal_mul, nsmul_eq_mul, ENNReal.ofReal_natCast
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
⊢ (a * b).toNNReal = a.toNNReal * b.toNNReal

Tactic:
WithTop.untopD_zero_mul a b

Premises used: WithTop.untopD_zero_mul, ENNReal.toNNReal
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
⊢ (a * ∞).toNNReal = 0

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
⊢ (∞ * a).toNNReal = 0

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
n : ℕ
⊢ (a ^ n).toNNReal = a.toNNReal ^ n

Tactic:
toNNRealHom.map_pow a n

Premises used: ENNReal.toNNRealHom, ENNReal.toNNReal, MonoidWithZeroHom.toMonoidHom, WithTop.untopD, WithTop.recTopCoe, MonoidHom.map_pow
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a b : ℝ≥0∞
⊢ (a * b).toReal = a.toReal * b.toReal

Tactic:
toRealHom.map_mul a b

Premises used: ENNReal.toRealHom, ENNReal.toReal, MonoidWithZeroHom.map_mul, NNReal.toReal
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
n : ℕ
⊢ (n • a).toReal = n • a.toReal

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
n : ℕ
⊢ (a ^ n).toReal = a.toReal ^ n

Tactic:
toRealHom.map_pow a n

Premises used: ENNReal.toRealHom, ENNReal.toReal, MonoidWithZeroHom.toMonoidHom, NNReal.toReal, MonoidHom.map_pow
-- Module: Mathlib.Data.ENNReal.Real
Goal:
c : ℝ
a : ℝ≥0∞
h : 0 ≤ c
rw : (ENNReal.ofReal c).toReal * a.toReal = c * a.toReal
rw₁ rw₂ : c * a.toReal = c * a.toReal
⊢ (ENNReal.ofReal c * a).toReal = c * a.toReal

Tactic:
rw [ENNReal.toReal_mul, ENNReal.toReal_ofReal h]

Premises used: ENNReal.toReal_ofReal, ENNReal.toReal_mul
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
rw : a.toReal * ENNReal.toReal ∞ = 0
rw₁ : a.toReal * 0 = 0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ (a * ∞).toReal = 0

Tactic:
rw [toReal_mul, toReal_top, mul_zero]

Premises used: MulZeroClass.mul_zero, ENNReal.toReal_mul, ENNReal.toReal_top
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
rw : (a * ∞).toReal = 0
⊢ (∞ * a).toReal = 0

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
⊢ (a * ∞).toReal = 0

Tactic:
toReal_mul_top _

Premises used: ENNReal.toReal_mul_top
-- Module: Mathlib.Data.ENNReal.Real
Goal:
a : ℝ≥0∞
⊢ (a * ∞).toReal = 0

Tactic:
exact toReal_mul_top _

Premises used: ENNReal.toReal_mul_top
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p : ℝ≥0∞
⊢ p = 0 ∨ p = ∞ ∨ 0 < p.toReal

Tactic:
simpa only [or_iff_not_imp_left] using toReal_pos

Premises used: ENNReal.toReal_pos, Classical.or_iff_not_imp_left
-- Module: Mathlib.Data.ENNReal.Real
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
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
⊢ 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))

Premises used: eq_or_lt_of_le, bot_le, rfl
-- Module: Mathlib.Data.ENNReal.Real
Goal:
q : ℝ≥0∞
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:
simpa using q.trichotomy

Premises used: ENNReal.trichotomy
-- Module: Mathlib.Data.ENNReal.Real
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 ∞
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
⊢ 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)

Premises used: eq_or_lt_of_le, le_top, rfl
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p : ℝ≥0∞
hp : 0 < p
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:
simpa using p.trichotomy

Premises used: ENNReal.trichotomy
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ∞
⊢ 0 < q

Tactic:
have hq' : 0 < q := lt_of_lt_of_le hp hpq
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ∞
hq' : 0 < q
⊢ p < ∞

Tactic:
have hp' : p < ∞ := lt_of_le_of_lt hpq hq
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ∞
hq' : 0 < q
hp' : 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:
simp [ENNReal.toReal_mono hq.ne hpq, ENNReal.toReal_pos_iff, hp, hp', hq', hq]

Premises used: ENNReal.toReal_pos_iff, ENNReal.toReal_mono, LT.lt.ne
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p : ℝ≥0∞
inst : Fact (1 ≤ p)
⊢ p = ∞ ∨ 0 < p.toReal ∧ 1 ≤ p.toReal

Tactic:
simpa using ENNReal.trichotomy₂ (Fact.out : 1 ≤ p)

Premises used: ENNReal.trichotomy₂, Fact.out
-- Module: Mathlib.Data.ENNReal.Real
Goal:
p : ℝ≥0∞
inst : Fact (1 ≤ p)
⊢ 0 < p.toReal ↔ p ≠ ∞

Tactic:
⟨fun h hp =>
    have : (0 : ℝ) ≠ 0 := toReal_top ▸ (hp ▸ h.ne : 0 ≠ ∞.toReal)
    this rfl,
    fun h => zero_lt_one.trans_le (p.dichotomy.resolve_left h)⟩

Premises used: Eq.rec, Or.resolve_left, zero_lt_one, LT.lt.trans_le, Iff.intro, ENNReal.dichotomy, ENNReal.toReal_top, rfl, LT.lt.ne
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ WithTop.some = Nat.cast

Tactic:
rfl

Premises used: WithTop.some, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : ℕ
⊢ Eq (α := ℕ∞) (↑a : ℕ∞) (↑b : ℕ∞) ↔ a = b

Tactic:
WithTop.coe_inj

Premises used: WithTop.coe_inj, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
⊢ Eq (α := ℕ∞) (@SuccOrder.succ _ instPreorderENat _ (↑n : ℕ∞)) (↑(n + 1) : ℕ∞)

Tactic:
WithTop.succ_coe

Premises used: Order.succ, ENat, WithTop.succ_coe
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ Eq (α := ℕ∞) (@SuccOrder.succ _ instPreorderENat _ ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n x : ℕ∞
top : @SuccOrder.succ _ instPreorderENat _ ⊤ = HAdd.hAdd (α := ℕ∞) ⊤ 1
coe : ∀ (a : ℕ), @SuccOrder.succ _ instPreorderENat _ (↑a : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) 1
⊢ @SuccOrder.succ _ instPreorderENat _ x = x + 1

Tactic:
cases x
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n : ℕ∞
⊢ @SuccOrder.succ _ instPreorderENat _ ⊤ = HAdd.hAdd (α := ℕ∞) ⊤ 1

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n : ℕ∞
a_1 : ℕ
⊢ @SuccOrder.succ _ instPreorderENat _ (↑a_1 : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑a_1 : ℕ∞) 1

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ Eq (α := ℕ∞) (↑0 : ℕ∞) 0

Tactic:
rfl

Premises used: WithTop.some, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ Eq (α := ℕ∞) (↑1 : ℕ∞) 1

Tactic:
rfl

Premises used: WithTop.some, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n : ℕ
⊢ (↑(m + n) : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)

Tactic:
rfl

Premises used: WithTop.map₂, WithTop.some, rfl, Option.map₂
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n : ℕ
⊢ (↑(m - n) : ℕ∞) = HSub.hSub (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)

Tactic:
rfl

Premises used: WithTop.some, WithTop.sub, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n : ℕ
⊢ (↑(m * n) : ℕ∞) = HMul.hMul (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)

Tactic:
rfl

Premises used: WithTop.some, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ∞
hm : m ≠ 0
⊢ m * ⊤ = ⊤

Tactic:
WithTop.mul_top hm

Premises used: WithTop.mul_top, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ∞
hm : m ≠ 0
⊢ ⊤ * m = ⊤

Tactic:
WithTop.top_mul hm

Premises used: WithTop.top_mul, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ∞
⊢ m * ⊤ = if m = 0 then 0 else ⊤

Tactic:
WithTop.mul_top' m

Premises used: WithTop.decidableEq._aux_1, WithTop.mul_top', ENat, instLinearOrderENat._aux_5
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ∞
⊢ ⊤ * m = if m = 0 then 0 else ⊤

Tactic:
WithTop.top_mul' m

Premises used: WithTop.top_mul', WithTop.decidableEq._aux_1, ENat, instLinearOrderENat._aux_5
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (α := ℕ∞) ⊤ n = ⊤

Tactic:
WithTop.top_pow hn

Premises used: ENat, WithTop.top_pow
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ∞
n : ℕ
⊢ a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0

Tactic:
WithTop.pow_eq_top_iff

Premises used: ENat, WithTop.pow_eq_top_iff
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ∞
n : ℕ
⊢ a ^ n ≠ ⊤ ↔ a ≠ ⊤ ∨ n = 0

Tactic:
WithTop.pow_ne_top_iff

Premises used: ENat, WithTop.pow_ne_top_iff
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ∞
n : ℕ
⊢ a ^ n < ⊤ ↔ a < ⊤ ∨ n = 0

Tactic:
WithTop.pow_lt_top_iff

Premises used: WithTop.pow_lt_top_iff
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ∞
n : ℕ
ha : a ^ n = ⊤
⊢ a = ⊤

Tactic:
WithTop.eq_top_of_pow n ha

Premises used: ENat, WithTop.eq_top_of_pow
-- Module: Mathlib.Data.ENat.Basic
Goal:
x : ℕ∞
h : x < ⊤
⊢ (↑(x.lift h) : ℕ∞) = x

Tactic:
WithTop.coe_untop x (WithTop.lt_top_iff_ne_top.mp h)

Premises used: WithTop.coe_untop, ENat, Iff.mp, ENat.lift, WithTop.lt_top_iff_ne_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
⊢ lift (↑n : ℕ∞) ⋯ = n

Tactic:
rfl

Premises used: WithTop.untop, ENat.lift, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
x : ℕ∞
h : x < ⊤
n : ℕ
⊢ x.lift h < n ↔ x < (↑n : ℕ∞)

Tactic:
WithTop.untop_lt_iff _

Premises used: WithTop.untop_lt_iff, ENat.lift
-- Module: Mathlib.Data.ENat.Basic
Goal:
x : ℕ∞
h : x < ⊤
n : ℕ
⊢ x.lift h ≤ n ↔ x ≤ (↑n : ℕ∞)

Tactic:
WithTop.untop_le_iff _

Premises used: WithTop.untop_le_iff, ENat.lift
-- Module: Mathlib.Data.ENat.Basic
Goal:
x : ℕ
n : ℕ∞
h : n < ⊤
⊢ x < n.lift h ↔ (↑x : ℕ∞) < n

Tactic:
WithTop.lt_untop_iff _

Premises used: WithTop.lt_untop_iff, ENat.lift
-- Module: Mathlib.Data.ENat.Basic
Goal:
x : ℕ
n : ℕ∞
h : n < ⊤
⊢ x ≤ n.lift h ↔ (↑x : ℕ∞) ≤ n

Tactic:
WithTop.le_untop_iff _

Premises used: WithTop.le_untop_iff, ENat.lift
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ lift 0 ⋯ = 0

Tactic:
rfl

Premises used: WithTop.untop, ENat.lift, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ lift 1 ⋯ = 1

Tactic:
rfl

Premises used: WithTop.untop, ENat.lift, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ lift (OfNat.ofNat n) ⋯ = OfNat.ofNat n

Tactic:
rfl

Premises used: WithTop.untop, ENat.lift, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : ℕ∞
⊢ a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤

Tactic:
WithTop.add_lt_top

Premises used: WithTop.add_lt_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : ℕ∞
h : a + b < ⊤
apply : Eq (α := ℕ∞) (↑((a + b).lift h) : ℕ∞) (↑(a.lift ⋯ + b.lift ⋯) : ℕ∞)
⊢ (a + b).lift h = a.lift ⋯ + b.lift ⋯

Tactic:
apply coe_inj.1

Premises used: ENat.coe_inj, Iff.mp
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : ℕ∞
h : a + b < ⊤
⊢ Eq (α := ℕ∞) (↑((a + b).lift h) : ℕ∞) (↑(a.lift ⋯ + b.lift ⋯) : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n : ℕ∞
⊢ CanLift ℕ∞ ℕ Nat.cast fun (x : ℕ∞) ↦ x ≠ ⊤

Tactic:
WithTop.canLift

Premises used: WithTop.canLift, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ (⇑toNatHom : (a : ℕ∞) → ℕ) = toNat

Tactic:
rfl

Premises used: ENat, ENat.toNat, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
⊢ (toNatHom : (a : ℕ∞) → ℕ) (↑n : ℕ∞) = toNat (↑n : ℕ∞)

Tactic:
rfl

Premises used: ENat.toNat, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
⊢ toNat (↑n : ℕ∞) = n

Tactic:
rfl

Premises used: ENat.toNat, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ toNat 0 = 0

Tactic:
rfl

Premises used: ENat.toNat, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ toNat 1 = 1

Tactic:
rfl

Premises used: ENat.toNat, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ toNat (OfNat.ofNat n) = n

Tactic:
rfl

Premises used: ENat.toNat, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ toNat ⊤ = 0

Tactic:
rfl

Premises used: ENat.toNat, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
⊢ n.toNat = 0 ↔ n = 0 ∨ n = ⊤

Tactic:
WithTop.untopD_eq_self_iff

Premises used: WithTop.some, ENat, ENat.toNat, WithTop.untopD_eq_self_iff
-- Module: Mathlib.Data.ENat.Basic
Goal:
x : ℕ∞
hx : x < ⊤
none : ∀ (hx : LT.lt (α := ℕ∞) Option.none ⊤), lift Option.none hx = toNat Option.none
some : ∀ (x : ℕ) (hx : Option.some x < ⊤), lift (Option.some x) hx = toNat (Option.some x)
⊢ x.lift hx = x.toNat

Tactic:
rcases x with ⟨⟩ | x
-- Module: Mathlib.Data.ENat.Basic
Goal:
hx : LT.lt (α := ℕ∞) none ⊤
⊢ lift none hx = toNat none

Tactic:
contradiction
-- Module: Mathlib.Data.ENat.Basic
Goal:
x : ℕ
hx : some x < ⊤
⊢ lift (some x) hx = toNat (some x)

Tactic:
rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
C : ℕ∞ → Sort u_1
d : C ⊤
f : (a : ℕ) → C (↑a : ℕ∞)
⊢ Eq (α := C 0) (recTopCoe (C := C) d f 0) (f 0)

Tactic:
rfl

Premises used: ENat.recTopCoe, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
C : ℕ∞ → Sort u_1
d : C ⊤
f : (a : ℕ) → C (↑a : ℕ∞)
⊢ Eq (α := C 1) (recTopCoe (C := C) d f 1) (f 1)

Tactic:
rfl

Premises used: ENat.recTopCoe, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
C : ℕ∞ → Sort u_1
d : C ⊤
f : (a : ℕ) → C (↑a : ℕ∞)
x : ℕ
inst : x.AtLeastTwo
⊢ Eq (α := C (OfNat.ofNat x)) (recTopCoe (C := C) d f (OfNat.ofNat x)) (f (OfNat.ofNat x))

Tactic:
rfl

Premises used: ENat.recTopCoe, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ
⊢ Ne (α := ℕ∞) ⊤ (↑a : ℕ∞)

Tactic:
nofun

Premises used: False, _private.0.ENat.top_ne_coe.match_1, Not
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ
inst : a.AtLeastTwo
⊢ Ne (α := ℕ∞) ⊤ (OfNat.ofNat a)

Tactic:
nofun

Premises used: False, _private.0.ENat.top_ne_ofNat.match_1, Not
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ Ne (α := ℕ∞) ⊤ 0

Tactic:
nofun

Premises used: False, _private.0.ENat.top_ne_zero.match_1, Not
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ Ne (α := ℕ∞) ⊤ 1

Tactic:
nofun

Premises used: False, _private.0.ENat.top_ne_one.match_1, Not
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ
⊢ Ne (α := ℕ∞) (↑a : ℕ∞) ⊤

Tactic:
nofun

Premises used: False, _private.0.ENat.coe_ne_top.match_1, Not
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ
inst : a.AtLeastTwo
⊢ Ne (α := ℕ∞) (OfNat.ofNat a) ⊤

Tactic:
nofun

Premises used: False, _private.0.ENat.ofNat_ne_top.match_1, Not
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ Ne (α := ℕ∞) 0 ⊤

Tactic:
nofun

Premises used: False, _private.0.ENat.zero_ne_top.match_1, Not
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ Ne (α := ℕ∞) 1 ⊤

Tactic:
nofun

Premises used: False, _private.0.ENat.one_ne_top.match_1, Not
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ
⊢ HSub.hSub (α := ℕ∞) ⊤ (↑a : ℕ∞) = ⊤

Tactic:
rfl

Premises used: WithTop.sub, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ HSub.hSub (α := ℕ∞) ⊤ 1 = ⊤

Tactic:
rfl

Premises used: WithTop.sub, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ
inst : a.AtLeastTwo
⊢ HSub.hSub (α := ℕ∞) ⊤ (OfNat.ofNat a) = ⊤

Tactic:
rfl

Premises used: WithTop.sub, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ LT.lt (α := ℕ∞) 0 ⊤

Tactic:
WithTop.top_pos

Premises used: WithTop.top_pos
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ LT.lt (α := ℕ∞) 1 ⊤

Tactic:
WithTop.one_lt_top

Premises used: WithTop.one_lt_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ∞
⊢ a - ⊤ = 0

Tactic:
WithTop.sub_top

Premises used: WithTop.some, ENat, WithTop.sub_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
⊢ Eq (α := ℕ∞) (↑(toNat ⊤) : ℕ∞) ⊤ ↔ Ne (α := ℕ∞) ⊤ ⊤

Tactic:
decide
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
x : ℕ
⊢ Eq (α := ℕ∞) (↑(toNat (↑x : ℕ∞)) : ℕ∞) (↑x : ℕ∞) ↔ Ne (α := ℕ∞) (↑x : ℕ∞) ⊤

Tactic:
simp [toNat_coe]

Premises used: ENat.toNat_coe
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
m : ℕ
inst : NeZero m
top : toNat ⊤ = m ↔ Eq (α := ℕ∞) ⊤ (↑m : ℕ∞)
coe : ∀ (a : ℕ), toNat (↑a : ℕ∞) = m ↔ Eq (α := ℕ∞) (↑a : ℕ∞) (↑m : ℕ∞)
⊢ n.toNat = m ↔ n = (↑m : ℕ∞)

Tactic:
cases n
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ
inst : NeZero m
⊢ toNat ⊤ = m ↔ Eq (α := ℕ∞) ⊤ (↑m : ℕ∞)

Tactic:
simpa using NeZero.ne' m

Premises used: NeZero.ne'
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ
inst : NeZero m
a : ℕ
⊢ toNat (↑a : ℕ∞) = m ↔ Eq (α := ℕ∞) (↑a : ℕ∞) (↑m : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
⊢ (↑n.toNat : ℕ∞) ≤ n

Tactic:
ENat.recTopCoe le_top (fun _ => le_rfl) n

Premises used: ENat.recTopCoe
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n : ℕ∞
hm : m ≠ ⊤
hn : n ≠ ⊤
⊢ m ≠ ⊤

Tactic:
hm
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n : ℕ∞
hm : m ≠ ⊤
hn : n ≠ ⊤
lift : ∀ (m : ℕ), ((↑m : ℕ∞) + n).toNat = toNat (↑m : ℕ∞) + n.toNat
⊢ (m + n).toNat = m.toNat + n.toNat

Tactic:
lift m to ℕ using hm
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
hn : n ≠ ⊤
m : ℕ
⊢ n ≠ ⊤

Tactic:
hn
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
hn : n ≠ ⊤
m : ℕ
lift : ∀ (n : ℕ), (HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)).toNat = toNat (↑m : ℕ∞) + toNat (↑n : ℕ∞)
⊢ ((↑m : ℕ∞) + n).toNat = toNat (↑m : ℕ∞) + n.toNat

Tactic:
lift n to ℕ using hn
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n : ℕ
⊢ (HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)).toNat = toNat (↑m : ℕ∞) + toNat (↑n : ℕ∞)

Tactic:
rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
hn : n ≠ ⊤
m : ℕ∞
⊢ n ≠ ⊤

Tactic:
hn
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
hn : n ≠ ⊤
m : ℕ∞
lift : ∀ (n : ℕ), (m - (↑n : ℕ∞)).toNat = m.toNat - toNat (↑n : ℕ∞)
⊢ (m - n).toNat = m.toNat - n.toNat

Tactic:
lift n to ℕ using hn
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ∞
n : ℕ
top : (HSub.hSub (α := ℕ∞) ⊤ (↑n : ℕ∞)).toNat = toNat ⊤ - toNat (↑n : ℕ∞)
coe : ∀ (a : ℕ), (HSub.hSub (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞)).toNat = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)
⊢ (m - (↑n : ℕ∞)).toNat = m.toNat - toNat (↑n : ℕ∞)

Tactic:
induction m
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
top : toNat ⊤ = toNat ⊤ - toNat (↑n : ℕ∞)
top₁ : 0 = 0 - toNat (↑n : ℕ∞)
top₂ top₃ : Eq (α := ℕ) 0 0
⊢ (HSub.hSub (α := ℕ∞) ⊤ (↑n : ℕ∞)).toNat = toNat ⊤ - toNat (↑n : ℕ∞)

Tactic:
rw [top_sub_coe, toNat_top, zero_tsub]

Premises used: ENat.top_sub_coe, ENat.toNat_top, zero_tsub
-- Module: Mathlib.Data.ENat.Basic
Goal:
n a : ℕ
coe : toNat (↑(a - n) : ℕ∞) = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)
coe₁ : a - n = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)
coe₂ : a - n = a - toNat (↑n : ℕ∞)
coe₃ coe₄ : a - n = a - n
⊢ (HSub.hSub (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞)).toNat = toNat (↑a : ℕ∞) - toNat (↑n : ℕ∞)

Tactic:
rw [← coe_sub, toNat_coe, toNat_coe, toNat_coe]

Premises used: ENat.coe_sub, ENat.toNat_coe
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : ℕ∞
top : (⊤ * b).toNat = toNat ⊤ * b.toNat
coe : ∀ (a : ℕ), ((↑a : ℕ∞) * b).toNat = toNat (↑a : ℕ∞) * b.toNat
⊢ (a * b).toNat = a.toNat * b.toNat

Tactic:
cases a
-- Module: Mathlib.Data.ENat.Basic
Goal:
b : ℕ∞
top : (HMul.hMul (α := ℕ∞) ⊤ ⊤).toNat = toNat ⊤ * toNat ⊤
top₁ : ∀ (a : ℕ), (HMul.hMul (α := ℕ∞) ⊤ (↑a : ℕ∞)).toNat = toNat ⊤ * toNat (↑a : ℕ∞)
⊢ (⊤ * b).toNat = toNat ⊤ * b.toNat

Tactic:
cases b
-- Module: Mathlib.Data.ENat.Basic
Goal:
b : ℕ∞
a : ℕ
coe : (HMul.hMul (α := ℕ∞) (↑a : ℕ∞) ⊤).toNat = toNat (↑a : ℕ∞) * toNat ⊤
coe₁ : ∀ (a_1 : ℕ), (HMul.hMul (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞)).toNat = toNat (↑a : ℕ∞) * toNat (↑a_1 : ℕ∞)
⊢ ((↑a : ℕ∞) * b).toNat = toNat (↑a : ℕ∞) * b.toNat

Tactic:
cases b
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ (HMul.hMul (α := ℕ∞) ⊤ ⊤).toNat = toNat ⊤ * toNat ⊤

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
b : ℕ
top : (HMul.hMul (α := ℕ∞) ⊤ (↑0 : ℕ∞)).toNat = toNat ⊤ * toNat (↑0 : ℕ∞)
top₁ : ∀ (n : ℕ), (HMul.hMul (α := ℕ∞) ⊤ (↑(n + 1) : ℕ∞)).toNat = toNat ⊤ * toNat (↑(n + 1) : ℕ∞)
⊢ (HMul.hMul (α := ℕ∞) ⊤ (↑b : ℕ∞)).toNat = toNat ⊤ * toNat (↑b : ℕ∞)

Tactic:
cases b
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ (HMul.hMul (α := ℕ∞) ⊤ (↑0 : ℕ∞)).toNat = toNat ⊤ * toNat (↑0 : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
⊢ (HMul.hMul (α := ℕ∞) ⊤ (↑(n + 1) : ℕ∞)).toNat = toNat ⊤ * toNat (↑(n + 1) : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ
coe : (HMul.hMul (α := ℕ∞) (↑0 : ℕ∞) ⊤).toNat = toNat (↑0 : ℕ∞) * toNat ⊤
coe₁ : ∀ (n : ℕ), (HMul.hMul (α := ℕ∞) (↑(n + 1) : ℕ∞) ⊤).toNat = toNat (↑(n + 1) : ℕ∞) * toNat ⊤
⊢ (HMul.hMul (α := ℕ∞) (↑a : ℕ∞) ⊤).toNat = toNat (↑a : ℕ∞) * toNat ⊤

Tactic:
cases a
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ (HMul.hMul (α := ℕ∞) (↑0 : ℕ∞) ⊤).toNat = toNat (↑0 : ℕ∞) * toNat ⊤

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
⊢ (HMul.hMul (α := ℕ∞) (↑(n + 1) : ℕ∞) ⊤).toNat = toNat (↑(n + 1) : ℕ∞) * toNat ⊤

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
a a_1 : ℕ
coe : (HMul.hMul (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞)).toNat = a * a_1
⊢ (HMul.hMul (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞)).toNat = toNat (↑a : ℕ∞) * toNat (↑a_1 : ℕ∞)

Tactic:
simp only [toNat_coe]

Premises used: ENat.toNat_coe
-- Module: Mathlib.Data.ENat.Basic
Goal:
a a_1 : ℕ
coe : toNat (↑(a * a_1) : ℕ∞) = a * a_1
coe₁ coe₂ : a * a_1 = a * a_1
⊢ (HMul.hMul (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞)).toNat = a * a_1

Tactic:
rw [← coe_mul, toNat_coe]

Premises used: ENat.coe_mul, ENat.toNat_coe
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ∞
n : ℕ
hn : n ≠ 0
top : toNat ⊤ = n ↔ Eq (α := ℕ∞) ⊤ (↑n : ℕ∞)
coe : ∀ (a : ℕ), toNat (↑a : ℕ∞) = n ↔ Eq (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞)
⊢ m.toNat = n ↔ m = (↑n : ℕ∞)

Tactic:
induction m
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
hn : n ≠ 0
⊢ toNat ⊤ = n ↔ Eq (α := ℕ∞) ⊤ (↑n : ℕ∞)

Tactic:
simp [hn.symm]

Premises used: Ne.symm
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ toNat (↑a : ℕ∞) = n ↔ Eq (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞)

Tactic:
simp [hn.symm]

Premises used: Ne.symm
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ∞
n : ℕ
h : m ≤ (↑n : ℕ∞)
⊢ m ≠ ⊤

Tactic:
ne_top_of_le_ne_top (coe_ne_top n) h

Premises used: ne_top_of_le_ne_top, ENat.coe_ne_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ∞
n : ℕ
h : m ≤ (↑n : ℕ∞)
lift : ∀ (m : ℕ) (h : LE.le (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)), toNat (↑m : ℕ∞) ≤ n
⊢ m.toNat ≤ n

Tactic:
lift m to ℕ using ne_top_of_le_ne_top (coe_ne_top n) h

Premises used: ne_top_of_le_ne_top, ENat.coe_ne_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
n m : ℕ
h : LE.le (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)
⊢ toNat (↑m : ℕ∞) ≤ n

Tactic:
simpa using h
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n : ℕ∞
h : m ≤ n
hn : n ≠ ⊤
⊢ m.toNat ≤ n.toNat

Tactic:
toNat_le_of_le_coe <| h.trans_eq (coe_toNat hn).symm

Premises used: LE.le.trans_eq, ENat.coe_toNat, ENat.toNat_le_of_le_coe, Eq.symm
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ∞
⊢ Order.succ m = m + 1

Tactic:
Order.succ_eq_add_one m

Premises used: Order.succ_eq_add_one
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n : ℕ∞
hm : m ≠ ⊤
⊢ m + 1 ≤ n ↔ m < n

Tactic:
Order.add_one_le_iff_of_not_isMax (not_isMax_iff_ne_top.mpr hm)

Premises used: Iff.mpr, Order.add_one_le_iff_of_not_isMax, not_isMax_iff_ne_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n : ℕ∞
hn : n ≠ ⊤
inl : HAdd.hAdd (α := ℕ∞) ⊤ 1 ≤ n ↔ ⊤ < n
inr : ∀ (hm : m ≠ ⊤), m + 1 ≤ n ↔ m < n
⊢ m + 1 ≤ n ↔ m < n

Tactic:
rcases eq_or_ne m ⊤ with rfl | hm

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
hn : n ≠ ⊤
⊢ HAdd.hAdd (α := ℕ∞) ⊤ 1 ≤ n ↔ ⊤ < n

Tactic:
simpa
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n : ℕ∞
hn : n ≠ ⊤
hm : m ≠ ⊤
⊢ m + 1 ≤ n ↔ m < n

Tactic:
add_one_le_iff hm

Premises used: ENat.add_one_le_iff