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
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor F')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C) (Discrete.functor F') (Discrete.functor f)
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ :
  (sigmaObj.{0, v, u} fun (j : Fin n) ↦
      obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) ⟶
    T
⊢ CategoryStruct.comp (Y :=
      obj.{0, v, 0, u}
        (obj (const (Discrete WalkingPair))
          (Cocone.pt (F :=
            pair (F' 0)
              (sigmaObj.{0, v, u} fun (j : Fin n) ↦
                obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }))
            (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
              (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ : Discrete (Fin (n + 1)) }))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (BinaryCofan.inr
        (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
          (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
      (Hc.desc
        (Cofan.mk T fun (i : Fin (n + 1)) ↦
          Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
            (fun (i : Fin n) ↦
              Sigma.ι.{0, v, u} (C := C)
                  (fun (j : Fin n) ↦ obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) })
                  i ≫
                f₂)
            i)) =
    f₂
have refine_2 : CategoryStruct.comp (Y := c.pt) (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })
    (Hc.desc
      (Cofan.mk T fun (i : Fin (n + 1)) ↦
        Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
          (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) i)) =
  f₂
Tactic: simp only [Discrete.functor_obj, pair_obj_right, BinaryCofan.mk_pt, Functor.const_obj_obj,
        BinaryCofan.mk_inr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor F')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C) (Discrete.functor F') (Discrete.functor f)
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ :
  (sigmaObj.{0, v, u} fun (j : Fin n) ↦
      obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) ⟶
    T
⊢ CategoryStruct.comp (Y := c.pt) (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })
      (Hc.desc
        (Cofan.mk T fun (i : Fin (n + 1)) ↦
          Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
            (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) i)) =
    f₂
have refine_2 : ∀ (j : Fin n),
  CategoryStruct.comp (Y := sigmaObj.{0, v, u} fun (j : Fin n) ↦ F' j.succ)
      (Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) j)
      (CategoryStruct.comp (Y := c.pt) (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })
        (Hc.desc
          (Cofan.mk T fun (i : Fin (n + 1)) ↦
            Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
              (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) i))) =
    Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) j ≫ f₂
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor F')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C) (Discrete.functor F') (Discrete.functor f)
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ :
  (sigmaObj.{0, v, u} fun (j : Fin n) ↦
      obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) ⟶
    T
f₃ :
  Cocone.pt (F :=
      pair (F' 0)
        (sigmaObj.{0, v, u} fun (j : Fin n) ↦
          obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }))
      (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
        (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ : Discrete (Fin (n + 1)) })) ⟶
    T
m₁ :
  BinaryCofan.inl
        (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
          (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })) ≫
      f₃ =
    f₁
m₂ :
  BinaryCofan.inr
        (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
          (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })) ≫
      f₃ =
    f₂
⊢ f₃ =
    Hc.desc
      (Cofan.mk T fun (i : Fin (n + 1)) ↦
        Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
          (fun (i : Fin n) ↦
            Sigma.ι.{0, v, u} (C := C)
                (fun (j : Fin n) ↦ obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) i ≫
              f₂)
          i)
have refine_2 : f₃ =
  Hc.desc
    (Cofan.mk T fun (i : Fin (n + 1)) ↦
      Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
        (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) i)
Tactic: simp only [Discrete.functor_obj_eq_as, pair_obj_left, BinaryCofan.mk_pt, const_obj_obj,
        BinaryCofan.mk_inl, pair_obj_right, BinaryCofan.mk_inr] at m₁ m₂ ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor F')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C) (Discrete.functor F') (Discrete.functor f)
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ :
  (sigmaObj.{0, v, u} fun (j : Fin n) ↦
      obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) ⟶
    T
f₃ :
  Cocone.pt (F :=
      pair (F' 0)
        (sigmaObj.{0, v, u} fun (j : Fin n) ↦
          obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }))
      (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
        (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ : Discrete (Fin (n + 1)) })) ⟶
    T
