awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
B : Bicone.{w, uC', uC} F
j : Discrete J
⊢ B.toCocone.ι.app j = B.ι j.as

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
B : Bicone.{w, uC', uC} F
j : J
⊢ Cofan.inj B.toCocone j = B.ι j

Tactic:
rfl

Premises used: CategoryTheory.Limits.Cofan.inj, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
B : Bicone.{w, uC', uC} F
j : J
⊢ B.toCocone.ι.app { as := j } = B.ι j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
B : Bicone.{w, uC', uC} F
j : J
⊢ IsSplitMono (B.ι j)

Tactic:
(B.retract j).instIsSplitMonoI

Premises used: CategoryTheory.Retract.instIsSplitMonoI, CategoryTheory.Limits.Bicone.retract
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
B : Bicone.{w, uC', uC} F
j : J
⊢ IsSplitEpi (B.π j)

Tactic:
(B.retract j).instIsSplitEpiR

Premises used: CategoryTheory.Retract.instIsSplitEpiR, CategoryTheory.Limits.Bicone.retract
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F f : J → C
t : Cone.{w, uC', w, uC} (Discrete.functor f)
ht : IsLimit t
j j' : J
⊢ Eq (α := f j ⟶ f j')
    (ht.lift (Fan.mk (f j) fun (j' : J) ↦ if h : j = j' then eqToHom ⋯ else 0) ≫ t.π.app { as := j' : Discrete J } :
      f j ⟶ f j')
    (if h : j = j' then eqToHom ⋯ else 0 : f j ⟶ f j')

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
f : J → C
t : Bicone.{w, uC', uC} f
ht : IsLimit t.toCone
j : J
j' : Discrete J
rw :
  t.ι j ≫ t.toCone.π.app j' = NatTrans.app (Cone.π (Fan.mk (f j) fun (j' : J) ↦ if h : j = j' then eqToHom ⋯ else 0)) j'
⊢ t.ι j ≫ t.toCone.π.app j' =
    ht.lift (Fan.mk (f j) fun (j' : J) ↦ if h : j = j' then eqToHom ⋯ else 0) ≫ t.toCone.π.app j'

Tactic:
rw [ht.fac]

Premises used: CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
f : J → C
t : Bicone.{w, uC', uC} f
ht : IsLimit t.toCone
j : J
j' : Discrete J
⊢ t.ι j ≫ t.toCone.π.app j' = NatTrans.app (Cone.π (Fan.mk (f j) fun (j' : J) ↦ if h : j = j' then eqToHom ⋯ else 0)) j'

Tactic:
simp [t.ι_π]

Premises used: CategoryTheory.Limits.Bicone.ι_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F f : J → C
t : Cocone.{w, uC', w, uC} (Discrete.functor f)
ht : IsColimit t
j j' : J
⊢ Eq (α := f j ⟶ f j')
    (t.ι.app { as := j : Discrete J } ≫
        ht.desc (Cofan.mk (f j') fun (j'_1 : J) ↦ if h : j'_1 = j' then eqToHom ⋯ else 0) :
      f j ⟶ f j')
    (if h : j = j' then eqToHom ⋯ else 0 : f j ⟶ f j')

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
f : J → C
t : Bicone.{w, uC', uC} f
ht : IsColimit t.toCocone
j : J
j' : Discrete J
rw :
  t.toCocone.ι.app j' ≫ t.π j =
    NatTrans.app (Cocone.ι (Cofan.mk (f j) fun (j' : J) ↦ if h : j' = j then eqToHom ⋯ else 0)) j'
⊢ t.toCocone.ι.app j' ≫ t.π j =
    t.toCocone.ι.app j' ≫ ht.desc (Cofan.mk (f j) fun (j' : J) ↦ if h : j' = j then eqToHom ⋯ else 0)

Tactic:
rw [ht.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
f : J → C
t : Bicone.{w, uC', uC} f
ht : IsColimit t.toCocone
j : J
j' : Discrete J
⊢ t.toCocone.ι.app j' ≫ t.π j =
    NatTrans.app (Cocone.ι (Cofan.mk (f j) fun (j' : J) ↦ if h : j' = j then eqToHom ⋯ else 0)) j'

Tactic:
simp [t.ι_π]

Premises used: CategoryTheory.Limits.Bicone.ι_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F f : J → C
c : Bicone.{w, uC', uC} f
⊢ Subsingleton c.IsBilimit

Tactic:
⟨fun _ _ => Bicone.IsBilimit.ext (Subsingleton.elim _ _) (Subsingleton.elim _ _)⟩

Premises used: CategoryTheory.Limits.Bicone.IsBilimit.isColimit, CategoryTheory.Limits.Bicone.IsBilimit.ext, Subsingleton.intro, CategoryTheory.Limits.Bicone.IsBilimit.isLimit, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
simp :
  Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k')
    (if h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J) then eqToHom ⋯ else 0)
    (if h : k = k' then eqToHom ⋯ else 0)
⊢ Eq (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k')
    (c.ι ((g : (a : K) → J) k) ≫ c.π ((g : (a : K) → J) k')) (if h : k = k' then eqToHom ⋯ else 0)

Tactic:
simp only [c.ι_π]

Premises used: CategoryTheory.Limits.Bicone.ι_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
pos :
  ∀ (h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)) (h' : k = k'),
    Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') (eqToHom ⋯) (eqToHom ⋯)
neg :
  ∀ (h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)) (h' : ¬k = k'),
    Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') (eqToHom ⋯) 0
pos₁ :
  ∀ (h : ¬Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)) (h' : k = k'),
    Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') 0 (eqToHom ⋯)
neg₁ :
  ∀ (h : ¬Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)) (h' : ¬k = k'),
    Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') 0 0
⊢ Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k')
    (if h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J) then eqToHom ⋯ else 0)
    (if h : k = k' then eqToHom ⋯ else 0)

Tactic:
split_ifs with h h' h'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)
h' : k = k'
⊢ k = k'

Tactic:
simp [Equiv.apply_eq_iff_eq g] at h h'

Premises used: Equiv.apply_eq_iff_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)
h' : ¬k = k'
⊢ k = k'

Tactic:
simp [Equiv.apply_eq_iff_eq g] at h h'

Premises used: Equiv.apply_eq_iff_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
h : ¬Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)
h' : k = k'
⊢ ¬k = k'

Tactic:
simp [Equiv.apply_eq_iff_eq g] at h h'

Premises used: Equiv.apply_eq_iff_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
h : ¬Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)
h' : ¬k = k'
⊢ ¬k = k'

Tactic:
simp [Equiv.apply_eq_iff_eq g] at h h'

Premises used: Equiv.apply_eq_iff_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
h_1 : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)
h' h : k = k'
⊢ Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') (eqToHom ⋯) (eqToHom ⋯)

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
h_1 : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)
h' : ¬k = k'
h : k = k'
⊢ Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') (eqToHom ⋯) 0

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
h' : k = k'
h : ¬k = k'
⊢ Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') 0 (eqToHom ⋯)

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
h' h : ¬k = k'
⊢ Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') 0 0

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
⊢ ∀ (j : Discrete K),
    (c.whisker g).toCone.π.app j =
      Iso.hom (Iso.refl (c.whisker g).toCone.pt) ≫
        NatTrans.app
          (Cone.π
            (obj (Cone.postcompose (Iso.inv (Discrete.functorComp f (⇑g : (a : K) → J))))
              (Cone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCone)))
          j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
⊢ ∀ (j : Discrete K),
    (c.whisker g).toCocone.ι.app j ≫ Iso.hom (Iso.refl (c.whisker g).toCocone.pt) =
      NatTrans.app
        (Cocone.ι
          (obj (Cocone.precompose (Iso.hom (Discrete.functorComp f (⇑g : (a : K) → J))))
            (Cocone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCocone)))
        j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
refine_1 : (hc : (c.whisker g).IsBilimit) → IsLimit c.toCone
refine_2 : (hc : (c.whisker g).IsBilimit) → IsColimit c.toCocone
refine_3 : (hc : c.IsBilimit) → IsLimit (c.whisker g).toCone
refine_4 : (hc : c.IsBilimit) → IsColimit (c.whisker g).toCocone
⊢ (c.whisker g).IsBilimit ≃ c.IsBilimit

Tactic:
refine equivOfSubsingletonOfSubsingleton (fun hc => ⟨?_, ?_⟩) fun hc => ⟨?_, ?_⟩

Premises used: equivOfSubsingletonOfSubsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
hc : (c.whisker g).IsBilimit
this_1 : IsLimit.{w', uC', w', uC} (J := Discrete K) (F := Discrete.functor (f ∘ (⇑g : (a : K) → J)))
  (obj (Cone.postcompose (Iso.inv (Discrete.functorComp f (⇑g : (a : K) → J))))
    (Cone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCone)) :=
  hc.isLimit.ofIsoLimit (c.whiskerToCone g)
this : IsLimit.{w', uC', w', uC} (J := Discrete K) (F :=
  Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J)) ⋙ Discrete.functor f)
  (Cone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCone) :=
  (IsLimit.postcomposeHomEquiv (Iso.symm (Discrete.functorComp f (⇑g : (a : K) → J)))
        (Cone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCone) :
      (a :
          IsLimit
            ((Cone.postcompose (Discrete.functorComp f (⇑g : (a : K) → J)).symm.hom).obj
              (Cone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCone))) →
        IsLimit (Cone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCone))
    this_1
⊢ IsLimit c.toCone

Tactic:
exact IsLimit.ofWhiskerEquivalence (Discrete.equivalence g) this

Premises used: CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.IsLimit.ofWhiskerEquivalence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
hc : (c.whisker g).IsBilimit
this_1 : IsColimit.{w', uC', w', uC} (J := Discrete K) (F := Discrete.functor (f ∘ (⇑g : (a : K) → J)))
  (obj (Cocone.precompose (Iso.hom (Discrete.functorComp f (⇑g : (a : K) → J))))
    (Cocone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCocone)) :=
  hc.isColimit.ofIsoColimit (c.whiskerToCocone g)
this : IsColimit.{w', uC', w', uC} (J := Discrete K) (F :=
  Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J)) ⋙ Discrete.functor f)
  (Cocone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCocone) :=
  (IsColimit.precomposeHomEquiv (Discrete.functorComp f (⇑g : (a : K) → J))
        (Cocone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCocone) :
      (a :
          IsColimit
            ((Cocone.precompose (Discrete.functorComp f (⇑g : (a : K) → J)).hom).obj
              (Cocone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCocone))) →
        IsColimit (Cocone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCocone))
    this_1
⊢ IsColimit c.toCocone

Tactic:
exact IsColimit.ofWhiskerEquivalence (Discrete.equivalence g) this

Premises used: CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.IsColimit.ofWhiskerEquivalence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
hc : c.IsBilimit
apply :
  IsLimit.{w', uC', w', uC} (J := Discrete K) (F := Discrete.functor (f ∘ (⇑g : (a : K) → J)))
    (obj (Cone.postcompose (Iso.inv (Discrete.functorComp f (⇑g : (a : K) → J))))
      (Cone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCone))
⊢ IsLimit (c.whisker g).toCone

Tactic:
apply IsLimit.ofIsoLimit _ (Bicone.whiskerToCone c g).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Limits.Bicone.whiskerToCone, CategoryTheory.Limits.IsLimit.ofIsoLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
hc : c.IsBilimit
apply :
  IsLimit.{w', uC', w', uC} (J := Discrete K) (F :=
    Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J)) ⋙ Discrete.functor f)
    (Cone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCone)
⊢ IsLimit.{w', uC', w', uC} (J := Discrete K) (F := Discrete.functor (f ∘ (⇑g : (a : K) → J)))
    (obj (Cone.postcompose (Iso.inv (Discrete.functorComp f (⇑g : (a : K) → J))))
      (Cone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCone))

Tactic:
apply (IsLimit.postcomposeHomEquiv (Discrete.functorComp f g).symm _).symm _

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, CategoryTheory.Discrete.functorComp, CategoryTheory.Iso.symm, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
hc : c.IsBilimit
⊢ IsLimit.{w', uC', w', uC} (J := Discrete K) (F :=
    Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J)) ⋙ Discrete.functor f)
    (Cone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCone)

Tactic:
exact IsLimit.whiskerEquivalence hc.isLimit (Discrete.equivalence g)

Premises used: CategoryTheory.Limits.IsLimit.whiskerEquivalence, CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.Bicone.IsBilimit.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
hc : c.IsBilimit
apply :
  IsColimit.{w', uC', w', uC} (J := Discrete K) (F := Discrete.functor (f ∘ (⇑g : (a : K) → J)))
    (obj (Cocone.precompose (Iso.hom (Discrete.functorComp f (⇑g : (a : K) → J))))
      (Cocone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCocone))
⊢ IsColimit (c.whisker g).toCocone

Tactic:
apply IsColimit.ofIsoColimit _ (Bicone.whiskerToCocone c g).symm

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Iso.symm, CategoryTheory.Limits.Bicone.whiskerToCocone
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
hc : c.IsBilimit
apply :
  IsColimit.{w', uC', w', uC} (J := Discrete K) (F :=
    Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J)) ⋙ Discrete.functor f)
    (Cocone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCocone)
⊢ IsColimit.{w', uC', w', uC} (J := Discrete K) (F := Discrete.functor (f ∘ (⇑g : (a : K) → J)))
    (obj (Cocone.precompose (Iso.hom (Discrete.functorComp f (⇑g : (a : K) → J))))
      (Cocone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCocone))

Tactic:
apply (IsColimit.precomposeHomEquiv (Discrete.functorComp f g) _).symm _

Premises used: CategoryTheory.Discrete.functorComp, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeHomEquiv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
hc : c.IsBilimit
⊢ IsColimit.{w', uC', w', uC} (J := Discrete K) (F :=
    Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J)) ⋙ Discrete.functor f)
    (Cocone.whisker (Discrete.functor (Discrete.mk ∘ (⇑g : (a : K) → J))) c.toCocone)

Tactic:
exact IsColimit.whiskerEquivalence hc.isColimit (Discrete.equivalence g)

Premises used: CategoryTheory.Limits.IsColimit.whiskerEquivalence, CategoryTheory.Limits.Bicone.IsBilimit.isColimit, CategoryTheory.Discrete.equivalence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
d : LimitBicone.{w, uC', uC} F
⊢ HasBiproduct.{w, uC', uC} F

Tactic:
⟨Nonempty.intro d⟩

Premises used: CategoryTheory.Limits.HasBiproduct.mk', Nonempty.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
inst_4 : HasBiproduct.{w, uC', uC} F
⊢ HasProduct.{w, uC', uC} F

Tactic:
HasLimit.mk
    { cone := (biproduct.bicone F).toCone
      isLimit := biproduct.isLimit F }

Premises used: CategoryTheory.Limits.biproduct.bicone, CategoryTheory.Limits.Bicone.toCone, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Limits.biproduct.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
inst_4 : HasBiproduct.{w, uC', uC} F
⊢ HasCoproduct.{w, uC', uC} F

Tactic:
HasColimit.mk
    { cocone := (biproduct.bicone F).toCocone
      isColimit := biproduct.isColimit F }

Premises used: CategoryTheory.Limits.biproduct.isColimit, CategoryTheory.Limits.biproduct.bicone, CategoryTheory.Limits.Bicone.toCocone, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
K : Type w'
inst_2 : HasBiproductsOfShape.{w', uC', uC} K C
e : J ≃ K
F : J → C
h : LimitBicone.{w', uC', uC} (J := K) (F ∘ (⇑e.symm : (a : K) → J))
c : Bicone.{w', uC', uC} (J := K) (F ∘ (⇑e.symm : (a : K) → J))
hc : c.IsBilimit
⊢ LimitBicone.{w, uC', uC} F

Tactic:
simpa only [Function.comp_def, e.symm_apply_apply] using
        LimitBicone.mk (c.whisker e) ((c.whiskerIsBilimitIff _).2 hc)

Premises used: Equiv.symm_apply_apply, Function.comp_def, CategoryTheory.Limits.Bicone.whisker, CategoryTheory.Limits.LimitBicone.mk, CategoryTheory.Limits.Bicone.whiskerIsBilimitIff, Equiv.invFun