awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
pos :
  z = b →
    cast ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - 1 - b with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] =>
          match (motive := (x : ℕ) → motive (b + -[x+1])) n with
          | 0 => pred b ⋯ zero
          | n.succ =>
            cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))) =
      pred z hz
        (cast ⋯
          (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - b with
          | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
          | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))
neg :
  ¬z = b →
    cast ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - 1 - b with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] =>
          match (motive := (x : ℕ) → motive (b + -[x+1])) n with
          | 0 => pred b ⋯ zero
          | n.succ =>
            cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))) =
      pred z hz
        (cast ⋯
          (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - b with
          | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
          | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))
⊢ cast ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - 1 - b with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] =>
        match (motive := (x : ℕ) → motive (b + -[x+1])) n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))) =
    pred z hz
      (cast ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - b with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))

Tactic:
by_cases z = b
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h : z = b
⊢ z - 1 - b = -[(b - z).toNat+1]

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h : z = b
⊢ z - b = 0

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h : z = b
pos :
  cast (α := (fun (x : ℤ) ↦ motive x) (b + -[(b - z).toNat+1])) ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) -[(b - z).toNat+1] with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] =>
        match (motive := (x : ℕ) → motive (b + -[x+1])) n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))) =
    pred z hz
      (cast (α := (fun (x : ℤ) ↦ motive x) (b + 0)) ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) 0 with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))
⊢ cast ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - 1 - b with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] =>
        match (motive := (x : ℕ) → motive (b + -[x+1])) n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))) =
    pred z hz
      (cast ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - b with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))

Tactic:
rw! [show z - 1 - b = -[(b - z).toNat+1] by lia, show z - b = 0 by lia]
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h : z = b
⊢ cast (α := (fun (x : ℤ) ↦ motive x) (b + -[(b - z).toNat+1])) ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) -[(b - z).toNat+1] with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] =>
        match (motive := (x : ℕ) → motive (b + -[x+1])) n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))) =
    pred z hz
      (cast (α := (fun (x : ℤ) ↦ motive x) (b + 0)) ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) 0 with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))

Tactic:
grind [inductionOn'.pos]

Premises used: Int.inductionOn'.pos
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h : ¬z = b
⊢ z - 1 - b = -[(b - z).toNat+1]

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h : ¬z = b
⊢ z - b = -[(b - z - 1).toNat+1]

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h : ¬z = b
neg :
  cast (α := (fun (x : ℤ) ↦ motive x) (b + -[(b - z).toNat+1])) ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) -[(b - z).toNat+1] with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] =>
        match (motive := (x : ℕ) → motive (b + -[x+1])) n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))) =
    pred z hz
      (cast (α := (fun (x : ℤ) ↦ motive x) (b + -[(b - z - 1).toNat+1])) ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) -[(b - z - 1).toNat+1] with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))
⊢ cast ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - 1 - b with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] =>
        match (motive := (x : ℕ) → motive (b + -[x+1])) n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))) =
    pred z hz
      (cast ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - b with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))

Tactic:
rw! [show z - 1 - b = -[(b - z).toNat+1] by lia, show z - b = -[(b - z - 1).toNat+1] by lia]
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h : ¬z = b
⊢ cast (α := (fun (x : ℤ) ↦ motive x) (b + -[(b - z).toNat+1])) ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) -[(b - z).toNat+1] with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] =>
        match (motive := (x : ℕ) → motive (b + -[x+1])) n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))) =
    pred z hz
      (cast (α := (fun (x : ℤ) ↦ motive x) (b + -[(b - z - 1).toNat+1])) ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) -[(b - z - 1).toNat+1] with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))

Tactic:
grind
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d m_1 n_1 m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
n x : ℤ
h : x ≤ m
x_1 : (hmn : m ≤ x) → motive x hmn
h_1 : m ≤ x - 1
⊢ False

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
rw :
  Int.inductionOn' (motive := fun (x : ℤ) ↦ (hmn : m ≤ x) → motive x hmn) m m (fun (x : m ≤ m) ↦ base)
      (fun (k : ℤ) (hle : m ≤ k) (ih : (hmn : m ≤ k) → motive k hmn) (x : m ≤ k + 1) ↦ succ k hle (ih hle))
      (fun (x : ℤ) (x_1 : x ≤ m) (x_2 : (hmn : m ≤ x) → motive x hmn) (x_3 : m ≤ x - 1) ↦ ⋯.elim) ⋯ =
    base
rw₁ rw₂ : base = base
⊢ Int.leInduction (motive := motive) base succ m ⋯ = base

