-- Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean
lemma functorMap_commSq_aux {n m k : ℕ} (h : n ≤ m) (hh : ¬(k < m)) :
    (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫ Pi.π _ k ≫
      eqToHom (functorObj_eq_neg (by omega : ¬(k < n))) =
        (Pi.π (fun i ↦ if _ : i < m then M i else N i) k) ≫
          eqToHom (functorObj_eq_neg hh)

Proof state:
case le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < m then M i else N i) k ≫ eqToHom ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ ((Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
        (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op) ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < m + 1 then M i else N i) k ≫ eqToHom ⋯

Tactic:
slice_lhs 2 4 => rw [ih]

Result:
case le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < m then M i else N i) k ≫ eqToHom ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun i => if x : i < m then M i else N i) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < m + 1 then M i else N i) k ≫ eqToHom ⋯

Proof state:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n m k : ℕ
h : n ≤ m
hh : ¬k < m
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < m then M i else N i) k ≫ eqToHom ⋯

Tactic:
induction' h using Nat.leRec with m h ih

Result:
case refl
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n m k : ℕ
hh : ¬k < n
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < n then M i else N i) k ≫ eqToHom ⋯

case le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n m✝ k m : ℕ
h : n ≤ m
ih :
  ∀ (hh : ¬k < m),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
        Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
      Pi.π (fun i => if x : i < m then M i else N i) k ≫ eqToHom ⋯
hh : ¬k < m + 1
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < m + 1 then M i else N i) k ≫ eqToHom ⋯

Proof state:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n m✝ k m : ℕ
h : n ≤ m
ih :
  ∀ (hh : ¬k < m),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
        Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
      Pi.π (fun i => if x : i < m then M i else N i) k ≫ eqToHom ⋯
hh : ¬k < m + 1
⊢ ¬k < m

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < m then M i else N i) k ≫ eqToHom ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ ¬k < m

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < m then M i else N i) k ≫ eqToHom ⋯
⊢ homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯

Tactic:
simp

Result:
no goals

Proof state:
case refl
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n m k : ℕ
hh : ¬k < n
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < n then M i else N i) k ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
case le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n m✝ k m : ℕ
h : n ≤ m
ih :
  ∀ (hh : ¬k < m),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
        Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
      Pi.π (fun i => if x : i < m then M i else N i) k ≫ eqToHom ⋯
hh : ¬k < m + 1
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < m + 1 then M i else N i) k ≫ eqToHom ⋯

Tactic:
specialize ih (by omega)

Result:
case le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < m then M i else N i) k ≫ eqToHom ⋯
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < m + 1 then M i else N i) k ≫ eqToHom ⋯

Proof state:
case le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < m then M i else N i) k ≫ eqToHom ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ limit.π (Discrete.functor fun m_1 => if m_1 < m + 1 then M m_1 else N m_1) { as := k } ≫
      (if h : k < m then eqToHom ⋯ else eqToHom ⋯) ≫ eqToHom ⋯ =
    Pi.π (fun i => if i < m + 1 then M i else N i) k ≫ eqToHom ⋯

Tactic:
simp [dif_neg (by omega : ¬(k < m))]

Result:
no goals

Proof state:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < m then M i else N i) k ≫ eqToHom ⋯
⊢ m ≤ m + 1

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < m then M i else N i) k ≫ eqToHom ⋯
⊢ n ≤ m + 1

Tactic:
omega

Result:
no goals