m₁ : c.ι.app { as := 0 } ≫ f₃ = f₁
m₂ : (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ }) ≫ f₃ = f₂
⊢ f₃ =
    Hc.desc
      (Cofan.mk T fun (i : Fin (n + 1)) ↦
        Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
          (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) i)
have refine_2 : ∀ (j : Discrete (Fin (n + 1))),
  c.ι.app j ≫ f₃ =
    NatTrans.app
      (Cocone.ι
        (Cofan.mk T fun (i : Fin (n + 1)) ↦
          Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
            (fun (i : Fin n) ↦
              Sigma.ι.{0, v, u} (C := C)
                  (fun (j : Fin n) ↦ obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) })
                  i ≫
                f₂)
            i))
      j
Tactic: refine Hc.uniq (Cofan.mk T (Fin.cases f₁
        (fun i ↦ Sigma.ι (fun (j : Fin n) ↦ (Discrete.functor F').obj ⟨j.succ⟩) _ ≫ f₂))) _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
j_1 : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor F')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C) (Discrete.functor F') (Discrete.functor f)
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ :
  (sigmaObj.{0, v, u} fun (j : Fin n) ↦
      obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) ⟶
    T
f₃ :
  Cocone.pt (F :=
      pair (F' 0)
        (sigmaObj.{0, v, u} fun (j : Fin n) ↦
          obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }))
      (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
        (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ : Discrete (Fin (n + 1)) })) ⟶
    T
m₁ : c.ι.app { as := 0 } ≫ f₃ = f₁
m₂ : (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ }) ≫ f₃ = f₂
j : Fin (n + 1)
⊢ Eq (α :=
    obj.{0, v, 0, u} (Discrete.functor F') { as := j : Discrete (Fin (n + 1)) } ⟶
      Cocone.pt.{0, v, 0, u} (J := Discrete (Fin (n + 1))) (F := Discrete.functor F')
        (Cofan.mk T fun (i : Fin (n + 1)) ↦
          Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
            (fun (i : Fin n) ↦
              Sigma.ι.{0, v, u} (C := C)
                  (fun (j : Fin n) ↦ obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) })
                  i ≫
                f₂)
            i))
    (c.ι.app { as := j } ≫ f₃)
    (NatTrans.app
      (Cocone.ι
        (Cofan.mk T fun (i : Fin (n + 1)) ↦
          Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
            (fun (i : Fin n) ↦
              Sigma.ι.{0, v, u} (C := C)
                  (fun (j : Fin n) ↦ obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) })
                  i ≫
                f₂)
            i))
      { as := j })
have refine_2 : Eq (α := F' j ⟶ T) (c.ι.app { as := j } ≫ f₃)
  (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
    (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) j)
Tactic: simp only [Discrete.functor_obj, Cofan.mk_pt, Functor.const_obj_obj, Cofan.mk_ι_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
j_1 : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor F')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C) (Discrete.functor F') (Discrete.functor f)
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ :
  (sigmaObj.{0, v, u} fun (j : Fin n) ↦
      obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) ⟶
    T
f₃ :
  Cocone.pt (F :=
      pair (F' 0)
        (sigmaObj.{0, v, u} fun (j : Fin n) ↦
          obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }))
      (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
        (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ : Discrete (Fin (n + 1)) })) ⟶
    T
m₁ : c.ι.app { as := 0 } ≫ f₃ = f₁
m₂ : (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ }) ≫ f₃ = f₂
j : Fin (n + 1)
⊢ Eq (α := F' j ⟶ T) (c.ι.app { as := j } ≫ f₃)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
      (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) j)
have refine_2 : Eq (α := F' 0 ⟶ T) (c.ι.app { as := 0 } ≫ f₃)
  (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
    (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) 0)
Tactic: induction j using Fin.inductionOn
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
j_1 : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor F')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C) (Discrete.functor F') (Discrete.functor f)
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ :
  (sigmaObj.{0, v, u} fun (j : Fin n) ↦
      obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) ⟶
    T
