awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ IsUniversalColimit c
have obtain : ∀ (n : ℕ) (e : ι ≃ Fin n), IsUniversalColimit c
Tactic: obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ IsUniversalColimit c
have apply : IsUniversalColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
Tactic: apply (IsUniversalColimit.whiskerEquivalence_iff (Discrete.equivalence e).symm).mp
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ IsUniversalColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
have hc₁ : IsColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
Tactic: apply FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
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
⊢ IsVanKampenColimit c
have this : F = Discrete.functor f
Tactic: have : F = Discrete.functor f :=
    Functor.hext (fun _ ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ IsVanKampenColimit c
have clear_value : ∀ (f : Fin n → C) (this : F = Discrete.functor f), IsVanKampenColimit c
Tactic: clear_value f
Cleared hypotheses: f, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ IsVanKampenColimit c
have subst : ∀ {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
Tactic: subst this
Cleared hypotheses: F, c, hc, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ IsVanKampenColimit c
have 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))
Tactic: apply IsVanKampenColimit.of_iso _
      ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ 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))
have 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))
Tactic: apply @isVanKampenColimit_extendCofan _ _ _ _ _ _ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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))
⊢ 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))
have 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)
Tactic: apply @isVanKampenColimit_extendCofan _ _ _ _ _ _ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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)
⊢ 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))
have 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
Tactic: apply @isVanKampenColimit_extendCofan _ _ _ _ _ _ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ 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))
have 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))
Tactic: apply IH
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ 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)
have 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)
Tactic: apply FinitaryExtensive.van_kampen'
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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 ⟶
        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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ IsVanKampenColimit c
have zero : ∀ (f : Fin 0 → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit 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
Cleared hypotheses: n, f, c, hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ IsVanKampenColimit c
have 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
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
Cleared hypotheses: n, f, c, hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ IsVanKampenColimit c
have obtain : ∀ (n : ℕ) (e : ι ≃ Fin n), IsVanKampenColimit c
Tactic: obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ IsVanKampenColimit c
have apply : IsVanKampenColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
Tactic: apply (IsVanKampenColimit.whiskerEquivalence_iff (Discrete.equivalence e).symm).mp
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ IsVanKampenColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
have hc₁ : IsColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
Tactic: apply FinitaryExtensive.isVanKampen_finiteCoproducts_Fin
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
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
⊢ HasPullback g (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.Extensive (goal)
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
⊢ HasPullback g (c.ι.app i)
have clear_value : ∀ (f : ι → C) (this : F = Discrete.functor f), HasPullback g (c.ι.app i)
Tactic: clear_value f
Cleared hypotheses: f, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ HasPullback g (c.ι.app i)
have 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)
Tactic: subst this
Cleared hypotheses: F, c, hc, g, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ HasPullback g (c.ι.app i)
have 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)
Tactic: change Cofan f at c
Cleared hypotheses: c, hc, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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
⊢ HasPullback g (c.ι.app i)
have 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 ι })
Tactic: obtain ⟨i⟩ := i
Cleared hypotheses: i, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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 ι }
⊢ 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 : ι)))
have 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 sorry ≫ 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 : ι)))
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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 : ι)))
⊢ 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 : ι)))
have 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 sorry ≫ 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 : ι)))
Tactic: ext j