awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.Basic
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
hn : m ≤ n
k : ℤ
hkm : k ≤ m
ih' :
  ∀
    (ih :
      ∀ (k_1 : ℤ),
        k_1 < k →
          ∀ (hn : m ≤ k_1),
            Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
              ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k),
    Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k → P k_1)
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
        (k_1 : ℤ) → k_1 < k → P k_1)
      fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
h_1 :
  ∀ (k_1 : ℤ),
    k_1 < k - 1 →
      ∀ (hn : m ≤ k_1),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
          ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
e_a :
  ∀ (l : ℤ) (hl : l < k - 1),
    Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) (k - 1) m lt
        (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
          if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
        (fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯) l hl =
      Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
⊢ Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k - 1 → P k_1)
    (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) (k - 1) m lt
        (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
          if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
        fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
      (k_1 : ℤ) → k_1 < k - 1 → P k_1)
    fun (k_1 : ℤ) (x : k_1 < k - 1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1

Tactic:
ext l hl
-- Module: Mathlib.Data.Int.Basic
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
hn : m ≤ n
h_1 :
  ∀ (k : ℤ),
    k < m →
      ∀ (hn : m ≤ k),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k =
          ge k hn fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
l : ℤ
hl : l < m
e_a : lt l hl = Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
e_a₁ e_a₂ : lt l hl = lt l hl
⊢ Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) m m lt
      (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
        if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
      (fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯) l hl =
    Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l

Tactic:
rw [inductionOn'_self, strongRec_of_lt hl]

Premises used: Int.strongRec_of_lt, Int.inductionOn'_self
-- Module: Mathlib.Data.Int.Basic
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  ∀
    (ih :
      ∀ (k_1 : ℤ),
        k_1 < k →
          ∀ (hn : m ≤ k_1),
            Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
              ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k),
    Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k → P k_1)
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
        (k_1 : ℤ) → k_1 < k → P k_1)
      fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
ih :
  ∀ (k_1 : ℤ),
    k_1 < k + 1 →
      ∀ (hn : m ≤ k_1),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
          ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
l : ℤ
hl : l < k + 1
e_a :
  (if hlm : l < m then lt l hlm
    else
      ge l ⋯ fun (k_1 : ℤ) (x : k_1 < l) ↦
        Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          (fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯) k_1 ⋯) =
    Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
⊢ Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) (k + 1) m lt
      (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
        if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
      (fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯) l hl =
    Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l

Tactic:
rw [inductionOn'_add_one hmk]

Premises used: Int.inductionOn'_add_one
-- Module: Mathlib.Data.Int.Basic
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  ∀
    (ih :
      ∀ (k_1 : ℤ),
        k_1 < k →
          ∀ (hn : m ≤ k_1),
            Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
              ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k),
    Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k → P k_1)
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
        (k_1 : ℤ) → k_1 < k → P k_1)
      fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
ih :
  ∀ (k_1 : ℤ),
    k_1 < k + 1 →
      ∀ (hn : m ≤ k_1),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
          ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
l : ℤ
hl : l < k + 1
pos : ∀ (hlm : l < m), lt l hlm = Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
neg :
  ∀ (hlm : ¬l < m),
    (ge l ⋯ fun (k_1 : ℤ) (x : k_1 < l) ↦
        Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          (fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯) k_1 ⋯) =
      Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
⊢ (if hlm : l < m then lt l hlm
    else
      ge l ⋯ fun (k_1 : ℤ) (x : k_1 < l) ↦
        Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          (fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯) k_1 ⋯) =
    Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l

Tactic:
split_ifs with hlm
-- Module: Mathlib.Data.Int.Basic
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  ∀
    (ih :
      ∀ (k_1 : ℤ),
        k_1 < k →
          ∀ (hn : m ≤ k_1),
            Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
              ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k),
    Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k → P k_1)
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
        (k_1 : ℤ) → k_1 < k → P k_1)
      fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
ih :
  ∀ (k_1 : ℤ),
    k_1 < k + 1 →
      ∀ (hn : m ≤ k_1),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
          ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
l : ℤ
hl : l < k + 1
hlm : l < m
pos pos₁ : lt l hlm = lt l hlm
⊢ lt l hlm = Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l

Tactic:
rw [strongRec_of_lt hlm]

Premises used: Int.strongRec_of_lt
-- Module: Mathlib.Data.Int.Basic
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  ∀
    (ih :
      ∀ (k_1 : ℤ),
        k_1 < k →
          ∀ (hn : m ≤ k_1),
            Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
              ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k),
    Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k → P k_1)
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
        (k_1 : ℤ) → k_1 < k → P k_1)
      fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
ih :
  ∀ (k_1 : ℤ),
    k_1 < k + 1 →
      ∀ (hn : m ≤ k_1),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
          ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
l : ℤ
hl : l < k + 1
hlm : ¬l < m
neg :
  (ge l ⋯ fun (k_1 : ℤ) (x : k_1 < l) ↦
      (fun (k_2 : ℤ) (x : k_2 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_2) k_1 ⋯) =
    Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
neg₁ :
  (ge l ⋯ fun (k_1 : ℤ) (x : k_1 < l) ↦
      (fun (k_2 : ℤ) (x : k_2 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_2) k_1 ⋯) =
    ge l ⋯ fun (k : ℤ) (x : k < l) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
neg₂ : m ≤ l
neg₃ :
  (ge l ⋯ fun (k_1 : ℤ) (x : k_1 < l) ↦
      (fun (k_2 : ℤ) (x : k_2 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_2) k_1 ⋯) =
    ge l ⋯ fun (k : ℤ) (x : k < l) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
neg₄ : m ≤ l
⊢ (ge l ⋯ fun (k_1 : ℤ) (x : k_1 < l) ↦
      Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
        (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
          if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
        (fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯) k_1 ⋯) =
    Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l

Tactic:
rw [ih' fun l hl ↦ ih l (Int.lt_trans hl k.lt_succ), ih _ hl]

Premises used: Int.lt_succ, Int.lt_trans
-- Module: Mathlib.Data.Int.Basic
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
hn : m ≤ n
k : ℤ
hkm : k ≤ m
ih' :
  ∀
    (ih :
      ∀ (k_1 : ℤ),
        k_1 < k →
          ∀ (hn : m ≤ k_1),
            Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
              ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k),
    Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k → P k_1)
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
        (k_1 : ℤ) → k_1 < k → P k_1)
      fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
h_1 :
  ∀ (k_1 : ℤ),
    k_1 < k - 1 →
      ∀ (hn : m ≤ k_1),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
          ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
l : ℤ
hl : l < k - 1
e_a :
  ∀ (k_1 : ℤ),
    k_1 < k →
      ∀ (hn : m ≤ k_1),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
          ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
⊢ Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) (k - 1) m lt
      (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
        if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
      (fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯) l hl =
    Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l

Tactic:
rw [inductionOn'_sub_one hkm, ih']

Premises used: Int.inductionOn'_sub_one
-- Module: Mathlib.Data.Int.Basic
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
hn : m ≤ n
k : ℤ
hkm : k ≤ m
ih' :
  ∀
    (ih :
      ∀ (k_1 : ℤ),
        k_1 < k →
          ∀ (hn : m ≤ k_1),
            Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
              ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k),
    Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k → P k_1)
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
        (k_1 : ℤ) → k_1 < k → P k_1)
      fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
h_1 :
  ∀ (k_1 : ℤ),
    k_1 < k - 1 →
      ∀ (hn : m ≤ k_1),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
          ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
l : ℤ
hl : l < k - 1
⊢ ∀ (k_1 : ℤ),
    k_1 < k →
      ∀ (hn : m ≤ k_1),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
          ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k

Tactic:
fun l hlk hml ↦ (Int.not_lt.mpr hkm <| Int.lt_of_le_of_lt hml hlk).elim

Premises used: Iff.mpr, Int.lt_of_le_of_lt, False.elim, Int.not_lt
-- Module: Mathlib.Data.Int.Basic
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
hn : m ≤ n
k : ℤ
hkm : k ≤ m
ih' :
  ∀
    (ih :
      ∀ (k_1 : ℤ),
        k_1 < k →
          ∀ (hn : m ≤ k_1),
            Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
              ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k),
    Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k → P k_1)
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
        (k_1 : ℤ) → k_1 < k → P k_1)
      fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
h_1 :
  ∀ (k_1 : ℤ),
    k_1 < k - 1 →
      ∀ (hn : m ≤ k_1),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
          ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
l : ℤ
hl : l < k - 1
⊢ ∀ (k_1 : ℤ),
    k_1 < k →
      ∀ (hn : m ≤ k_1),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
          ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k

