awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Init
Goal:
m n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
mn : m ≤ n
msn : m ≤ n + 1
dsimp :
  Eq.{u_1} (α := motive m msn)
    (leRec (motive := fun {n : ℕ} (mn : m ≤ n) ↦
        {motive : (m : ℕ) → m ≤ n → Sort u_1} →
          (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → (self : motive n ⋯) → motive m mn)
        (fun {motive : (m_1 : ℕ) → m_1 ≤ m → Sort u_1} (of_succ : (k : ℕ) → (h : k < m) → motive (k + 1) h → motive k ⋯)
            (self : motive m ⋯) ↦
          self)
        (fun ⦃k : ℕ⦄ (h : m ≤ k)
            (ih :
              {motive : (m : ℕ) → m ≤ k → Sort u_1} →
                (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯) →
                  (self : motive k ⋯) → motive m h)
            {motive : (m : ℕ) → m ≤ k + 1 → Sort u_1}
            (of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 ⋯) (self : motive (k + 1) ⋯) ↦
          ih (motive := fun {m : ℕ} (h : m ≤ k) ↦ motive m ⋯) (fun (i : ℕ) (hi : i < k) ↦ of_succ i ⋯)
            (of_succ k ⋯ self))
        msn (motive := motive) of_succ self :
      motive m msn)
    (leRec (motive := fun {n : ℕ} (mn : m ≤ n) ↦
        {motive : (m : ℕ) → m ≤ n → Sort u_1} →
          (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → (self : motive n ⋯) → motive m mn)
        (fun {motive : (m_1 : ℕ) → m_1 ≤ m → Sort u_1} (of_succ : (k : ℕ) → (h : k < m) → motive (k + 1) h → motive k ⋯)
            (self : motive m ⋯) ↦
          self)
        (fun ⦃k : ℕ⦄ (h : m ≤ k)
            (ih :
              {motive : (m : ℕ) → m ≤ k → Sort u_1} →
                (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯) →
                  (self : motive k ⋯) → motive m h)
            {motive : (m : ℕ) → m ≤ k + 1 → Sort u_1}
            (of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 ⋯) (self : motive (k + 1) ⋯) ↦
          ih (motive := fun {m : ℕ} (h : m ≤ k) ↦ motive m ⋯) (fun (i : ℕ) (hi : i < k) ↦ of_succ i ⋯)
            (of_succ k ⋯ self))
        mn (motive := fun (m : ℕ) (h : m ≤ n) ↦ motive m ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (of_succ n ⋯ self) :
      motive m ⋯)
⊢ decreasingInduction (motive := motive) of_succ self msn =
    decreasingInduction (motive := fun (m : ℕ) (h : m ≤ n) ↦ motive m ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
      (of_succ n ⋯ self) mn

Tactic:
dsimp only [decreasingInduction]
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
dsimp :
  leRec (motive := fun {n_1 : ℕ} (mn : n ≤ n_1) ↦
      {motive : (m : ℕ) → m ≤ n_1 → Sort u_1} →
        (of_succ : (k : ℕ) → (h : k < n_1) → motive (k + 1) h → motive k ⋯) → (self : motive n_1 ⋯) → motive n mn)
      (fun {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯)
          (self : motive n ⋯) ↦
        self)
      (fun ⦃k : ℕ⦄ (h : n ≤ k)
          (ih :
            {motive : (m : ℕ) → m ≤ k → Sort u_1} →
              (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯) →
                (self : motive k ⋯) → motive n h)
          {motive : (m : ℕ) → m ≤ k + 1 → Sort u_1}
          (of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 ⋯) (self : motive (k + 1) ⋯) ↦
        ih (motive := fun {m : ℕ} (h : m ≤ k) ↦ motive m ⋯) (fun (i : ℕ) (hi : i < k) ↦ of_succ i ⋯) (of_succ k ⋯ self))
      ⋯ (motive := motive) of_succ self =
    of_succ n ⋯ self
⊢ decreasingInduction (motive := motive) of_succ self ⋯ = of_succ n ⋯ self

Tactic:
dsimp only [decreasingInduction]
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
rw rw₁ :
  (fun {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯)
          (self : motive n ⋯) ↦
        self)
      (motive := fun {m : ℕ} (h : m ≤ n) ↦ motive m ⋯) (fun (i : ℕ) (hi : i < n) ↦ of_succ i ⋯) (of_succ n ⋯ self) =
    of_succ n ⋯ self
⊢ leRec (motive := fun {n_1 : ℕ} (mn : n ≤ n_1) ↦
      {motive : (m : ℕ) → m ≤ n_1 → Sort u_1} →
        (of_succ : (k : ℕ) → (h : k < n_1) → motive (k + 1) h → motive k ⋯) → (self : motive n_1 ⋯) → motive n mn)
      (fun {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯)
          (self : motive n ⋯) ↦
        self)
      (fun ⦃k : ℕ⦄ (h : n ≤ k)
          (ih :
            {motive : (m : ℕ) → m ≤ k → Sort u_1} →
              (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯) →
                (self : motive k ⋯) → motive n h)
          {motive : (m : ℕ) → m ≤ k + 1 → Sort u_1}
          (of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 ⋯) (self : motive (k + 1) ⋯) ↦
        ih (motive := fun {m : ℕ} (h : m ≤ k) ↦ motive m ⋯) (fun (i : ℕ) (hi : i < k) ↦ of_succ i ⋯) (of_succ k ⋯ self))
      ⋯ (motive := motive) of_succ self =
    of_succ n ⋯ self

Tactic:
rw [leRec_succ']

Premises used: Nat.leRec_succ'
-- Module: Mathlib.Data.Nat.Init
Goal:
m n k : ℕ
hmn : m ≤ n
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
refl refl₁ :
  decreasingInduction (motive := motive) of_succ self ⋯ =
    decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
      self hmn
⊢ decreasingInduction (motive := motive) of_succ self ⋯ =
    decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) of_succ self ⋯) hmn

Tactic:
rw [decreasingInduction_self]

Premises used: Nat.decreasingInduction_self
-- Module: Mathlib.Data.Nat.Init
Goal:
m n k : ℕ
motive : (m : ℕ) → m ≤ k → Sort u_1
hmn : m ≤ n
hnk : n ≤ k
of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯
self : motive k ⋯
refl :
  ∀ {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯)
    (self : motive n ⋯),
    decreasingInduction (motive := motive) of_succ self ⋯ =
      decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) of_succ self ⋯) hmn
step :
  ∀ {m_1 : ℕ} (hnk : n.le m_1)
    (ih :
      ∀ {motive : (m : ℕ) → m ≤ m_1 → Sort u_1} (of_succ : (k : ℕ) → (h : k < m_1) → motive (k + 1) h → motive k ⋯)
        (self : motive m_1 ⋯),
        decreasingInduction (motive := motive) of_succ self ⋯ =
          decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯)
            (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
            (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1) ↦ motive x ⋯) of_succ self hnk) hmn)
    {motive : (m : ℕ) → m ≤ m_1.succ → Sort u_1}
    (of_succ : (k : ℕ) → (h : k < m_1.succ) → motive (k + 1) h → motive k ⋯) (self : motive m_1.succ ⋯),
    decreasingInduction (motive := motive) of_succ self ⋯ =
      decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x ⋯) of_succ self ⋯) hmn
