[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
⊢ (b : Fin (n + 1)) → c₂.pt ⟶ f b
[PROOFSTEP]
refine' Fin.cases _ _
[GOAL]
case refine'_1
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
⊢ c₂.pt ⟶ f 0
[PROOFSTEP]
apply c₂.fst
[GOAL]
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
⊢ (i : Fin n) → c₂.pt ⟶ f (Fin.succ i)
[PROOFSTEP]
intro i
[GOAL]
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
i : Fin n
⊢ c₂.pt ⟶ f (Fin.succ i)
[PROOFSTEP]
apply c₂.snd ≫ c₁.π.app ⟨i⟩
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
⊢ s.pt ⟶ (extendFan c₁ c₂).pt
[PROOFSTEP]
apply (BinaryFan.IsLimit.lift' t₂ (s.π.app ⟨0⟩) _).1
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
⊢ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₁.pt
[PROOFSTEP]
apply t₁.lift ⟨_, Discrete.natTrans fun ⟨i⟩ => s.π.app ⟨i.succ⟩⟩
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
x✝ : Discrete (Fin (n + 1))
j : Fin (n + 1)
⊢ (fun s =>
          ↑(BinaryFan.IsLimit.lift' t₂ (NatTrans.app s.π { as := 0 })
              (IsLimit.lift t₁
                { pt := s.pt,
                  π :=
                    Discrete.natTrans fun x =>
                      match x with
                      | { as := i } => NatTrans.app s.π { as := Fin.succ i } })))
        s ≫
      NatTrans.app (extendFan c₁ c₂).π { as := j } =
    NatTrans.app s.π { as := j }
[PROOFSTEP]
refine' Fin.inductionOn j ?_ ?_
[GOAL]
case refine'_1
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
x✝ : Discrete (Fin (n + 1))
j : Fin (n + 1)
⊢ (fun s =>
          ↑(BinaryFan.IsLimit.lift' t₂ (NatTrans.app s.π { as := 0 })
              (IsLimit.lift t₁
                { pt := s.pt,
                  π :=
                    Discrete.natTrans fun x =>
                      match x with
                      | { as := i } => NatTrans.app s.π { as := Fin.succ i } })))
        s ≫
      NatTrans.app (extendFan c₁ c₂).π { as := 0 } =
    NatTrans.app s.π { as := 0 }
[PROOFSTEP]
apply (BinaryFan.IsLimit.lift' t₂ _ _).2.1
[GOAL]
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
x✝ : Discrete (Fin (n + 1))
j : Fin (n + 1)
⊢ ∀ (i : Fin n),
    (fun s =>
              ↑(BinaryFan.IsLimit.lift' t₂ (NatTrans.app s.π { as := 0 })
                  (IsLimit.lift t₁
                    { pt := s.pt,
                      π :=
                        Discrete.natTrans fun x =>
                          match x with
                          | { as := i } => NatTrans.app s.π { as := Fin.succ i } })))
            s ≫
          NatTrans.app (extendFan c₁ c₂).π { as := Fin.castSucc i } =
        NatTrans.app s.π { as := Fin.castSucc i } →
      (fun s =>
              ↑(BinaryFan.IsLimit.lift' t₂ (NatTrans.app s.π { as := 0 })
                  (IsLimit.lift t₁
                    { pt := s.pt,
                      π :=
                        Discrete.natTrans fun x =>
                          match x with
                          | { as := i } => NatTrans.app s.π { as := Fin.succ i } })))
            s ≫
          NatTrans.app (extendFan c₁ c₂).π { as := Fin.succ i } =
        NatTrans.app s.π { as := Fin.succ i }
[PROOFSTEP]
rintro i -
[GOAL]
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
x✝ : Discrete (Fin (n + 1))
j : Fin (n + 1)
i : Fin n
⊢ (fun s =>
          ↑(BinaryFan.IsLimit.lift' t₂ (NatTrans.app s.π { as := 0 })
              (IsLimit.lift t₁
                { pt := s.pt,
                  π :=
                    Discrete.natTrans fun x =>
                      match x with
                      | { as := i } => NatTrans.app s.π { as := Fin.succ i } })))
        s ≫
      NatTrans.app (extendFan c₁ c₂).π { as := Fin.succ i } =
    NatTrans.app s.π { as := Fin.succ i }
[PROOFSTEP]
dsimp only [extendFan_π_app]
[GOAL]
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
x✝ : Discrete (Fin (n + 1))
j : Fin (n + 1)
i : Fin n
⊢ ↑(BinaryFan.IsLimit.lift' t₂ (NatTrans.app s.π { as := 0 })
          (IsLimit.lift t₁ { pt := s.pt, π := Discrete.natTrans fun x => NatTrans.app s.π { as := Fin.succ x.as } })) ≫
      Fin.cases (BinaryFan.fst c₂) (fun i => BinaryFan.snd c₂ ≫ NatTrans.app c₁.π { as := i }) (Fin.succ i) =
    NatTrans.app s.π { as := Fin.succ i }
[PROOFSTEP]
rw [Fin.cases_succ, ← assoc, (BinaryFan.IsLimit.lift' t₂ _ _).2.2, t₁.fac]
[GOAL]
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
x✝ : Discrete (Fin (n + 1))
j : Fin (n + 1)
i : Fin n
⊢ NatTrans.app { pt := s.pt, π := Discrete.natTrans fun x => NatTrans.app s.π { as := Fin.succ x.as } }.π { as := i } =
    NatTrans.app s.π { as := Fin.succ i }
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ NatTrans.app (extendFan c₁ c₂).π j = NatTrans.app s.π j
⊢ m =
    (fun s =>
        ↑(BinaryFan.IsLimit.lift' t₂ (NatTrans.app s.π { as := 0 })
            (IsLimit.lift t₁
              { pt := s.pt,
                π :=
                  Discrete.natTrans fun x =>
                    match x with
                    | { as := i } => NatTrans.app s.π { as := Fin.succ i } })))
      s
[PROOFSTEP]
apply BinaryFan.IsLimit.hom_ext t₂
[GOAL]
case h₁
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ NatTrans.app (extendFan c₁ c₂).π j = NatTrans.app s.π j
⊢ m ≫ BinaryFan.fst c₂ =
    (fun s =>
          ↑(BinaryFan.IsLimit.lift' t₂ (NatTrans.app s.π { as := 0 })
              (IsLimit.lift t₁
                { pt := s.pt,
                  π :=
                    Discrete.natTrans fun x =>
                      match x with
                      | { as := i } => NatTrans.app s.π { as := Fin.succ i } })))
        s ≫
      BinaryFan.fst c₂
[PROOFSTEP]
rw [(BinaryFan.IsLimit.lift' t₂ _ _).2.1]
[GOAL]
case h₁
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ NatTrans.app (extendFan c₁ c₂).π j = NatTrans.app s.π j
⊢ m ≫ BinaryFan.fst c₂ = NatTrans.app s.π { as := 0 }
[PROOFSTEP]
apply w ⟨0⟩
[GOAL]
case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ NatTrans.app (extendFan c₁ c₂).π j = NatTrans.app s.π j
⊢ m ≫ BinaryFan.snd c₂ =
    (fun s =>
          ↑(BinaryFan.IsLimit.lift' t₂ (NatTrans.app s.π { as := 0 })
              (IsLimit.lift t₁
                { pt := s.pt,
                  π :=
                    Discrete.natTrans fun x =>
                      match x with
                      | { as := i } => NatTrans.app s.π { as := Fin.succ i } })))
        s ≫
      BinaryFan.snd c₂
[PROOFSTEP]
rw [(BinaryFan.IsLimit.lift' t₂ _ _).2.2]
[GOAL]
case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ NatTrans.app (extendFan c₁ c₂).π j = NatTrans.app s.π j
⊢ m ≫ BinaryFan.snd c₂ =
    IsLimit.lift t₁
      { pt := s.pt,
        π :=
          Discrete.natTrans fun x =>
            match x with
            | { as := i } => NatTrans.app s.π { as := Fin.succ i } }
[PROOFSTEP]
apply t₁.uniq ⟨_, _⟩
[GOAL]
case h₂.x
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ NatTrans.app (extendFan c₁ c₂).π j = NatTrans.app s.π j
⊢ ∀ (j : Discrete (Fin n)),
    (m ≫ BinaryFan.snd c₂) ≫ NatTrans.app c₁.π j =
      NatTrans.app
        { pt := s.1,
            π :=
              Discrete.natTrans fun x =>
                match x with
                | { as := i } => NatTrans.app s.π { as := Fin.succ i } }.π
        j
[PROOFSTEP]
rintro ⟨j⟩
[GOAL]
case h₂.x.mk
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ NatTrans.app (extendFan c₁ c₂).π j = NatTrans.app s.π j
j : Fin n
⊢ (m ≫ BinaryFan.snd c₂) ≫ NatTrans.app c₁.π { as := j } =
    NatTrans.app
      { pt := s.1,
          π :=
            Discrete.natTrans fun x =>
              match x with
              | { as := i } => NatTrans.app s.π { as := Fin.succ i } }.π
      { as := j }
[PROOFSTEP]
rw [assoc]
[GOAL]
case h₂.x.mk
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ NatTrans.app (extendFan c₁ c₂).π j = NatTrans.app s.π j
j : Fin n
⊢ m ≫ BinaryFan.snd c₂ ≫ NatTrans.app c₁.π { as := j } =
    NatTrans.app
      { pt := s.1,
          π :=
            Discrete.natTrans fun x =>
              match x with
              | { as := i } => NatTrans.app s.π { as := Fin.succ i } }.π
      { as := j }
[PROOFSTEP]
dsimp only [Discrete.natTrans_app]
[GOAL]
case h₂.x.mk
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ NatTrans.app (extendFan c₁ c₂).π j = NatTrans.app s.π j
j : Fin n
⊢ m ≫ BinaryFan.snd c₂ ≫ NatTrans.app c₁.π { as := j } = NatTrans.app s.π { as := Fin.succ j }
[PROOFSTEP]
rw [← w ⟨j.succ⟩]
[GOAL]
case h₂.x.mk
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ NatTrans.app (extendFan c₁ c₂).π j = NatTrans.app s.π j
j : Fin n
⊢ m ≫ BinaryFan.snd c₂ ≫ NatTrans.app c₁.π { as := j } = m ≫ NatTrans.app (extendFan c₁ c₂).π { as := Fin.succ j }
[PROOFSTEP]
dsimp only [extendFan_π_app]
[GOAL]
case h₂.x.mk
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i => f (Fin.succ i)
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ NatTrans.app (extendFan c₁ c₂).π j = NatTrans.app s.π j
j : Fin n
⊢ m ≫ BinaryFan.snd c₂ ≫ NatTrans.app c₁.π { as := j } =
    m ≫ Fin.cases (BinaryFan.fst c₂) (fun i => BinaryFan.snd c₂ ≫ NatTrans.app c₁.π { as := i }) (Fin.succ j)
[PROOFSTEP]
rw [Fin.cases_succ]
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
f : Fin 0 → C
⊢ HasProduct f
[PROOFSTEP]
letI : HasLimitsOfShape (Discrete (Fin 0)) C :=
  hasLimitsOfShape_of_equivalence (Discrete.equivalence.{0} finZeroEquiv'.symm)
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
f : Fin 0 → C
this : HasLimitsOfShape (Discrete (Fin 0)) C :=
  hasLimitsOfShape_of_equivalence (Discrete.equivalence finZeroEquiv'.symm)
⊢ HasProduct f
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
n : ℕ
f : Fin (n + 1) → C
⊢ HasProduct f
[PROOFSTEP]
haveI := hasProduct_fin n
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
n : ℕ
f : Fin (n + 1) → C
this : ∀ (f : Fin n → C), HasProduct f
⊢ HasProduct f
[PROOFSTEP]
apply HasLimit.mk ⟨_, extendFanIsLimit f (limit.isLimit _) (limit.isLimit _)⟩
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
⊢ HasFiniteProducts C
[PROOFSTEP]
refine' ⟨fun n => ⟨fun K => _⟩⟩
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
n : ℕ
K : Discrete (Fin n) ⥤ C
⊢ HasLimit K
[PROOFSTEP]
letI := hasProduct_fin n fun n => K.obj ⟨n⟩
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
n : ℕ
K : Discrete (Fin n) ⥤ C
this : HasProduct fun n_1 => K.obj { as := n_1 } := CategoryTheory.hasProduct_fin n fun n_1 => K.obj { as := n_1 }
⊢ HasLimit K
[PROOFSTEP]
let that : (Discrete.functor fun n => K.obj ⟨n⟩) ≅ K := Discrete.natIso fun ⟨i⟩ => Iso.refl _
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
n : ℕ
K : Discrete (Fin n) ⥤ C
this : HasProduct fun n_1 => K.obj { as := n_1 } := CategoryTheory.hasProduct_fin n fun n_1 => K.obj { as := n_1 }
that : (Discrete.functor fun n_1 => K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 => K.obj { as := n_1 }).obj { as := i })
⊢ HasLimit K
[PROOFSTEP]
apply @hasLimitOfIso _ _ _ _ _ _ this that
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
f : Fin 0 → C
⊢ PreservesLimit (Discrete.functor f) F
[PROOFSTEP]
letI : PreservesLimitsOfShape (Discrete (Fin 0)) F :=
  preservesLimitsOfShapeOfEquiv.{0, 0} (Discrete.equivalence finZeroEquiv'.symm) _
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
f : Fin 0 → C
this : PreservesLimitsOfShape (Discrete (Fin 0)) F :=
  preservesLimitsOfShapeOfEquiv (Discrete.equivalence finZeroEquiv'.symm) F
⊢ PreservesLimit (Discrete.functor f) F
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
⊢ (f : Fin (n + 1) → C) → PreservesLimit (Discrete.functor f) F
[PROOFSTEP]
haveI := preservesFinOfPreservesBinaryAndTerminal n
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
⊢ (f : Fin (n + 1) → C) → PreservesLimit (Discrete.functor f) F
[PROOFSTEP]
intro f
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ PreservesLimit (Discrete.functor f) F
[PROOFSTEP]
refine' preservesLimitOfPreservesLimitCone (extendFanIsLimit f (limit.isLimit _) (limit.isLimit _)) _
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ IsLimit
    (F.mapCone
      (extendFan (limit.cone (Discrete.functor fun i => f (Fin.succ i)))
        (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt))))
[PROOFSTEP]
apply (isLimitMapConeFanMkEquiv _ _ _).symm _
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ IsLimit
    (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt) fun j =>
      F.map
        (Fin.cases (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)))
          (fun i =>
            BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)) ≫
              NatTrans.app (limit.cone (Discrete.functor fun i => f (Fin.succ i))).π { as := i })
          j))
[PROOFSTEP]
let this :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F _)
    (isLimitOfHasBinaryProductOfPreservesLimit F _ _)
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f (Fin.succ i))
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ fun i => f (Fin.succ i)))
⊢ IsLimit
    (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt) fun j =>
      F.map
        (Fin.cases (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)))
          (fun i =>
            BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)) ≫
              NatTrans.app (limit.cone (Discrete.functor fun i => f (Fin.succ i))).π { as := i })
          j))
