awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
F : Functor.{u_1, v, u_1, u} (Discrete ι) C
c : Cocone F
hc : IsColimit c
obtain : ∀ (n : ℕ) (e : ι ≃ Fin n), IsUniversalColimit c
⊢ IsUniversalColimit c

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
F : Functor.{u_1, v, u_1, u} (Discrete ι) C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
apply : IsUniversalColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
⊢ IsUniversalColimit c

Tactic:
apply (IsUniversalColimit.whiskerEquivalence_iff (Discrete.equivalence e).symm).mp

Premises used: CategoryTheory.Discrete.equivalence, Iff.mp, CategoryTheory.IsUniversalColimit.whiskerEquivalence_iff, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
F : Functor.{u_1, v, u_1, u} (Discrete ι) C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
hc₁ : IsColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
⊢ IsUniversalColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)

Tactic:
apply FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin

Premises used: CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
F : Functor.{u_1, v, u_1, u} (Discrete ι) C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)

Tactic:
exact (IsColimit.whiskerEquivalenceEquiv (Discrete.equivalence e).symm) hc

Premises used: CategoryTheory.Discrete.equivalence, DFunLike.coe, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
n : ℕ
F : Functor.{0, v, 0, u} (Discrete (Fin n)) C
c : Cocone F
hc : IsColimit c
f : Fin n → C := F.obj ∘ Discrete.mk
i : Fin n
⊢ HEq
    (F.map
      { down := { down := ⋯ : PLift ({ as := i : Discrete (Fin n) }.as = { as := i : Discrete (Fin n) }.as) } :
        ULift.{0, 0} (PLift ({ as := i : Discrete (Fin n) }.as = { as := i : Discrete (Fin n) }.as)) })
    (β :=
    Functor.obj.{0, v, 0, u} (Discrete.functor f) { as := i : Discrete (Fin n) } ⟶
      Functor.obj.{0, v, 0, u} (Discrete.functor f) { as := i : Discrete (Fin n) })
    (Functor.map (Discrete.functor f) { down := { down := ⋯ } })

Tactic:
simp [f]
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
n : ℕ
F : Functor.{0, v, 0, u} (Discrete (Fin n)) C
c : Cocone F
hc : IsColimit c
f : Fin n → C := F.obj ∘ Discrete.mk
⊢ F = Discrete.functor f