Tactic:
exact fun l hlk hml ↦ (Int.not_lt.mpr hkm <| Int.lt_of_le_of_lt hml hlk).elim

Premises used: Iff.mpr, Int.lt_of_le_of_lt, False.elim, Int.not_lt
-- Module: Mathlib.Data.Int.Basic
Goal:
⊢ Function.Surjective natAbs

Tactic:
fun n => ⟨n, natAbs_natCast n⟩

Premises used: Nat.cast, Exists.intro, Int.natAbs_natCast, Function.Surjective
-- Module: Mathlib.Data.Int.Basic
Goal:
a : ℤ
h : 1 < a.natAbs
⊢ Function.Injective (β := ℤ) fun (x : ℕ) ↦ a ^ x

Tactic:
(?_ : (natAbs ∘ (a ^ · : ℕ → ℤ)).Injective).of_comp

Premises used: Function.Injective.of_comp
-- Module: Mathlib.Data.Int.Basic
Goal:
a : ℤ
h : 1 < a.natAbs
refine : Function.Injective (α := ℕ) (natAbs ∘ fun (x : ℕ) ↦ a ^ x)
⊢ Function.Injective (β := ℤ) fun (x : ℕ) ↦ a ^ x

Tactic:
refine (?_ : (natAbs ∘ (a ^ · : ℕ → ℤ)).Injective).of_comp

Premises used: Function.Injective.of_comp
-- Module: Mathlib.Data.Int.Basic
Goal:
a : ℤ
h : 1 < a.natAbs
⊢ Function.Injective (β := ℕ) fun (x : ℕ) ↦ a.natAbs ^ x

Tactic:
Nat.pow_right_injective h

Premises used: Nat.pow_right_injective
-- Module: Mathlib.Data.Int.Basic
Goal:
a : ℤ
h : 1 < a.natAbs
h₁ : ∀ (x : ℕ), (natAbs ∘ fun (x : ℕ) ↦ a ^ x) x = a.natAbs ^ x
⊢ Function.Injective (α := ℕ) (natAbs ∘ fun (x : ℕ) ↦ a ^ x)

Tactic:
convert! Nat.pow_right_injective h using 2

Premises used: Nat.pow_right_injective
-- Module: Mathlib.Data.Int.Basic
Goal:
a : ℤ
h : 1 < a.natAbs
x : ℕ
h₁ : (a ^ x).natAbs = a.natAbs ^ x
h₂ h₃ : a.natAbs ^ x = a.natAbs ^ x
⊢ (natAbs ∘ fun (x : ℕ) ↦ a ^ x) x = a.natAbs ^ x

Tactic:
rw [Function.comp_apply, natAbs_pow]

Premises used: Int.natAbs_pow, Function.comp_apply
-- Module: Mathlib.Data.Int.Basic
Goal:
x y : ℕ
⊢ Dvd.dvd (α := ℤ) (OfNat.ofNat x) (↑y : ℤ) ↔ OfNat.ofNat x ∣ y

Tactic:
natCast_dvd_natCast

Premises used: Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Int.Basic
Goal:
x y : ℕ
⊢ Dvd.dvd (α := ℤ) (↑x : ℤ) (OfNat.ofNat y) ↔ x ∣ OfNat.ofNat y

Tactic:
natCast_dvd_natCast

Premises used: Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Int.Basic
Goal:
n : ℤ
m : ℕ
inl : ∀ (hn : n = (↑n.natAbs : ℤ)), (↑m : ℤ) ∣ n ↔ m ∣ n.natAbs
inr : ∀ (hn : n = -(↑n.natAbs : ℤ)), (↑m : ℤ) ∣ n ↔ m ∣ n.natAbs
⊢ (↑m : ℤ) ∣ n ↔ m ∣ n.natAbs

Tactic:
obtain hn | hn := natAbs_eq n

Premises used: Int.natAbs_eq
-- Module: Mathlib.Data.Int.Basic
Goal:
n : ℤ
m : ℕ
hn : n = (↑n.natAbs : ℤ)
inl : Dvd.dvd (α := ℤ) (↑m : ℤ) (↑n.natAbs : ℤ) ↔ m ∣ natAbs (↑n.natAbs : ℤ)
⊢ (↑m : ℤ) ∣ n ↔ m ∣ n.natAbs

