-- Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean
lemma functorMap_epi (n : ℕ) : Epi (functorMap f n)

Proof state:
case inst
C : Type u_1
M N : ℕ → C
inst✝⁵ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝⁴ : HasProductsOfShape ℕ C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi
    (prod.map
      (Pi.map fun i =>
        if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯)
      (Pi.map fun i =>
        if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯))

Tactic:
apply ( config := { allowSynthFailures := true } ) prod.map_epi

Result:
case inst
C : Type u_1
M N : ℕ → C
inst✝⁵ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝⁴ : HasProductsOfShape ℕ C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi
    (Pi.map fun i =>
      if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯)

case inst
C : Type u_1
M N : ℕ → C
inst✝⁵ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝⁴ : HasProductsOfShape ℕ C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi
    (Pi.map fun i =>
      if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯)

Proof state:
case inst
C : Type u_1
M N : ℕ → C
inst✝⁵ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝⁴ : HasProductsOfShape ℕ C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi
    (Pi.map fun i =>
      if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯)

Tactic:
apply ( config := { allowSynthFailures := true } ) IsIso.epi_of_iso

Result:
case inst
C : Type u_1
M N : ℕ → C
inst✝⁵ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝⁴ : HasProductsOfShape ℕ C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ IsIso
    (Pi.map fun i =>
      if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else 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
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi
    (((Pi.binaryFanOfPropIsLimit (fun m => if x : m < n + 1 then M m else N m) fun m =>
              m < n + 1).conePointUniqueUpToIso
          (prodIsProd (∏ᶜ fun i => if x : ↑i < n + 1 then M ↑i else N ↑i)
            (∏ᶜ fun i => if x : ↑i < n + 1 then M ↑i else N ↑i))).hom ≫
      prod.map
          (Pi.map fun i =>
            if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯)
          (Pi.map fun i =>
            if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯) ≫
        ((Pi.binaryFanOfPropIsLimit (fun m => if x : m < n then M m else N m) fun m => m < n + 1).conePointUniqueUpToIso
            (prodIsProd (∏ᶜ fun i => if x : ↑i < n then M ↑i else N ↑i)
              (∏ᶜ fun i => if x : ↑i < n then M ↑i else N ↑i))).inv)

Tactic:
apply ( config := { allowSynthFailures := true } ) epi_comp

Result:
case inst
C : Type u_1
M N : ℕ → C
inst✝⁵ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝⁴ : HasProductsOfShape ℕ C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi
    (prod.map
        (Pi.map fun i =>
          if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯)
        (Pi.map fun i =>
          if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯) ≫
      ((Pi.binaryFanOfPropIsLimit (fun m => if x : m < n then M m else N m) fun m => m < n + 1).conePointUniqueUpToIso
          (prodIsProd (∏ᶜ fun i => if x : ↑i < n then M ↑i else N ↑i)
            (∏ᶜ fun i => if x : ↑i < n then M ↑i else N ↑i))).inv)

Proof state:
case inst
C : Type u_1
M N : ℕ → C
inst✝⁵ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝⁴ : HasProductsOfShape ℕ C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ ∀ (j : { x // x < n + 1 }),
    Epi (if h : ↑j < n then eqToHom ⋯ else if h' : ↑j < n + 1 then eqToHom ⋯ ≫ f ↑j ≫ eqToHom ⋯ else eqToHom ⋯)

Tactic:
intro ⟨_, _⟩

Result:
case inst
C : Type u_1
M N : ℕ → C
inst✝⁵ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝⁴ : HasProductsOfShape ℕ C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : val✝ < n + 1
⊢ Epi
    (if h : ↑⟨val✝, property✝⟩ < n then eqToHom ⋯
    else if h' : ↑⟨val✝, property✝⟩ < n + 1 then eqToHom ⋯ ≫ f ↑⟨val✝, property✝⟩ ≫ eqToHom ⋯ else eqToHom ⋯)

Proof state:
case inst.isFalse
C : Type u_1
M N : ℕ → C
inst✝⁵ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝⁴ : HasProductsOfShape ℕ C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : ¬val✝ < n + 1
h✝ : ¬↑⟨val✝, property✝⟩ < n
⊢ IsIso (eqToHom ⋯)

Tactic:
infer_instance

Result:
no goals

Proof state:
case inst
C : Type u_1
M N : ℕ → C
inst✝⁵ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝⁴ : HasProductsOfShape ℕ C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : val✝ < n + 1
⊢ Epi
    (if h : ↑⟨val✝, property✝⟩ < n then eqToHom ⋯
    else if h' : ↑⟨val✝, property✝⟩ < n + 1 then eqToHom ⋯ ≫ f ↑⟨val✝, property✝⟩ ≫ eqToHom ⋯ else eqToHom ⋯)

Tactic:
split

Result:
case inst.isTrue
C : Type u_1
M N : ℕ → C
inst✝⁵ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝⁴ : HasProductsOfShape ℕ C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : val✝ < n + 1
h✝ : ↑⟨val✝, property✝⟩ < n
⊢ Epi (eqToHom ⋯)

case inst.isFalse
C : Type u_1
M N : ℕ → C
inst✝⁵ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝⁴ : HasProductsOfShape ℕ C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : val✝ < n + 1
h✝ : ¬↑⟨val✝, property✝⟩ < n
⊢ Epi (eqToHom ⋯ ≫ f ↑⟨val✝, property✝⟩ ≫ eqToHom ⋯)

Proof state:
case inst
C : Type u_1
M N : ℕ → C
inst✝⁵ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝⁴ : HasProductsOfShape ℕ C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : ¬val✝ < n + 1
⊢ IsIso
    (if h : ↑⟨val✝, property✝⟩ < n then eqToHom ⋯
    else if h' : ↑⟨val✝, property✝⟩ < n + 1 then eqToHom ⋯ ≫ f ↑⟨val✝, property✝⟩ ≫ eqToHom ⋯ else eqToHom ⋯)

Tactic:
split

Result:
case inst.isTrue
C : Type u_1
M N : ℕ → C
inst✝⁵ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝⁴ : HasProductsOfShape ℕ C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : ¬val✝ < n + 1
h✝ : ↑⟨val✝, property✝⟩ < n
⊢ IsIso (eqToHom ⋯)

case inst.isFalse
C : Type u_1
M N : ℕ → C
inst✝⁵ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝⁴ : HasProductsOfShape ℕ C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
inst✝¹ : HasCountableProducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : ¬val✝ < n + 1
h✝ : ¬↑⟨val✝, property✝⟩ < n
⊢ IsIso (eqToHom ⋯)