awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n : ℕ∞
hn : n ≠ ⊤
hm : m ≠ ⊤
⊢ m + 1 ≤ n ↔ m < n

Tactic:
exact add_one_le_iff hm

Premises used: ENat.add_one_le_iff
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
⊢ 1 ≤ n ↔ n ≠ 0

Tactic:
Order.one_le_iff_pos.trans pos_iff_ne_zero

Premises used: Iff.trans, pos_iff_ne_zero, Order.one_le_iff_pos
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
⊢ n < 1 ↔ n = 0

Tactic:
not_le.symm.trans one_le_iff_ne_zero.not_left

Premises used: not_le, Iff.not_left, Iff.trans, Iff.symm, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
h : n = 0 ∨ n = 1
inl : n = 0 → n ≤ 1
inr : n = 1 → n ≤ 1
⊢ n ≤ 1

Tactic:
cases h
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
h : n = 0
⊢ n ≤ 1

Tactic:
simp_all
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
h : n = 1
⊢ n ≤ 1

Tactic:
simp_all
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
refine : ∀ (h : n ≤ 1), n = 0 ∨ n = 1
⊢ n ≤ 1 ↔ n = 0 ∨ n = 1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by cases h <;> simp_all⟩
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
h : n ≤ 1
top : ∀ (h : LE.le (α := ℕ∞) ⊤ 1), Eq (α := ℕ∞) ⊤ 0 ∨ Eq (α := ℕ∞) ⊤ 1
coe : ∀ (a : ℕ) (h : LE.le (α := ℕ∞) (↑a : ℕ∞) 1), Eq (α := ℕ∞) (↑a : ℕ∞) 0 ∨ Eq (α := ℕ∞) (↑a : ℕ∞) 1
⊢ n = 0 ∨ n = 1

Tactic:
cases n
-- Module: Mathlib.Data.ENat.Basic
Goal:
h : LE.le (α := ℕ∞) ⊤ 1
⊢ Eq (α := ℕ∞) ⊤ 0 ∨ Eq (α := ℕ∞) ⊤ 1

Tactic:
simp at h
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ
h : LE.le (α := ℕ∞) (↑a : ℕ∞) 1
coe : LT.lt (α := ℕ∞) (↑a : ℕ∞) 1 ∨ Eq (α := ℕ∞) (↑a : ℕ∞) 1
coe₁ coe₂ coe₃ coe₄ : LE.le (α := ℕ∞) (↑a : ℕ∞) 1
⊢ Eq (α := ℕ∞) (↑a : ℕ∞) 0 ∨ Eq (α := ℕ∞) (↑a : ℕ∞) 1

Tactic:
rwa [← lt_one_iff_eq_zero, ← le_iff_lt_or_eq]

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

Tactic:
Order.lt_add_one_iff_of_not_isMax (not_isMax_iff_ne_top.mpr hm)

Premises used: Iff.mpr, Order.lt_add_one_iff_of_not_isMax, not_isMax_iff_ne_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n k : ℕ∞
h : k ≠ ⊤
⊢ k + n ≤ k + m ↔ n ≤ m

Tactic:
WithTop.add_le_add_iff_left h

Premises used: WithTop.add_le_add_iff_left
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n k : ℕ∞
h : k ≠ ⊤
⊢ n + k ≤ m + k ↔ n ≤ m

Tactic:
WithTop.add_le_add_iff_right h

Premises used: WithTop.add_le_add_iff_right
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n : ℕ∞
hm : m ≠ ⊤
rw : m + 1 ≤ n + 1 ↔ m ≤ n
rw₁ rw₂ : m ≤ n ↔ m ≤ n
⊢ m < n + 1 ↔ m ≤ n

Tactic:
rw [← add_one_le_iff hm, add_le_add_iff_right one_ne_top]

Premises used: ENat.one_ne_top, ENat.add_one_le_iff, ENat.add_le_add_iff_right
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ∞
n : ℕ
⊢ m < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ m ≤ (↑n : ℕ∞)

Tactic:
lt_add_one_iff (coe_ne_top n)

Premises used: ENat.lt_add_one_iff, ENat.coe_ne_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
k : ℕ
⊢ n ≤ (↑k : ℕ∞) ↔ ∃ (n₀ : ℕ), n = (↑n₀ : ℕ∞) ∧ n₀ ≤ k

Tactic:
WithTop.le_coe_iff

Premises used: WithTop.le_coe_iff, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
⊢ ¬n < 0

