awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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
⊢ 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))
have pos : z = b →
  cast sorry
      (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 sorry zero
        | n.succ => cast sorry (pred (b + -[n+1]) sorry (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))) =
    pred z hz
      (cast sorry
        (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
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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))
⊢ 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))
have neg : ¬z = b →
  cast sorry
      (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 sorry zero
        | n.succ => cast sorry (pred (b + -[n+1]) sorry (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))) =
    pred z hz
      (cast sorry
        (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
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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 ⋯
      (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))
have pos : cast (α := (fun (x : ℤ) ↦ motive x) (b + -[(b - z).toNat+1])) sorry
    (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 sorry zero
      | n.succ => cast sorry (pred (b + -[n+1]) sorry (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))) =
  pred z hz
    (cast (α := (fun (x : ℤ) ↦ motive x) (b + 0)) sorry
      (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: rw! [show z - 1 - b = -[(b - z).toNat+1] by lia, show z - b = 0 by lia]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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 ⋯
      (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))
have neg : cast (α := (fun (x : ℤ) ↦ motive x) (b + -[(b - z).toNat+1])) sorry
    (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 sorry zero
      | n.succ => cast sorry (pred (b + -[n+1]) sorry (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])) sorry
      (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: rw! [show z - 1 - b = -[(b - z).toNat+1] by lia, show z - b = -[(b - z - 1).toNat+1] by lia]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
⊢ Int.leInduction (motive := motive) base succ m ⋯ = base
have 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) ↦ sorry.elim) sorry =
  base
Tactic: rw [Int.leInduction, inductionOn'_self]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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
⊢ Int.leInduction (motive := motive) base succ m ⋯ = base
have rw₁ : base = base
Tactic: rw [Int.leInduction, inductionOn'_self]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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
⊢ Int.leInduction (motive := motive) base succ (n + 1) ⋯ =
    succ n hmn (Int.leInduction (motive := motive) base succ n hmn)
have 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) ↦ sorry.elim) hmn) =
  succ n hmn (Int.leInduction (motive := motive) base succ n hmn)
Tactic: rw [Int.leInduction, inductionOn'_add_one hmn]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
⊢ Int.leInductionDown (motive := motive) base pred m ⋯ = base
have 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) ↦ sorry.elim)
    (fun (k : ℤ) (hle : k ≤ m) (ih : (hnm : k ≤ m) → motive k hnm) (x : k - 1 ≤ m) ↦ pred k hle (ih hle)) sorry =
  base