Tactic:
have : F = Discrete.functor f :=
    Functor.hext (fun _ ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
n : ℕ
F : Functor.{0, v, 0, u} (Discrete (Fin n)) C
c : Cocone F
hc : IsColimit c
f : Fin n → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor f
clear_value : ∀ (f : Fin n → C) (this : F = Discrete.functor f), IsVanKampenColimit c
⊢ IsVanKampenColimit c

Tactic:
clear_value f
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
n : ℕ
F : Functor.{0, v, 0, u} (Discrete (Fin n)) C
c : Cocone F
hc : IsColimit c
f : Fin n → C
this : F = Discrete.functor f
subst : ∀ {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
⊢ IsVanKampenColimit c

Tactic:
subst this
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
f : Fin 0 → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
isVanKampenColimit_of_isEmpty _ hc

Premises used: CategoryTheory.isVanKampenColimit_of_isEmpty
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
f : Fin 0 → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
exact isVanKampenColimit_of_isEmpty _ hc

Premises used: CategoryTheory.isVanKampenColimit_of_isEmpty
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
apply :
  IsVanKampenColimit.{0, 0, v, u} (J := Discrete (Fin (n + 1))) (C := C) (F := Discrete.functor f)
    (extendCofan (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))
      (BinaryCofan.mk (P :=
        coprod.{v, u} (f 0)
          (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
            (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
        coprod.inl coprod.inr))
⊢ IsVanKampenColimit c

Tactic:
apply IsVanKampenColimit.of_iso _
      ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.extendCofanIsColimit, CategoryTheory.IsVanKampenColimit.of_iso, CategoryTheory.Limits.IsColimit.uniqueUpToIso, CategoryTheory.Limits.coproductIsCoproduct
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
apply :
  IsVanKampenColimit.{0, 0, v, u} (J := Discrete (Fin n)) (C := C) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
    (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))
apply₁ :
  IsVanKampenColimit.{0, 0, v, u} (C := C) (F :=
    pair (f 0)
      (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
        (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
    (BinaryCofan.mk (P :=
      coprod.{v, u} (f 0)
        (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
          (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
      coprod.inl coprod.inr)
apply₂ :
  ∀ {Z : C}
    (i :
      Z ⟶
        Cocone.pt.{0, v, 0, u} (F :=
          pair (f 0)
            (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
              (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
          (BinaryCofan.mk (P :=
            coprod.{v, u} (f 0)
              (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
            coprod.inl coprod.inr)),
    HasPullback
      (BinaryCofan.inr
        (BinaryCofan.mk (P :=
          coprod.{v, u} (f 0)
            (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
              (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
          coprod.inl coprod.inr))
      i
⊢ IsVanKampenColimit.{0, 0, v, u} (J := Discrete (Fin (n + 1))) (C := C) (F := Discrete.functor f)
    (extendCofan (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))
      (BinaryCofan.mk (P :=
        coprod.{v, u} (f 0)
          (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
            (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
        coprod.inl coprod.inr))

Tactic:
apply @isVanKampenColimit_extendCofan _ _ _ _ _ _ _ _ ?_

Premises used: CategoryTheory.isVanKampenColimit_extendCofan
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
hc₁ :
  IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
    (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))
⊢ IsVanKampenColimit.{0, 0, v, u} (J := Discrete (Fin n)) (C := C) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
    (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))

Tactic:
apply IH
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
⊢ IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
    (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))

Tactic:
exact coproductIsCoproduct _

Premises used: CategoryTheory.Limits.coproductIsCoproduct
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
a :
  IsColimit.{0, v, 0, u} (C := C) (F :=
    pair (f 0)
      (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
        (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
    (BinaryCofan.mk (P :=
      coprod.{v, u} (f 0)
        (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
          (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
      coprod.inl coprod.inr)
⊢ IsVanKampenColimit.{0, 0, v, u} (C := C) (F :=
    pair (f 0)
      (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
        (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
    (BinaryCofan.mk (P :=
      coprod.{v, u} (f 0)
        (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
          (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
      coprod.inl coprod.inr)

Tactic:
apply FinitaryExtensive.van_kampen'

Premises used: CategoryTheory.FinitaryExtensive.van_kampen'
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
⊢ IsColimit.{0, v, 0, u} (C := C) (F :=
    pair (f 0)
      (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
        (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
    (BinaryCofan.mk (P :=
      coprod.{v, u} (f 0)
        (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
          (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
      coprod.inl coprod.inr)

Tactic:
exact coprodIsCoprod _ _

Premises used: CategoryTheory.Limits.coprodIsCoprod
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
dsimp :
  ∀ {Z : C} (i : Z ⟶ coprod.{v, u} (f 0) (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)), HasPullback coprod.inr i
⊢ ∀ {Z : C}
    (i :
      Z ⟶
        Cocone.pt.{0, v, 0, u} (F :=
          pair (f 0)
            (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
              (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
          (BinaryCofan.mk (P :=
            coprod.{v, u} (f 0)
              (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
            coprod.inl coprod.inr)),
    HasPullback
      (BinaryCofan.inr
        (BinaryCofan.mk (P :=
          coprod.{v, u} (f 0)
            (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
              (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
          coprod.inl coprod.inr))
      i

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
⊢ ∀ {Z : C} (i : Z ⟶ coprod.{v, u} (f 0) (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)), HasPullback coprod.inr i

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
n : ℕ
f : Fin n → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
zero : ∀ (f : Fin 0 → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
succ :
  ∀ (n : ℕ)
    (IH : ∀ (f : Fin n → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c)
    (f : Fin (n + 1) → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
⊢ IsVanKampenColimit c

Tactic:
induction n with
  | zero => exact isVanKampenColimit_of_isEmpty _ hc
  | succ n IH =>
    apply IsVanKampenColimit.of_iso _
      ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)
    apply @isVanKampenColimit_extendCofan _ _ _ _ _ _ _ _ ?_
    · apply IH
      exact coproductIsCoproduct _
    · apply FinitaryExtensive.van_kampen'
      exact coprodIsCoprod _ _
    · dsimp
      infer_instance

Premises used: CategoryTheory.FinitaryExtensive.van_kampen', CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.isVanKampenColimit_extendCofan, CategoryTheory.Limits.coproductIsCoproduct
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
F : Functor.{u_1, v, u_1, u} (Discrete ι) C
c : Cocone F
hc : IsColimit c
obtain : ∀ (n : ℕ) (e : ι ≃ Fin n), IsVanKampenColimit c
⊢ IsVanKampenColimit c

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
F : Functor.{u_1, v, u_1, u} (Discrete ι) C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
apply : IsVanKampenColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
⊢ IsVanKampenColimit c

Tactic:
apply (IsVanKampenColimit.whiskerEquivalence_iff (Discrete.equivalence e).symm).mp

Premises used: CategoryTheory.Discrete.equivalence, CategoryTheory.IsVanKampenColimit.whiskerEquivalence_iff, Iff.mp, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
F : Functor.{u_1, v, u_1, u} (Discrete ι) C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
hc₁ : IsColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
⊢ IsVanKampenColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)

Tactic:
apply FinitaryExtensive.isVanKampen_finiteCoproducts_Fin

Premises used: CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts_Fin
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
F : Functor.{u_1, v, u_1, u} (Discrete ι) C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)

Tactic:
exact (IsColimit.whiskerEquivalenceEquiv (Discrete.equivalence e).symm) hc

Premises used: CategoryTheory.Discrete.equivalence, DFunLike.coe, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
F : Functor.{u_1, v, u_1, u} (Discrete ι) C
c : Cocone F
hc : IsColimit c
i_1 : Discrete ι
X : C
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) i_1
f : ι → C := F.obj ∘ Discrete.mk
i : ι
⊢ HEq
    (F.map
      { down := { down := ⋯ : PLift ({ as := i : Discrete ι }.as = { as := i : Discrete ι }.as) } :
        ULift.{u_1, 0} (PLift ({ as := i : Discrete ι }.as = { as := i : Discrete ι }.as)) })
    (β :=
    Functor.obj.{u_1, v, u_1, u} (Discrete.functor f) { as := i : Discrete ι } ⟶
      Functor.obj.{u_1, v, u_1, u} (Discrete.functor f) { as := i : Discrete ι })
    (Functor.map (Discrete.functor f) { down := { down := ⋯ } })

Tactic:
simp [f]
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
F : Functor.{u_1, v, u_1, u} (Discrete ι) C
c : Cocone F
hc : IsColimit c
i : Discrete ι
X : C
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) i
f : ι → C := F.obj ∘ Discrete.mk
⊢ F = Discrete.functor f

Tactic:
have : F = Discrete.functor f :=
    Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
F : Functor.{u_1, v, u_1, u} (Discrete ι) C
c : Cocone F
hc : IsColimit c
i : Discrete ι
X : C
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) i
f : ι → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor f
clear_value : ∀ (f : ι → C) (this : F = Discrete.functor f), HasPullback g (c.ι.app i)
⊢ HasPullback g (c.ι.app i)

Tactic:
clear_value f
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
F : Functor.{u_1, v, u_1, u} (Discrete ι) C
c : Cocone F
hc : IsColimit c
i : Discrete ι
X : C
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) i
f : ι → C
this : F = Discrete.functor f
subst :
  ∀ {c : Cocone.{u_1, v, u_1, u} (Discrete.functor f)} (hc : IsColimit c)
    (g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) i), HasPullback g (c.ι.app i)
⊢ HasPullback g (c.ι.app i)

Tactic:
subst this
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
i : Discrete ι
X : C
f : ι → C
c : Cocone.{u_1, v, u_1, u} (Discrete.functor f)
hc : IsColimit c
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) i
change :
  ∀ {c : Cofan.{u_1, v, u} f} (hc : IsColimit c)
    (g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) i), HasPullback g (c.ι.app i)
⊢ HasPullback g (c.ι.app i)

Tactic:
change Cofan f at c

Premises used: CategoryTheory.Limits.Cofan
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
i : Discrete ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) i
obtain :
  ∀ (i : ι)
    (g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }),
    HasPullback g (c.ι.app { as := i : Discrete ι })
⊢ HasPullback g (c.ι.app i)

Tactic:
obtain ⟨i⟩ := i
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
i : ι
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }
h₁ :
  CategoryStruct.comp (Y := coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
      coprod.inl
      (CategoryStruct.comp (Y := sigmaObj.{u_1, v, u} f)
        (coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)))
        (Sigma.desc fun (j : ι) ↦
          if h : j = i then eqToHom ⋯ ≫ coprod.inl
          else
            Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
                (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
              coprod.inr)) =
    coprod.inl ≫ 𝟙 (coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
h₂ :
  ∀ (j : (↑{i}ᶜ : Type u_1)),
    CategoryStruct.comp (Y := sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
        (Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) j)
        (CategoryStruct.comp (Y := coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
          coprod.inr
          (CategoryStruct.comp (Y := sigmaObj.{u_1, v, u} f)
            (coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)))
            (Sigma.desc fun (j : ι) ↦
              if h : j = i then eqToHom ⋯ ≫ coprod.inl
              else
                Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
                    (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
                  coprod.inr))) =
      Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) j ≫
        coprod.inr ≫ 𝟙 (coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
⊢ CategoryStruct.comp (Y := sigmaObj.{u_1, v, u} f)
      (coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)))
      (Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ coprod.inl
        else
          Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
              (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
            coprod.inr) =
    𝟙 (coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))

Tactic:
ext j