Tactic:
not_lt_zero

Premises used: not_lt_zero
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) ⊤

Tactic:
WithTop.coe_lt_top n

Premises used: WithTop.coe_lt_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
n m : ℕ
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞) ↔ n < m

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
n m : ℕ
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞) ↔ n ≤ m

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
motive : ℕ∞ → Prop
a : ℕ∞
zero : motive 0
succ : ∀ (n : ℕ), motive (↑n : ℕ∞) → motive (↑n.succ : ℕ∞)
top : (∀ (n : ℕ), motive (↑n : ℕ∞)) → motive ⊤
have : ∀ (A : ∀ (n : ℕ), motive (↑n : ℕ∞)), motive a
⊢ motive a

Tactic:
have A : ∀ n : ℕ, motive n := fun n => Nat.recOn n zero succ
-- Module: Mathlib.Data.ENat.Basic
Goal:
motive : ℕ∞ → Prop
a : ℕ∞
zero : motive 0
succ : ∀ (n : ℕ), motive (↑n : ℕ∞) → motive (↑n.succ : ℕ∞)
top : (∀ (n : ℕ), motive (↑n : ℕ∞)) → motive ⊤
A : ∀ (n : ℕ), motive (↑n : ℕ∞)
top₁ : motive ⊤
coe : ∀ (a : ℕ), motive (↑a : ℕ∞)
⊢ motive a

Tactic:
cases a
-- Module: Mathlib.Data.ENat.Basic
Goal:
motive : ℕ∞ → Prop
zero : motive 0
succ : ∀ (n : ℕ), motive (↑n : ℕ∞) → motive (↑n.succ : ℕ∞)
top : (∀ (n : ℕ), motive (↑n : ℕ∞)) → motive ⊤
A : ∀ (n : ℕ), motive (↑n : ℕ∞)
⊢ motive ⊤

Tactic:
top A
-- Module: Mathlib.Data.ENat.Basic
Goal:
motive : ℕ∞ → Prop
zero : motive 0
succ : ∀ (n : ℕ), motive (↑n : ℕ∞) → motive (↑n.succ : ℕ∞)
top : (∀ (n : ℕ), motive (↑n : ℕ∞)) → motive ⊤
A : ∀ (n : ℕ), motive (↑n : ℕ∞)
⊢ motive ⊤

Tactic:
exact top A
-- Module: Mathlib.Data.ENat.Basic
Goal:
motive : ℕ∞ → Prop
zero : motive 0
succ : ∀ (n : ℕ), motive (↑n : ℕ∞) → motive (↑n.succ : ℕ∞)
top : (∀ (n : ℕ), motive (↑n : ℕ∞)) → motive ⊤
A : ∀ (n : ℕ), motive (↑n : ℕ∞)
a : ℕ
⊢ motive (↑a : ℕ∞)

Tactic:
A _
-- Module: Mathlib.Data.ENat.Basic
Goal:
motive : ℕ∞ → Prop
zero : motive 0
succ : ∀ (n : ℕ), motive (↑n : ℕ∞) → motive (↑n.succ : ℕ∞)
top : (∀ (n : ℕ), motive (↑n : ℕ∞)) → motive ⊤
A : ∀ (n : ℕ), motive (↑n : ℕ∞)
a : ℕ
⊢ motive (↑a : ℕ∞)

Tactic:
exact A _
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
⊢ 0 < n + 1

Tactic:
succ_def n ▸ Order.bot_lt_succ n

Premises used: Eq.rec, ENat.succ_def, Order.bot_lt_succ
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
rw : n < n + 1
⊢ (↑n : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, coe_lt_coe]

Premises used: Nat.cast_add, ENat.coe_lt_coe, Nat.cast_one
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
⊢ n < n + 1

Tactic:
lt_add_one n

Premises used: lt_add_one
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
⊢ n < n + 1

Tactic:
exact lt_add_one n

Premises used: lt_add_one
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n k : ℕ∞
h : k ≠ ⊤
⊢ n + k < m + k ↔ n < m

Tactic:
WithTop.add_lt_add_iff_right h

Premises used: WithTop.add_lt_add_iff_right
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n k : ℕ∞
h : k ≠ ⊤
⊢ k + n < k + m ↔ n < m

Tactic:
WithTop.add_lt_add_iff_left h

Premises used: WithTop.add_lt_add_iff_left
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d : ℕ∞
hac : a < c
hbd : b < d
⊢ a + b < c + d