Tactic: rw [Int.leInductionDown, inductionOn'_self]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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
⊢ Int.leInductionDown (motive := motive) base pred m ⋯ = base
have rw₁ : base = base
Tactic: rw [Int.leInductionDown, inductionOn'_self]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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
⊢ Int.leInductionDown (motive := motive) base pred (n - 1) ⋯ =
    pred n hnm (Int.leInductionDown (motive := motive) base pred n hnm)
have 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) ↦ sorry.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: rw [Int.leInductionDown, inductionOn'_sub_one hnm]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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 : ℤ
⊢ motive n
have 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
Tactic: refine if hnm : n < m then lt n hnm else ge n (by lia) (n.inductionOn' m lt ?_ ?_)
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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
⊢ motive n
have 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
Tactic: refine if hnm : n < m then lt n hnm else ge n (by lia) (n.inductionOn' m lt ?_ ?_)
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
⊢ -[m+1].ediv (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    -((HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - 1) / HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)
have rw : -[m+1].ediv (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = -((↑m : ℤ) / HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)
Tactic: rw [Int.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
a b c d : ℤ
hb : b ≠ 0
hbc : b ∣ c
h : b * a = c * d
⊢ a = c / b * d
have obtain : ∀ (k : ℤ) (h : b * a = b * k * d), a = b * k / b * d
Tactic: obtain ⟨k, rfl⟩ := hbc
Cleared hypotheses: c, hbc, h
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = b * k / b * d
have rw : a = k * d
Tactic: rw [Int.mul_ediv_cancel_left _ hb]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = k * d
have rwa : ∀ (h : b * a = b * (k * d)), a = k * d
Tactic: rwa [Int.mul_assoc, Int.mul_eq_mul_left_iff hb] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
rwa : ∀ (h : b * a = b * (k * d)), a = k * d
⊢ a = k * d
have rwa₁ : ∀ (h : a = k * d), a = k * d
Tactic: rwa [Int.mul_assoc, Int.mul_eq_mul_left_iff hb] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
m n : ℕ
h : n.succ ≤ m
⊢ ofNat m + -[n+1] = ofNat (m - n.succ)
have rw : ofNat m + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = ofNat (m - n.succ)
Tactic: rw [negSucc_eq, ofNat_eq_natCast, ofNat_eq_natCast, ← Int.natCast_one, ← Int.natCast_add,
    ← Int.sub_eq_add_neg, ← Int.natCast_sub h]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
m n : ℕ
h : n.succ ≤ m
rw : ofNat m + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = ofNat (m - n.succ)
⊢ ofNat m + -[n+1] = ofNat (m - n.succ)
have rw₁ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = ofNat (m - n.succ)
Tactic: rw [negSucc_eq, ofNat_eq_natCast, ofNat_eq_natCast, ← Int.natCast_one, ← Int.natCast_add,
    ← Int.sub_eq_add_neg, ← Int.natCast_sub h]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
m n : ℕ
h : n.succ ≤ m
rw : ofNat m + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = ofNat (m - n.succ)
rw₁ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = ofNat (m - n.succ)
⊢ ofNat m + -[n+1] = ofNat (m - n.succ)
have rw₂ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = (↑(m - n.succ) : ℤ)
Tactic: rw [negSucc_eq, ofNat_eq_natCast, ofNat_eq_natCast, ← Int.natCast_one, ← Int.natCast_add,
    ← Int.sub_eq_add_neg, ← Int.natCast_sub h]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
m n : ℕ
h : n.succ ≤ m
rw : ofNat m + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = ofNat (m - n.succ)
rw₁ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = ofNat (m - n.succ)
rw₂ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = (↑(m - n.succ) : ℤ)
⊢ ofNat m + -[n+1] = ofNat (m - n.succ)
have rw₃ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) = (↑(m - n.succ) : ℤ)
Tactic: rw [negSucc_eq, ofNat_eq_natCast, ofNat_eq_natCast, ← Int.natCast_one, ← Int.natCast_add,
    ← Int.sub_eq_add_neg, ← Int.natCast_sub h]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
m n : ℕ
h : n.succ ≤ m
rw : ofNat m + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = ofNat (m - n.succ)
rw₁ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = ofNat (m - n.succ)
rw₂ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = (↑(m - n.succ) : ℤ)
rw₃ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) = (↑(m - n.succ) : ℤ)
⊢ ofNat m + -[n+1] = ofNat (m - n.succ)
have rw₄ : HAdd.hAdd (α := ℤ) (↑m : ℤ) (-(↑(n + 1) : ℤ)) = (↑(m - n.succ) : ℤ)
Tactic: rw [negSucc_eq, ofNat_eq_natCast, ofNat_eq_natCast, ← Int.natCast_one, ← Int.natCast_add,
    ← Int.sub_eq_add_neg, ← Int.natCast_sub h]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
m n : ℕ
h : n.succ ≤ m
rw : ofNat m + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = ofNat (m - n.succ)
rw₁ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = ofNat (m - n.succ)
rw₂ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = (↑(m - n.succ) : ℤ)
rw₃ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) = (↑(m - n.succ) : ℤ)
rw₄ : HAdd.hAdd (α := ℤ) (↑m : ℤ) (-(↑(n + 1) : ℤ)) = (↑(m - n.succ) : ℤ)
⊢ ofNat m + -[n+1] = ofNat (m - n.succ)
have rw₅ : HSub.hSub (α := ℤ) (↑m : ℤ) (↑(n + 1) : ℤ) = (↑(m - n.succ) : ℤ)
Tactic: rw [negSucc_eq, ofNat_eq_natCast, ofNat_eq_natCast, ← Int.natCast_one, ← Int.natCast_add,
    ← Int.sub_eq_add_neg, ← Int.natCast_sub h]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
m n : ℕ
h : n.succ ≤ m
rw : ofNat m + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = ofNat (m - n.succ)
rw₁ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = ofNat (m - n.succ)
rw₂ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = (↑(m - n.succ) : ℤ)
rw₃ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) = (↑(m - n.succ) : ℤ)
rw₄ : HAdd.hAdd (α := ℤ) (↑m : ℤ) (-(↑(n + 1) : ℤ)) = (↑(m - n.succ) : ℤ)
rw₅ : HSub.hSub (α := ℤ) (↑m : ℤ) (↑(n + 1) : ℤ) = (↑(m - n.succ) : ℤ)
⊢ ofNat m + -[n+1] = ofNat (m - n.succ)
have rw₆ : Eq (α := ℤ) (↑(m - n.succ) : ℤ) (↑(m - n.succ) : ℤ)
Tactic: rw [negSucc_eq, ofNat_eq_natCast, ofNat_eq_natCast, ← Int.natCast_one, ← Int.natCast_add,
    ← Int.sub_eq_add_neg, ← Int.natCast_sub h]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
a b c : ℤ
ha : 0 < a
hab : a ∣ c - b
⊢ a + b ≤ c ↔ b < c
have rw : a ≤ c - b ↔ b < c
Tactic: rw [Int.add_le_iff_le_sub, ← Int.sub_pos, le_iff_pos_of_dvd ha hab]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
a b c : ℤ
ha : 0 < a
hab : a ∣ c - b
rw : a ≤ c - b ↔ b < c
⊢ a + b ≤ c ↔ b < c
have rw₁ : a ≤ c - b ↔ 0 < c - b
Tactic: rw [Int.add_le_iff_le_sub, ← Int.sub_pos, le_iff_pos_of_dvd ha hab]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
a b c : ℤ
ha : 0 < a
hab : a ∣ c - b
rw : a ≤ c - b ↔ b < c
rw₁ : a ≤ c - b ↔ 0 < c - b
⊢ a + b ≤ c ↔ b < c
have rw₂ : 0 < c - b ↔ 0 < c - b
Tactic: rw [Int.add_le_iff_le_sub, ← Int.sub_pos, le_iff_pos_of_dvd ha hab]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
⊢ x ∈ map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding a)) (range (b + 1 - a).toNat) ↔ a ≤ x ∧ x ≤ b
have simp_rw : (∃ a_1 < (b + 1 - a).toNat, a + (↑a_1 : ℤ) = x) ↔ a ≤ x ∧ x ≤ b
Tactic: simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
      addLeftEmbedding_apply]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
