awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i j : Discrete ι
hi : i ≠ j
f : ι → C
c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)
hc : IsVanKampenColimit c
this : ∀ (i : Discrete ι), Subsingleton.{v + 1} (initial.{v, u} C ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)
⊢ IsPullback (P := initial.{v, u} C) (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
    (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) j)) (c.ι.app i) (c.ι.app j)
have h : initial.{v, u} C = if j.as = i.as then f i.as else initial.{v, u} C
Tactic: convert! isPullback_of_cofan_isVanKampen hc i.as j.as
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 j : Discrete ι
hi : i ≠ j
let let₁ let₂ : IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
⊢ IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
have let₃ : let f := F.obj ∘ Discrete.mk;
∀ (this : F = Discrete.functor f),
  IsPullback (P := initial.{v, u} C) (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 j : Discrete ι
hi : i ≠ j
let let₁ let₂ : IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
let₃ :
  let f := F.obj ∘ Discrete.mk;
  ∀ (this : F = Discrete.functor f),
    IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
⊢ IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
have let₄ : ∀ (f : ι → C) (this : F = Discrete.functor f),
  IsPullback (P := initial.{v, u} C) (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 j : Discrete ι
hi : i ≠ j
let let₁ let₂ : IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
let₃ :
  let f := F.obj ∘ Discrete.mk;
  ∀ (this : F = Discrete.functor f),
    IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
let₄ :
  ∀ (f : ι → C) (this : F = Discrete.functor f),
    IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
⊢ IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
have let₅ : ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
  IsPullback (P := initial.{v, u} C) (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
    (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) 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
Cleared hypotheses: F, c, hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 j : Discrete ι
hi : i ≠ j
let let₁ let₂ : IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
let₃ :
  let f := F.obj ∘ Discrete.mk;
  ∀ (this : F = Discrete.functor f),
    IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
let₄ :
  ∀ (f : ι → C) (this : F = Discrete.functor f),
    IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
let₅ :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
    IsPullback (P := initial.{v, u} C) (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
      (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) j)) (c.ι.app i) (c.ι.app j)
⊢ IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
have let₆ : ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c)
  (this : ∀ (i : Discrete ι), Subsingleton.{v + 1} (initial.{v, u} C ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)),
  IsPullback (P := initial.{v, u} C) (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
    (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) 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
Cleared hypotheses: F, c, hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 j : Discrete ι
hi : i ≠ j
let let₁ let₂ : IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
let₃ :
  let f := F.obj ∘ Discrete.mk;
  ∀ (this : F = Discrete.functor f),
    IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
let₄ :
  ∀ (f : ι → C) (this : F = Discrete.functor f),
    IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
let₅ :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
    IsPullback (P := initial.{v, u} C) (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
      (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) j)) (c.ι.app i) (c.ι.app j)
let₆ :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c)
    (this : ∀ (i : Discrete ι), Subsingleton.{v + 1} (initial.{v, u} C ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)),
    IsPullback (P := initial.{v, u} C) (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
      (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) j)) (c.ι.app i) (c.ι.app j)
⊢ IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
have h : ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c)
  (this : ∀ (i : Discrete ι), Subsingleton.{v + 1} (initial.{v, u} C ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)),
  initial.{v, u} C = if j.as = i.as then f i.as else initial.{v, u} C
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
Cleared hypotheses: F, c, hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
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 ι
f : ι → C := F.obj ∘ Discrete.mk
⊢ Mono (c.ι.app i)
have this : F = Discrete.functor f
Tactic: have : F = Discrete.functor f :=
    Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 ι
f : ι → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor f
⊢ Mono (c.ι.app i)
have clear_value : ∀ (f : ι → C) (this : F = Discrete.functor f), Mono (c.ι.app i)
Tactic: clear_value f
Cleared hypotheses: f, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 ι
f : ι → C
this : F = Discrete.functor f
⊢ Mono (c.ι.app i)
have subst : ∀ {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c), Mono (c.ι.app i)
Tactic: subst this
Cleared hypotheses: F, c, hc, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ Mono (c.ι.app i)
have refine : 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)
Tactic: refine PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i : Discrete ι
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)
have nth_rw : 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)
Tactic: nth_rw 1 [← Category.id_comp (c.ι.app i)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i : Discrete ι
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)
have h : 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 sorry)
      (if h : i.as = i.as then eqToHom sorry else eqToHom sorry ≫ initial.to (f i.as)))
Tactic: convert! IsPullback.paste_vert _ (isPullback_of_cofan_isVanKampen hc i.as i.as)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)
hc : IsVanKampenColimit c
h :
  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)))
⊢ 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)
have convert_4 : 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
Tactic: convert! IsPullback.paste_vert _ (isPullback_of_cofan_isVanKampen hc i.as i.as)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)
hc : IsVanKampenColimit c
h :
  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 : 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
⊢ 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)
have convert_6 : 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 sorry) (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
  (if h : i.as = i.as then eqToHom sorry else eqToHom sorry ≫ initial.to (f i.as))
Tactic: convert! IsPullback.paste_vert _ (isPullback_of_cofan_isVanKampen hc i.as i.as)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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)
⊢ Mono (c.ι.app i)
have let₃ : let f := F.obj ∘ Discrete.mk;
∀ (this : F = Discrete.functor f), 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⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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)
⊢ Mono (c.ι.app i)
have let₄ : ∀ (f : ι → C) (this : F = Discrete.functor f), 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⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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)
⊢ Mono (c.ι.app i)
have let₅ : ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c), 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⟩
Cleared hypotheses: F, c, hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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)
⊢ Mono (c.ι.app i)
have 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)
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⟩
Cleared hypotheses: F, c, hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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)
⊢ Mono (c.ι.app i)
have 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)
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⟩
Cleared hypotheses: F, c, hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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)
⊢ Mono (c.ι.app i)
have 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 sorry)
        (if h : i.as = i.as then eqToHom sorry else eqToHom sorry ≫ initial.to (f i.as)))
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⟩
Cleared hypotheses: F, c, hc