Tactic:
WithTop.add_lt_add hac hbd

Premises used: WithTop.add_lt_add
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d : ℕ∞
⊢ a ≠ ⊤ → a ≤ b → c < d → a + c < b + d

Tactic:
WithTop.add_lt_add_of_le_of_lt

Premises used: ENat, WithTop.add_lt_add_of_le_of_lt
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d : ℕ∞
⊢ c ≠ ⊤ → a < b → c ≤ d → a + c < b + d

Tactic:
WithTop.add_lt_add_of_lt_of_le

Premises used: WithTop.add_lt_add_of_lt_of_le, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
⊢ n ≠ ⊤ ↔ ∃ (m : ℕ), (↑m : ℕ∞) = n

Tactic:
WithTop.ne_top_iff_exists

Premises used: WithTop.ne_top_iff_exists, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
⊢ n = ⊤ ↔ ∀ (m : ℕ), (↑m : ℕ∞) ≠ n

Tactic:
WithTop.eq_top_iff_forall_ne

Premises used: WithTop.eq_top_iff_forall_ne, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
p : ℕ∞ → Prop
⊢ (∀ (x : ℕ∞), x ≠ ⊤ → p x) ↔ ∀ (x : ℕ), p (↑x : ℕ∞)

Tactic:
WithTop.forall_ne_top

Premises used: ENat, WithTop.forall_ne_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
p : ℕ∞ → Prop
⊢ (∃ (x : ℕ∞), x ≠ ⊤ ∧ p x) ↔ ∃ (x : ℕ), p (↑x : ℕ∞)

Tactic:
WithTop.exists_ne_top

Premises used: ENat, WithTop.exists_ne_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
⊢ n = ⊤ ↔ ∀ (m : ℕ), (↑m : ℕ∞) < n

Tactic:
WithTop.eq_top_iff_forall_gt

Premises used: WithTop.eq_top_iff_forall_gt, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
⊢ n = ⊤ ↔ ∀ (m : ℕ), (↑m : ℕ∞) ≤ n

Tactic:
WithTop.eq_top_iff_forall_ge

Premises used: WithTop.eq_top_iff_forall_ge, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n : ℕ∞
⊢ (∀ (a : ℕ), (↑a : ℕ∞) ≤ m → (↑a : ℕ∞) ≤ n) ↔ m ≤ n

Tactic:
WithTop.forall_coe_le_iff_le

Premises used: WithTop.forall_coe_le_iff_le
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n : ℕ∞
hm : ∀ (a : ℕ), (↑a : ℕ∞) ≤ m ↔ (↑a : ℕ∞) ≤ n
⊢ m = n

Tactic:
WithTop.eq_of_forall_coe_le_iff hm

Premises used: ENat, WithTop.eq_of_forall_coe_le_iff
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
hn : n ≠ ⊤
simp_rw : ∃ (m : ℕ), ¬(↑m : ℕ∞) ≤ n
⊢ ∃ (m : ℕ), n < (↑m : ℕ∞)

Tactic:
simp_rw [lt_iff_not_ge]

Premises used: lt_iff_not_ge
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
hn : n ≠ ⊤
⊢ ∃ (m : ℕ), ¬(↑m : ℕ∞) ≤ n

Tactic:
not_forall.mp <| eq_top_iff_forall_ge.2.mt hn

Premises used: Iff.mpr, Function.mt, Iff.mp, ENat.eq_top_iff_forall_ge, Classical.not_forall
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
hn : n ≠ ⊤
⊢ ∃ (m : ℕ), ¬(↑m : ℕ∞) ≤ n

Tactic:
exact not_forall.mp <| eq_top_iff_forall_ge.2.mt hn

Premises used: Iff.mpr, Function.mt, Iff.mp, ENat.eq_top_iff_forall_ge, Classical.not_forall
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : ℕ∞
⊢ a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

Tactic:
WithTop.sub_eq_top_iff

Premises used: WithTop.sub_eq_top_iff, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : ℕ∞
⊢ a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤

Tactic:
WithTop.sub_ne_top_iff

Premises used: WithTop.sub_ne_top_iff, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ∞
⊢ a ≠ ⊤ → AddLECancellable a

Tactic:
WithTop.addLECancellable_of_ne_top

Premises used: ENat, WithTop.addLECancellable_of_ne_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ∞
⊢ a < ⊤ → AddLECancellable a

Tactic:
WithTop.addLECancellable_of_lt_top

