mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
s : { p // p.1 ≫ f = p.2 ≫ g }
i✝ : T.I
⊢ (↑((fun m ↦ ⟨(m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd), ⋯⟩)
                ((fun s ↦
                    { f := fun i ↦ ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩,
                      φ := fun i ↦
                        (hpb ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).lift (PullbackCone.mk ((↑s).1.φ i) ((↑s).2.φ i) ⋯) })
                  s))).2.φ
        i✝ ≫
      eqToHom ⋯ =
    (↑s).2.φ i✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasCoproducts A
J : Type w
f : J → FormalCoproduct C
F✝ F : C ⥤ A
x : C
⊢ (Sigma.ι (fun x_1 ↦ F.obj x) PUnit.unit ≫ Sigma.desc fun x_1 ↦ 𝟙 (F.obj (((incl C).obj x).obj x_1))) =
    𝟙 (((𝟭 (C ⥤ A)).obj F).obj x)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasProducts A
J : Type w
f : J → FormalCoproduct C
F✝ F : Cᵒᵖ ⥤ A
x : Cᵒᵖ
⊢ (Pi.lift fun x_1 ↦ 𝟙 (((𝟭 (Cᵒᵖ ⥤ A)).obj F).obj x)) ≫
      Pi.π (fun i ↦ F.obj (op ((unop ((incl C).op.obj x)).obj i))) PUnit.unit =
    𝟙 (((𝟭 (Cᵒᵖ ⥤ A)).obj F).obj x)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: case inl
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
x✝ : C
val✝ : F.obj x✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (𝟙 x✝))) ⇑(hom (G.map (𝟙 x✝))))).toFun (Sum.inl val✝) =
    (hom (𝟙 (F.obj x✝ ⊕ G.obj x✝))).toFun (Sum.inl val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: case inr
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
x✝ : C
val✝ : G.obj x✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (𝟙 x✝))) ⇑(hom (G.map (𝟙 x✝))))).toFun (Sum.inr val✝) =
    (hom (𝟙 (F.obj x✝ ⊕ G.obj x✝))).toFun (Sum.inr val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: case inl
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
val✝ : F.obj X✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (x✝¹ ≫ x✝))) ⇑(hom (G.map (x✝¹ ≫ x✝))))).toFun (Sum.inl val✝) =
    (hom (↾Sum.map ⇑(hom (F.map x✝¹)) ⇑(hom (G.map x✝¹)) ≫ ↾Sum.map ⇑(hom (F.map x✝)) ⇑(hom (G.map x✝)))).toFun
      (Sum.inl val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: case inr
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
val✝ : G.obj X✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (x✝¹ ≫ x✝))) ⇑(hom (G.map (x✝¹ ≫ x✝))))).toFun (Sum.inr val✝) =
    (hom (↾Sum.map ⇑(hom (F.map x✝¹)) ⇑(hom (G.map x✝¹)) ≫ ↾Sum.map ⇑(hom (F.map x✝)) ⇑(hom (G.map x✝)))).toFun
      (Sum.inr val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: case inl
C : Type u
inst✝ : Category.{v, u} C
F G F₁ F₂ : C ⥤ Type w
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
val✝ : F₁.obj x✝²
⊢ (hom ((coprod F₁ F₂).map x✝ ≫ ↾Sum.elim ⇑(hom (τ₁.app x✝¹)) ⇑(hom (τ₂.app x✝¹)))).toFun (Sum.inl val✝) =
    (hom (↾Sum.elim ⇑(hom (τ₁.app x✝²)) ⇑(hom (τ₂.app x✝²)) ≫ F.map x✝)).toFun (Sum.inl val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: case inr
C : Type u
inst✝ : Category.{v, u} C
F G F₁ F₂ : C ⥤ Type w
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
val✝ : F₂.obj x✝²
⊢ (hom ((coprod F₁ F₂).map x✝ ≫ ↾Sum.elim ⇑(hom (τ₁.app x✝¹)) ⇑(hom (τ₂.app x✝¹)))).toFun (Sum.inr val✝) =
    (hom (↾Sum.elim ⇑(hom (τ₁.app x✝²)) ⇑(hom (τ₂.app x✝²)) ≫ F.map x✝)).toFun (Sum.inr val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁ ≫ f₁ = h.p₂ ≫ f₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂ ≫ f₂ = h.p₃ ≫ f₃

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁ ≫ f₁ = h.p₃ ≫ f₃

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁₂ ≫ h₁₂.p₁ = h.p₁₃ ≫ h₁₃.p₁

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
x✝ : C
a : x✝ ⟶ h₁₂.pullback
b : x✝ ⟶ h₁₃.pullback
w : a ≫ h₁₂.p₁ = b ≫ h₁₃.p₁
⊢ (a ≫ h₁₂.p₂) ≫ f₂ = (a ≫ h₁₂.p₁) ≫ f₁

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁₃ ≫ h₁₃.p₂ = h.p₂₃ ≫ h₂₃.p₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
x✝ : C
a : x✝ ⟶ h₁₃.pullback
b : x✝ ⟶ h₂₃.pullback
w : a ≫ h₁₃.p₂ = b ≫ h₂₃.p₂
⊢ (a ≫ h₁₃.p₂) ≫ f₃ = (a ≫ h₁₃.p₁) ≫ f₁

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 0 ≫ 𝟙 X = 0 ≫ 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ CommSq 0 (𝟙 X) 0 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ((zeroProdIso X).symm ≪≫ (pullbackZeroZeroIso 0 X).symm).hom ≫ pullback.snd 0 0 = 𝟙 X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ b.inl ≫ b.snd = 0 ≫ 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback (b.inl ≫ b.fst) 0 0 (0 ≫ 0)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 ≫ 0 = b.inr ≫ b.fst

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback 0 (b.inr ≫ b.snd) (0 ≫ 0) 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 ≫ b.inl = 0 ≫ b.inr

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback (0 ≫ 0) 0 0 (b.inr ≫ b.snd)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 0 ≫ 0 = 𝟙 X ≫ 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case of.of
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
i j : J
⊢ ∀ (f : WithTerminal.of i ⟶ WithTerminal.of j),
    (WithTerminal.liftFromOver.obj c).map f ≫
        (WithTerminal.casesOn (WithTerminal.of j)
            (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom =
      (WithTerminal.casesOn (WithTerminal.of i)
            (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom ≫
        (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case of.star
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
i : J
⊢ (WithTerminal.liftFromOver.obj c).map PUnit.unit ≫
      (WithTerminal.casesOn WithTerminal.star
          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom =
    (WithTerminal.casesOn (WithTerminal.of i)
          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom ≫
      (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map PUnit.unit

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case star.star
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
⊢ (WithTerminal.liftFromOver.obj c).map PUnit.unit ≫
      (WithTerminal.casesOn WithTerminal.star
          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom =
    (WithTerminal.casesOn WithTerminal.star
          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom ≫
      (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map PUnit.unit

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ ∀ (j : WalkingSpan), (PushoutCocone.mk 0 0 ⋯).ι.app j ≫ 0 = s.ι.app j

Tactic:
have c :=
              @PushoutCocone.coequalizer_ext _ _ _ _ _ _ _ s _ 0 (𝟙 _)
                (by simp [eq_iff_true_of_subsingleton]) (by simpa using PushoutCocone.condition s)
            dsimp at c
            simpa using c

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ CommSq 0 0 (𝟙 X) 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 𝟙 X ≫ ((coprodZeroIso X).symm ≪≫ (pushoutZeroZeroIso X 0).symm).hom = pushout.inl 0 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 ≫ 0 = b.inl ≫ b.snd

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout (0 ≫ 0) 0 0 (b.inr ≫ b.snd)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ b.inr ≫ b.fst = 0 ≫ 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout 0 (0 ≫ 0) (b.inl ≫ b.fst) 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ b.fst ≫ 0 = b.snd ≫ 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout (b.inl ≫ b.fst) 0 0 (0 ≫ 0)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case of
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
a✝ : J
⊢ ((Cone.postcompose
                (NatIso.ofComponents
                    (fun i ↦
                      WithTerminal.casesOn i
                        (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
                        (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star)))
                    ⋯).hom).obj
            (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })).π.app
      (WithTerminal.of a✝) =
    (Iso.refl
          ((Cone.postcompose
                  (NatIso.ofComponents
                      (fun i ↦
                        WithTerminal.casesOn i
                          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
                          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star)))
                      ⋯).hom).obj
              (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })).pt).hom ≫
      ((Over.forget F).mapCone
              { pt := G,
                π :=
                  {
                    app := fun i ↦
                      WithTerminal.casesOn i α.app
                        (Over.mkIdTerminal.from (((const (WithTerminal J)).obj G).obj WithTerminal.star)),
                    naturality := ⋯ } }).π.app
        (WithTerminal.of a✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case star
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
⊢ ((Cone.postcompose
                (NatIso.ofComponents
                    (fun i ↦
                      WithTerminal.casesOn i
                        (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
                        (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star)))
                    ⋯).hom).obj
            (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })).π.app
      WithTerminal.star =
    (Iso.refl
          ((Cone.postcompose
                  (NatIso.ofComponents
                      (fun i ↦
                        WithTerminal.casesOn i
                          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
                          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star)))
                      ⋯).hom).obj
              (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })).pt).hom ≫
      ((Over.forget F).mapCone
              { pt := G,
                π :=
                  {
                    app := fun i ↦
                      WithTerminal.casesOn i α.app
                        (Over.mkIdTerminal.from (((const (WithTerminal J)).obj G).obj WithTerminal.star)),
                    naturality := ⋯ } }).π.app
        WithTerminal.star

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case pos
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : m < n
h✝ : m < n + 1
⊢ M m = M m

pp: case neg
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : m < n
h✝ : ¬m < n + 1
⊢ N m = M m

Tactic:
try rfl; try lia

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case refine_2
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ M m = M m

Tactic:
try rfl; try lia

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case refine_3
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ N m = N m

Tactic:
try rfl; try lia

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case refine_4
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : ¬m < n + 1
⊢ N m = N m

Tactic:
try rfl; try lia

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
⊢ G.left.map f ≫ G.hom.app j = G.hom.app i ≫ F.map f

Tactic:
simp

Goal state after: