awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Upto
Goal:
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) fun (y : Upto p) ↦ x - (↑y : ℕ)
⊢ WellFounded (α := Upto p) (InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) fun (y : Upto p) ↦ x - (↑y : ℕ))

Tactic:
exact (measure _).wf

Premises used: WellFoundedRelation.wf
-- Module: Mathlib.Data.Nat.Upto
Goal:
p : ℕ → Prop
x : ℕ
h : p x
suffices : Upto.GT p = InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) fun (y : Upto p) ↦ x - (↑y : ℕ)
⊢ WellFounded (Upto.GT p)

Tactic:
suffices Upto.GT p = InvImage (· < ·) fun y : Nat.Upto p => x - y.val by
      rw [this]
      exact (measure _).wf
-- Module: Mathlib.Data.Nat.Upto
Goal:
p : ℕ → Prop
x : ℕ
h : p x
h₁ :
  ∀ (a : ℕ) (ha : ∀ (j : ℕ), j < a → ¬p j) (b : ℕ) (property : ∀ (j : ℕ), j < b → ¬p j),
    Upto.GT p (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) a ha)
        (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) b property) ↔
      InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (y : Upto p) ↦ x - (↑y : ℕ))
        (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) a ha)
        (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) b property)
⊢ Upto.GT p = InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) fun (y : Upto p) ↦ x - (↑y : ℕ)

Tactic:
ext ⟨a, ha⟩ ⟨b, _⟩
-- Module: Mathlib.Data.Nat.Upto
Goal:
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ (j : ℕ), j < a → ¬p j
b : ℕ
property : ∀ (j : ℕ), j < b → ¬p j
h₁ : a > b ↔ x - a < x - b
⊢ Upto.GT p (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) a ha)
      (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) b property) ↔
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (y : Upto p) ↦ x - (↑y : ℕ))
      (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) a ha)
      (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) b property)

Tactic:
dsimp [InvImage, Upto.GT]

Premises used: InvImage, Nat.Upto.GT
-- Module: Mathlib.Data.Nat.Upto
Goal:
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ (j : ℕ), j < a → ¬p j
b : ℕ
property : ∀ (j : ℕ), j < b → ¬p j
h₁ h₂ : a > b ↔ b < a
⊢ a > b ↔ x - a < x - b

Tactic:
rw [tsub_lt_tsub_iff_left_of_le (le_of_not_gt fun h' => ha _ h' h)]