[PROOFSTEP]
refine' IsLimit.ofIsoLimit this _
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f (Fin.succ i))
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ fun i => f (Fin.succ i)))
⊢ extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
      (BinaryFan.mk (F.map prod.fst) (F.map prod.snd)) ≅
    Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt) fun j =>
      F.map
        (Fin.cases (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)))
          (fun i =>
            BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)) ≫
              NatTrans.app (limit.cone (Discrete.functor fun i => f (Fin.succ i))).π { as := i })
          j)
[PROOFSTEP]
apply Cones.ext _ _
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f (Fin.succ i))
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ fun i => f (Fin.succ i)))
⊢ (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
        (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt ≅
    (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt) fun j =>
        F.map
          (Fin.cases
            (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)))
            (fun i =>
              BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)) ≫
                NatTrans.app (limit.cone (Discrete.functor fun i => f (Fin.succ i))).π { as := i })
            j)).pt
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f (Fin.succ i))
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ fun i => f (Fin.succ i)))
⊢ ∀ (j : Discrete (Fin (n + 1))),
    NatTrans.app
        (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
            (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π
        j =
      ?m.14831.hom ≫
        NatTrans.app
          (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
              fun j =>
              F.map
                (Fin.cases
                  (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                  (fun i =>
                    BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)) ≫
                      NatTrans.app (limit.cone (Discrete.functor fun i => f (Fin.succ i))).π { as := i })
                  j)).π
          j
[PROOFSTEP]
apply Iso.refl _
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f (Fin.succ i))
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ fun i => f (Fin.succ i)))
⊢ ∀ (j : Discrete (Fin (n + 1))),
    NatTrans.app
        (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
            (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π
        j =
      (Iso.refl
            (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
                (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt).hom ≫
        NatTrans.app
          (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
              fun j =>
              F.map
                (Fin.cases
                  (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                  (fun i =>
                    BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)) ≫
                      NatTrans.app (limit.cone (Discrete.functor fun i => f (Fin.succ i))).π { as := i })
                  j)).π
          j
[PROOFSTEP]
rintro ⟨j⟩
[GOAL]
case mk
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f (Fin.succ i))
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ fun i => f (Fin.succ i)))
j : Fin (n + 1)
⊢ NatTrans.app
      (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
          (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π
      { as := j } =
    (Iso.refl
          (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
              (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt).hom ≫
      NatTrans.app
        (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt) fun j =>
            F.map
              (Fin.cases
                (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                (fun i =>
                  BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)) ≫
                    NatTrans.app (limit.cone (Discrete.functor fun i => f (Fin.succ i))).π { as := i })
                j)).π
        { as := j }
[PROOFSTEP]
refine' Fin.inductionOn j ?_ ?_
[GOAL]
case mk.refine'_1
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f (Fin.succ i))
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ fun i => f (Fin.succ i)))
j : Fin (n + 1)
⊢ NatTrans.app
      (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
          (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π
      { as := 0 } =
    (Iso.refl
          (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
              (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt).hom ≫
      NatTrans.app
        (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt) fun j =>
            F.map
              (Fin.cases
                (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                (fun i =>
                  BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)) ≫
                    NatTrans.app (limit.cone (Discrete.functor fun i => f (Fin.succ i))).π { as := i })
                j)).π
        { as := 0 }
[PROOFSTEP]
apply (Category.id_comp _).symm
[GOAL]
case mk.refine'_2
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f (Fin.succ i))
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ fun i => f (Fin.succ i)))
j : Fin (n + 1)
⊢ ∀ (i : Fin n),
    NatTrans.app
          (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
              (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π
          { as := Fin.castSucc i } =
        (Iso.refl
              (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
                  (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt).hom ≫
          NatTrans.app
            (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
                fun j =>
                F.map
                  (Fin.cases
                    (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                    (fun i =>
                      BinaryFan.snd
                          (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)) ≫
                        NatTrans.app (limit.cone (Discrete.functor fun i => f (Fin.succ i))).π { as := i })
                    j)).π
            { as := Fin.castSucc i } →
      NatTrans.app
          (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
              (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π
          { as := Fin.succ i } =
        (Iso.refl
              (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
                  (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt).hom ≫
          NatTrans.app
            (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
                fun j =>
                F.map
                  (Fin.cases
                    (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                    (fun i =>
                      BinaryFan.snd
                          (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)) ≫
                        NatTrans.app (limit.cone (Discrete.functor fun i => f (Fin.succ i))).π { as := i })
                    j)).π
            { as := Fin.succ i }
[PROOFSTEP]
rintro i _
[GOAL]
case mk.refine'_2
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f (Fin.succ i))
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ fun i => f (Fin.succ i)))
j : Fin (n + 1)
i : Fin n
a✝ :
  NatTrans.app
      (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
          (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π
      { as := Fin.castSucc i } =
    (Iso.refl
          (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
              (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt).hom ≫
      NatTrans.app
        (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt) fun j =>
            F.map
              (Fin.cases
                (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                (fun i =>
                  BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)) ≫
                    NatTrans.app (limit.cone (Discrete.functor fun i => f (Fin.succ i))).π { as := i })
                j)).π
        { as := Fin.castSucc i }
⊢ NatTrans.app
      (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
          (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π
      { as := Fin.succ i } =
    (Iso.refl
          (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
              (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt).hom ≫
      NatTrans.app
        (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt) fun j =>
            F.map
              (Fin.cases
                (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                (fun i =>
                  BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)) ≫
                    NatTrans.app (limit.cone (Discrete.functor fun i => f (Fin.succ i))).π { as := i })
                j)).π
        { as := Fin.succ i }
[PROOFSTEP]
dsimp [extendFan_π_app, Iso.refl_hom, Fan.mk_π_app]
[GOAL]
case mk.refine'_2
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f (Fin.succ i))
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ fun i => f (Fin.succ i)))
j : Fin (n + 1)
i : Fin n
a✝ :
  NatTrans.app
      (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
          (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π
      { as := Fin.castSucc i } =
    (Iso.refl
          (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
              (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt).hom ≫
      NatTrans.app
        (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt) fun j =>
            F.map
              (Fin.cases
                (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                (fun i =>
                  BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)) ≫
                    NatTrans.app (limit.cone (Discrete.functor fun i => f (Fin.succ i))).π { as := i })
                j)).π
        { as := Fin.castSucc i }
⊢ F.map prod.snd ≫ F.map (Pi.π (fun i => f (Fin.succ i)) i) =
    𝟙 (F.obj (f 0 ⨯ ∏ fun i => f (Fin.succ i))) ≫
      F.map
        (BinaryFan.snd (limit.cone (pair (f 0) (limit (Discrete.functor fun i => f (Fin.succ i))))) ≫
          limit.π (Discrete.functor fun i => f (Fin.succ i)) { as := i })
[PROOFSTEP]
change F.map _ ≫ _ = 𝟙 _ ≫ _
[GOAL]
case mk.refine'_2
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f (Fin.succ i))
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ fun i => f (Fin.succ i)))
j : Fin (n + 1)
i : Fin n
a✝ :
  NatTrans.app
      (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
          (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π
      { as := Fin.castSucc i } =
    (Iso.refl
          (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
              (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt).hom ≫
      NatTrans.app
        (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt) fun j =>
            F.map
              (Fin.cases
                (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                (fun i =>
                  BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)) ≫
                    NatTrans.app (limit.cone (Discrete.functor fun i => f (Fin.succ i))).π { as := i })
                j)).π
        { as := Fin.castSucc i }
⊢ F.map prod.snd ≫ F.map (Pi.π (fun i => f (Fin.succ i)) i) =
    𝟙 (F.obj (f 0 ⨯ ∏ fun i => f (Fin.succ i))) ≫
      F.map
        (BinaryFan.snd (limit.cone (pair (f 0) (limit (Discrete.functor fun i => f (Fin.succ i))))) ≫
          limit.π (Discrete.functor fun i => f (Fin.succ i)) { as := i })
[PROOFSTEP]
simp only [id_comp, ← F.map_comp]
[GOAL]
case mk.refine'_2
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f (Fin.succ i))
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ fun i => f (Fin.succ i)))
j : Fin (n + 1)
i : Fin n
a✝ :
  NatTrans.app
      (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
          (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π
      { as := Fin.castSucc i } =
    (Iso.refl
          (extendFan (Fan.mk (F.obj (∏ fun i => f (Fin.succ i))) fun j => F.map (Pi.π (fun i => f (Fin.succ i)) j))
              (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt).hom ≫
      NatTrans.app
        (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt) fun j =>
            F.map
              (Fin.cases
                (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                (fun i =>
                  BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f (Fin.succ i))).pt)) ≫
                    NatTrans.app (limit.cone (Discrete.functor fun i => f (Fin.succ i))).π { as := i })
                j)).π
        { as := Fin.castSucc i }
⊢ F.map (prod.snd ≫ Pi.π (fun i => f (Fin.succ i)) i) =
    F.map
      (BinaryFan.snd (limit.cone (pair (f 0) (limit (Discrete.functor fun i => f (Fin.succ i))))) ≫
        limit.π (Discrete.functor fun i => f (Fin.succ i)) { as := i })
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
⊢ PreservesLimit K F
[PROOFSTEP]
let that : (Discrete.functor fun n => K.obj ⟨n⟩) ≅ K := Discrete.natIso fun ⟨i⟩ => Iso.refl _
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : (Discrete.functor fun n_1 => K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 => K.obj { as := n_1 }).obj { as := i })
⊢ PreservesLimit K F
[PROOFSTEP]
haveI := preservesFinOfPreservesBinaryAndTerminal F n fun n => K.obj ⟨n⟩
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteProducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : (Discrete.functor fun n_1 => K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 => K.obj { as := n_1 }).obj { as := i })
this : PreservesLimit (Discrete.functor fun n_1 => K.obj { as := n_1 }) F
⊢ PreservesLimit K F
[PROOFSTEP]
apply preservesLimitOfIsoDiagram F that
[GOAL]
J✝ : Type v
inst✝⁶ : SmallCategory J✝
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝² : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝¹ : HasFiniteProducts C
J : Type
inst✝ : Fintype J
⊢ PreservesLimitsOfShape (Discrete J) F
[PROOFSTEP]
classical
let e := Fintype.equivFin J
haveI := preservesShapeFinOfPreservesBinaryAndTerminal F (Fintype.card J)
apply preservesLimitsOfShapeOfEquiv.{0, 0} (Discrete.equivalence e).symm
[GOAL]
J✝ : Type v
inst✝⁶ : SmallCategory J✝
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝² : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝¹ : HasFiniteProducts C
J : Type
inst✝ : Fintype J
⊢ PreservesLimitsOfShape (Discrete J) F
[PROOFSTEP]
let e := Fintype.equivFin J
[GOAL]
J✝ : Type v
inst✝⁶ : SmallCategory J✝
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝² : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝¹ : HasFiniteProducts C
J : Type
inst✝ : Fintype J
e : J ≃ Fin (Fintype.card J) := Fintype.equivFin J
⊢ PreservesLimitsOfShape (Discrete J) F
[PROOFSTEP]
haveI := preservesShapeFinOfPreservesBinaryAndTerminal F (Fintype.card J)
[GOAL]
J✝ : Type v
inst✝⁶ : SmallCategory J✝
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝² : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝¹ : HasFiniteProducts C
J : Type
inst✝ : Fintype J
e : J ≃ Fin (Fintype.card J) := Fintype.equivFin J
this : PreservesLimitsOfShape (Discrete (Fin (Fintype.card J))) F
⊢ PreservesLimitsOfShape (Discrete J) F
[PROOFSTEP]
apply preservesLimitsOfShapeOfEquiv.{0, 0} (Discrete.equivalence e).symm
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
⊢ (b : Fin (n + 1)) → f b ⟶ c₂.pt
[PROOFSTEP]
refine' Fin.cases _ _
[GOAL]
case refine'_1
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
⊢ f 0 ⟶ c₂.pt
[PROOFSTEP]
apply c₂.inl
[GOAL]
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
⊢ (i : Fin n) → f (Fin.succ i) ⟶ c₂.pt
[PROOFSTEP]
intro i
[GOAL]
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
i : Fin n
⊢ f (Fin.succ i) ⟶ c₂.pt
[PROOFSTEP]
apply c₁.ι.app ⟨i⟩ ≫ c₂.inr
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
⊢ (extendCofan c₁ c₂).pt ⟶ s.pt
[PROOFSTEP]
apply (BinaryCofan.IsColimit.desc' t₂ (s.ι.app ⟨0⟩) _).1
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
⊢ c₁.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 }
[PROOFSTEP]
apply t₁.desc ⟨_, Discrete.natTrans fun i => s.ι.app ⟨i.as.succ⟩⟩
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
⊢ ∀ (j : Discrete (Fin (n + 1))),
    NatTrans.app (extendCofan c₁ c₂).ι j ≫
        (fun s =>
            ↑(BinaryCofan.IsColimit.desc' t₂ (NatTrans.app s.ι { as := 0 })
                (IsColimit.desc t₁
                  { pt := s.pt, ι := Discrete.natTrans fun i => NatTrans.app s.ι { as := Fin.succ i.as } })))
          s =
      NatTrans.app s.ι j
[PROOFSTEP]
rintro ⟨j⟩
[GOAL]
case mk
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
j : Fin (n + 1)
⊢ NatTrans.app (extendCofan c₁ c₂).ι { as := j } ≫
      (fun s =>
          ↑(BinaryCofan.IsColimit.desc' t₂ (NatTrans.app s.ι { as := 0 })
              (IsColimit.desc t₁
                { pt := s.pt, ι := Discrete.natTrans fun i => NatTrans.app s.ι { as := Fin.succ i.as } })))
        s =
    NatTrans.app s.ι { as := j }
[PROOFSTEP]
refine' Fin.inductionOn j ?_ ?_
[GOAL]
case mk.refine'_1
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
j : Fin (n + 1)
⊢ NatTrans.app (extendCofan c₁ c₂).ι { as := 0 } ≫
      (fun s =>
          ↑(BinaryCofan.IsColimit.desc' t₂ (NatTrans.app s.ι { as := 0 })
              (IsColimit.desc t₁
                { pt := s.pt, ι := Discrete.natTrans fun i => NatTrans.app s.ι { as := Fin.succ i.as } })))
        s =
    NatTrans.app s.ι { as := 0 }
[PROOFSTEP]
apply (BinaryCofan.IsColimit.desc' t₂ _ _).2.1
[GOAL]
case mk.refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
j : Fin (n + 1)
⊢ ∀ (i : Fin n),
    NatTrans.app (extendCofan c₁ c₂).ι { as := Fin.castSucc i } ≫
          (fun s =>
              ↑(BinaryCofan.IsColimit.desc' t₂ (NatTrans.app s.ι { as := 0 })
                  (IsColimit.desc t₁
                    { pt := s.pt, ι := Discrete.natTrans fun i => NatTrans.app s.ι { as := Fin.succ i.as } })))
            s =
        NatTrans.app s.ι { as := Fin.castSucc i } →
      NatTrans.app (extendCofan c₁ c₂).ι { as := Fin.succ i } ≫
          (fun s =>
              ↑(BinaryCofan.IsColimit.desc' t₂ (NatTrans.app s.ι { as := 0 })
                  (IsColimit.desc t₁
                    { pt := s.pt, ι := Discrete.natTrans fun i => NatTrans.app s.ι { as := Fin.succ i.as } })))
            s =
        NatTrans.app s.ι { as := Fin.succ i }
[PROOFSTEP]
rintro i -
[GOAL]
case mk.refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
j : Fin (n + 1)
i : Fin n
⊢ NatTrans.app (extendCofan c₁ c₂).ι { as := Fin.succ i } ≫
      (fun s =>
          ↑(BinaryCofan.IsColimit.desc' t₂ (NatTrans.app s.ι { as := 0 })
              (IsColimit.desc t₁
                { pt := s.pt, ι := Discrete.natTrans fun i => NatTrans.app s.ι { as := Fin.succ i.as } })))
        s =
    NatTrans.app s.ι { as := Fin.succ i }
[PROOFSTEP]
dsimp only [extendCofan_ι_app]
[GOAL]
case mk.refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
j : Fin (n + 1)
i : Fin n
⊢ Fin.cases (BinaryCofan.inl c₂) (fun i => NatTrans.app c₁.ι { as := i } ≫ BinaryCofan.inr c₂) (Fin.succ i) ≫
      ↑(BinaryCofan.IsColimit.desc' t₂ (NatTrans.app s.ι { as := 0 })
          (IsColimit.desc t₁
            { pt := s.pt, ι := Discrete.natTrans fun i => NatTrans.app s.ι { as := Fin.succ i.as } })) =
    NatTrans.app s.ι { as := Fin.succ i }
[PROOFSTEP]
rw [Fin.cases_succ, assoc, (BinaryCofan.IsColimit.desc' t₂ _ _).2.2, t₁.fac]
[GOAL]
case mk.refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
j : Fin (n + 1)
i : Fin n
⊢ NatTrans.app { pt := s.pt, ι := Discrete.natTrans fun i => NatTrans.app s.ι { as := Fin.succ i.as } }.ι { as := i } =
    NatTrans.app s.ι { as := Fin.succ i }
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), NatTrans.app (extendCofan c₁ c₂).ι j ≫ m = NatTrans.app s.ι j
⊢ m =
    (fun s =>
        ↑(BinaryCofan.IsColimit.desc' t₂ (NatTrans.app s.ι { as := 0 })
            (IsColimit.desc t₁
              { pt := s.pt, ι := Discrete.natTrans fun i => NatTrans.app s.ι { as := Fin.succ i.as } })))
      s
[PROOFSTEP]
apply BinaryCofan.IsColimit.hom_ext t₂
[GOAL]
case h₁
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), NatTrans.app (extendCofan c₁ c₂).ι j ≫ m = NatTrans.app s.ι j
⊢ BinaryCofan.inl c₂ ≫ m =
    BinaryCofan.inl c₂ ≫
      (fun s =>
          ↑(BinaryCofan.IsColimit.desc' t₂ (NatTrans.app s.ι { as := 0 })
              (IsColimit.desc t₁
                { pt := s.pt, ι := Discrete.natTrans fun i => NatTrans.app s.ι { as := Fin.succ i.as } })))
        s
[PROOFSTEP]
rw [(BinaryCofan.IsColimit.desc' t₂ _ _).2.1]
[GOAL]
case h₁
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), NatTrans.app (extendCofan c₁ c₂).ι j ≫ m = NatTrans.app s.ι j
⊢ BinaryCofan.inl c₂ ≫ m = NatTrans.app s.ι { as := 0 }
[PROOFSTEP]
apply w ⟨0⟩
[GOAL]
case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), NatTrans.app (extendCofan c₁ c₂).ι j ≫ m = NatTrans.app s.ι j
⊢ BinaryCofan.inr c₂ ≫ m =
    BinaryCofan.inr c₂ ≫
      (fun s =>
          ↑(BinaryCofan.IsColimit.desc' t₂ (NatTrans.app s.ι { as := 0 })
              (IsColimit.desc t₁
                { pt := s.pt, ι := Discrete.natTrans fun i => NatTrans.app s.ι { as := Fin.succ i.as } })))
        s
[PROOFSTEP]
rw [(BinaryCofan.IsColimit.desc' t₂ _ _).2.2]
[GOAL]
case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), NatTrans.app (extendCofan c₁ c₂).ι j ≫ m = NatTrans.app s.ι j
⊢ BinaryCofan.inr c₂ ≫ m =
    IsColimit.desc t₁ { pt := s.pt, ι := Discrete.natTrans fun i => NatTrans.app s.ι { as := Fin.succ i.as } }
[PROOFSTEP]
apply t₁.uniq ⟨_, _⟩
[GOAL]
case h₂.x
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), NatTrans.app (extendCofan c₁ c₂).ι j ≫ m = NatTrans.app s.ι j
⊢ ∀ (j : Discrete (Fin n)),
    NatTrans.app c₁.ι j ≫ BinaryCofan.inr c₂ ≫ m =
      NatTrans.app { pt := s.1, ι := Discrete.natTrans fun i => NatTrans.app s.ι { as := Fin.succ i.as } }.ι j
[PROOFSTEP]
rintro ⟨j⟩
[GOAL]
case h₂.x.mk
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), NatTrans.app (extendCofan c₁ c₂).ι j ≫ m = NatTrans.app s.ι j
j : Fin n
⊢ NatTrans.app c₁.ι { as := j } ≫ BinaryCofan.inr c₂ ≫ m =
    NatTrans.app { pt := s.1, ι := Discrete.natTrans fun i => NatTrans.app s.ι { as := Fin.succ i.as } }.ι { as := j }
[PROOFSTEP]
dsimp only [Discrete.natTrans_app]
[GOAL]
case h₂.x.mk
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), NatTrans.app (extendCofan c₁ c₂).ι j ≫ m = NatTrans.app s.ι j
j : Fin n
⊢ NatTrans.app c₁.ι { as := j } ≫ BinaryCofan.inr c₂ ≫ m = NatTrans.app s.ι { as := Fin.succ j }
[PROOFSTEP]
rw [← w ⟨j.succ⟩]
[GOAL]
case h₂.x.mk
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), NatTrans.app (extendCofan c₁ c₂).ι j ≫ m = NatTrans.app s.ι j
j : Fin n
⊢ NatTrans.app c₁.ι { as := j } ≫ BinaryCofan.inr c₂ ≫ m = NatTrans.app (extendCofan c₁ c₂).ι { as := Fin.succ j } ≫ m
[PROOFSTEP]
dsimp only [extendCofan_ι_app]
[GOAL]
case h₂.x.mk
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f (Fin.succ i)
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), NatTrans.app (extendCofan c₁ c₂).ι j ≫ m = NatTrans.app s.ι j
j : Fin n
⊢ NatTrans.app c₁.ι { as := j } ≫ BinaryCofan.inr c₂ ≫ m =
    Fin.cases (BinaryCofan.inl c₂) (fun i => NatTrans.app c₁.ι { as := i } ≫ BinaryCofan.inr c₂) (Fin.succ j) ≫ m