Tactic:
rw [Int.leInduction, inductionOn'_self]

Premises used: Int.inductionOn'_self
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d m_1 n_1 m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
n : ℤ
hmn : m ≤ n
⊢ m ≤ n + 1

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
n : ℤ
hmn : m ≤ n
rw :
  succ n hmn
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (hmn : m ≤ x) → motive x hmn) n m (fun (x : m ≤ m) ↦ base)
        (fun (k : ℤ) (hle : m ≤ k) (ih : (hmn : m ≤ k) → motive k hmn) (x : m ≤ k + 1) ↦ succ k hle (ih hle))
        (fun (x : ℤ) (x_1 : x ≤ m) (x_2 : (hmn : m ≤ x) → motive x hmn) (x_3 : m ≤ x - 1) ↦ ⋯.elim) hmn) =
    succ n hmn (Int.leInduction (motive := motive) base succ n hmn)
⊢ Int.leInduction (motive := motive) base succ (n + 1) ⋯ =
    succ n hmn (Int.leInduction (motive := motive) base succ n hmn)

Tactic:
rw [Int.leInduction, inductionOn'_add_one hmn]

Premises used: Int.inductionOn'_add_one
-- Module: Mathlib.Data.Int.Init
Goal:
m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
n : ℤ
hmn : m ≤ n
⊢ succ n hmn
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (hmn : m ≤ x) → motive x hmn) n m (fun (x : m ≤ m) ↦ base)
        (fun (k : ℤ) (hle : m ≤ k) (ih : (hmn : m ≤ k) → motive k hmn) (x : m ≤ k + 1) ↦ succ k hle (ih hle))
        (fun (x : ℤ) (x_1 : x ≤ m) (x_2 : (hmn : m ≤ x) → motive x hmn) (x_3 : m ≤ x - 1) ↦ ⋯.elim) hmn) =
    succ n hmn (Int.leInduction (motive := motive) base succ n hmn)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d m_1 n_1 m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
n : ℤ
hnm : n ≤ m
⊢ n - 1 ≤ m

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d m_1 n_1 m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n x : ℤ
h : m ≤ x
x_1 : (hnm : x ≤ m) → motive x hnm
h_1 : x + 1 ≤ m
⊢ False

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
rw :
  Int.inductionOn' (motive := fun (x : ℤ) ↦ (hnm : x ≤ m) → motive x hnm) m m (fun (x : m ≤ m) ↦ base)
      (fun (x : ℤ) (x_1 : m ≤ x) (x_2 : (hnm : x ≤ m) → motive x hnm) (x_3 : x + 1 ≤ m) ↦ ⋯.elim)
      (fun (k : ℤ) (hle : k ≤ m) (ih : (hnm : k ≤ m) → motive k hnm) (x : k - 1 ≤ m) ↦ pred k hle (ih hle)) ⋯ =
    base
rw₁ rw₂ : base = base
⊢ Int.leInductionDown (motive := motive) base pred m ⋯ = base

Tactic:
rw [Int.leInductionDown, inductionOn'_self]

Premises used: Int.inductionOn'_self
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d m_1 n_1 m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n : ℤ
hnm : n ≤ m
⊢ n - 1 ≤ m

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n : ℤ
hnm : n ≤ m
rw :
  pred n hnm
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (hnm : x ≤ m) → motive x hnm) n m (fun (x : m ≤ m) ↦ base)
        (fun (x : ℤ) (x_1 : m ≤ x) (x_2 : (hnm : x ≤ m) → motive x hnm) (x_3 : x + 1 ≤ m) ↦ ⋯.elim)
        (fun (k : ℤ) (hle : k ≤ m) (ih : (hnm : k ≤ m) → motive k hnm) (x : k - 1 ≤ m) ↦ pred k hle (ih hle)) hnm) =
    pred n hnm (Int.leInductionDown (motive := motive) base pred n hnm)
⊢ Int.leInductionDown (motive := motive) base pred (n - 1) ⋯ =
    pred n hnm (Int.leInductionDown (motive := motive) base pred n hnm)

Tactic:
rw [Int.leInductionDown, inductionOn'_sub_one hnm]

Premises used: Int.inductionOn'_sub_one
-- Module: Mathlib.Data.Int.Init
Goal:
m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n : ℤ
hnm : n ≤ m
⊢ pred n hnm
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (hnm : x ≤ m) → motive x hnm) n m (fun (x : m ≤ m) ↦ base)
        (fun (x : ℤ) (x_1 : m ≤ x) (x_2 : (hnm : x ≤ m) → motive x hnm) (x_3 : x + 1 ≤ m) ↦ ⋯.elim)
        (fun (k : ℤ) (hle : k ≤ m) (ih : (hnm : k ≤ m) → motive k hnm) (x : k - 1 ≤ m) ↦ pred k hle (ih hle)) hnm) =
    pred n hnm (Int.leInductionDown (motive := motive) base pred n hnm)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d m n_1 : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