Premises used: tsub_lt_tsub_iff_left_of_le, le_of_not_gt
-- Module: Mathlib.Data.Nat.Upto
Goal:
p : ℕ → Prop
x : Upto p
h : ¬p (↑x : ℕ)
j : ℕ
h' : j < (↑x : ℕ).succ
inl : ∀ (h' : j < (↑x : ℕ)), ¬p j
inr : ∀ (h' : (↑x : ℕ) < (↑x : ℕ).succ), ¬p (↑x : ℕ)
⊢ ¬p j

Tactic:
rcases Nat.lt_succ_iff_lt_or_eq.1 h' with (h' | rfl)

Premises used: Iff.mp, Nat.lt_succ_iff_lt_or_eq, rfl
-- Module: Mathlib.Data.Nat.Upto
Goal:
p : ℕ → Prop
x : Upto p
h : ¬p (↑x : ℕ)
j : ℕ
h'_1 : j < (↑x : ℕ).succ
h' : j < (↑x : ℕ)
⊢ ¬p j

Tactic:
x.2 _ h'

Premises used: Subtype.property
-- Module: Mathlib.Data.Nat.Upto
Goal:
p : ℕ → Prop
x : Upto p
h : ¬p (↑x : ℕ)
j : ℕ
h'_1 : j < (↑x : ℕ).succ
h' : j < (↑x : ℕ)
⊢ ¬p j

Tactic:
exact x.2 _ h'

Premises used: Subtype.property
-- Module: Mathlib.Data.Nat.Upto
Goal:
p : ℕ → Prop
x : Upto p
h : ¬p (↑x : ℕ)
h' : (↑x : ℕ) < (↑x : ℕ).succ
⊢ ¬p (↑x : ℕ)

Tactic:
h
-- Module: Mathlib.Data.Nat.Upto
Goal:
p : ℕ → Prop
x : Upto p
h : ¬p (↑x : ℕ)
h' : (↑x : ℕ) < (↑x : ℕ).succ
⊢ ¬p (↑x : ℕ)

Tactic:
exact h
-- Module: Mathlib.Data.Nat.Upto
Goal:
p : ℕ → Prop
x : Upto p
h : ¬p (↑x : ℕ)
j : ℕ
h' : j < (↑x : ℕ).succ
inl : ∀ (h' : j < (↑x : ℕ)), ¬p j
inr : ∀ (h' : (↑x : ℕ) < (↑x : ℕ).succ), ¬p (↑x : ℕ)
inl₁ : ∀ (h' : j < (↑x : ℕ)), ¬p j
inr₁ : ∀ (h' : (↑x : ℕ) < (↑x : ℕ).succ), ¬p (↑x : ℕ)
⊢ ¬p j

Tactic:
rcases Nat.lt_succ_iff_lt_or_eq.1 h' with (h' | rfl) <;> [exact x.2 _ h'; exact h]

Premises used: Iff.mp, Nat.lt_succ_iff_lt_or_eq, rfl, Subtype.property
-- Module: Mathlib.Data.Nat.WithBot
Goal:
n m : WithBot ℕ
bot : ⊥ + m = 0 ↔ Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 0
coe : ∀ (a : ℕ), (↑a : WithBot ℕ) + m = 0 ↔ (↑a : WithBot ℕ) = 0 ∧ m = 0
⊢ n + m = 0 ↔ n = 0 ∧ m = 0

Tactic:
cases n
-- Module: Mathlib.Data.Nat.WithBot
Goal:
m : WithBot ℕ
⊢ ⊥ + m = 0 ↔ Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 0

Tactic:
simp [WithBot.bot_add]

Premises used: WithBot.bot_add
-- Module: Mathlib.Data.Nat.WithBot
Goal:
m : WithBot ℕ
a : ℕ
coe : (↑a : WithBot ℕ) + ⊥ = 0 ↔ (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 0
coe₁ : ∀ (a_1 : ℕ), (↑a : WithBot ℕ) + (↑a_1 : WithBot ℕ) = 0 ↔ (↑a : WithBot ℕ) = 0 ∧ (↑a_1 : WithBot ℕ) = 0
⊢ (↑a : WithBot ℕ) + m = 0 ↔ (↑a : WithBot ℕ) = 0 ∧ m = 0

Tactic:
cases m
-- Module: Mathlib.Data.Nat.WithBot
Goal:
a : ℕ
⊢ (↑a : WithBot ℕ) + ⊥ = 0 ↔ (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 0

Tactic:
simp [WithBot.add_bot]

Premises used: WithBot.add_bot
-- Module: Mathlib.Data.Nat.WithBot
Goal:
a a_1 : ℕ
⊢ (↑a : WithBot ℕ) + (↑a_1 : WithBot ℕ) = 0 ↔ (↑a : WithBot ℕ) = 0 ∧ (↑a_1 : WithBot ℕ) = 0

Tactic:
simp [← WithBot.coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Data.Nat.WithBot
Goal:
n m : WithBot ℕ
bot : ⊥ + m = 1 ↔ Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 1 ∨ Eq (α := WithBot ℕ) ⊥ 1 ∧ m = 0
coe : ∀ (a : ℕ), (↑a : WithBot ℕ) + m = 1 ↔ (↑a : WithBot ℕ) = 0 ∧ m = 1 ∨ (↑a : WithBot ℕ) = 1 ∧ m = 0
⊢ n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0

Tactic:
cases n
-- Module: Mathlib.Data.Nat.WithBot
Goal:
m : WithBot ℕ
⊢ ⊥ + m = 1 ↔ Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 1 ∨ Eq (α := WithBot ℕ) ⊥ 1 ∧ m = 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.WithBot
Goal:
m : WithBot ℕ
a : ℕ
coe :
  (↑a : WithBot ℕ) + ⊥ = 1 ↔
    (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 1 ∨ (↑a : WithBot ℕ) = 1 ∧ Eq (α := WithBot ℕ) ⊥ 0
coe₁ :
  ∀ (a_1 : ℕ),
    (↑a : WithBot ℕ) + (↑a_1 : WithBot ℕ) = 1 ↔
      (↑a : WithBot ℕ) = 0 ∧ (↑a_1 : WithBot ℕ) = 1 ∨ (↑a : WithBot ℕ) = 1 ∧ (↑a_1 : WithBot ℕ) = 0
⊢ (↑a : WithBot ℕ) + m = 1 ↔ (↑a : WithBot ℕ) = 0 ∧ m = 1 ∨ (↑a : WithBot ℕ) = 1 ∧ m = 0

Tactic:
cases m
-- Module: Mathlib.Data.Nat.WithBot
Goal:
a : ℕ
⊢ (↑a : WithBot ℕ) + ⊥ = 1 ↔
    (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 1 ∨ (↑a : WithBot ℕ) = 1 ∧ Eq (α := WithBot ℕ) ⊥ 0

Tactic:
simp [WithBot.add_bot]

Premises used: WithBot.add_bot
-- Module: Mathlib.Data.Nat.WithBot
Goal:
a a_1 : ℕ
⊢ (↑a : WithBot ℕ) + (↑a_1 : WithBot ℕ) = 1 ↔
    (↑a : WithBot ℕ) = 0 ∧ (↑a_1 : WithBot ℕ) = 1 ∨ (↑a : WithBot ℕ) = 1 ∧ (↑a_1 : WithBot ℕ) = 0

Tactic:
simp [← WithBot.coe_add, Nat.add_eq_one_iff]

Premises used: WithBot.coe_add, Nat.add_eq_one_iff
-- Module: Mathlib.Data.Nat.WithBot
Goal:
n m : WithBot ℕ
bot : ⊥ + m = 2 ↔ Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 2 ∨ Eq (α := WithBot ℕ) ⊥ 1 ∧ m = 1 ∨ Eq (α := WithBot ℕ) ⊥ 2 ∧ m = 0
coe :
  ∀ (a : ℕ),
    (↑a : WithBot ℕ) + m = 2 ↔
      (↑a : WithBot ℕ) = 0 ∧ m = 2 ∨ (↑a : WithBot ℕ) = 1 ∧ m = 1 ∨ (↑a : WithBot ℕ) = 2 ∧ m = 0
⊢ n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0

Tactic:
cases n
-- Module: Mathlib.Data.Nat.WithBot
Goal:
m : WithBot ℕ
⊢ ⊥ + m = 2 ↔ Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 2 ∨ Eq (α := WithBot ℕ) ⊥ 1 ∧ m = 1 ∨ Eq (α := WithBot ℕ) ⊥ 2 ∧ m = 0

Tactic:
simp [WithBot.bot_add]

Premises used: WithBot.bot_add
-- Module: Mathlib.Data.Nat.WithBot
Goal:
m : WithBot ℕ
a : ℕ
coe :
  (↑a : WithBot ℕ) + ⊥ = 2 ↔
    (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 2 ∨
      (↑a : WithBot ℕ) = 1 ∧ Eq (α := WithBot ℕ) ⊥ 1 ∨ (↑a : WithBot ℕ) = 2 ∧ Eq (α := WithBot ℕ) ⊥ 0
coe₁ :
  ∀ (a_1 : ℕ),
    (↑a : WithBot ℕ) + (↑a_1 : WithBot ℕ) = 2 ↔
      (↑a : WithBot ℕ) = 0 ∧ (↑a_1 : WithBot ℕ) = 2 ∨
        (↑a : WithBot ℕ) = 1 ∧ (↑a_1 : WithBot ℕ) = 1 ∨ (↑a : WithBot ℕ) = 2 ∧ (↑a_1 : WithBot ℕ) = 0
⊢ (↑a : WithBot ℕ) + m = 2 ↔ (↑a : WithBot ℕ) = 0 ∧ m = 2 ∨ (↑a : WithBot ℕ) = 1 ∧ m = 1 ∨ (↑a : WithBot ℕ) = 2 ∧ m = 0

Tactic:
cases m
-- Module: Mathlib.Data.Nat.WithBot
Goal:
a : ℕ
⊢ (↑a : WithBot ℕ) + ⊥ = 2 ↔
    (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 2 ∨
      (↑a : WithBot ℕ) = 1 ∧ Eq (α := WithBot ℕ) ⊥ 1 ∨ (↑a : WithBot ℕ) = 2 ∧ Eq (α := WithBot ℕ) ⊥ 0

Tactic:
simp [WithBot.add_bot]

Premises used: WithBot.add_bot
-- Module: Mathlib.Data.Nat.WithBot
Goal:
a a_1 : ℕ
⊢ (↑a : WithBot ℕ) + (↑a_1 : WithBot ℕ) = 2 ↔
    (↑a : WithBot ℕ) = 0 ∧ (↑a_1 : WithBot ℕ) = 2 ∨
      (↑a : WithBot ℕ) = 1 ∧ (↑a_1 : WithBot ℕ) = 1 ∨ (↑a : WithBot ℕ) = 2 ∧ (↑a_1 : WithBot ℕ) = 0

Tactic:
simp [← WithBot.coe_add, Nat.add_eq_two_iff]

Premises used: Nat.add_eq_two_iff, WithBot.coe_add
-- Module: Mathlib.Data.Nat.WithBot
Goal:
n m : WithBot ℕ
bot :
  ⊥ + m = 3 ↔
    Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 3 ∨
      Eq (α := WithBot ℕ) ⊥ 1 ∧ m = 2 ∨ Eq (α := WithBot ℕ) ⊥ 2 ∧ m = 1 ∨ Eq (α := WithBot ℕ) ⊥ 3 ∧ m = 0
coe :
  ∀ (a : ℕ),
    (↑a : WithBot ℕ) + m = 3 ↔
      (↑a : WithBot ℕ) = 0 ∧ m = 3 ∨
        (↑a : WithBot ℕ) = 1 ∧ m = 2 ∨ (↑a : WithBot ℕ) = 2 ∧ m = 1 ∨ (↑a : WithBot ℕ) = 3 ∧ m = 0
⊢ n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0

Tactic:
cases n
-- Module: Mathlib.Data.Nat.WithBot
Goal:
m : WithBot ℕ
⊢ ⊥ + m = 3 ↔
    Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 3 ∨
      Eq (α := WithBot ℕ) ⊥ 1 ∧ m = 2 ∨ Eq (α := WithBot ℕ) ⊥ 2 ∧ m = 1 ∨ Eq (α := WithBot ℕ) ⊥ 3 ∧ m = 0

Tactic:
simp [WithBot.bot_add]

Premises used: WithBot.bot_add
-- Module: Mathlib.Data.Nat.WithBot
Goal:
m : WithBot ℕ
a : ℕ
coe :
  (↑a : WithBot ℕ) + ⊥ = 3 ↔
    (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 3 ∨
      (↑a : WithBot ℕ) = 1 ∧ Eq (α := WithBot ℕ) ⊥ 2 ∨
        (↑a : WithBot ℕ) = 2 ∧ Eq (α := WithBot ℕ) ⊥ 1 ∨ (↑a : WithBot ℕ) = 3 ∧ Eq (α := WithBot ℕ) ⊥ 0
coe₁ :
  ∀ (a_1 : ℕ),
    (↑a : WithBot ℕ) + (↑a_1 : WithBot ℕ) = 3 ↔
      (↑a : WithBot ℕ) = 0 ∧ (↑a_1 : WithBot ℕ) = 3 ∨
        (↑a : WithBot ℕ) = 1 ∧ (↑a_1 : WithBot ℕ) = 2 ∨
          (↑a : WithBot ℕ) = 2 ∧ (↑a_1 : WithBot ℕ) = 1 ∨ (↑a : WithBot ℕ) = 3 ∧ (↑a_1 : WithBot ℕ) = 0
⊢ (↑a : WithBot ℕ) + m = 3 ↔
    (↑a : WithBot ℕ) = 0 ∧ m = 3 ∨
      (↑a : WithBot ℕ) = 1 ∧ m = 2 ∨ (↑a : WithBot ℕ) = 2 ∧ m = 1 ∨ (↑a : WithBot ℕ) = 3 ∧ m = 0

Tactic:
cases m
-- Module: Mathlib.Data.Nat.WithBot
Goal:
a : ℕ
⊢ (↑a : WithBot ℕ) + ⊥ = 3 ↔
    (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 3 ∨
      (↑a : WithBot ℕ) = 1 ∧ Eq (α := WithBot ℕ) ⊥ 2 ∨
        (↑a : WithBot ℕ) = 2 ∧ Eq (α := WithBot ℕ) ⊥ 1 ∨ (↑a : WithBot ℕ) = 3 ∧ Eq (α := WithBot ℕ) ⊥ 0

Tactic:
simp [WithBot.add_bot]

Premises used: WithBot.add_bot
-- Module: Mathlib.Data.Nat.WithBot
Goal:
a a_1 : ℕ
⊢ (↑a : WithBot ℕ) + (↑a_1 : WithBot ℕ) = 3 ↔
    (↑a : WithBot ℕ) = 0 ∧ (↑a_1 : WithBot ℕ) = 3 ∨
      (↑a : WithBot ℕ) = 1 ∧ (↑a_1 : WithBot ℕ) = 2 ∨
        (↑a : WithBot ℕ) = 2 ∧ (↑a_1 : WithBot ℕ) = 1 ∨ (↑a : WithBot ℕ) = 3 ∧ (↑a_1 : WithBot ℕ) = 0

Tactic:
simp [← WithBot.coe_add, Nat.add_eq_three_iff]

Premises used: WithBot.coe_add, Nat.add_eq_three_iff
-- Module: Mathlib.Data.Nat.WithBot
Goal:
n : ℕ
rw : 0 ≤ n
⊢ LE.le (α := WithBot ℕ) 0 (↑n : WithBot ℕ)

Tactic:
rw [← WithBot.coe_zero, cast_withBot, WithBot.coe_le_coe]

Premises used: WithBot.coe_le_coe, Nat.cast_withBot, WithBot.coe_zero
-- Module: Mathlib.Data.Nat.WithBot
Goal:
n : ℕ
⊢ 0 ≤ n

Tactic:
n.zero_le

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.WithBot
Goal:
n : ℕ
⊢ 0 ≤ n

Tactic:
exact n.zero_le

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.WithBot
Goal:
n : WithBot ℕ
⊢ n < 0 ↔ n = ⊥

Tactic:
WithBot.lt_coe_bot

Premises used: WithBot.lt_coe_bot
-- Module: Mathlib.Data.Nat.WithBot
Goal:
x : WithBot ℕ
⊢ 1 ≤ x ↔ 0 < x

Tactic:
⟨zero_lt_one.trans_le, fun h => ?_⟩

Premises used: zero_lt_one, LT.lt.trans_le, Iff.intro
-- Module: Mathlib.Data.Nat.WithBot
Goal:
x : WithBot ℕ
refine : ∀ (h : 0 < x), 1 ≤ x
⊢ 1 ≤ x ↔ 0 < x

Tactic:
refine ⟨zero_lt_one.trans_le, fun h => ?_⟩
-- Module: Mathlib.Data.Nat.WithBot
Goal:
x : WithBot ℕ
h : 0 < x
bot : ∀ (h : LT.lt (α := WithBot ℕ) 0 ⊥), LE.le (α := WithBot ℕ) 1 ⊥
coe : ∀ (a : ℕ) (h : 0 < (↑a : WithBot ℕ)), 1 ≤ (↑a : WithBot ℕ)
⊢ 1 ≤ x

Tactic:
cases x
-- Module: Mathlib.Data.Nat.WithBot
Goal:
h : LT.lt (α := WithBot ℕ) 0 ⊥
⊢ LE.le (α := WithBot ℕ) 1 ⊥

Tactic:
(not_lt_bot h).elim

Premises used: False.elim, not_lt_bot
-- Module: Mathlib.Data.Nat.WithBot
Goal:
h : LT.lt (α := WithBot ℕ) 0 ⊥
⊢ LE.le (α := WithBot ℕ) 1 ⊥

Tactic:
exact (not_lt_bot h).elim

Premises used: False.elim, not_lt_bot
-- Module: Mathlib.Data.Nat.WithBot
Goal:
a : ℕ
h : 0 < (↑a : WithBot ℕ)
coe : ∀ (h : (↑0 : WithBot ℕ) < (↑a : WithBot ℕ)), 1 ≤ (↑a : WithBot ℕ)
coe₁ : ∀ (h : 0 < a), 1 ≤ (↑a : WithBot ℕ)
coe₂ : ∀ (h : HAdd.hAdd (α := ℕ) 0 1 ≤ a), 1 ≤ (↑a : WithBot ℕ)
coe₃ : ∀ (h : 1 ≤ a), 1 ≤ (↑a : WithBot ℕ)
coe₄ : ∀ (h : (↑1 : WithBot ℕ) ≤ (↑a : WithBot ℕ)), 1 ≤ (↑a : WithBot ℕ)
coe₅ coe₆ coe₇ coe₈ : ∀ (h : 1 ≤ (↑a : WithBot ℕ)), 1 ≤ (↑a : WithBot ℕ)
⊢ 1 ≤ (↑a : WithBot ℕ)

Tactic:
rwa [← WithBot.coe_zero, WithBot.coe_lt_coe, ← Nat.add_one_le_iff, zero_add,
      ← WithBot.coe_le_coe, WithBot.coe_one] at h

Premises used: zero_add, WithBot.coe_le_coe, Nat.add_one_le_iff, WithBot.coe_lt_coe, WithBot.coe_one, WithBot.coe_zero
-- Module: Mathlib.Data.Nat.WithBot
Goal:
x : WithBot ℕ
⊢ ¬x < 1 ↔ ¬x ≤ 0

Tactic:
simpa using one_le_iff_zero_lt

Premises used: Nat.WithBot.one_le_iff_zero_lt
-- Module: Mathlib.Data.Nat.WithBot
Goal:
n m : WithBot ℕ
h : n < m
bot : ∀ (h : ⊥ < m), HAdd.hAdd (α := WithBot ℕ) ⊥ 1 ≤ m
coe : ∀ (a : ℕ) (h : (↑a : WithBot ℕ) < m), (↑a : WithBot ℕ) + 1 ≤ m
⊢ n + 1 ≤ m

Tactic:
cases n
-- Module: Mathlib.Data.Nat.WithBot
Goal:
m : WithBot ℕ
h : ⊥ < m
⊢ HAdd.hAdd (α := WithBot ℕ) ⊥ 1 ≤ m

Tactic:
simp only [WithBot.bot_add, bot_le]

Premises used: WithBot.bot_add, bot_le
-- Module: Mathlib.Data.Nat.WithBot
Goal:
m : WithBot ℕ
a : ℕ
h : (↑a : WithBot ℕ) < m
coe : ∀ (h : (↑a : WithBot ℕ) < ⊥), (↑a : WithBot ℕ) + 1 ≤ ⊥
coe₁ : ∀ (a_1 : ℕ) (h : (↑a : WithBot ℕ) < (↑a_1 : WithBot ℕ)), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
⊢ (↑a : WithBot ℕ) + 1 ≤ m

Tactic:
cases m
-- Module: Mathlib.Data.Nat.WithBot
Goal:
a : ℕ
h : (↑a : WithBot ℕ) < ⊥
⊢ (↑a : WithBot ℕ) + 1 ≤ ⊥

Tactic:
(not_lt_bot h).elim

Premises used: False.elim, not_lt_bot
-- Module: Mathlib.Data.Nat.WithBot
Goal:
a : ℕ
h : (↑a : WithBot ℕ) < ⊥
⊢ (↑a : WithBot ℕ) + 1 ≤ ⊥

Tactic:
exact (not_lt_bot h).elim

Premises used: False.elim, not_lt_bot
-- Module: Mathlib.Data.Nat.WithBot
Goal:
a a_1 : ℕ
h : (↑a : WithBot ℕ) < (↑a_1 : WithBot ℕ)
coe : ∀ (h : a < a_1), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
coe₁ : ∀ (h : a + 1 ≤ a_1), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
coe₂ : ∀ (h : (↑(a + 1) : WithBot ℕ) ≤ (↑a_1 : WithBot ℕ)), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
coe₃ : ∀ (h : (↑a : WithBot ℕ) + (↑1 : WithBot ℕ) ≤ (↑a_1 : WithBot ℕ)), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
coe₄ coe₅ coe₆ coe₇ : ∀ (h : (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
⊢ (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)

Tactic:
rwa [WithBot.coe_lt_coe, ← Nat.add_one_le_iff, ← WithBot.coe_le_coe, WithBot.coe_add,
      WithBot.coe_one] at h

Premises used: WithBot.coe_le_coe, Nat.add_one_le_iff, WithBot.coe_lt_coe, WithBot.coe_one, WithBot.coe_add
-- Module: Mathlib.Data.Num.Basic
Goal:
a b : PosNum
⊢ Decidable (a.cmp b = lt)

Tactic:
infer_instance
-- Module: Mathlib.Data.Num.Basic
Goal:
a b : PosNum
⊢ Decidable ¬b < a

Tactic:
infer_instance
-- Module: Mathlib.Data.Num.Basic
Goal:
a b : Num
⊢ Decidable (a.cmp b = lt)

Tactic:
infer_instance
-- Module: Mathlib.Data.Num.Basic
Goal:
a b : Num
⊢ Decidable ¬b < a

Tactic:
infer_instance
-- Module: Mathlib.Data.Num.Bitwise
Goal:
p q : PosNum
⊢ p.lor q = p ||| q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Num.Bitwise
Goal:
p q : PosNum
⊢ p.land q = p &&& q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Num.Bitwise
Goal:
p q : PosNum
⊢ p.lxor q = p ^^^ q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Num.Bitwise
Goal:
p : PosNum
n : ℕ
⊢ p.shiftl n = p <<< n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Num.Bitwise
Goal:
p : PosNum
n : ℕ
⊢ p.shiftr n = p >>> n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Num.Bitwise
Goal:
p q : Num
⊢ p.lor q = p ||| q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Num.Bitwise
Goal:
p q : Num
⊢ p.land q = p &&& q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Num.Bitwise
Goal:
p q : Num
⊢ p.lxor q = p ^^^ q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Num.Bitwise
Goal:
p : Num
n : ℕ
⊢ p.shiftl n = p <<< n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Num.Bitwise
Goal:
p : Num
n : ℕ
⊢ p.shiftr n = p >>> n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Num.Bitwise
Goal:
b : Bool
false : (Bool.false::zero Bool.false) = zero Bool.false
true : (Bool.true::zero Bool.true) = zero Bool.true
⊢ (b::zero b) = zero b

Tactic:
cases b
-- Module: Mathlib.Data.Num.Bitwise
Goal:
⊢ (false::zero false) = zero false

Tactic:
rfl
-- Module: Mathlib.Data.Num.Bitwise
Goal:
⊢ (true::zero true) = zero true

Tactic:
rfl
-- Module: Mathlib.Data.Num.Bitwise
Goal:
b : Bool
false : (Bool.false::zero (decide ¬Bool.false = Bool.true)) = nz (msb Bool.false)
true : (Bool.true::zero (decide ¬Bool.true = Bool.true)) = nz (msb Bool.true)
⊢ (b::zero (decide ¬b = Bool.true)) = nz (msb b)

Tactic:
cases b
-- Module: Mathlib.Data.Num.Bitwise
Goal:
⊢ (false::zero (decide ¬false = true)) = nz (msb false)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Bitwise
Goal:
⊢ (true::zero (decide ¬true = true)) = nz (msb true)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Bitwise
Goal:
C : SNum → Sort u_1
z : (b : Bool) → C (zero b)
s : (b : Bool) → (p : SNum) → C p → C (b::p)
b : Bool
rw : C (b::zero (decide ¬b = true))
⊢ C (nz (msb b))

Tactic:
rw [← bit_one]

Premises used: SNum.bit_one
-- Module: Mathlib.Data.Num.Bitwise
Goal:
C : SNum → Sort u_1
z : (b : Bool) → C (zero b)
s : (b : Bool) → (p : SNum) → C p → C (b::p)
b : Bool
⊢ C (b::zero (decide ¬b = true))

Tactic:
exact s b (SNum.zero (Not b)) (z (Not b))

Premises used: Bool.true, SNum.zero, Decidable.decide, Eq, Not
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : One α
inst_1 : Add α
⊢ Eq.{u_1 + 1} (α := α) (↑1 : α) 1

Tactic:
rfl

Premises used: castPosNum, rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : One α
inst_1 : Add α
⊢ Eq.{u_1 + 1} (α := α) (↑one : α) 1

Tactic:
rfl

Premises used: castPosNum, rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : One α
inst_1 : Add α
n : PosNum
⊢ (↑n.bit0 : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α)

Tactic:
rfl

Premises used: castPosNum, rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : One α
inst_1 : Add α
n : PosNum
⊢ (↑n.bit1 : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α) + 1

Tactic:
rfl

Premises used: castPosNum, rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : AddMonoidWithOne α
p : PosNum
dsimp : (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)) : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑p.bit0 : ℕ) : α) (↑p.bit0 : α)

Tactic:
dsimp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : AddMonoidWithOne α
p : PosNum
rw : HAdd.hAdd (α := α) (↑(↑p : ℕ) : α) (↑(↑p : ℕ) : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α)
rw₁ rw₂ : HAdd.hAdd (α := α) (↑p : α) (↑p : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α)
⊢ (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)) : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α)

Tactic:
rw [Nat.cast_add, p.cast_to_nat]

Premises used: Nat.cast_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : AddMonoidWithOne α
p : PosNum
dsimp : (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ) + 1) : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
⊢ Eq.{u_1 + 1} (α := α) (↑(↑p.bit1 : ℕ) : α) (↑p.bit1 : α)

Tactic:
dsimp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : AddMonoidWithOne α
p : PosNum
rw :
  HAdd.hAdd (α := α) (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)) : α) (↑1 : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
rw₁ : HAdd.hAdd (α := α) (↑(↑p : ℕ) : α) (↑(↑p : ℕ) : α) + (↑1 : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
rw₂ : HAdd.hAdd (α := α) (↑(↑p : ℕ) : α) (↑(↑p : ℕ) : α) + 1 = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
rw₃ rw₄ : HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1 = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
⊢ (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ) + 1) : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1

Tactic:
rw [Nat.cast_add, Nat.cast_add, Nat.cast_one, p.cast_to_nat]

Premises used: Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ Eq (α := ℤ) (↑(↑n : ℕ) : ℤ) (↑n : ℤ)

Tactic:
cast_to_nat _

Premises used: PosNum.cast_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : PosNum
rw : Eq.{u_1 + 1} (α := α) (↑(↑(↑n : ℕ) : ℤ) : α) (↑n : α)
rw₁ : Eq.{u_1 + 1} (α := α) (↑(↑n : ℕ) : α) (↑n : α)
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (↑n : α) (↑n : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ℤ) : α) (↑n : α)

Tactic:
rw [← to_nat_to_int, Int.cast_natCast, cast_to_nat]

Premises used: Int.cast_natCast, PosNum.cast_to_nat, PosNum.to_nat_to_int
-- Module: Mathlib.Data.Num.Lemmas
Goal:
p : PosNum
⊢ HAdd.hAdd (α := ℕ) (↑p : ℕ) 1 + (↑p : ℕ) + 1 = HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ) + 1 + 1

Tactic:
simp [add_left_comm]

Premises used: add_left_comm
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
one : 1 + PosNum.one = PosNum.one.succ
bit1 : ∀ (a : PosNum), 1 + a.bit1 = a.bit1.succ
bit0 : ∀ (a : PosNum), 1 + a.bit0 = a.bit0.succ
⊢ 1 + n = n.succ

Tactic:
cases n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ 1 + one = one.succ

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ 1 + a.bit1 = a.bit1.succ

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ 1 + a.bit0 = a.bit0.succ

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
one : PosNum.one + 1 = PosNum.one.succ
bit1 : ∀ (a : PosNum), a.bit1 + 1 = a.bit1.succ
bit0 : ∀ (a : PosNum), a.bit0 + 1 = a.bit0.succ
⊢ n + 1 = n.succ

Tactic:
cases n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ one + 1 = one.succ

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ a.bit1 + 1 = a.bit1.succ

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ a.bit0 + 1 = a.bit0.succ

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
b : PosNum
rw : (↑b.succ : ℕ) = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
rw₁ : HAdd.hAdd (α := ℕ) (↑b : ℕ) 1 = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
rw₂ : HAdd.hAdd (α := ℕ) 1 (↑b : ℕ) = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
rw₃ rw₄ : HAdd.hAdd (α := ℕ) 1 (↑b : ℕ) = HAdd.hAdd (α := ℕ) 1 (↑b : ℕ)
⊢ (↑(1 + b) : ℕ) = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)

Tactic:
rw [one_add b, succ_to_nat, add_comm, cast_one]

Premises used: PosNum.cast_one, add_comm, PosNum.succ_to_nat, PosNum.one_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
rw : (↑a.succ : ℕ) = HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑1 : ℕ)
rw₁ : HAdd.hAdd (α := ℕ) (↑a : ℕ) 1 = HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑1 : ℕ)
rw₂ rw₃ : HAdd.hAdd (α := ℕ) (↑a : ℕ) 1 = HAdd.hAdd (α := ℕ) (↑a : ℕ) 1
⊢ (↑(a + 1) : ℕ) = HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑1 : ℕ)

Tactic:
rw [add_one a, succ_to_nat, cast_one]

Premises used: PosNum.cast_one, PosNum.add_one, PosNum.succ_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
⊢ HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) + HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) + 1 =
    HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1)

Tactic:
simp [add_left_comm]

Premises used: add_left_comm
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
⊢ HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) + HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) + 1 =
    HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 + HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
rw :
  HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) + 1 + (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) + 1) =
    HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 + (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1)
⊢ HAdd.hAdd (α := ℕ) (↑(a + b).succ : ℕ) (↑(a + b).succ : ℕ) =
    HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 + (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1)

Tactic:
rw [succ_to_nat, add_to_nat a b]

Premises used: PosNum.succ_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
⊢ HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) + 1 + (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) + 1) =
    HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 + (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1)

Tactic:
simp [add_left_comm]

Premises used: add_left_comm
-- Module: Mathlib.Data.Num.Lemmas
Goal:
b : PosNum
⊢ 1 + b.succ = (1 + b).succ

Tactic:
simp [one_add]

Premises used: PosNum.one_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
p : PosNum
rw : p.bit0.succ.bit0 = p.bit1.bit0
rw₁ rw₂ : p.bit1.bit0 = p.bit1.bit0
⊢ (p + p).succ.bit0 = p.bit1.bit0

Tactic:
rw [bit0_of_bit0 p, succ]

Premises used: PosNum.succ