Premises used: ENat, WithTop.addLECancellable_of_lt_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ
⊢ AddLECancellable (α := ℕ∞) (↑a : ℕ∞)

Tactic:
WithTop.addLECancellable_coe _

Premises used: WithTop.addLECancellable_coe, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c : ℕ∞
ha : a ≠ ⊤
⊢ a + b ≤ c → b ≤ c - a

Tactic:
(addLECancellable_of_ne_top ha).le_tsub_of_add_le_left

Premises used: ENat.addLECancellable_of_ne_top, AddLECancellable.le_tsub_of_add_le_left
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c : ℕ∞
hb : b ≠ ⊤
⊢ a + b ≤ c → a ≤ c - b

Tactic:
(addLECancellable_of_ne_top hb).le_tsub_of_add_le_right

Premises used: AddLECancellable.le_tsub_of_add_le_right, ENat.addLECancellable_of_ne_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : ℕ∞
h : a < b
top : ∀ (h : a < ⊤), a ≤ HSub.hSub (α := ℕ∞) ⊤ 1
coe : ∀ (a_1 : ℕ) (h : a < (↑a_1 : ℕ∞)), a ≤ HSub.hSub (α := ℕ∞) (↑a_1 : ℕ∞) 1
⊢ a ≤ b - 1

Tactic:
cases b
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ∞
h : a < ⊤
⊢ a ≤ HSub.hSub (α := ℕ∞) ⊤ 1

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ∞
a_1 : ℕ
h : a < (↑a_1 : ℕ∞)
⊢ a ≤ HSub.hSub (α := ℕ∞) (↑a_1 : ℕ∞) 1

Tactic:
ENat.le_sub_of_add_le_right one_ne_top <| lt_coe_add_one_iff.mp <| lt_tsub_iff_right.mp h

Premises used: ENat.le_sub_of_add_le_right, lt_tsub_iff_right, ENat.one_ne_top, Iff.mp, ENat.lt_coe_add_one_iff
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ∞
a_1 : ℕ
h : a < (↑a_1 : ℕ∞)
⊢ a ≤ HSub.hSub (α := ℕ∞) (↑a_1 : ℕ∞) 1

Tactic:
exact ENat.le_sub_of_add_le_right one_ne_top <| lt_coe_add_one_iff.mp <| lt_tsub_iff_right.mp h

Premises used: ENat.le_sub_of_add_le_right, lt_tsub_iff_right, ENat.one_ne_top, Iff.mp, ENat.lt_coe_add_one_iff
-- Module: Mathlib.Data.ENat.Basic
Goal:
n k : ℕ∞
h : n ≠ ⊤
h' : 0 < k
⊢ n < k + n

Tactic:
calc
    _ = 0 + n := (zero_add n).symm
    _ < k + n := (add_lt_add_iff_right h).mpr h'

Premises used: Iff.mpr, Trans.trans, zero_add, Eq.symm, ENat.add_lt_add_iff_right
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : ℕ∞
h : a ≠ ⊤
h2 : b ≤ a
⊢ a - (a - b) = b

Tactic:
(addLECancellable_of_ne_top <| ne_top_of_le_ne_top h tsub_le_self).tsub_tsub_cancel_of_le h2

Premises used: tsub_le_self, ne_top_of_le_ne_top, ENat.addLECancellable_of_ne_top, AddLECancellable.tsub_tsub_cancel_of_le
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
hn : n ≠ ⊤
a b : ℕ∞
e : Eq (α := ℕ∞) ((fun (x : ℕ∞) ↦ x + n) a) ((fun (x : ℕ∞) ↦ x + n) b)
⊢ a = b

Tactic:
le_antisymm
    ((WithTop.add_le_add_iff_right hn).mp e.le)
    ((WithTop.add_le_add_iff_right hn).mp e.ge)

Premises used: Eq.ge, Eq.le, le_antisymm, Iff.mp, WithTop.add_le_add_iff_right
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
hn : n ≠ ⊤
a b : ℕ∞
e : Eq (α := ℕ∞) ((fun (x : ℕ∞) ↦ x + n) a) ((fun (x : ℕ∞) ↦ x + n) b)
⊢ a = b

Tactic:
exact le_antisymm
    ((WithTop.add_le_add_iff_right hn).mp e.le)
    ((WithTop.add_le_add_iff_right hn).mp e.ge)