⊢ (∃ a_1 < (b + 1 - a).toNat, a + (↑a_1 : ℤ) = x) ↔ a ≤ x ∧ x ≤ b
have mp : (∃ a_1 < (b + 1 - a).toNat, a + (↑a_1 : ℤ) = x) → a ≤ x ∧ x ≤ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
mp : (∃ a_1 < (b + 1 - a).toNat, a + (↑a_1 : ℤ) = x) → a ≤ x ∧ x ≤ b
⊢ (∃ a_1 < (b + 1 - a).toNat, a + (↑a_1 : ℤ) = x) ↔ a ≤ x ∧ x ≤ b
have mpr : a ≤ x ∧ x ≤ b → ∃ a_2 < (b + 1 - a).toNat, a + (↑a_2 : ℤ) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
h : a ≤ x ∧ x ≤ b
⊢ ∃ a_1 < (b + 1 - a).toNat, a + (↑a_1 : ℤ) = x
have h : (x - a).toNat < (b + 1 - a).toNat ∧ a + (↑(x - a).toNat : ℤ) = x
Tactic: use (x - a).toNat
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
⊢ x ∈ map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding a)) (range (b - a).toNat) ↔ a ≤ x ∧ x < b
have simp_rw : (∃ a_1 < (b - a).toNat, a + (↑a_1 : ℤ) = x) ↔ a ≤ x ∧ x < b
Tactic: simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
      addLeftEmbedding_apply]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + (↑a_1 : ℤ) = x) ↔ a ≤ x ∧ x < b
