-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem negSucc_mul_subNatNat (m n k : Nat) :
    -[m+1] * subNatNat n k = subNatNat (succ m * k) (succ m * n)

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

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

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

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

Tactic:
rw [subNatNat_of_lt h, subNatNat_of_le (Nat.le_of_lt h')]

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

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

Tactic:
rw [Nat.le_antisymm h h', subNatNat_self, subNatNat_self, Int.mul_zero]

Result:
no goals

Proof state:
m n k : Nat
⊢ -[m+1] * subNatNat n k = subNatNat (m.succ * k) (m.succ * n)

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)
  rw [subNatNat_of_lt h, subNatNat_of_le (Nat.le_of_lt h')]
  simp [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), Nat.mul_sub_left_distrib]
| inr h => cases Nat.lt_or_ge k n with
  | inl h' =>
    have h₁ : succ m * n > succ m * k := Nat.mul_lt_mul_of_pos_left h' (Nat.succ_pos m)
    rw [subNatNat_of_le h, subNatNat_of_lt h₁, negSucc_mul_ofNat,
      Nat.mul_sub_left_distrib, ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁)]; rfl
  | inr h' => rw [Nat.le_antisymm h h', subNatNat_self, subNatNat_self, Int.mul_zero]

Result:
no goals

Proof state:
case inr.inl
m n k : Nat
h : n ≥ k
h' : k < n
h₁ : m.succ * n > m.succ * k
⊢ -↑(m.succ * n - m.succ * k).pred.succ = -[(m.succ * n - m.succ * k).pred.succ.pred+1]

Tactic:
rfl

Result:
no goals

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

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

Result:
case inr.inl
m n k : Nat
h : n ≥ k
h' : k < n
h₁ : m.succ * n > m.succ * k
⊢ -[m+1] * subNatNat n k = subNatNat (m.succ * k) (m.succ * n)

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

Tactic:
rw [subNatNat_of_le h, subNatNat_of_lt h₁, negSucc_mul_ofNat,
  Nat.mul_sub_left_distrib, ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁)]

Result:
case inr.inl
m n k : Nat
h : n ≥ k
h' : k < n
h₁ : m.succ * n > m.succ * k
⊢ -↑(m.succ * n - m.succ * k).pred.succ = -[(m.succ * n - m.succ * k).pred.succ.pred+1]

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

Tactic:
cases Nat.lt_or_ge k n with
| inl h' =>
have h₁ : succ m * n > succ m * k := Nat.mul_lt_mul_of_pos_left h' (Nat.succ_pos m)
rw [subNatNat_of_le h, subNatNat_of_lt h₁, negSucc_mul_ofNat,
Nat.mul_sub_left_distrib, ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁)]; rfl
| inr h' => rw [Nat.le_antisymm h h', subNatNat_self, subNatNat_self, Int.mul_zero]

Result:
no goals

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

Tactic:
simp [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), Nat.mul_sub_left_distrib]

Result:
no goals