Premises used: Eq.ge, Eq.le, le_antisymm, Iff.mp, WithTop.add_le_add_iff_right
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
hn : n ≠ ⊤
simp_rw : Injective (β := ℕ∞) fun (x : ℕ∞) ↦ x + n
⊢ Injective (β := ℕ∞) fun (x : ℕ∞) ↦ n + x

Tactic:
simp_rw [add_comm n _]

Premises used: add_comm
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
hn : n ≠ ⊤
⊢ Injective (β := ℕ∞) fun (x : ℕ∞) ↦ x + n

Tactic:
add_left_injective_of_ne_top hn

Premises used: ENat.add_left_injective_of_ne_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
hn : n ≠ ⊤
⊢ Injective (β := ℕ∞) fun (x : ℕ∞) ↦ x + n

Tactic:
exact add_left_injective_of_ne_top hn

Premises used: ENat.add_left_injective_of_ne_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ∞
ha : a ≠ 0
h_top : a ≠ ⊤
⊢ StrictMono (β := ℕ∞) fun (x : ℕ∞) ↦ a * x

Tactic:
WithTop.mul_right_strictMono (pos_iff_ne_zero.2 ha) h_top

Premises used: Iff.mpr, ENat, pos_iff_ne_zero, WithTop.mul_right_strictMono
-- Module: Mathlib.Data.ENat.Basic
Goal:
a : ℕ∞
ha : a ≠ 0
h_top : a ≠ ⊤
⊢ StrictMono (β := ℕ∞) fun (x : ℕ∞) ↦ x * a

Tactic:
WithTop.mul_left_strictMono (pos_iff_ne_zero.2 ha) h_top

Premises used: Iff.mpr, ENat, WithTop.mul_left_strictMono, pos_iff_ne_zero
-- Module: Mathlib.Data.ENat.Basic
Goal:
a x y : ℕ∞
ha : a ≠ 0
h_top : a ≠ ⊤
⊢ a * x ≤ a * y ↔ x ≤ y

Tactic:
(ENat.mul_right_strictMono ha h_top).le_iff_le

Premises used: StrictMono.le_iff_le, ENat.mul_right_strictMono
-- Module: Mathlib.Data.ENat.Basic
Goal:
a x y : ℕ∞
ha : a ≠ 0
h_top : a ≠ ⊤
⊢ x * a ≤ y * a ↔ x ≤ y

Tactic:
(ENat.mul_left_strictMono ha h_top).le_iff_le

Premises used: ENat.mul_left_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Data.ENat.Basic
Goal:
a x y : ℕ∞
hxy : x ≤ y
ha : a ≠ 0
h_top : a ≠ ⊤
⊢ x * a ≤ y * a

Tactic:
simpa [ha, h_top]
-- Module: Mathlib.Data.ENat.Basic
Goal:
c a : ℕ∞
hc : c ≠ 0
inl : ⊤ ≤ ⊤ * c
inr : ∀ (hne : a ≠ ⊤), a ≤ a * c
⊢ a ≤ a * c

Tactic:
obtain rfl | hne := eq_or_ne a ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
c : ℕ∞
hc : c ≠ 0
⊢ ⊤ ≤ ⊤ * c

Tactic:
simp [top_mul hc]

Premises used: ENat.top_mul
-- Module: Mathlib.Data.ENat.Basic
Goal:
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
inr : ∀ (hne : Ne (α := ℕ∞) 0 ⊤), 0 ≤ 0 * c
inr₁ : ∀ (h0 : a ≠ 0), a ≤ a * c
⊢ a ≤ a * c

Tactic:
obtain rfl | h0 := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
c : ℕ∞
hc : c ≠ 0
hne : Ne (α := ℕ∞) 0 ⊤
⊢ 0 ≤ 0 * c

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
h0 : a ≠ 0
inr : c ≠ 0
⊢ a ≤ a * c

Tactic:
nth_rewrite 1 [← mul_one a, ENat.mul_le_mul_left_iff h0 hne, ENat.one_le_iff_ne_zero]

Premises used: mul_one, ENat.mul_le_mul_left_iff, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Data.ENat.Basic
Goal:
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
h0 : a ≠ 0
⊢ c ≠ 0

Tactic:
assumption
-- Module: Mathlib.Data.ENat.Basic
Goal:
c a : ℕ∞
hc : c ≠ 0
rw : a ≤ a * c
⊢ a ≤ c * a

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.ENat.Basic
Goal:
c a : ℕ∞
hc : c ≠ 0
⊢ a ≤ a * c

