-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
F : Functor.{u_3, v, u_3, u} (Discrete ι) C
c : Cocone F
hc : IsVanKampenColimit c
i : Discrete ι
let let₁ let₂ : Mono (c.ι.app i)
let₃ :
  let f := F.obj ∘ Discrete.mk;
  ∀ (this : F = Discrete.functor f), Mono (c.ι.app i)
let₄ : ∀ (f : ι → C) (this : F = Discrete.functor f), Mono (c.ι.app i)
let₅ : ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c), Mono (c.ι.app i)
let₆ :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
    IsPullback (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i)) (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
      (c.ι.app i) (c.ι.app i)
let₇ :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
    IsPullback (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i)) (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
      (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i) ≫ c.ι.app i) (c.ι.app i)
h :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
    obj.{u_3, v, u_3, u} (Discrete.functor f) i = f i.as →
      Eq.{v + 1} (α := obj.{u_3, v, u_3, u} (Discrete.functor f) i ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)
        (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
        (CategoryStruct.comp (Y := if i.as = i.as then f i.as else initial.{v, u} C) (eqToHom ⋯)
          (if h : i.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as)))
convert_4 :
  (f : ι → C) →
    {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} →
      (hc : IsVanKampenColimit c) →
        obj.{u_3, v, u_3, u} (Discrete.functor f) i ⟶ if i.as = i.as then f i.as else initial.{v, u} C
convert_6 :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
    IsPullback.{v, u} (Y := if i.as = i.as then f i.as else initial.{v, u} C)
      (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i)) (eqToHom ⋯) (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
      (if h : i.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as))
convert_4₁ :
  (f : ι → C) →
    {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} →
      (hc : IsVanKampenColimit c) →
        obj.{u_3, v, u_3, u} (Discrete.functor f) i ⟶ if i.as = i.as then f i.as else initial.{v, u} C
h₁ :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
    obj.{u_3, v, u_3, u} (Discrete.functor f) i = f i.as →
      Eq.{v + 1} (α := obj.{u_3, v, u_3, u} (Discrete.functor f) i ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)
        (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
        (CategoryStruct.comp (Y := if i.as = i.as then f i.as else initial.{v, u} C) (eqToHom ⋯)
          (if h : i.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as)))
convert_6₁ :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
    IsPullback.{v, u} (Y := if i.as = i.as then f i.as else initial.{v, u} C)
      (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i)) (eqToHom ⋯) (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
      (if h : i.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as))
h₂ :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
    obj.{u_3, v, u_3, u} (Discrete.functor f) i = f i.as →
      Eq.{v + 1} (α := obj.{u_3, v, u_3, u} (Discrete.functor f) i ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)
        (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
        (CategoryStruct.comp (Y := if i.as = i.as then f i.as else initial.{v, u} C) (eqToHom ⋯)
          (if h : i.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as)))
convert_6₂ convert_6₃ :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
    IsPullback.{v, u} (Y := if i.as = i.as then f i.as else initial.{v, u} C)
      (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i)) (eqToHom ⋯) (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
      (if h : i.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as))
⊢ Mono (c.ι.app i)

Tactic:
classical
  let f : ι → C := F.obj ∘ Discrete.mk
  have : F = Discrete.functor f :=
    Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
  clear_value f
  subst this
  refine PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit ?_)
  nth_rw 1 [← Category.id_comp (c.ι.app i)]
  convert! IsPullback.paste_vert _ (isPullback_of_cofan_isVanKampen hc i.as i.as)
  swap
  · exact (eqToHom (if_pos rfl).symm)
  · simp
  · exact IsPullback.of_vert_isIso ⟨by simp⟩

Premises used: CategoryTheory.IsPullback.of_vert_isIso, CategoryTheory.eqToHom, CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId, CategoryTheory.CommSq.mk, if_pos, CategoryTheory.Limits.Cocone.ι, Eq.symm, CategoryTheory.NatTrans.app, rfl, CategoryTheory.Category.id_comp, CategoryTheory.IsPullback.isLimit