f₃ :
  Cocone.pt (F :=
      pair (F' 0)
        (sigmaObj.{0, v, u} fun (j : Fin n) ↦
          obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }))
      (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
        (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ : Discrete (Fin (n + 1)) })) ⟶
    T
m₁ : c.ι.app { as := 0 } ≫ f₃ = f₁
m₂ : (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ }) ≫ f₃ = f₂
j : Fin (n + 1)
refine_2 :
  Eq (α := F' 0 ⟶ T) (c.ι.app { as := 0 } ≫ f₃)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
      (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) 0)
⊢ Eq (α := F' j ⟶ T) (c.ι.app { as := j } ≫ f₃)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
      (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) j)
have refine_2₁ : ∀ (i : Fin n),
  Eq (α := F' i.castSucc ⟶ T) (c.ι.app { as := i.castSucc } ≫ f₃)
      (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
        (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) i.castSucc) →
    Eq (α := F' i.succ ⟶ T) (c.ι.app { as := i.succ } ≫ f₃)
      (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
        (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) i.succ)
Tactic: induction j using Fin.inductionOn
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
F : Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
t₂' :
  ∀ (j : Discrete WalkingPair),
    IsPullback (P :=
      obj.{0, v, 0, u} (pair (F.obj { as := 0 }) (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ })) j)
      (NatTrans.app
        (Cocone.ι
          (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
            (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
        j)
      (NatTrans.app (mapPair (α.app { as := 0 }) (Sigma.desc fun (b : Fin n) ↦ α.app { as := b.succ } ≫ c₁.inj b)) j) i
      (c₂.ι.app j)
j : Fin n
h :
  IsPullback (P := F.obj { as := j.castSucc }) (c.ι.app { as := j.castSucc }) (α.app { as := j.castSucc }) i
    ((extendCofan c₁ c₂).ι.app { as := j.castSucc })
⊢ IsPullback (P := F.obj { as := j.succ }) (c.ι.app { as := j.succ }) (α.app { as := j.succ }) i
    ((extendCofan c₁ c₂).ι.app { as := j.succ })
have refine_3 : ∀
  (t₁' :
    IsPullback (P :=
      obj.{0, v, 0, u} (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ }) { as := j : Discrete (Fin n) }) (X :=
      obj.{0, v, 0, u}
        (obj (const (Discrete (Fin n)))
          (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F :=
            Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })
            (Cofan.mk (colimit.cocone (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })).1
              (Sigma.ι fun (j : Fin n) ↦ F.obj { as := j.succ }))))
        { as := j : Discrete (Fin n) })
      (NatTrans.app
        (Cocone.ι
          (Cofan.mk (colimit.cocone (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })).1
            (Sigma.ι fun (j : Fin n) ↦ F.obj { as := j.succ })))
        { as := j })
      (NatTrans.app (Discrete.natTrans fun (i : Discrete (Fin n)) ↦ α.app { as := i.as.succ }) { as := j })
      (Sigma.desc fun (j : Fin n) ↦ α.app { as := j.succ } ≫ c₁.inj j) (c₁.ι.app { as := j : Discrete (Fin n) })),
  IsPullback (P := F.obj { as := j.succ }) (c.ι.app { as := j.succ }) (α.app { as := j.succ }) i
    ((extendCofan c₁ c₂).ι.app { as := j.succ })
Tactic: have t₁' := (@t₁ (Discrete.functor (fun j ↦ F.obj ⟨j.succ⟩)) (Cofan.mk _ _) (Discrete.natTrans
      fun i ↦ α.app _) (Sigma.desc (fun j ↦ α.app _ ≫ c₁.inj _)) ?_
      (.of_discrete _)).mp ⟨coproductIsCoproduct _⟩ ⟨j⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
F : Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
t₂' :
  ∀ (j : Discrete WalkingPair),
    IsPullback (P :=
      obj.{0, v, 0, u} (pair (F.obj { as := 0 }) (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ })) j)
      (NatTrans.app
        (Cocone.ι
          (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
            (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
        j)
      (NatTrans.app (mapPair (α.app { as := 0 }) (Sigma.desc fun (b : Fin n) ↦ α.app { as := b.succ } ≫ c₁.inj b)) j) i
      (c₂.ι.app j)
j_1 : Fin n
h :
  IsPullback (P := F.obj { as := j_1.castSucc }) (c.ι.app { as := j_1.castSucc }) (α.app { as := j_1.castSucc }) i
    ((extendCofan c₁ c₂).ι.app { as := j_1.castSucc })
j : Fin n
⊢ Eq (α :=
    obj.{0, v, 0, u} (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ }) { as := j : Discrete (Fin n) } ⟶
      obj.{0, v, 0, u} (obj (const (Discrete (Fin n))) c₁.pt) { as := j : Discrete (Fin n) })
    (NatTrans.app ((Discrete.natTrans fun (i : Discrete (Fin n)) ↦ α.app { as := i.as.succ }) ≫ c₁.ι) { as := j })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete (Fin n)))
          (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F :=
            Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })
            (Cofan.mk (colimit.cocone (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })).1
              (Sigma.ι fun (j : Fin n) ↦ F.obj { as := j.succ }))))
        (Cocone.ι
          (Cofan.mk (colimit.cocone (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })).1
            (Sigma.ι fun (j : Fin n) ↦ F.obj { as := j.succ })))
        (map (const (Discrete (Fin n))) (Sigma.desc fun (j : Fin n) ↦ α.app { as := j.succ } ≫ c₁.inj j)))
      { as := j })
have refine_3 : Eq (α := F.obj { as := j.succ : Discrete (Fin (n + 1)) } ⟶ c₁.pt)
  (α.app { as := j.succ : Discrete (Fin (n + 1)) } ≫ c₁.ι.app { as := j })
  (CategoryStruct.comp (Y :=
    colimit.{0, 0, v, u} (J := Discrete (Fin n)) (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ }))
    (Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F.obj { as := j.succ }) j)
    (Sigma.desc fun (j : Fin n) ↦ α.app { as := j.succ } ≫ c₁.inj j))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
F : Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
t₂' :
  ∀ (j : Discrete WalkingPair),
    IsPullback (P :=
      obj.{0, v, 0, u} (pair (F.obj { as := 0 }) (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ })) j)
      (NatTrans.app
        (Cocone.ι
          (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
            (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
        j)
      (NatTrans.app (mapPair (α.app { as := 0 }) (Sigma.desc fun (b : Fin n) ↦ α.app { as := b.succ } ≫ c₁.inj b)) j) i
      (c₂.ι.app j)
j_1 : Fin n
h :
  IsPullback (P := F.obj { as := j_1.castSucc }) (c.ι.app { as := j_1.castSucc }) (α.app { as := j_1.castSucc }) i
    ((extendCofan c₁ c₂).ι.app { as := j_1.castSucc })
j : Fin n
⊢ Eq (α := F.obj { as := j.succ : Discrete (Fin (n + 1)) } ⟶ c₁.pt)
    (α.app { as := j.succ : Discrete (Fin (n + 1)) } ≫ c₁.ι.app { as := j })
    (CategoryStruct.comp (Y :=
      colimit.{0, 0, v, u} (J := Discrete (Fin n)) (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ }))
      (Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F.obj { as := j.succ }) j)
      (Sigma.desc fun (j : Fin n) ↦ α.app { as := j.succ } ≫ c₁.inj j))
have refine_3 : Eq (α := F.obj { as := j.succ : Discrete (Fin (n + 1)) } ⟶ c₁.pt)
  (α.app { as := j.succ : Discrete (Fin (n + 1)) } ≫ c₁.ι.app { as := j })
  (NatTrans.app (Cocone.ι (Cofan.mk c₁.pt fun (j : Fin n) ↦ α.app { as := j.succ } ≫ c₁.inj j)) { as := j })
Tactic: rw [colimit.ι_desc]