Tactic:
ENat.self_le_mul_right a hc

Premises used: ENat.self_le_mul_right
-- Module: Mathlib.Data.ENat.Basic
Goal:
c a : ℕ∞
hc : c ≠ 0
⊢ a ≤ a * c

Tactic:
exact ENat.self_le_mul_right a hc

Premises used: ENat.self_le_mul_right
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
⊢ (↑x : ℕ∞) * x.inv = 1

Tactic:
have := x.val_inv
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : (↑x : ℕ∞) * x.inv = 1
h : (↑x : ℕ∞) = ⊤
⊢ False

Tactic:
simp [h] at this
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : (↑x : ℕ∞) * x.inv = 1
⊢ (↑x : ℕ∞) ≠ ⊤

Tactic:
have x_top : x.val ≠ ⊤ := by
      intro h
      simp [h] at this
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : (↑x : ℕ∞) * x.inv = 1
x_top : (↑x : ℕ∞) ≠ ⊤
h : x.inv = ⊤
⊢ False

Tactic:
simp only [h, ne_eq, x.ne_zero, not_false_eq_true, mul_top, top_ne_one] at this

Premises used: ENat.top_ne_one, Units.ne_zero, ne_eq, ENat.mul_top, not_false_eq_true
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : (↑x : ℕ∞) * x.inv = 1
x_top : (↑x : ℕ∞) ≠ ⊤
⊢ x.inv ≠ ⊤

Tactic:
have x_inv_top : x.inv ≠ ⊤ := by
      intro h
      simp only [h, ne_eq, x.ne_zero, not_false_eq_true, mul_top, top_ne_one] at this
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : (↑x : ℕ∞) * x.inv = 1
x_top : (↑x : ℕ∞) ≠ ⊤
x_inv_top : x.inv ≠ ⊤
obtain : ∀ (y : ℕ) (x_y : (↑y : ℕ∞) = (↑x : ℕ∞)), x = default
⊢ x = default

Tactic:
obtain ⟨y, x_y⟩ := ne_top_iff_exists.1 x_top

Premises used: ENat.ne_top_iff_exists, Iff.mp
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : (↑x : ℕ∞) * x.inv = 1
x_top : (↑x : ℕ∞) ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y : ℕ
x_y : (↑y : ℕ∞) = (↑x : ℕ∞)
obtain : ∀ (z : ℕ) (x_z : (↑z : ℕ∞) = x.inv), x = default
⊢ x = default

Tactic:
obtain ⟨z, x_z⟩ := ne_top_iff_exists.1 x_inv_top

Premises used: ENat.ne_top_iff_exists, Iff.mp
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : (↑x : ℕ∞) * x.inv = 1
x_top : (↑x : ℕ∞) ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y : ℕ
x_y : (↑y : ℕ∞) = (↑x : ℕ∞)
z : ℕ
x_z : (↑z : ℕ∞) = x.inv
⊢ (↑x : ℕ∞) = (↑y : ℕ∞)

Tactic:
replace x_y := x_y.symm
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : (↑x : ℕ∞) * x.inv = 1
x_top : (↑x : ℕ∞) ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
x_z : (↑z : ℕ∞) = x.inv
x_y : (↑x : ℕ∞) = (↑y : ℕ∞)
rw : ∀ (z : ℕ) (this : y = 1 ∧ z = 1) (x_z : (↑z : ℕ∞) = x.inv) (x_y : (↑x : ℕ∞) = (↑y : ℕ∞)), x = default
⊢ x = default

Tactic:
rw [x_y, ← x_z, ← coe_mul, ← coe_one, coe_inj, _root_.mul_eq_one] at this

Premises used: ENat.coe_one, ENat.coe_mul, ENat.coe_inj, mul_eq_one
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
x_top : (↑x : ℕ∞) ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
this : y = 1 ∧ z = 1
x_z : (↑z : ℕ∞) = x.inv
x_y : (↑x : ℕ∞) = (↑y : ℕ∞)
rwa : ∀ (x_y : (↑x : ℕ∞) = (↑1 : ℕ∞)), x = default
rwa₁ : ∀ (x_y : (↑x : ℕ∞) = 1), x = default
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (x_y : x = 1), x = default
⊢ x = default

Tactic:
rwa [this.1, Nat.cast_one, Units.val_eq_one] at x_y