⊢ n ≥ m

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d m n_1 : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
refine_1 : (hnm : ¬n < m) → (k : ℤ) → m ≤ k → ((k_1 : ℤ) → k_1 < k → motive k_1) → (k_1 : ℤ) → k_1 < k + 1 → motive k_1
refine_2 : (hnm : ¬n < m) → (k : ℤ) → k ≤ m → ((k_1 : ℤ) → k_1 < k → motive k_1) → (k_1 : ℤ) → k_1 < k - 1 → motive k_1
⊢ motive n

Tactic:
refine if hnm : n < m then lt n hnm else ge n (by lia) (n.inductionOn' m lt ?_ ?_)

Premises used: Int.inductionOn'
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d m n_1 : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
_n : ℤ
refine_1 : m ≤ _n → ((k : ℤ) → k < _n → motive k) → (k : ℤ) → k < _n + 1 → motive k
⊢ m ≤ _n → ((k : ℤ) → k < _n → motive k) → (k : ℤ) → k < _n + 1 → motive k

Tactic:
_
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d m n_1 : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
_n : ℤ
h : m ≤ _n
ih : (k : ℤ) → k < _n → motive k
l : ℤ
refine_1 : l < _n + 1 → motive l
⊢ l < _n + 1 → motive l

Tactic:
_
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d m n_1 : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
_n : ℤ
h : m ≤ _n
ih : (k : ℤ) → k < _n → motive k
l : ℤ
h_1 : l < _n + 1
hlm : ¬l < m
⊢ l ≥ m

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d m n_1 : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
_n : ℤ
h : m ≤ _n
ih : (k : ℤ) → k < _n → motive k
l : ℤ
h_1 : l < _n + 1
hlm : ¬l < m
k : ℤ
h_2 : k < l
⊢ k < _n

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d m n_1 : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
_n : ℤ
h : m ≤ _n
ih : (k : ℤ) → k < _n → motive k
l : ℤ
h_1 : l < _n + 1
⊢ motive l

Tactic:
exact if hlm : l < m then lt l hlm else ge l (by lia) fun k _ ↦ ih k (by lia)
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d m n_1 : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n_2 : ℤ
hnm : ¬n_2 < m
n : ℤ
h : n ≤ m
hn : (k : ℤ) → k < n → motive k
l : ℤ
h_1 : l < n - 1
⊢ l < n

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d m n_1 : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
⊢ (k : ℤ) → k ≤ m → ((k_1 : ℤ) → k_1 < k → motive k_1) → (k_1 : ℤ) → k_1 < k - 1 → motive k_1

Tactic:
exact fun n _ hn l _ ↦ hn l (by lia)
-- Module: Mathlib.Data.Int.Init
Goal:
m n : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
hn : n < m
⊢ Int.strongRec (motive := fun (x : ℤ) ↦ motive x) lt ge n = lt n hn

Tactic:
dif_pos _

Premises used: Int.strongRec, dif_pos
-- Module: Mathlib.Data.Int.Init
Goal:
a : ℤ
⊢ a.sign * a = (↑a.natAbs : ℤ)

Tactic:
sign_mul_self a

Premises used: Int.sign_mul_self
-- Module: Mathlib.Data.Int.Init
Goal:
m n : ℕ
⊢ (↑(m / n) : ℤ) = HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑n : ℤ)

Tactic:
natCast_ediv m n

Premises used: Int.natCast_ediv
-- Module: Mathlib.Data.Int.Init
Goal:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
⊢ - -[m+1] = HAdd.hAdd (α := ℤ) (↑m : ℤ) 1