Tactic:
rw [hn]
-- Module: Mathlib.Data.Int.Basic
Goal:
n : ℤ
m : ℕ
hn : n = -(↑n.natAbs : ℤ)
inr : Dvd.dvd (α := ℤ) (↑m : ℤ) (-(↑n.natAbs : ℤ)) ↔ m ∣ natAbs (-(↑n.natAbs : ℤ))
⊢ (↑m : ℤ) ∣ n ↔ m ∣ n.natAbs

Tactic:
rw [hn]
-- Module: Mathlib.Data.Int.Basic
Goal:
n : ℤ
m : ℕ
hn : n = (↑n.natAbs : ℤ)
⊢ Dvd.dvd (α := ℤ) (↑m : ℤ) (↑n.natAbs : ℤ) ↔ m ∣ natAbs (↑n.natAbs : ℤ)

Tactic:
simp [← natCast_dvd_natCast, Int.dvd_neg]

Premises used: Int.dvd_neg, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Int.Basic
Goal:
n : ℤ
m : ℕ
hn : n = -(↑n.natAbs : ℤ)
⊢ Dvd.dvd (α := ℤ) (↑m : ℤ) (-(↑n.natAbs : ℤ)) ↔ m ∣ natAbs (-(↑n.natAbs : ℤ))

Tactic:
simp [← natCast_dvd_natCast, Int.dvd_neg]

Premises used: Int.dvd_neg, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Int.Basic
Goal:
m : ℤ
n : ℕ
inl : ∀ (hn : m = (↑m.natAbs : ℤ)), m ∣ (↑n : ℤ) ↔ m.natAbs ∣ n
inr : ∀ (hn : m = -(↑m.natAbs : ℤ)), m ∣ (↑n : ℤ) ↔ m.natAbs ∣ n
⊢ m ∣ (↑n : ℤ) ↔ m.natAbs ∣ n

Tactic:
obtain hn | hn := natAbs_eq m

Premises used: Int.natAbs_eq
-- Module: Mathlib.Data.Int.Basic
Goal:
m : ℤ
n : ℕ
hn : m = (↑m.natAbs : ℤ)
inl : Dvd.dvd (α := ℤ) (↑m.natAbs : ℤ) (↑n : ℤ) ↔ natAbs (↑m.natAbs : ℤ) ∣ n
⊢ m ∣ (↑n : ℤ) ↔ m.natAbs ∣ n

Tactic:
rw [hn]
-- Module: Mathlib.Data.Int.Basic
Goal:
m : ℤ
n : ℕ
hn : m = -(↑m.natAbs : ℤ)
inr : Dvd.dvd (α := ℤ) (-(↑m.natAbs : ℤ)) (↑n : ℤ) ↔ natAbs (-(↑m.natAbs : ℤ)) ∣ n
⊢ m ∣ (↑n : ℤ) ↔ m.natAbs ∣ n

Tactic:
rw [hn]
-- Module: Mathlib.Data.Int.Basic
Goal:
m : ℤ
n : ℕ
hn : m = (↑m.natAbs : ℤ)
⊢ Dvd.dvd (α := ℤ) (↑m.natAbs : ℤ) (↑n : ℤ) ↔ natAbs (↑m.natAbs : ℤ) ∣ n

Tactic:
simp [← natCast_dvd_natCast, Int.neg_dvd]

Premises used: Int.neg_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Int.Basic
Goal:
m : ℤ
n : ℕ
hn : m = -(↑m.natAbs : ℤ)
⊢ Dvd.dvd (α := ℤ) (-(↑m.natAbs : ℤ)) (↑n : ℤ) ↔ natAbs (-(↑m.natAbs : ℤ)) ∣ n

Tactic:
simp [← natCast_dvd_natCast, Int.neg_dvd]

Premises used: Int.neg_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Int.Basic
Goal:
m n : ℤ
hm : 0 ≤ m
hmn : m < n
hnm : n ∣ m
⊢ m = 0

Tactic:
eq_zero_of_dvd_of_natAbs_lt_natAbs hnm (natAbs_lt_natAbs_of_nonneg_of_lt hm hmn)

Premises used: Int.natAbs_lt_natAbs_of_nonneg_of_lt, Int.eq_zero_of_dvd_of_natAbs_lt_natAbs
-- Module: Mathlib.Data.Int.Basic
Goal:
a b c : ℤ
h1 : a % b = c
h2 : (a - c).natAbs < b.natAbs
⊢ a = c