Premises used: And.left, Units.val_eq_one, Nat.cast_one
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ
n : WithTop ℕ∞
h : LT.lt (α := WithTop ℕ∞) (↑m : WithTop ℕ∞) ⊤
⊢ LE.le (α := WithTop ℕ∞) (↑(m + 1) : WithTop ℕ∞) ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ
n : WithTop ℕ∞
h : LT.lt (α := WithTop ℕ∞) (↑m : WithTop ℕ∞) ⊤
⊢ LE.le (α := WithTop ℕ∞) (↑(m + 1) : WithTop ℕ∞) ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ
n : WithTop ℕ∞
h : LT.lt (α := WithTop ℕ∞) (↑m : WithTop ℕ∞) (↑⊤ : WithTop ℕ∞)
⊢ LE.le (α := WithTop ℕ∞) (↑(m + 1) : WithTop ℕ∞) (↑⊤ : WithTop ℕ∞)

Tactic:
WithTop.coe_le_coe.2 (OrderTop.le_top _)

Premises used: Iff.mpr, OrderTop.le_top, WithTop.coe_le_coe
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ
n : WithTop ℕ∞
h : LT.lt (α := WithTop ℕ∞) (↑m : WithTop ℕ∞) (↑⊤ : WithTop ℕ∞)
⊢ LE.le (α := WithTop ℕ∞) (↑(m + 1) : WithTop ℕ∞) (↑⊤ : WithTop ℕ∞)

Tactic:
exact WithTop.coe_le_coe.2 (OrderTop.le_top _)

Premises used: Iff.mpr, OrderTop.le_top, WithTop.coe_le_coe
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ
n_1 : WithTop ℕ∞
n : ℕ
h : LT.lt (α := WithTop ℕ∞) (↑m : WithTop ℕ∞) (↑n : WithTop ℕ∞)
⊢ LE.le (α := WithTop ℕ∞) (↑(m + 1) : WithTop ℕ∞) (↑n : WithTop ℕ∞)

Tactic:
simpa only [Nat.cast_le, ge_iff_le, Nat.cast_lt] using h

Premises used: ge_iff_le, Nat.cast_le, Nat.cast_lt
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ
n : WithTop ℕ∞
h : (↑m : WithTop ℕ∞) < n
⊢ (↑(m + 1) : WithTop ℕ∞) ≤ n

Tactic:
match n with
  | ⊤ => exact le_top
  | (⊤ : ℕ∞) => exact WithTop.coe_le_coe.2 (OrderTop.le_top _)
  | (n : ℕ) => simpa only [Nat.cast_le, ge_iff_le, Nat.cast_lt] using h
-- Module: Mathlib.Data.ENat.Basic
Goal:
⊢ HAdd.hAdd (α := WithTop ℕ∞) (↑⊤ : WithTop ℕ∞) 1 = (↑⊤ : WithTop ℕ∞)

Tactic:
rfl

Premises used: WithTop.map₂, WithTop.some, rfl, Option.map₂
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : WithTop ℕ∞
⊢ HAdd.hAdd (α := WithTop ℕ∞) ⊤ 1 = (↑⊤ : WithTop ℕ∞) ↔ Eq (α := WithTop ℕ∞) ⊤ (↑⊤ : WithTop ℕ∞)

Tactic:
Iff.rfl