have mp : (∃ a_1 < (b - a).toNat, a + (↑a_1 : ℤ) = x) → a ≤ x ∧ x < b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
mp : (∃ a_1 < (b - a).toNat, a + (↑a_1 : ℤ) = x) → a ≤ x ∧ x < b
⊢ (∃ a_1 < (b - a).toNat, a + (↑a_1 : ℤ) = x) ↔ a ≤ x ∧ x < b
have mpr : a ≤ x ∧ x < b → ∃ a_2 < (b - a).toNat, a + (↑a_2 : ℤ) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
h : a ≤ x ∧ x < b
⊢ ∃ a_1 < (b - a).toNat, a + (↑a_1 : ℤ) = x
have h : (x - a).toNat < (b - a).toNat ∧ a + (↑(x - a).toNat : ℤ) = x
Tactic: use (x - a).toNat
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
⊢ x ∈ map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (a + 1))) (range (b - a).toNat) ↔ a < x ∧ x ≤ b
have simp_rw : (∃ a_1 < (b - a).toNat, a + 1 + (↑a_1 : ℤ) = x) ↔ a < x ∧ x ≤ b
Tactic: simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
      addLeftEmbedding_apply]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + 1 + (↑a_1 : ℤ) = x) ↔ a < x ∧ x ≤ b
have mp : (∃ a_1 < (b - a).toNat, a + 1 + (↑a_1 : ℤ) = x) → a < x ∧ x ≤ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
mp : (∃ a_1 < (b - a).toNat, a + 1 + (↑a_1 : ℤ) = x) → a < x ∧ x ≤ b
⊢ (∃ a_1 < (b - a).toNat, a + 1 + (↑a_1 : ℤ) = x) ↔ a < x ∧ x ≤ b
have mpr : a < x ∧ x ≤ b → ∃ a_2 < (b - a).toNat, a + 1 + (↑a_2 : ℤ) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
h : a < x ∧ x ≤ b
⊢ ∃ a_1 < (b - a).toNat, a + 1 + (↑a_1 : ℤ) = x
have h : (x - (a + 1)).toNat < (b - a).toNat ∧ a + 1 + (↑(x - (a + 1)).toNat : ℤ) = x
Tactic: use (x - (a + 1)).toNat
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
⊢ x ∈ map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (a + 1))) (range (b - a - 1).toNat) ↔
    a < x ∧ x < b
have simp_rw : (∃ a_1 < (b - a - 1).toNat, a + 1 + (↑a_1 : ℤ) = x) ↔ a < x ∧ x < b
Tactic: simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
      addLeftEmbedding_apply]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
⊢ (∃ a_1 < (b - a - 1).toNat, a + 1 + (↑a_1 : ℤ) = x) ↔ a < x ∧ x < b
have mp : (∃ a_1 < (b - a - 1).toNat, a + 1 + (↑a_1 : ℤ) = x) → a < x ∧ x < b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
mp : (∃ a_1 < (b - a - 1).toNat, a + 1 + (↑a_1 : ℤ) = x) → a < x ∧ x < b
⊢ (∃ a_1 < (b - a - 1).toNat, a + 1 + (↑a_1 : ℤ) = x) ↔ a < x ∧ x < b
have mpr : a < x ∧ x < b → ∃ a_2 < (b - a - 1).toNat, a + 1 + (↑a_2 : ℤ) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b x : ℤ
h : a < x ∧ x < b
⊢ ∃ a_1 < (b - a - 1).toNat, a + 1 + (↑a_1 : ℤ) = x
have h : (x - (a + 1)).toNat < (b - a - 1).toNat ∧ a + 1 + (↑(x - (a + 1)).toNat : ℤ) = x
Tactic: use (x - (a + 1)).toNat
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
⊢ Eq (α := ℤ) (↑(#(range (max a b + 1 - min a b).toNat)) : ℤ) (↑((b - a).natAbs + 1) : ℤ)
have rw : Eq (α := ℤ) (↑(max a b + 1 - min a b).toNat : ℤ) (↑((b - a).natAbs + 1) : ℤ)
Tactic: rw [card_range,
        Int.toNat_of_nonneg (sub_nonneg_of_le <| le_add_one min_le_max), Int.natCast_add,
        Int.natCast_natAbs, add_comm, add_sub_assoc, max_sub_min_eq_abs, add_comm, Int.ofNat_one]