awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
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
⊢ 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
have e_a : lt l hl = Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
Tactic: rw [inductionOn'_self, strongRec_of_lt hl]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
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
⊢ 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
have e_a₁ : lt l hl = lt l hl
Tactic: rw [inductionOn'_self, strongRec_of_lt hl]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
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
⊢ 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
have e_a : (if hlm : l < m then lt l hlm
  else
    ge l sorry 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 sorry fun (k : ℤ) (x : k < l) ↦ ih k sorry)
        (fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l sorry) k_1 sorry) =
  Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
Tactic: rw [inductionOn'_add_one hmk]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
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
⊢ (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
have pos : ∀ (hlm : l < m), lt l hlm = Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
Tactic: split_ifs with hlm
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
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
⊢ (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
have neg : ∀ (hlm : ¬l < m),
  (ge l sorry 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 sorry fun (k : ℤ) (x : k < l) ↦ ih k sorry)
        (fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l sorry) k_1 sorry) =
    Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
Tactic: split_ifs with hlm
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
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
⊢ lt l hlm = Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
have pos : lt l hlm = lt l hlm
Tactic: rw [strongRec_of_lt hlm]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
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
⊢ (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
have neg : (ge l sorry 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 sorry) =
  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]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
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
⊢ (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
have neg₁ : (ge l sorry 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 sorry) =
  ge l sorry fun (k : ℤ) (x : k < l) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
Tactic: rw [ih' fun l hl ↦ ih l (Int.lt_trans hl k.lt_succ), ih _ hl]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
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
⊢ (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
have neg₂ : m ≤ l
Tactic: rw [ih' fun l hl ↦ ih l (Int.lt_trans hl k.lt_succ), ih _ hl]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
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
⊢ 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
have 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
Tactic: rw [inductionOn'_sub_one hkm, ih']
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
a : ℤ
h : 1 < a.natAbs
⊢ Function.Injective (β := ℤ) fun (x : ℕ) ↦ a ^ x
have refine : Function.Injective (α := ℕ) (natAbs ∘ fun (x : ℕ) ↦ a ^ x)
Tactic: refine (?_ : (natAbs ∘ (a ^ · : ℕ → ℤ)).Injective).of_comp
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
a : ℤ
h : 1 < a.natAbs
⊢ Function.Injective (α := ℕ) (natAbs ∘ fun (x : ℕ) ↦ a ^ x)
have h₁ : ∀ (x : ℕ), (natAbs ∘ fun (x : ℕ) ↦ a ^ x) x = a.natAbs ^ x
Tactic: convert! Nat.pow_right_injective h using 2
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
a : ℤ
h : 1 < a.natAbs
x : ℕ
⊢ (natAbs ∘ fun (x : ℕ) ↦ a ^ x) x = a.natAbs ^ x
have h₁ : (a ^ x).natAbs = a.natAbs ^ x
Tactic: rw [Function.comp_apply, natAbs_pow]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
a : ℤ
h : 1 < a.natAbs
x : ℕ
h₁ : (a ^ x).natAbs = a.natAbs ^ x
⊢ (natAbs ∘ fun (x : ℕ) ↦ a ^ x) x = a.natAbs ^ x
have h₂ : a.natAbs ^ x = a.natAbs ^ x
Tactic: rw [Function.comp_apply, natAbs_pow]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
n : ℤ
m : ℕ
⊢ (↑m : ℤ) ∣ n ↔ m ∣ n.natAbs
have inl : ∀ (hn : n = (↑n.natAbs : ℤ)), (↑m : ℤ) ∣ n ↔ m ∣ n.natAbs
Tactic: obtain hn | hn := natAbs_eq n
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
n : ℤ
m : ℕ
inl : ∀ (hn : n = (↑n.natAbs : ℤ)), (↑m : ℤ) ∣ n ↔ m ∣ n.natAbs
⊢ (↑m : ℤ) ∣ n ↔ m ∣ n.natAbs
have inr : ∀ (hn : n = -(↑n.natAbs : ℤ)), (↑m : ℤ) ∣ n ↔ m ∣ n.natAbs
Tactic: obtain hn | hn := natAbs_eq n
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
n : ℤ
m : ℕ
hn : n = (↑n.natAbs : ℤ)
⊢ (↑m : ℤ) ∣ n ↔ m ∣ n.natAbs
have inl : Dvd.dvd (α := ℤ) (↑m : ℤ) (↑n.natAbs : ℤ) ↔ m ∣ natAbs (↑n.natAbs : ℤ)
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
n : ℤ
m : ℕ
hn : n = -(↑n.natAbs : ℤ)
⊢ (↑m : ℤ) ∣ n ↔ m ∣ n.natAbs
have inr : Dvd.dvd (α := ℤ) (↑m : ℤ) (-(↑n.natAbs : ℤ)) ↔ m ∣ natAbs (-(↑n.natAbs : ℤ))
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m : ℤ
n : ℕ
⊢ m ∣ (↑n : ℤ) ↔ m.natAbs ∣ n
have inl : ∀ (hn : m = (↑m.natAbs : ℤ)), m ∣ (↑n : ℤ) ↔ m.natAbs ∣ n
Tactic: obtain hn | hn := natAbs_eq m
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m : ℤ
n : ℕ
inl : ∀ (hn : m = (↑m.natAbs : ℤ)), m ∣ (↑n : ℤ) ↔ m.natAbs ∣ n
⊢ m ∣ (↑n : ℤ) ↔ m.natAbs ∣ n
have inr : ∀ (hn : m = -(↑m.natAbs : ℤ)), m ∣ (↑n : ℤ) ↔ m.natAbs ∣ n
Tactic: obtain hn | hn := natAbs_eq m
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m : ℤ
n : ℕ
hn : m = (↑m.natAbs : ℤ)
⊢ m ∣ (↑n : ℤ) ↔ m.natAbs ∣ n
have inl : Dvd.dvd (α := ℤ) (↑m.natAbs : ℤ) (↑n : ℤ) ↔ natAbs (↑m.natAbs : ℤ) ∣ n
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m : ℤ
n : ℕ
hn : m = -(↑m.natAbs : ℤ)
⊢ m ∣ (↑n : ℤ) ↔ m.natAbs ∣ n
have inr : Dvd.dvd (α := ℤ) (-(↑m.natAbs : ℤ)) (↑n : ℤ) ↔ natAbs (-(↑m.natAbs : ℤ)) ∣ n
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m n : ℤ
| m.gcd n
have rw : (m % n).gcd n
Tactic: rw [← m.emod_add_mul_ediv n, gcd_add_mul_left_left]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m n : ℤ
⊢ (m % n).gcd n = m.gcd n
have conv_rhs : (m % n).gcd n = m.gcd n
Tactic: conv_rhs => rw [← m.emod_add_mul_ediv n, gcd_add_mul_left_left]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m n : ℤ
conv_rhs : (m % n).gcd n = m.gcd n
⊢ (m % n).gcd n = m.gcd n
have conv_rhs₁ : (m % n).gcd n = (m % n).gcd n
Tactic: conv_rhs => rw [← m.emod_add_mul_ediv n, gcd_add_mul_left_left]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ (subNatNat m n).bodd = (m.bodd ^^ n.bodd)
have hp : ∀ (i n : ℕ), bodd (↑i : ℤ) = ((n + i).bodd ^^ n.bodd)
Tactic: apply subNatNat_elim m n fun m n i => bodd i = xor m.bodd n.bodd
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
hp : ∀ (i n : ℕ), bodd (↑i : ℤ) = ((n + i).bodd ^^ n.bodd)
⊢ (subNatNat m n).bodd = (m.bodd ^^ n.bodd)
have hn : ∀ (i m : ℕ), -[i+1].bodd = (m.bodd ^^ (m + i + 1).bodd)
Tactic: apply subNatNat_elim m n fun m n i => bodd i = xor m.bodd n.bodd
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n i j : ℕ
⊢ bodd (↑i : ℤ) = ((j + i).bodd ^^ j.bodd)
have hp : i.bodd = (j.bodd ^^ i.bodd ^^ j.bodd)
Tactic: simp only [Int.bodd, Nat.bodd_add]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n i j : ℕ
⊢ -[i+1].bodd = (j.bodd ^^ (j + i + 1).bodd)
have hn : (!i.bodd) = (j.bodd ^^ (j.bodd ^^ i.bodd ^^ Nat.bodd 1))
Tactic: simp only [Int.bodd, Nat.bodd_add]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n i j : ℕ
⊢ i.bodd = (j.bodd ^^ i.bodd ^^ j.bodd)
have hp : false = (j.bodd ^^ false ^^ j.bodd)
Tactic: cases Nat.bodd i
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n i j : ℕ
hp : false = (j.bodd ^^ false ^^ j.bodd)
⊢ i.bodd = (j.bodd ^^ i.bodd ^^ j.bodd)
have hp₁ : true = (j.bodd ^^ true ^^ j.bodd)
Tactic: cases Nat.bodd i
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n i j : ℕ
⊢ (!i.bodd) = (j.bodd ^^ (j.bodd ^^ i.bodd ^^ Nat.bodd 1))
have hn : (!false) = (j.bodd ^^ (j.bodd ^^ false ^^ Nat.bodd 1))
Tactic: cases Nat.bodd i
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n i j : ℕ
hn : (!false) = (j.bodd ^^ (j.bodd ^^ false ^^ Nat.bodd 1))
⊢ (!i.bodd) = (j.bodd ^^ (j.bodd ^^ i.bodd ^^ Nat.bodd 1))
have hn₁ : (!true) = (j.bodd ^^ (j.bodd ^^ true ^^ Nat.bodd 1))
Tactic: cases Nat.bodd i
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℕ
⊢ (negOfNat n).bodd = n.bodd
have zero : (negOfNat 0).bodd = Nat.bodd 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℕ
zero : (negOfNat 0).bodd = Nat.bodd 0
⊢ (negOfNat n).bodd = n.bodd
have succ : ∀ (n : ℕ), (negOfNat (n + 1)).bodd = (n + 1).bodd
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℕ
⊢ (negOfNat (n + 1)).bodd = (n + 1).bodd
have succ : (negOfNat (n + 1)).bodd = !n.bodd
Tactic: simp +decide