-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem ofNat_mul_subNatNat (m n k : Nat) :
    m * subNatNat n k = subNatNat (m * n) (m * k)

Proof state:
case succ.inl
n k m : Nat
h : n < k
h' : m.succ * n < m.succ * k
⊢ ↑(m + 1) * subNatNat n k = subNatNat ((m + 1) * n) ((m + 1) * k)

Tactic:
simp [subNatNat_of_lt h, subNatNat_of_lt h']

Result:
case succ.inl
n k m : Nat
h : n < k
h' : m.succ * n < m.succ * k
⊢ negOfNat ((m + 1) * (k - n - 1 + 1)) = -[(m + 1) * k - (m + 1) * n - 1+1]

Proof state:
m n k : Nat
⊢ ↑m * subNatNat n k = subNatNat (m * n) (m * k)

Tactic:
cases m with
| zero => simp [ofNat_zero, Int.zero_mul, Nat.zero_mul]
| succ m => cases n.lt_or_ge k with
  | inl h =>
    have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
    simp [subNatNat_of_lt h, subNatNat_of_lt h']
    rw [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), ← neg_ofNat_succ, Nat.mul_sub_left_distrib,
      ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]; rfl
  | inr h =>
    have h' : succ m * k ≤ succ m * n := Nat.mul_le_mul_left _ h
    simp [subNatNat_of_le h, subNatNat_of_le h', Nat.mul_sub_left_distrib]

Result:
no goals

Proof state:
case succ.inl
n k m : Nat
h : n < k
h' : m.succ * n < m.succ * k
⊢ negOfNat ((m + 1) * (k - n - 1 + 1)) = -[(m + 1) * k - (m + 1) * n - 1+1]

Tactic:
rw [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), ← neg_ofNat_succ, Nat.mul_sub_left_distrib,
  ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]

Result:
case succ.inl
n k m : Nat
h : n < k
h' : m.succ * n < m.succ * k
⊢ negOfNat (m.succ * k - m.succ * n).pred.succ = -↑((m.succ * k - m.succ * n).pred.succ - 1).succ

Proof state:
case zero
n k : Nat
⊢ ↑0 * subNatNat n k = subNatNat (0 * n) (0 * k)

Tactic:
simp [ofNat_zero, Int.zero_mul, Nat.zero_mul]

Result:
no goals

Proof state:
case succ.inl
n k m : Nat
h : n < k
⊢ ↑(m + 1) * subNatNat n k = subNatNat ((m + 1) * n) ((m + 1) * k)

Tactic:
have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)

Result:
case succ.inl
n k m : Nat
h : n < k
h' : m.succ * n < m.succ * k
⊢ ↑(m + 1) * subNatNat n k = subNatNat ((m + 1) * n) ((m + 1) * k)

Proof state:
case succ
n k m : Nat
⊢ ↑(m + 1) * subNatNat n k = subNatNat ((m + 1) * n) ((m + 1) * k)

Tactic:
cases n.lt_or_ge k with
| inl h =>
have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
simp [subNatNat_of_lt h, subNatNat_of_lt h']
rw [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), ← neg_ofNat_succ, Nat.mul_sub_left_distrib,
← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]; rfl
| inr h =>
have h' : succ m * k ≤ succ m * n := Nat.mul_le_mul_left _ h
simp [subNatNat_of_le h, subNatNat_of_le h', Nat.mul_sub_left_distrib]

Result:
no goals

Proof state:
case succ.inl
n k m : Nat
h : n < k
h' : m.succ * n < m.succ * k
⊢ negOfNat (m.succ * k - m.succ * n).pred.succ = -↑((m.succ * k - m.succ * n).pred.succ - 1).succ

Tactic:
rfl

Result:
no goals

Proof state:
case succ.inr
n k m : Nat
h : n ≥ k
h' : m.succ * k ≤ m.succ * n
⊢ ↑(m + 1) * subNatNat n k = subNatNat ((m + 1) * n) ((m + 1) * k)

Tactic:
simp [subNatNat_of_le h, subNatNat_of_le h', Nat.mul_sub_left_distrib]

Result:
no goals

Proof state:
case succ.inr
n k m : Nat
h : n ≥ k
⊢ ↑(m + 1) * subNatNat n k = subNatNat ((m + 1) * n) ((m + 1) * k)

Tactic:
have h' : succ m * k ≤ succ m * n := Nat.mul_le_mul_left _ h

Result:
case succ.inr
n k m : Nat
h : n ≥ k
h' : m.succ * k ≤ m.succ * n
⊢ ↑(m + 1) * subNatNat n k = subNatNat ((m + 1) * n) ((m + 1) * k)