-- Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean
theorem limit_π_isIso_of_is_strict_terminal (F : J ⥤ C) [HasLimit F] (i : J)
    (H : ∀ (j) (_ : j ≠ i), IsTerminal (F.obj j)) [Subsingleton (i ⟶ i)] : IsIso (limit.π F i)

Proof state:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫ eqToHom ⋯ = eqToHom ⋯ ≫ F.map f

Tactic:
cases h

Result:
case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : j = i
f : j ⟶ i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫ eqToHom ⋯ = eqToHom ⋯ ≫ F.map f

Proof state:
case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.π F i ≫ 𝟙 (((Functor.const J).obj (F.toPrefunctor.1 i)).obj i) = limit.π F i

Tactic:
exact comp_id _

Result:
no goals

Proof state:
case refine_3.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
⊢ (limit.π F i ≫
      if h : j✝ = i then eqToHom ⋯ else (H j✝ h).from (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j✝)) =
    𝟙 (limit F) ≫ limit.π F j✝

Tactic:
split_ifs with h

Result:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
h : j✝ = i
⊢ limit.π F i ≫ eqToHom ⋯ = 𝟙 (limit F) ≫ limit.π F j✝

case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
h : ¬j✝ = i
⊢ limit.π F i ≫ (H j✝ h).from (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j✝) = 𝟙 (limit F) ≫ limit.π F j✝

Proof state:
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
h : ¬j✝ = i
⊢ limit.π F i ≫ (H j✝ h).from (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j✝) = 𝟙 (limit F) ≫ limit.π F j✝

Tactic:
apply (H _ h).hom_ext

Result:
no goals

Proof state:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ (X : J) → ((Functor.const J).obj (F.toPrefunctor.1 i)).obj X ⟶ F.obj X

Tactic:
exact fun j =>
  dite (j = i)
    (fun h => eqToHom (by cases h; rfl))
    fun h => (H _ h).from _

Result:
no goals

Proof state:
case refine_3.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
⊢ limit.π F i ≫
      { pt := F.toPrefunctor.1 i,
              π :=
                {
                  app := fun j =>
                    if h : j = i then eqToHom ⋯ else (H j h).from (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j),
                  naturality := ⋯ } }.π.app
        j✝ =
    𝟙 (limit F) ≫ limit.π F j✝

Tactic:
dsimp only

Result:
case refine_3.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
⊢ (limit.π F i ≫
      if h : j✝ = i then eqToHom ⋯ else (H j✝ h).from (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j✝)) =
    𝟙 (limit F) ≫ limit.π F j✝

Proof state:
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫ eqToHom ⋯ =
    (H j h_1).from (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) ≫ F.map f

Tactic:
cases h

Result:
case neg.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫ eqToHom ⋯ =
    (H j h_1).from (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) ≫ F.map f

Proof state:
case pos.refl.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
f : i ⟶ i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫ eqToHom ⋯ = eqToHom ⋯ ≫ F.map f

Tactic:
obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _

Result:
case pos.refl.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map (𝟙 i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ F.map (𝟙 i)

Proof state:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      (H k h).from (((Functor.const J).obj (F.toPrefunctor.1 i)).obj k) =
    eqToHom ⋯ ≫ F.map f

Tactic:
cases h_1

Result:
case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
k : J
h : ¬k = i
f : i ⟶ k
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      (H k h).from (((Functor.const J).obj (F.toPrefunctor.1 i)).obj k) =
    eqToHom ⋯ ≫ F.map f

Proof state:
case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : j = i
f : j ⟶ i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫ eqToHom ⋯ = eqToHom ⋯ ≫ F.map f

Tactic:
cases h_1

Result:
case pos.refl.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
f : i ⟶ i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫ eqToHom ⋯ = eqToHom ⋯ ≫ F.map f