Premises used: Iff.rfl, WithTop.map₂, Option.map₂
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : WithTop ℕ∞
⊢ HAdd.hAdd (α := WithTop ℕ∞) ⊤ 1 = (↑⊤ : WithTop ℕ∞) ↔ Eq (α := WithTop ℕ∞) ⊤ (↑⊤ : WithTop ℕ∞)

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : WithTop ℕ∞
⊢ HAdd.hAdd (α := WithTop ℕ∞) (↑⊤ : WithTop ℕ∞) 1 = (↑⊤ : WithTop ℕ∞) ↔
    Eq (α := WithTop ℕ∞) (↑⊤ : WithTop ℕ∞) (↑⊤ : WithTop ℕ∞)

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
n_1 : WithTop ℕ∞
n : ℕ
norm_cast : Eq (α := ℕ∞) (↑(n + 1) : ℕ∞) ⊤ ↔ Eq (α := ℕ∞) (↑n : ℕ∞) ⊤
⊢ HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1 = (↑⊤ : WithTop ℕ∞) ↔
    Eq (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) (↑⊤ : WithTop ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.Data.ENat.Basic
Goal:
n_1 : WithTop ℕ∞
n : ℕ
⊢ Eq (α := ℕ∞) (↑(n + 1) : ℕ∞) ⊤ ↔ Eq (α := ℕ∞) (↑n : ℕ∞) ⊤

Tactic:
simp only [coe_ne_top]

Premises used: ENat.coe_ne_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : WithTop ℕ∞
⊢ n + 1 = (↑⊤ : WithTop ℕ∞) ↔ n = (↑⊤ : WithTop ℕ∞)

Tactic:
match n with
  | ⊤ => exact Iff.rfl
  | (⊤ : ℕ∞) => simp
  | (n : ℕ) =>
    norm_cast
    simp only [coe_ne_top]
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
⊢ Ne (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) (↑⊤ : WithTop ℕ∞)

Tactic:
nofun

Premises used: False, _private.0.ENat.natCast_ne_coe_top.match_1, Not
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : WithTop ℕ∞
⊢ 1 ≤ n ↔ n ≠ 0

Tactic:
⟨fun h ↦ (zero_lt_one.trans_le h).ne',
    fun h ↦ add_one_natCast_le_withTop_of_lt (pos_iff_ne_zero.mpr h)⟩

Premises used: Iff.mpr, ENat.add_one_natCast_le_withTop_of_lt, LT.lt.ne', zero_lt_one, LT.lt.trans_le, Iff.intro, pos_iff_ne_zero
-- Module: Mathlib.Data.ENat.Basic
Goal:
N : WithTop ℕ∞
hN : (↑⊤ : WithTop ℕ∞) ≤ N
n : ℕ
⊢ (↑n : WithTop ℕ∞) ≤ N

Tactic:
le_trans (mod_cast le_top) hN

Premises used: le_trans
-- Module: Mathlib.Data.ENat.Basic
Goal:
N : WithTop ℕ∞
hN : (↑⊤ : WithTop ℕ∞) ≤ N
n : ℕ
⊢ (↑n : WithTop ℕ∞) < N

Tactic:
lt_of_lt_of_le (mod_cast lt_add_one n) (natCast_le_of_coe_top_le_withTop hN (n + 1))

Premises used: ENat.natCast_le_of_coe_top_le_withTop, HAdd.hAdd, OfNat.ofNat, lt_of_lt_of_le
-- Module: Mathlib.Data.ENat.Basic
Goal:
α : Type u_1
f : ℕ → α
⊢ map f ⊤ = ⊤

Tactic:
rfl

Premises used: WithTop.map, ENat.map, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
α : Type u_1
f : ℕ → α
a : ℕ
⊢ map f (↑a : ℕ∞) = (↑(f a) : WithTop α)

Tactic:
rfl

Premises used: WithTop.map, WithTop.some, ENat.map, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
α : Type u_1
f : ℕ → α
⊢ map f 0 = (↑(f 0) : WithTop α)

Tactic:
rfl

Premises used: WithTop.map, WithTop.some, ENat.map, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
α : Type u_1
f : ℕ → α
⊢ map f 1 = (↑(f 1) : WithTop α)

Tactic:
rfl

Premises used: WithTop.map, WithTop.some, ENat.map, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
α : Type u_1
f : ℕ → α
n : ℕ
inst : n.AtLeastTwo
⊢ map f (OfNat.ofNat n) = (↑(f n) : WithTop α)

Tactic:
rfl

Premises used: WithTop.map, WithTop.some, ENat.map, rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
α : Type u_1
f : ℕ → α
⊢ map f n = ⊤ ↔ n = ⊤

Tactic:
WithTop.map_eq_top_iff

Premises used: WithTop.map_eq_top_iff, ENat.map, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
α : Type u_1
f : ℕ → α
inst : Preorder α
⊢ StrictMono (map f) ↔ StrictMono f

Tactic:
WithTop.strictMono_map_iff

Premises used: WithTop.strictMono_map_iff, ENat.map, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
α : Type u_1
f : ℕ → α
inst : Preorder α
⊢ Monotone (map f) ↔ Monotone f

Tactic:
WithTop.monotone_map_iff

Premises used: WithTop.monotone_map_iff, ENat.map, ENat
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
top : LE.le.{u_1} (α := WithTop α) 0 (map Nat.cast ⊤)
coe : ∀ (a : ℕ), LE.le.{u_1} (α := WithTop α) 0 (map Nat.cast (↑a : ℕ∞))
⊢ LE.le.{u_1} (α := WithTop α) 0 (map Nat.cast n)

Tactic:
cases n