-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem isPullback_initial_to_of_cofan_isVanKampen [HasInitial C] {ι : Type*} {F : Discrete ι ⥤ C}
    {c : Cocone F} (hc : IsVanKampenColimit c) (i j : Discrete ι) (hi : i ≠ j) :
    IsPullback (initial.to _) (initial.to _) (c.ι.app i) (c.ι.app j)

Proof state:
case h.e'_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i j : Discrete ι
hi : i ≠ j
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
this : ∀ (i : Discrete ι), Subsingleton (⊥_ C ⟶ (Discrete.functor f).obj i)
⊢ (⊥_ C) = if j.as = i.as then f i.as else ⊥_ C

Tactic:
exact (if_neg (mt Discrete.ext hi.symm)).symm

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i j : Discrete ι
hi : i ≠ j
⊢ IsPullback (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

Tactic:
let f : ι → C := F.obj ∘ Discrete.mk

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i j : Discrete ι
hi : i ≠ j
f : ι → C := F.obj ∘ Discrete.mk
⊢ IsPullback (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i j : Discrete ι
hi : i ≠ j
f : ι → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor f
⊢ IsPullback (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

Tactic:
clear_value f

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i j : Discrete ι
hi : i ≠ j
f : ι → C
this : F = Discrete.functor f
⊢ IsPullback (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

Proof state:
case mk.mk.up.up
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i✝ j : Discrete ι
hi : i✝ ≠ j
f : ι → C := F.obj ∘ Discrete.mk
i : ι
⊢ HEq (F.map { down := { down := ⋯ } }) ((Discrete.functor f).map { down := { down := ⋯ } })

Tactic:
simp [f]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i j : Discrete ι
hi : i ≠ j
f : ι → C := F.obj ∘ Discrete.mk
⊢ ∀ (X Y : Discrete ι) (f_1 : X ⟶ Y), HEq (F.map f_1) ((Discrete.functor f).map f_1)

Tactic:
rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩

Result:
case mk.mk.up.up
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i✝ j : Discrete ι
hi : i✝ ≠ j
f : ι → C := F.obj ∘ Discrete.mk
i : ι
⊢ HEq (F.map { down := { down := ⋯ } }) ((Discrete.functor f).map { down := { down := ⋯ } })

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i j : Discrete ι
hi : i ≠ j
f : ι → C
this : F = Discrete.functor f
⊢ IsPullback (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

Tactic:
subst this

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i j : Discrete ι
hi : i ≠ j
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ IsPullback (initial.to ((Discrete.functor f).obj i)) (initial.to ((Discrete.functor f).obj j)) (c.ι.app i) (c.ι.app j)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i j : Discrete ι
hi : i ≠ j
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ IsPullback (initial.to ((Discrete.functor f).obj i)) (initial.to ((Discrete.functor f).obj j)) (c.ι.app i) (c.ι.app j)

Tactic:
have : ∀ i, Subsingleton (⊥_ C ⟶ (Discrete.functor f).obj i) := inferInstance

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i j : Discrete ι
hi : i ≠ j
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
this : ∀ (i : Discrete ι), Subsingleton (⊥_ C ⟶ (Discrete.functor f).obj i)
⊢ IsPullback (initial.to ((Discrete.functor f).obj i)) (initial.to ((Discrete.functor f).obj j)) (c.ι.app i) (c.ι.app j)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i j : Discrete ι
hi : i ≠ j
f : ι → C := F.obj ∘ Discrete.mk
⊢ IsPullback (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

Tactic:
have : F = Discrete.functor f :=
  Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i j : Discrete ι
hi : i ≠ j
f : ι → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor f
⊢ IsPullback (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i j : Discrete ι
hi : i ≠ j
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
this : ∀ (i : Discrete ι), Subsingleton (⊥_ C ⟶ (Discrete.functor f).obj i)
⊢ IsPullback (initial.to ((Discrete.functor f).obj i)) (initial.to ((Discrete.functor f).obj j)) (c.ι.app i) (c.ι.app j)

Tactic:
convert isPullback_of_cofan_isVanKampen hc i.as j.as

Result:
case h.e'_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i j : Discrete ι
hi : i ≠ j
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
this : ∀ (i : Discrete ι), Subsingleton (⊥_ C ⟶ (Discrete.functor f).obj i)
⊢ (⊥_ C) = if j.as = i.as then f i.as else ⊥_ C

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i j : Discrete ι
hi : i ≠ j
⊢ IsPullback (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

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
have : ∀ i, Subsingleton (⊥_ C ⟶ (Discrete.functor f).obj i) := inferInstance
convert isPullback_of_cofan_isVanKampen hc i.as j.as
exact (if_neg (mt Discrete.ext hi.symm)).symm

Result:
no goals