-- Mathlib/CategoryTheory/Limits/Types.lean
/--
Given surjections `⋯ ⟶ Xₙ₊₁ ⟶ Xₙ ⟶ ⋯ ⟶ X₀`, the projection map `lim Xₙ ⟶ X₀` is surjective.
-/
lemma surjective_π_app_zero_of_surjective_map
    (hc : IsLimit c)
    (hF : ∀ n, Function.Surjective (F.map (homOfLE (Nat.le_succ n)).op)) :
    Function.Surjective (c.π.app ⟨0⟩)

Proof state:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
⊢ Function.Surjective (c.π.app (Opposite.op 0))

Tactic:
have : c.π.app ⟨0⟩ = i.hom ≫ (limitCone F).π.app ⟨0⟩ := by simp [i]

Result:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Function.Surjective (c.π.app (Opposite.op 0))

Proof state:
case hf
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Epi i.hom

Tactic:
infer_instance

Result:
no goals

Proof state:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
⊢ c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)

Tactic:
simp [i]

Result:
no goals

Proof state:
case hg
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Function.Surjective ((limitCone F).π.app (Opposite.op 0))

Tactic:
exact surjective_π_app_zero_of_surjective_map_aux hF

Result:
no goals

Proof state:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
⊢ Function.Surjective (c.π.app (Opposite.op 0))

Tactic:
let i := hc.conePointUniqueUpToIso (limitConeIsLimit F)

Result:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
⊢ Function.Surjective (c.π.app (Opposite.op 0))

Proof state:
case hf
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Function.Surjective i.hom

Tactic:
rw [← epi_iff_surjective]

Result:
case hf
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Epi i.hom

Proof state:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Function.Surjective (i.hom ≫ (limitCone F).π.app (Opposite.op 0))

Tactic:
apply Function.Surjective.comp

Result:
case hg
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Function.Surjective ((limitCone F).π.app (Opposite.op 0))

case hf
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Function.Surjective i.hom

Proof state:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Function.Surjective (c.π.app (Opposite.op 0))

Tactic:
rw [this]

Result:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Function.Surjective (i.hom ≫ (limitCone F).π.app (Opposite.op 0))