⊢ decreasingInduction (motive := motive) of_succ self ⋯ =
    decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ k) ↦ motive x ⋯) of_succ self hnk) hmn

Tactic:
induction hnk with
  | refl => rw [decreasingInduction_self]
  | step hnk ih =>
      rw [decreasingInduction_succ _ _ (Nat.le_trans hmn hnk), ih, decreasingInduction_succ]

Premises used: Nat.decreasingInduction_self, Nat.le_trans, Nat.decreasingInduction_succ
-- Module: Mathlib.Data.Nat.Init
Goal:
m n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
smn : m + 1 ≤ n
mn : m ≤ n
rw :
  decreasingInduction (motive := motive) of_succ self ⋯ =
    of_succ m smn (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x x_1) of_succ self smn)
rw₁ :
  decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m + 1) ↦ motive x ⋯)
      (fun (x : ℕ) (x_1 : x < m + 1) ↦ of_succ x ⋯)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) of_succ self smn) ⋯ =
    of_succ m smn (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x x_1) of_succ self smn)
hnk : m + 1 ≤ n
rw₂ :
  of_succ m ⋯ (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) of_succ self smn) =
    of_succ m smn (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x x_1) of_succ self smn)
hnk₁ : m + 1 ≤ n
rw₃ :
  of_succ m ⋯ (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) of_succ self smn) =
    of_succ m smn (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x x_1) of_succ self smn)
