-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Box (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : Ring β
inst_4 : PartialOrder β
inst_5 : IsOrderedRing β
inst_6 : LocallyFiniteOrder α
inst_7 : LocallyFiniteOrder β
inst_8 : DecidableEq α
inst_9 : DecidableEq β
inst_10 : DecidableLE (α × β)
n : ℕ
simp_rw :
  card.{u_1} (α := α) (Icc (-(↑(n + 1) : α × β)).1 (↑(n + 1) : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑(n + 1) : α × β)).2 (↑(n + 1) : α × β).2) -
      card.{u_1} (α := α) (Icc (-(↑n : α × β)).1 (↑n : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑n : α × β)).2 (↑n : α × β).2) =
    card.{u_1} (α := α) (Icc (-(↑(n + 1) : α)) (↑(n + 1) : α)) *
        card.{u_2} (α := β) (Icc (-(↑(n + 1) : β)) (↑(n + 1) : β)) -
      card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))
simp_rw₁ :
  #(Icc (-HAdd.hAdd (α := α × β) (↑n : α × β) (↑1 : α × β)).1 (HAdd.hAdd (α := α × β) (↑n : α × β) (↑1 : α × β)).1) *
        #(Icc (-HAdd.hAdd (α := α × β) (↑n : α × β) (↑1 : α × β)).2
            (HAdd.hAdd (α := α × β) (↑n : α × β) (↑1 : α × β)).2) -
      card.{u_1} (α := α) (Icc (-(↑n : α × β)).1 (↑n : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑n : α × β)).2 (↑n : α × β).2) =
    #(Icc (-HAdd.hAdd (α := α) (↑n : α) (↑1 : α)) (HAdd.hAdd (α := α) (↑n : α) (↑1 : α))) *
        #(Icc (-HAdd.hAdd (α := β) (↑n : β) (↑1 : β)) (HAdd.hAdd (α := β) (↑n : β) (↑1 : β))) -
      card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))
simp_rw₂ :
  #(Icc (-HAdd.hAdd (α := α × β) (↑n : α × β) 1).1 (HAdd.hAdd (α := α × β) (↑n : α × β) 1).1) *
        #(Icc (-HAdd.hAdd (α := α × β) (↑n : α × β) 1).2 (HAdd.hAdd (α := α × β) (↑n : α × β) 1).2) -
      card.{u_1} (α := α) (Icc (-(↑n : α × β)).1 (↑n : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑n : α × β)).2 (↑n : α × β).2) =
    #(Icc (-HAdd.hAdd (α := α) (↑n : α) 1) (HAdd.hAdd (α := α) (↑n : α) 1)) *
        #(Icc (-HAdd.hAdd (α := β) (↑n : β) 1) (HAdd.hAdd (α := β) (↑n : β) 1)) -
      card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))
⊢ card.{u_1} (α := α) (Icc (-(↑n.succ : α × β)).1 (↑n.succ : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑n.succ : α × β)).2 (↑n.succ : α × β).2) -
      card.{u_1} (α := α) (Icc (-(↑n : α × β)).1 (↑n : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑n : α × β)).2 (↑n : α × β).2) =
    card.{u_1} (α := α) (Icc (-(↑n.succ : α)) (↑n.succ : α)) *
        card.{u_2} (α := β) (Icc (-(↑n.succ : β)) (↑n.succ : β)) -
      card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))
have simp_rw₃ : #(Icc (HAdd.hAdd (α := α × β) (-1) (-(↑n : α × β))).1 (HAdd.hAdd (α := α × β) (↑n : α × β) 1).1) *
      #(Icc (HAdd.hAdd (α := α × β) (-1) (-(↑n : α × β))).2 (HAdd.hAdd (α := α × β) (↑n : α × β) 1).2) -
    card.{u_1} (α := α) (Icc (-(↑n : α × β)).1 (↑n : α × β).1) *
      card.{u_2} (α := β) (Icc (-(↑n : α × β)).2 (↑n : α × β).2) =
  #(Icc (HAdd.hAdd (α := α) (-1) (-(↑n : α))) (HAdd.hAdd (α := α) (↑n : α) 1)) *
      #(Icc (HAdd.hAdd (α := β) (-1) (-(↑n : β))) (HAdd.hAdd (α := β) (↑n : β) 1)) -
    card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))
Tactic: simp_rw [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, neg_add_rev, fst_add, fst_neg,
    fst_one, fst_natCast, snd_add, snd_neg, snd_one, snd_natCast]