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

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

Tactic:
subst this

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

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 : ℕ
h : ¬0 < n
⊢ n = 0

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 : ℕ
h : ¬m + 1 < n
⊢ n ≤ m + 1 + 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 : ℕ
h : ¬m + 1 < n
⊢ homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯

Tactic:
simp

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 : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ ¬m + 1 < m + 1

Tactic:
omega

Result:
no goals

Proof state:
case succ
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 : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ ((Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
        (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op) ≫
      Pi.π (fun m => if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯ =
    functorMap f (m + 1) ≫ Pi.π (fun m_1 => if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯

Tactic:
simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
  Category.assoc, add_le_iff_nonpos_right, nonpos_iff_eq_zero, one_ne_zero]

Result:
case succ
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 : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ functorMap f (m + 1) ≫
      (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
        Pi.π (fun m => if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯ =
    functorMap f (m + 1) ≫ Pi.π (fun m_1 => if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ 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 : ℕ
h : ¬m < 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) m ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯ ≫ f m

Tactic:
cases m with
| zero =>
    have : n = 0 := by omega
    subst this
    simp [functorMap]
| succ m =>
    rw [← functorMap_commSq_succ f (m + 1)]
    simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, dite_eq_ite,
      Functor.ofOpSequence_map_homOfLE_succ, add_le_iff_nonpos_right, nonpos_iff_eq_zero,
      one_ne_zero]
    have : homOfLE (by omega : n ≤ m + 1 + 1) =
        homOfLE (by omega : n ≤ m + 1) ≫ homOfLE (by omega : m + 1 ≤ m + 1 + 1) := by simp
    rw [this, op_comp, Functor.map_comp]
    simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
      Category.assoc, add_le_iff_nonpos_right, nonpos_iff_eq_zero, one_ne_zero]
    congr 1
    exact functorMap_commSq_aux f (by omega) (by 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 : ℕ
h : ¬m + 1 < n
⊢ n ≤ m + 1

Tactic:
omega

Result:
no goals