[PROOFSTEP]
rw [Fin.cases_succ, assoc]
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
f : Fin 0 → C
⊢ HasCoproduct f
[PROOFSTEP]
letI : HasColimitsOfShape (Discrete (Fin 0)) C :=
  hasColimitsOfShape_of_equivalence (Discrete.equivalence.{0} finZeroEquiv'.symm)
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
f : Fin 0 → C
this : HasColimitsOfShape (Discrete (Fin 0)) C :=
  hasColimitsOfShape_of_equivalence (Discrete.equivalence finZeroEquiv'.symm)
⊢ HasCoproduct f
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
n : ℕ
f : Fin (n + 1) → C
⊢ HasCoproduct f
[PROOFSTEP]
haveI := hasCoproduct_fin n
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
n : ℕ
f : Fin (n + 1) → C
this : ∀ (f : Fin n → C), HasCoproduct f
⊢ HasCoproduct f
[PROOFSTEP]
apply HasColimit.mk ⟨_, extendCofanIsColimit f (colimit.isColimit _) (colimit.isColimit _)⟩
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
⊢ HasFiniteCoproducts C
[PROOFSTEP]
refine' ⟨fun n => ⟨fun K => _⟩⟩
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
n : ℕ
K : Discrete (Fin n) ⥤ C
⊢ HasColimit K
[PROOFSTEP]
letI := hasCoproduct_fin n fun n => K.obj ⟨n⟩
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
n : ℕ
K : Discrete (Fin n) ⥤ C
this : HasCoproduct fun n_1 => K.obj { as := n_1 } := CategoryTheory.hasCoproduct_fin n fun n_1 => K.obj { as := n_1 }
⊢ HasColimit K
[PROOFSTEP]
let that : K ≅ Discrete.functor fun n => K.obj ⟨n⟩ := Discrete.natIso fun ⟨i⟩ => Iso.refl _
[GOAL]
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
n : ℕ
K : Discrete (Fin n) ⥤ C
this : HasCoproduct fun n_1 => K.obj { as := n_1 } := CategoryTheory.hasCoproduct_fin n fun n_1 => K.obj { as := n_1 }
that : K ≅ Discrete.functor fun n_1 => K.obj { as := n_1 } :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl (K.obj { as := i })
⊢ HasColimit K
[PROOFSTEP]
apply @hasColimitOfIso _ _ _ _ _ _ this that
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
f : Fin 0 → C
⊢ PreservesColimit (Discrete.functor f) F
[PROOFSTEP]
letI : PreservesColimitsOfShape (Discrete (Fin 0)) F :=
  preservesColimitsOfShapeOfEquiv.{0, 0} (Discrete.equivalence finZeroEquiv'.symm) _
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
f : Fin 0 → C
this : PreservesColimitsOfShape (Discrete (Fin 0)) F :=
  preservesColimitsOfShapeOfEquiv (Discrete.equivalence finZeroEquiv'.symm) F
⊢ PreservesColimit (Discrete.functor f) F
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
⊢ (f : Fin (n + 1) → C) → PreservesColimit (Discrete.functor f) F
[PROOFSTEP]
haveI := preservesFinOfPreservesBinaryAndInitial n
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this : (f : Fin n → C) → PreservesColimit (Discrete.functor f) F
⊢ (f : Fin (n + 1) → C) → PreservesColimit (Discrete.functor f) F
[PROOFSTEP]
intro f
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this : (f : Fin n → C) → PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ PreservesColimit (Discrete.functor f) F
[PROOFSTEP]
refine' preservesColimitOfPreservesColimitCocone (extendCofanIsColimit f (colimit.isColimit _) (colimit.isColimit _)) _
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this : (f : Fin n → C) → PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ IsColimit
    (F.mapCocone
      (extendCofan (colimit.cocone (Discrete.functor fun i => f (Fin.succ i)))
        (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt))))
[PROOFSTEP]
apply (isColimitMapCoconeCofanMkEquiv _ _ _).symm _
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this : (f : Fin n → C) → PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ IsColimit
    (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
      fun j =>
      F.map
        (Fin.cases
          (BinaryCofan.inl (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
          (fun i =>
            NatTrans.app (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).ι { as := i } ≫
              BinaryCofan.inr
                (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
          j))
[PROOFSTEP]
let this :=
  extendCofanIsColimit (fun i => F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F _)
    (isColimitOfHasBinaryCoproductOfPreservesColimit F _ _)
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i => F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i => f (Fin.succ i))
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i => f (Fin.succ i)))
⊢ IsColimit
    (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
      fun j =>
      F.map
        (Fin.cases
          (BinaryCofan.inl (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
          (fun i =>
            NatTrans.app (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).ι { as := i } ≫
              BinaryCofan.inr
                (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
          j))
[PROOFSTEP]
refine' IsColimit.ofIsoColimit this _
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i => F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i => f (Fin.succ i))
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i => f (Fin.succ i)))
⊢ extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
      (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr)) ≅
    Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
      fun j =>
      F.map
        (Fin.cases
          (BinaryCofan.inl (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
          (fun i =>
            NatTrans.app (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).ι { as := i } ≫
              BinaryCofan.inr
                (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
          j)
[PROOFSTEP]
apply Cocones.ext _ _
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i => F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i => f (Fin.succ i))
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i => f (Fin.succ i)))
⊢ (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
        (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).pt ≅
    (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
        fun j =>
        F.map
          (Fin.cases
            (BinaryCofan.inl
              (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
            (fun i =>
              NatTrans.app (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).ι { as := i } ≫
                BinaryCofan.inr
                  (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
            j)).pt
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i => F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i => f (Fin.succ i))
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i => f (Fin.succ i)))
⊢ ∀ (j : Discrete (Fin (n + 1))),
    NatTrans.app
          (extendCofan
              (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
              (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).ι
          j ≫
        ?m.38703.hom =
      NatTrans.app
        (Cofan.mk
            (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
            fun j =>
            F.map
              (Fin.cases
                (BinaryCofan.inl
                  (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                (fun i =>
                  NatTrans.app (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).ι { as := i } ≫
                    BinaryCofan.inr
                      (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                j)).ι
        j
[PROOFSTEP]
apply Iso.refl _
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i => F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i => f (Fin.succ i))
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i => f (Fin.succ i)))
⊢ ∀ (j : Discrete (Fin (n + 1))),
    NatTrans.app
          (extendCofan
              (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
              (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).ι
          j ≫
        (Iso.refl
            (extendCofan
                (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
                (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).pt).hom =
      NatTrans.app
        (Cofan.mk
            (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
            fun j =>
            F.map
              (Fin.cases
                (BinaryCofan.inl
                  (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                (fun i =>
                  NatTrans.app (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).ι { as := i } ≫
                    BinaryCofan.inr
                      (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                j)).ι
        j
[PROOFSTEP]
rintro ⟨j⟩
[GOAL]
case mk
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i => F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i => f (Fin.succ i))
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i => f (Fin.succ i)))
j : Fin (n + 1)
⊢ NatTrans.app
        (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
            (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).ι
        { as := j } ≫
      (Iso.refl
          (extendCofan
              (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
              (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).pt).hom =
    NatTrans.app
      (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
          fun j =>
          F.map
            (Fin.cases
              (BinaryCofan.inl
                (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
              (fun i =>
                NatTrans.app (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).ι { as := i } ≫
                  BinaryCofan.inr
                    (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
              j)).ι
      { as := j }
[PROOFSTEP]
refine' Fin.inductionOn j ?_ ?_
[GOAL]
case mk.refine'_1
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i => F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i => f (Fin.succ i))
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i => f (Fin.succ i)))
j : Fin (n + 1)
⊢ NatTrans.app
        (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
            (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).ι
        { as := 0 } ≫
      (Iso.refl
          (extendCofan
              (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
              (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).pt).hom =
    NatTrans.app
      (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
          fun j =>
          F.map
            (Fin.cases
              (BinaryCofan.inl
                (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
              (fun i =>
                NatTrans.app (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).ι { as := i } ≫
                  BinaryCofan.inr
                    (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
              j)).ι
      { as := 0 }
[PROOFSTEP]
apply Category.comp_id
[GOAL]
case mk.refine'_2
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i => F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i => f (Fin.succ i))
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i => f (Fin.succ i)))
j : Fin (n + 1)
⊢ ∀ (i : Fin n),
    NatTrans.app
            (extendCofan
                (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
                (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).ι
            { as := Fin.castSucc i } ≫
          (Iso.refl
              (extendCofan
                  (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
                  (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).pt).hom =
        NatTrans.app
          (Cofan.mk
              (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
              fun j =>
              F.map
                (Fin.cases
                  (BinaryCofan.inl
                    (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                  (fun i =>
                    NatTrans.app (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).ι { as := i } ≫
                      BinaryCofan.inr
                        (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                  j)).ι
          { as := Fin.castSucc i } →
      NatTrans.app
            (extendCofan
                (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
                (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).ι
            { as := Fin.succ i } ≫
          (Iso.refl
              (extendCofan
                  (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
                  (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).pt).hom =
        NatTrans.app
          (Cofan.mk
              (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
              fun j =>
              F.map
                (Fin.cases
                  (BinaryCofan.inl
                    (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                  (fun i =>
                    NatTrans.app (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).ι { as := i } ≫
                      BinaryCofan.inr
                        (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
                  j)).ι
          { as := Fin.succ i }
[PROOFSTEP]
rintro i _
[GOAL]
case mk.refine'_2
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i => F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i => f (Fin.succ i))
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i => f (Fin.succ i)))
j : Fin (n + 1)
i : Fin n
a✝ :
  NatTrans.app
        (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
            (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).ι
        { as := Fin.castSucc i } ≫
      (Iso.refl
          (extendCofan
              (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
              (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).pt).hom =
    NatTrans.app
      (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
          fun j =>
          F.map
            (Fin.cases
              (BinaryCofan.inl
                (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
              (fun i =>
                NatTrans.app (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).ι { as := i } ≫
                  BinaryCofan.inr
                    (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
              j)).ι
      { as := Fin.castSucc i }
⊢ NatTrans.app
        (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
            (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).ι
        { as := Fin.succ i } ≫
      (Iso.refl
          (extendCofan
              (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
              (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).pt).hom =
    NatTrans.app
      (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
          fun j =>
          F.map
            (Fin.cases
              (BinaryCofan.inl
                (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
              (fun i =>
                NatTrans.app (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).ι { as := i } ≫
                  BinaryCofan.inr
                    (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
              j)).ι
      { as := Fin.succ i }
[PROOFSTEP]
dsimp [extendCofan_ι_app, Iso.refl_hom, Cofan.mk_ι_app]
[GOAL]
case mk.refine'_2
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this✝ : (f : Fin n → C) → PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i => F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i => f (Fin.succ i))
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i => f (Fin.succ i)))
j : Fin (n + 1)
i : Fin n
a✝ :
  NatTrans.app
        (extendCofan (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
            (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).ι
        { as := Fin.castSucc i } ≫
      (Iso.refl
          (extendCofan
              (Cofan.mk (F.obj (∐ fun i => f (Fin.succ i))) fun j => F.map (Sigma.ι (fun i => f (Fin.succ i)) j))
              (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).pt).hom =
    NatTrans.app
      (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)).pt)
          fun j =>
          F.map
            (Fin.cases
              (BinaryCofan.inl
                (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
              (fun i =>
                NatTrans.app (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).ι { as := i } ≫
                  BinaryCofan.inr
                    (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i => f (Fin.succ i))).pt)))
              j)).ι
      { as := Fin.castSucc i }
⊢ (F.map (Sigma.ι (fun i => f (Fin.succ i)) i) ≫ F.map coprod.inr) ≫ 𝟙 (F.obj (f 0 ⨿ ∐ fun i => f (Fin.succ i))) =
    F.map
      (colimit.ι (Discrete.functor fun i => f (Fin.succ i)) { as := i } ≫
        colimit.ι (pair (f 0) (colimit (Discrete.functor fun i => f (Fin.succ i)))) { as := WalkingPair.right })
[PROOFSTEP]
rw [comp_id, ← F.map_comp]
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
⊢ PreservesColimit K F
[PROOFSTEP]
let that : (Discrete.functor fun n => K.obj ⟨n⟩) ≅ K := Discrete.natIso fun ⟨i⟩ => Iso.refl _
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : (Discrete.functor fun n_1 => K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 => K.obj { as := n_1 }).obj { as := i })
⊢ PreservesColimit K F
[PROOFSTEP]
haveI := preservesFinOfPreservesBinaryAndInitial F n fun n => K.obj ⟨n⟩
[GOAL]
J : Type v
inst✝⁵ : SmallCategory J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : HasFiniteCoproducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : (Discrete.functor fun n_1 => K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 => K.obj { as := n_1 }).obj { as := i })
this : PreservesColimit (Discrete.functor fun n_1 => K.obj { as := n_1 }) F
⊢ PreservesColimit K F
[PROOFSTEP]
apply preservesColimitOfIsoDiagram F that
[GOAL]
J✝ : Type v
inst✝⁶ : SmallCategory J✝
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝² : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝¹ : HasFiniteCoproducts C
J : Type
inst✝ : Fintype J
⊢ PreservesColimitsOfShape (Discrete J) F
[PROOFSTEP]
classical
let e := Fintype.equivFin J
haveI := preservesShapeFinOfPreservesBinaryAndInitial F (Fintype.card J)
apply preservesColimitsOfShapeOfEquiv.{0, 0} (Discrete.equivalence e).symm
[GOAL]
J✝ : Type v
inst✝⁶ : SmallCategory J✝
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝² : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝¹ : HasFiniteCoproducts C
J : Type
inst✝ : Fintype J
⊢ PreservesColimitsOfShape (Discrete J) F
[PROOFSTEP]
let e := Fintype.equivFin J
[GOAL]
J✝ : Type v
inst✝⁶ : SmallCategory J✝
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝² : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝¹ : HasFiniteCoproducts C
J : Type
inst✝ : Fintype J
e : J ≃ Fin (Fintype.card J) := Fintype.equivFin J
⊢ PreservesColimitsOfShape (Discrete J) F
[PROOFSTEP]
haveI := preservesShapeFinOfPreservesBinaryAndInitial F (Fintype.card J)
[GOAL]
J✝ : Type v
inst✝⁶ : SmallCategory J✝
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝² : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝¹ : HasFiniteCoproducts C
J : Type
inst✝ : Fintype J
e : J ≃ Fin (Fintype.card J) := Fintype.equivFin J
this : PreservesColimitsOfShape (Discrete (Fin (Fintype.card J))) F
⊢ PreservesColimitsOfShape (Discrete J) F
[PROOFSTEP]
apply preservesColimitsOfShapeOfEquiv.{0, 0} (Discrete.equivalence e).symm