hnk₂ : m + 1 ≤ n
⊢ decreasingInduction (motive := motive) of_succ self mn =
    of_succ m smn (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x x_1) of_succ self smn)

Tactic:
rw [Subsingleton.elim mn (Nat.le_trans (le_succ m) smn),
    decreasingInduction_trans (n := m + 1) (Nat.le_succ m),
    decreasingInduction_succ']

Premises used: Nat.decreasingInduction_trans, Nat.le_succ, Nat.le_trans, Subsingleton.elim, Nat.decreasingInduction_succ'
-- Module: Mathlib.Data.Nat.Init
Goal:
a b c d e m n k : ℕ
p : ℕ → Prop
P : ℕ → Sort u_1
hP : P n
h : (k : ℕ) → k < n → n ≤ k → P (k + 1) → P k
⊢ P n

Tactic:
exact hP
-- Module: Mathlib.Data.Nat.Init
Goal:
a b c d e m n k_1 : ℕ
p : ℕ → Prop
P : ℕ → Sort u_1
hP : P n
k : ℕ
hk : k < n
ih : (h : (k_2 : ℕ) → k_2 < n → k + 1 ≤ k_2 → P (k_2 + 1) → P k_2) → P (k + 1)
h : (k_2 : ℕ) → k_2 < n → k ≤ k_2 → P (k_2 + 1) → P k_2
⊢ P k

Tactic:
exact h _ (lt_of_succ_le hk) (Nat.le_refl _)
      (ih fun k' hk' h'' => h k' hk' <| le_of_succ_le h'')

Premises used: Nat.le_refl, Nat.le_of_succ_le, Nat.lt_of_succ_le
-- Module: Mathlib.Data.Nat.Init
Goal:
a b c d e m n k : ℕ
p : ℕ → Prop
P : ℕ → Sort u_1
h : (k : ℕ) → k < n → m ≤ k → P (k + 1) → P k
mn : m ≤ n
hP : P n
self : (h : (k : ℕ) → k < n → n ≤ k → P (k + 1) → P k) → P n
of_succ :
  (k : ℕ) →
    (hk : k < n) →
      (ih : (h : (k_1 : ℕ) → k_1 < n → k + 1 ≤ k_1 → P (k_1 + 1) → P k_1) → P (k + 1)) →
        (h : (k_1 : ℕ) → k_1 < n → k ≤ k_1 → P (k_1 + 1) → P k_1) → P k
⊢ P m

Tactic:
induction mn using decreasingInduction with
  | self => exact hP
  | of_succ k hk ih =>
    exact h _ (lt_of_succ_le hk) (Nat.le_refl _)
      (ih fun k' hk' h'' => h k' hk' <| le_of_succ_le h'')
-- Module: Mathlib.Data.Nat.Init
Goal:
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
a₁ : P (a + 1) b
a₂ : P a (b + 1)
⊢ P (a + 1) (b + 1)

Tactic:
apply hd _ _ (Nat.add_lt_add_iff_right.1 h)

Premises used: Iff.mp, Nat.add_lt_add_iff_right
-- Module: Mathlib.Data.Nat.Init
Goal:
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ a + 1 = b ∨ a + 1 < b

Tactic:
lia
-- Module: Mathlib.Data.Nat.Init
Goal:
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
a₁ : ∀ (this : a + 1 = b ∨ a + 1 < b), P (a + 1) b
⊢ P (a + 1) b

Tactic:
have this : a + 1 = b ∨ a + 1 < b := by lia
-- Module: Mathlib.Data.Nat.Init
Goal:
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
this : a + 1 = b ∨ a + 1 < b
a₁ : ∀ (h : a + 1 < a + 1 + 1), P (a + 1) (a + 1)
a₂ : ∀ (h : a + 1 < b), P (a + 1) b
⊢ P (a + 1) b

Tactic:
rcases this with (rfl | h)

Premises used: rfl
-- Module: Mathlib.Data.Nat.Init
Goal:
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a : ℕ
h : a + 1 < a + 1 + 1
⊢ P (a + 1) (a + 1)

Tactic:
ha _
-- Module: Mathlib.Data.Nat.Init
Goal:
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a : ℕ
h : a + 1 < a + 1 + 1
⊢ P (a + 1) (a + 1)

Tactic:
exact ha _
-- Module: Mathlib.Data.Nat.Init
Goal:
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h_1 : a + 1 < b + 1
h : a + 1 < b
⊢ P (a + 1) b

Tactic:
apply diag_induction P ha hb hd (a + 1) b h

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Init
Goal:
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
a₁ : a < b + 1
⊢ P a (b + 1)

Tactic:
apply diag_induction P ha hb hd a (b + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Init
Goal:
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ a < b + 1

Tactic:
apply Nat.lt_of_le_of_lt (Nat.le_succ _) h

Premises used: Nat.lt_of_le_of_lt, Nat.le_succ
-- Module: Mathlib.Data.Nat.Init
Goal:
a n : ℕ
ha : 1 < a
hn : 1 < n
⊢ ¬a ^ n ∣ a

Tactic:
not_dvd_of_pos_of_lt (Nat.lt_trans Nat.zero_lt_one ha)
    (lt_of_eq_of_lt (Nat.pow_one a).symm ((Nat.pow_lt_pow_iff_right ha).2 hn))

Premises used: Iff.mpr, Nat.not_dvd_of_pos_of_lt, lt_of_eq_of_lt, Nat.pow_lt_pow_iff_right, Nat.pow_one, Nat.lt_trans, Eq.symm, Nat.zero_lt_one
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
⊢ ¬2 ∣ 2 * n + 1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Init
Goal:
m n : ℕ
⊢ m ∣ m + n ↔ m ∣ n

Tactic:
Nat.dvd_add_right (Nat.dvd_refl m)

Premises used: Nat.dvd_add_right, Nat.dvd_refl
-- Module: Mathlib.Data.Nat.Init
Goal:
m n : ℕ
⊢ m ∣ n + m ↔ m ∣ n

Tactic:
Nat.dvd_add_left (Nat.dvd_refl m)

Premises used: Nat.dvd_add_left, Nat.dvd_refl
-- Module: Mathlib.Data.Nat.Init
Goal:
m n_1 : ℕ
h : m = n_1
n : ℕ
rw rw₁ : n_1 ∣ n ↔ n_1 ∣ n
⊢ m ∣ n ↔ n_1 ∣ n

Tactic:
rw [h]
-- Module: Mathlib.Data.Nat.Init
Goal:
m n_1 : ℕ
h : m = n_1
n : ℕ
rw rw₁ : n ∣ n_1 ↔ n ∣ n_1
⊢ n ∣ m ↔ n ∣ n_1

Tactic:
rw [h]
-- Module: Mathlib.Data.Nat.Init
Goal:
a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst : DecidablePred P
⊢ (∀ (x : ℕ), x < hi - lo → P (lo + x)) ↔ ∀ (x : ℕ), lo ≤ x → x < hi → P x

Tactic:
⟨fun al x hl hh ↦ ?_,
      fun al x h ↦ al _ (Nat.le_add_right _ _) (Nat.lt_sub_iff_add_lt'.1 h)⟩

Premises used: Nat.le_add_right, Nat.lt_sub_iff_add_lt', HAdd.hAdd, Iff.intro, Iff.mp
-- Module: Mathlib.Data.Nat.Init
Goal:
a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst : DecidablePred P
refine : ∀ (al : ∀ (x : ℕ), x < hi - lo → P (lo + x)) (x : ℕ) (hl : lo ≤ x) (hh : x < hi), P x
⊢ (∀ (x : ℕ), x < hi - lo → P (lo + x)) ↔ ∀ (x : ℕ), lo ≤ x → x < hi → P x

Tactic:
refine ⟨fun al x hl hh ↦ ?_,
      fun al x h ↦ al _ (Nat.le_add_right _ _) (Nat.lt_sub_iff_add_lt'.1 h)⟩
-- Module: Mathlib.Data.Nat.Init
Goal:
a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst : DecidablePred P
al : ∀ (x : ℕ), x < hi - lo → P (lo + x)
x : ℕ
hl : lo ≤ x
hh : x < hi
have : ∀ (this : P (lo + (x - lo))), P x
⊢ P x

Tactic:
have := al (x - lo) ((Nat.sub_lt_sub_iff_right hl).2 hh)
-- Module: Mathlib.Data.Nat.Init
Goal:
a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst : DecidablePred P
al : ∀ (x : ℕ), x < hi - lo → P (lo + x)
x : ℕ
hl : lo ≤ x
hh : x < hi
this : P (lo + (x - lo))
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : P x), P x
⊢ P x

Tactic:
rwa [Nat.add_sub_cancel' hl] at this

Premises used: Nat.add_sub_cancel'
-- Module: Mathlib.Data.Nat.Init
Goal:
a b c d e m n_1 k : ℕ
p : ℕ → Prop
n : ℕ
inst : NeZero n
⊢ (n + 1).AtLeastTwo

Tactic:
⟨add_le_add (one_le_iff_ne_zero.mpr (NeZero.ne n)) (Nat.le_refl 1)⟩

Premises used: Iff.mpr, Nat.le_refl, Nat.add_le_add, Nat.one_le_iff_ne_zero, OfNat.ofNat, Nat.AtLeastTwo.mk, NeZero.ne
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ 1 < n

Tactic:
prop

Premises used: Nat.AtLeastTwo.prop, Nat.lt
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ n ≠ 1

Tactic:
Nat.ne_of_gt one_lt

Premises used: Nat.AtLeastTwo.one_lt, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Init
Goal:
a b c d e m n_1 k : ℕ
p : ℕ → Prop
n_2 : ℕ
inst : n_2.AtLeastTwo
n : ℕ
inst_1 : n.AtLeastTwo
⊢ NeZero n

Tactic:
⟨Nat.ne_of_gt (Nat.le_of_lt one_lt)⟩

Premises used: NeZero.mk, Nat.AtLeastTwo.one_lt, Nat.le_of_lt, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ 2 ≤ n

Tactic:
have := prop (n := n)
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
inst : n.AtLeastTwo
this : 2 ≤ n
⊢ n - 1 ≠ 0

Tactic:
lia
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : s.Nonempty
⊢ sInf s = Nat.find (p := fun (n : ℕ) ↦ n ∈ s) h

Tactic:
dif_pos _

Premises used: dif_pos
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : ∃ (n : ℕ), ∀ a ∈ s, a ≤ n
⊢ sSup s = Nat.find (p := fun (n : ℕ) ↦ ∀ a ∈ s, a ≤ n) h

Tactic:
dif_pos _

Premises used: dif_pos
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : s.Infinite
⊢ sSup s = 0

Tactic:
dif_neg fun ⟨n, hn⟩ ↦
    let ⟨k, hks, hk⟩ := h.exists_gt n
    (hn k hks).not_gt hk

Premises used: dif_neg
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : ¬BddAbove s
⊢ sSup s = 0

Tactic:
Set.Infinite.Nat.sSup_eq_zero <| Set.infinite_of_not_bddAbove h

Premises used: Set.infinite_of_not_bddAbove, Set.Infinite.Nat.sSup_eq_zero
-- Module: Mathlib.Data.Nat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ
h : ¬BddAbove (range f)
⊢ Eq (α := ℕ) (⨆ (i : ι), f i) 0

Tactic:
Nat.sSup_of_not_bddAbove h

Premises used: Nat.sSup_of_not_bddAbove, iSup
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : s = ∅
inl : Eq (α := ℕ) (sInf ∅) 0 ↔ Membership.mem (γ := Set ℕ) ∅ 0 ∨ Eq (α := Set ℕ) ∅ ∅
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅

Tactic:
subst h
-- Module: Mathlib.Data.Nat.Lattice
Goal:
⊢ Eq (α := ℕ) (sInf ∅) 0 ↔ Membership.mem (γ := Set ℕ) ∅ 0 ∨ Eq (α := Set ℕ) ∅ ∅

Tactic:
simp only [or_true, InfSet.sInf,
                        mem_empty_iff_false, exists_false, dif_neg, not_false_iff]

Premises used: dif_neg, exists_false, Set.mem_empty_iff_false, not_false_iff, or_true, InfSet.sInf
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : s.Nonempty
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅

Tactic:
simp only [h.ne_empty, or_false, Nat.sInf_def, h, Nat.find_eq_zero]

Premises used: Set.Nonempty.ne_empty, Nat.sInf_def, Nat.find_eq_zero, or_false
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
⊢ s = ∅ ∨ s.Nonempty

Tactic:
cases eq_empty_or_nonempty s with
  | inl h => subst h
             simp only [or_true, InfSet.sInf,
                        mem_empty_iff_false, exists_false, dif_neg, not_false_iff]
  | inr h => simp only [h.ne_empty, or_false, Nat.sInf_def, h, Nat.find_eq_zero]

Premises used: Nat.sInf_def, Nat.find_eq_zero, dif_neg, Set.eq_empty_or_nonempty, exists_false, Set.mem_empty_iff_false, or_false, not_false_iff, or_true, InfSet.sInf
-- Module: Mathlib.Data.Nat.Lattice
Goal:
rw : Membership.mem (γ := Set ℕ) ∅ 0 ∨ Eq (α := Set ℕ) ∅ ∅
⊢ Eq (α := ℕ) (sInf ∅) 0

Tactic:
rw [sInf_eq_zero]

Premises used: Nat.sInf_eq_zero
-- Module: Mathlib.Data.Nat.Lattice
Goal:
h : Eq (α := Set ℕ) ∅ ∅
⊢ Membership.mem (γ := Set ℕ) ∅ 0 ∨ Eq (α := Set ℕ) ∅ ∅

Tactic:
right
-- Module: Mathlib.Data.Nat.Lattice
Goal:
⊢ Eq (α := Set ℕ) ∅ ∅

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Lattice
Goal:
ι : Sort u_1
inst : IsEmpty ι
f : ι → ℕ
rw : Eq (α := ℕ) (sInf ∅) 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ iInf f = 0

Tactic:
rw [iInf_of_isEmpty, sInf_empty]

Premises used: Nat.sInf_empty, iInf_of_isEmpty
-- Module: Mathlib.Data.Nat.Lattice
Goal:
ι : Sort u_1
h : IsEmpty ι
⊢ Eq (α := ℕ) (⨅ (x : ι), 0) 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Lattice
Goal:
ι : Sort u_1
h : Nonempty ι
⊢ Membership.mem (γ := Set ℕ) (range fun (x : ι) ↦ 0) 0 ∨ Eq (α := Set ℕ) (range fun (x : ι) ↦ 0) ∅

Tactic:
simp
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : s.Nonempty
rw : Nat.find (p := fun (n : ℕ) ↦ n ∈ s) h ∈ s
⊢ sInf s ∈ s

Tactic:
rw [Nat.sInf_def h]

Premises used: Nat.sInf_def
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : s.Nonempty
⊢ Nat.find (p := fun (n : ℕ) ↦ n ∈ s) h ∈ s

Tactic:
Nat.find_spec h

Premises used: Set.Mem, Nat.find_spec
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : s.Nonempty
⊢ Nat.find (p := fun (n : ℕ) ↦ n ∈ s) h ∈ s

Tactic:
exact Nat.find_spec h

Premises used: Nat.find_spec
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : s.Nonempty
rw rw₁ rw₂ : Nat.find (p := fun (n : ℕ) ↦ n ∈ s) h ∈ s
⊢ sInf s ∈ s

Tactic:
classical
  rw [Nat.sInf_def h]
  exact Nat.find_spec h

Premises used: Nat.sInf_def
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s = ∅
inl : ∀ (hm : m < sInf ∅), m ∉ ∅
⊢ m ∉ s

Tactic:
subst h
-- Module: Mathlib.Data.Nat.Lattice
Goal:
m : ℕ
hm : m < sInf ∅
⊢ m ∉ ∅

Tactic:
apply notMem_empty

Premises used: Set.notMem_empty
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s.Nonempty
⊢ m < Nat.find (p := fun (n : ℕ) ↦ n ∈ s) h

Tactic:
rw [Nat.sInf_def h] at hm

Premises used: Nat.sInf_def
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
m : ℕ
h : s.Nonempty
hm : m < Nat.find (p := fun (n : ℕ) ↦ n ∈ s) h
⊢ m ∉ s

Tactic:
Nat.find_min h hm

Premises used: Nat.find_min
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
m : ℕ
h : s.Nonempty
hm : m < Nat.find (p := fun (n : ℕ) ↦ n ∈ s) h
⊢ m ∉ s

Tactic:
exact Nat.find_min h hm

Premises used: Nat.find_min
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
m : ℕ
hm : m < sInf s
⊢ s = ∅ ∨ s.Nonempty

Tactic:
cases eq_empty_or_nonempty s with
  | inl h => subst h; apply notMem_empty
  | inr h => rw [Nat.sInf_def h] at hm; exact Nat.find_min h hm

Premises used: Set.eq_empty_or_nonempty, Set.notMem_empty
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
m : ℕ
hm : m < sInf s
⊢ s = ∅ ∨ s.Nonempty

Tactic:
classical
  cases eq_empty_or_nonempty s with
  | inl h => subst h; apply notMem_empty
  | inr h => rw [Nat.sInf_def h] at hm; exact Nat.find_min h hm

Premises used: Set.eq_empty_or_nonempty, Set.notMem_empty
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
m : ℕ
hm : m ∈ s
rw : Nat.find (p := fun (n : ℕ) ↦ n ∈ s) ⋯ ≤ m
⊢ sInf s ≤ m

Tactic:
rw [Nat.sInf_def ⟨m, hm⟩]

Premises used: Nat.sInf_def, Exists.intro
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ Nat.find (p := fun (n : ℕ) ↦ n ∈ s) ⋯ ≤ m

Tactic:
Nat.find_min' ⟨m, hm⟩ hm

Premises used: Nat.find_min', Exists.intro
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ Nat.find (p := fun (n : ℕ) ↦ n ∈ s) ⋯ ≤ m

Tactic:
exact Nat.find_min' ⟨m, hm⟩ hm

Premises used: Nat.find_min', Exists.intro
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
m : ℕ
hm : m ∈ s
rw rw₁ rw₂ : Nat.find (p := fun (n : ℕ) ↦ n ∈ s) ⋯ ≤ m
⊢ sInf s ≤ m

Tactic:
classical
  rw [Nat.sInf_def ⟨m, hm⟩]
  exact Nat.find_min' ⟨m, hm⟩ hm

Premises used: Nat.sInf_def, Exists.intro
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : 0 < sInf s
by_contra : ∀ (contra : ¬s.Nonempty), False
⊢ s.Nonempty

Tactic:
by_contra contra
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : 0 < sInf s
contra : ¬s.Nonempty
⊢ s = ∅

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at contra

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
⊢ sInf s ≠ 0

Tactic:
have h' : sInf s ≠ 0 := ne_of_gt h
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
apply : sInf s = 0
⊢ False

Tactic:
apply h'