Tactic:
Int.eq_of_sub_eq_zero (eq_zero_of_dvd_of_natAbs_lt_natAbs (dvd_self_sub_of_emod_eq h1) h2)

Premises used: Int.eq_zero_of_dvd_of_natAbs_lt_natAbs, Int.dvd_self_sub_of_emod_eq, Int.eq_of_sub_eq_zero
-- Module: Mathlib.Data.Int.Basic
Goal:
m n : ℤ
hmn : m ∣ n
hn : n ≠ 0
⊢ m.natAbs ≤ n.natAbs

Tactic:
not_lt.mp (mt (eq_zero_of_dvd_of_natAbs_lt_natAbs hmn) hn)

Premises used: mt, Int.eq_zero_of_dvd_of_natAbs_lt_natAbs, not_lt, Iff.mp
-- Module: Mathlib.Data.Int.Basic
Goal:
m n : ℤ
rw : (m % n).gcd n
| m.gcd n

Tactic:
rw [← m.emod_add_mul_ediv n, gcd_add_mul_left_left]

Premises used: Int.emod_add_mul_ediv, Int.gcd_add_mul_left_left
-- Module: Mathlib.Data.Int.Basic
Goal:
m n : ℤ
conv_rhs : (m % n).gcd n = m.gcd n
conv_rhs₁ : (m % n).gcd n = (m % n).gcd n
⊢ (m % n).gcd n = m.gcd n

Tactic:
conv_rhs => rw [← m.emod_add_mul_ediv n, gcd_add_mul_left_left]

Premises used: Int.emod_add_mul_ediv, Int.gcd_add_mul_left_left
-- Module: Mathlib.Data.Int.Bitwise
Goal:
⊢ bodd 0 = false

Tactic:
rfl

Premises used: Int.bodd, Nat.testBit, rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
⊢ bodd 1 = true

Tactic:
rfl

Premises used: Int.bodd, Nat.testBit, rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
⊢ bodd 2 = false

Tactic:
rfl

Premises used: Int.bodd, Nat.testBit, rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
⊢ bodd (↑n : ℤ) = n.bodd

Tactic:
rfl

Premises used: Int.bodd, rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
hp : ∀ (i n : ℕ), bodd (↑i : ℤ) = ((n + i).bodd ^^ n.bodd)
hn : ∀ (i m : ℕ), -[i+1].bodd = (m.bodd ^^ (m + i + 1).bodd)
⊢ (subNatNat m n).bodd = (m.bodd ^^ n.bodd)

Tactic:
apply subNatNat_elim m n fun m n i => bodd i = xor m.bodd n.bodd

Premises used: Int.bodd, Bool.xor, Int.subNatNat_elim, Nat.bodd, Eq
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n i j : ℕ
hp : i.bodd = (j.bodd ^^ i.bodd ^^ j.bodd)
⊢ bodd (↑i : ℤ) = ((j + i).bodd ^^ j.bodd)

Tactic:
simp only [Int.bodd, Nat.bodd_add]

Premises used: Int.bodd, Nat.bodd_add
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n i j : ℕ
hn : (!i.bodd) = (j.bodd ^^ (j.bodd ^^ i.bodd ^^ Nat.bodd 1))
⊢ -[i+1].bodd = (j.bodd ^^ (j + i + 1).bodd)

Tactic:
simp only [Int.bodd, Nat.bodd_add]

Premises used: Int.bodd, Nat.bodd_add
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n i j : ℕ
hp : false = (j.bodd ^^ false ^^ j.bodd)
hp₁ : true = (j.bodd ^^ true ^^ j.bodd)
⊢ i.bodd = (j.bodd ^^ i.bodd ^^ j.bodd)

Tactic:
cases Nat.bodd i

Premises used: Nat.bodd
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n i j : ℕ
hn : (!false) = (j.bodd ^^ (j.bodd ^^ false ^^ Nat.bodd 1))
hn₁ : (!true) = (j.bodd ^^ (j.bodd ^^ true ^^ Nat.bodd 1))
⊢ (!i.bodd) = (j.bodd ^^ (j.bodd ^^ i.bodd ^^ Nat.bodd 1))

Tactic:
cases Nat.bodd i

Premises used: Nat.bodd
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n i j : ℕ
⊢ false = (j.bodd ^^ false ^^ j.bodd)

Tactic:
simp