Tactic:
rfl
-- Module: Mathlib.Data.Int.Init
Goal:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
rw : -[m+1].ediv (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = -((↑m : ℤ) / HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)
⊢ -[m+1].ediv (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    -((HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - 1) / HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)

Tactic:
rw [Int.add_sub_cancel]

Premises used: Int.add_sub_cancel
-- Module: Mathlib.Data.Int.Init
Goal:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
⊢ -[m+1].ediv (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = -((↑m : ℤ) / HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Init
Goal:
m n : ℕ
⊢ (↑(m % n) : ℤ) = HMod.hMod (α := ℤ) (↑m : ℤ) (↑n : ℤ)

Tactic:
rfl

Premises used: Int.emod, Int.natAbs, rfl
-- Module: Mathlib.Data.Int.Init
Goal:
a b c : ℤ
hb : 0 < b
hba : b ∣ a
⊢ a / b ≤ c ↔ a ≤ b * c

Tactic:
ediv_le_iff_of_dvd_of_pos hb hba

Premises used: Int.ediv_le_iff_of_dvd_of_pos
-- Module: Mathlib.Data.Int.Init
Goal:
a b c : ℤ
hb : b < 0
hba : b ∣ a
⊢ a / b ≤ c ↔ b * c ≤ a

Tactic:
ediv_le_iff_of_dvd_of_neg hb hba

Premises used: Int.ediv_le_iff_of_dvd_of_neg
-- Module: Mathlib.Data.Int.Init
Goal:
a b c : ℤ
hb : 0 < b
hba : b ∣ a
⊢ a / b < c ↔ a < b * c

Tactic:
ediv_lt_iff_of_dvd_of_pos hb hba

Premises used: Int.ediv_lt_iff_of_dvd_of_pos
-- Module: Mathlib.Data.Int.Init
Goal:
a b c : ℤ
hb : b < 0
hba : b ∣ a
⊢ a / b < c ↔ b * c < a

Tactic:
ediv_lt_iff_of_dvd_of_neg hb hba

Premises used: Int.ediv_lt_iff_of_dvd_of_neg
-- Module: Mathlib.Data.Int.Init
Goal:
a b c : ℤ
hc : 0 < c
hcb : c ∣ b
⊢ a ≤ b / c ↔ c * a ≤ b

Tactic:
le_ediv_iff_of_dvd_of_pos hc hcb

Premises used: Int.le_ediv_iff_of_dvd_of_pos
-- Module: Mathlib.Data.Int.Init
Goal:
a b c : ℤ
hc : c < 0
hcb : c ∣ b
⊢ a ≤ b / c ↔ b ≤ c * a

Tactic:
le_ediv_iff_of_dvd_of_neg hc hcb

Premises used: Int.le_ediv_iff_of_dvd_of_neg
-- Module: Mathlib.Data.Int.Init
Goal:
a b c : ℤ
hc : 0 < c
hcb : c ∣ b
⊢ a < b / c ↔ c * a < b

Tactic:
lt_ediv_iff_of_dvd_of_pos hc hcb

Premises used: Int.lt_ediv_iff_of_dvd_of_pos
-- Module: Mathlib.Data.Int.Init
Goal:
a b c : ℤ
hc : c < 0
hcb : c ∣ b
⊢ a < b / c ↔ b < c * a

Tactic:
lt_ediv_iff_of_dvd_of_neg hc hcb

Premises used: Int.lt_ediv_iff_of_dvd_of_neg
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d : ℤ
hb : 0 < b
hd : 0 < d
hba : b ∣ a
hdc : d ∣ c
⊢ a / b ≤ c / d ↔ d * a ≤ c * b

Tactic:
ediv_le_ediv_iff_of_dvd_of_pos_of_pos hb hd hba hdc

Premises used: Int.ediv_le_ediv_iff_of_dvd_of_pos_of_pos
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d : ℤ
hb : 0 < b
hd : d < 0
hba : b ∣ a
hdc : d ∣ c
⊢ a / b ≤ c / d ↔ c * b ≤ d * a

Tactic:
ediv_le_ediv_iff_of_dvd_of_pos_of_neg hb hd hba hdc

Premises used: Int.ediv_le_ediv_iff_of_dvd_of_pos_of_neg
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d : ℤ
hb : b < 0
hd : 0 < d
hba : b ∣ a
hdc : d ∣ c
⊢ a / b ≤ c / d ↔ c * b ≤ d * a

Tactic:
ediv_le_ediv_iff_of_dvd_of_neg_of_pos hb hd hba hdc

Premises used: Int.ediv_le_ediv_iff_of_dvd_of_neg_of_pos
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d : ℤ
hb : b < 0
hd : d < 0
hba : b ∣ a
hdc : d ∣ c
⊢ a / b ≤ c / d ↔ d * a ≤ c * b

Tactic:
ediv_le_ediv_iff_of_dvd_of_neg_of_neg hb hd hba hdc

Premises used: Int.ediv_le_ediv_iff_of_dvd_of_neg_of_neg
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d : ℤ
hb : 0 < b
hd : 0 < d
hba : b ∣ a
hdc : d ∣ c
⊢ a / b < c / d ↔ d * a < c * b

Tactic:
ediv_lt_ediv_iff_of_dvd_of_pos hb hd hba hdc

Premises used: Int.ediv_lt_ediv_iff_of_dvd_of_pos
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d : ℤ
hb : 0 < b
hd : d < 0
hba : b ∣ a
hdc : d ∣ c
⊢ a / b < c / d ↔ c * b < d * a

Tactic:
ediv_lt_ediv_iff_of_dvd_of_pos_of_neg hb hd hba hdc

Premises used: Int.ediv_lt_ediv_iff_of_dvd_of_pos_of_neg
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d : ℤ
hb : b < 0
hd : 0 < d
hba : b ∣ a
hdc : d ∣ c
⊢ a / b < c / d ↔ c * b < d * a

Tactic:
ediv_lt_ediv_iff_of_dvd_of_neg_of_pos hb hd hba hdc

Premises used: Int.ediv_lt_ediv_iff_of_dvd_of_neg_of_pos
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d : ℤ
hb : b < 0
hd : d < 0
hba : b ∣ a
hdc : d ∣ c
⊢ a / b < c / d ↔ d * a < c * b

Tactic:
ediv_lt_ediv_iff_of_dvd_of_neg_of_neg hb hd hba hdc

Premises used: Int.ediv_lt_ediv_iff_of_dvd_of_neg_of_neg
-- Module: Mathlib.Data.Int.Init
Goal:
n : ℤ
⊢ n % 2 = 0 ∨ n % 2 = 1

Tactic:
emod_two_eq n

Premises used: Int.emod_two_eq
-- Module: Mathlib.Data.Int.Init
Goal:
a b c : ℤ
h : b ∣ a
hdiv : a / b ∣ c
⊢ a ∣ b * c

Tactic:
dvd_mul_of_ediv_dvd h hdiv

Premises used: Int.dvd_mul_of_ediv_dvd
-- Module: Mathlib.Data.Int.Init
Goal:
a b c : ℤ
h : b ∣ a
hb : b ≠ 0
⊢ a / b ∣ c ↔ a ∣ b * c

Tactic:
ediv_dvd_iff_dvd_mul h hb

Premises used: Int.ediv_dvd_iff_dvd_mul
-- Module: Mathlib.Data.Int.Init
Goal:
a b c : ℤ
hcb : c ∣ b
h : a ∣ b / c
⊢ c * a ∣ b

Tactic:
mul_dvd_of_dvd_ediv hcb h

Premises used: Int.mul_dvd_of_dvd_ediv
-- Module: Mathlib.Data.Int.Init
Goal:
a b c : ℤ
h : a * b ∣ c
⊢ b ∣ c / a

Tactic:
dvd_ediv_of_mul_dvd h

Premises used: Int.dvd_ediv_of_mul_dvd
-- Module: Mathlib.Data.Int.Init
Goal:
a b c : ℤ
hbc : c ∣ b
⊢ a ∣ b / c ↔ c * a ∣ b

Tactic:
simp [hbc]
-- Module: Mathlib.Data.Int.Init
Goal:
n m : ℤ
hn : 0 < n
⊢ (∃ (k : ℤ), n * k < m ∧ m < n * (k + 1)) ↔ ¬n ∣ m

Tactic:
(not_dvd_iff_lt_mul_succ m hn).symm

Premises used: Int.not_dvd_iff_lt_mul_succ, Iff.symm
-- Module: Mathlib.Data.Int.Init
Goal:
a b c d : ℤ
hb : b ≠ 0
hbc : b ∣ c
h : b * a = c * d
obtain : ∀ (k : ℤ) (h : b * a = b * k * d), a = b * k / b * d
⊢ a = c / b * d

Tactic:
obtain ⟨k, rfl⟩ := hbc

Premises used: rfl
-- Module: Mathlib.Data.Int.Init
Goal:
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
rw : a = k * d
⊢ a = b * k / b * d

Tactic:
rw [Int.mul_ediv_cancel_left _ hb]

Premises used: Int.mul_ediv_cancel_left
-- Module: Mathlib.Data.Int.Init
Goal:
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
rwa : ∀ (h : b * a = b * (k * d)), a = k * d
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : a = k * d), a = k * d
⊢ a = k * d

Tactic:
rwa [Int.mul_assoc, Int.mul_eq_mul_left_iff hb] at h

Premises used: Int.mul_eq_mul_left_iff, Int.mul_assoc