mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ j' ∈ {j, j', j''}

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ j'' ∈ {j, j', j''}

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ ⟨j, ⟨j', ⟨⋯, ⟨⋯, i⟩⟩⟩⟩ ∈ {⟨j, ⟨j', ⟨⋯, ⟨⋯, i⟩⟩⟩⟩}

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
U : FormalCoproduct C
T : C
hT : IsTerminal T
X✝ Y✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
⊢ ∀ (j : Fin ((Opposite.unop Y✝).len + 1)),
    (U.cech.map f ≫ (U.cechIsoCechNerveApp hT Y✝).hom) ≫
        WidePullback.π (fun x ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).hom) j =
      ((U.cechIsoCechNerveApp hT X✝).hom ≫ (Arrow.mk ((isTerminalIncl T hT).from U)).cechNerve.map f) ≫
        WidePullback.π (fun x ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).hom) j

Tactic:
by 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
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
i : Y.I
⊢ Y.obj i = Y.obj (e (e.symm i))

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Category.{v₂, u₂} B
inst✝⁵ : HasEqualizers A
inst✝⁴ : HasImages A
inst✝³ : StrongEpiCategory B
inst✝² : HasImages B
L : A ⥤ B
inst✝¹ : ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) L
inst✝ : ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
⊢ factorThruImage (L.map f) ≫ (iso L f).hom = L.map (factorThruImage f)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Category.{v₂, u₂} B
inst✝⁵ : HasEqualizers A
inst✝⁴ : HasImages A
inst✝³ : StrongEpiCategory B
inst✝² : HasImages B
L : A ⥤ B
inst✝¹ : ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) L
inst✝ : ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
⊢ (iso L f).inv ≫ image.ι (L.map f) = L.map (image.ι f)

Tactic:
by 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
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
m : T ⟶ (pullbackCone f g pb).pt
⊢ (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd).1 ≫ f =
    (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd).2 ≫ g

Tactic:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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 0 (𝟙 X) 0

Tactic:
by 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:
by 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:
by 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:
by 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:
by simp

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:
by simp

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
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1, π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
k : J
⊢ { pt := s.1, π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }.π.app
        k ≫
      (c.obj k).left.map f =
    s.fst ≫ (Over.Hom.left (α.app k)).app j

Tactic:
by simp

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
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1, π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
k : J
⊢ { pt := s.1, π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }.π.app
        k ≫
      (c.obj k).hom.app i =
    s.snd

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
f : j ⟶ j'
x : (F.obj (op j')).obj j
⊢ (hom ((F.map f.op).app j)) x = (Hom.hom ((F.map f.op).app j)) x ∧
    (hom ((F.obj (op j')).map f)) x = (Hom.hom ((F.obj (op j')).map f)) x

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
f : c'.pt ⟶ P
⊢ ∀ (j : Jᵒᵖ),
    c'.ι.app j ≫
        (fun s ↦ hc'.desc { pt := P, ι := { app := fun j ↦ shrinkYonedaEquiv.symm (↑s (unop j)), naturality := ⋯ } })
          ((fun f ↦ ⟨fun j ↦ shrinkYonedaEquiv (c'.ι.app (op j) ≫ f), ⋯⟩) f) =
      c'.ι.app j ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
inst✝ : HasWeakEqualizer f g
⊢ (Iso.refl (weakLimit.cone (parallelPair f g)).pt).hom ≫ (Fork.ofι (weakEqualizer.ι f g) ⋯).ι =
    Fork.ι (weakLimit.cone (parallelPair f g))

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f g : X ⟶ Y
inst✝ : HasWeakKernel f
⊢ (Iso.refl (weakLimit.cone (parallelPair f 0)).pt).hom ≫ (Fork.ofι (weakKernel.ι f) ⋯).ι =
    Fork.ι (weakLimit.cone (parallelPair f 0))

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasWeakPullback f g
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ lift h k ⋯ ≫ fst f g = h ∧ lift h k ⋯ ≫ snd f g = k

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W✝ X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsWeakLimit t
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ lift ht h k w ≫ t.fst = h ∧ lift ht h k w ≫ t.snd = k

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasWeakLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
⊢ ∀ (s : PullbackCone f g),
    weakEqualizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ ≫
        weakEqualizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.fst =
      s.fst

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasWeakLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
⊢ ∀ (s : PullbackCone f g),
    weakEqualizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ ≫
        weakEqualizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.snd =
      s.snd

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
C : Type u'
inst✝ : Category.{v', u'} C
W : J ⥤ Type w
F✝ : J ⥤ C
pt : C
π : ⦃j : J⦄ → W.obj j → (pt ⟶ F✝.obj j)
hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), π x ≫ F✝.map f = π ((ConcreteCategory.hom (W.map f)) x)
F : J ⥤ C
j : J
s : Cone (CategoryOfElements.π (coyoneda.obj (op j)) ⋙ F)
x : (coyoneda.obj (op j)).Elements
⊢ (ConcreteCategory.hom ((coyoneda.obj (op j)).map x.snd)) ((coyoneda.obj (op j)).elementsMk j (𝟙 j)).snd = x.snd

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝⁴ : Category.{v, u} J
C : Type u'
inst✝³ : Category.{v', u'} C
W W' W'' : J ⥤ Type w
g : W ⟶ W'
g' : W' ⟶ W''
F : J ⥤ C
inst✝² : HasWeightedLimit W F
inst✝¹ : HasWeightedLimit W' F
inst✝ : HasWeightedLimit W'' F
j₁ j₂ : J
x : W.obj j₁
f : j₁ ⟶ j₂
⊢ W.weightedLimObjObjπ F x ≫ F.map f = W.weightedLimObjObjπ F ((ConcreteCategory.hom (W.map f)) x)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝⁴ : Category.{v, u} J
C : Type u'
inst✝³ : Category.{v', u'} C
W W' W'' : J ⥤ Type w
g : W ⟶ W'
g' : W' ⟶ W''
F : J ⥤ C
inst✝² : HasWeightedLimit W F
inst✝¹ : HasWeightedLimit W' F
inst✝ : HasWeightedLimit W'' F
⊢ ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂),
    W'.weightedLimObjObjπ F ((ConcreteCategory.hom (g.app j₁)) x) ≫ F.map f =
      W'.weightedLimObjObjπ F ((ConcreteCategory.hom (g.app j₂)) ((ConcreteCategory.hom (W.map f)) x))

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
x✝¹ : X ⥤ F ⊡ G
x✝ : X
⊢ F.map (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x✝¹).obj x✝).fst).hom ≫
      (((toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X).obj x✝¹).obj x✝).iso.hom =
    (((𝟭 (X ⥤ F ⊡ G)).obj x✝¹).obj x✝).iso.hom ≫ G.map (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x✝¹).obj x✝).snd).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ ψ' : CatCospanTransform F G F₁ G₁
η : ψ ⟶ ψ'
S : CatCommSqOver F G X
x y : X
f : x ⟶ y
⊢ ({
                  obj := fun S ↦
                    { fst := S.fst ⋙ ψ.left, snd := S.snd ⋙ ψ.right,
                      iso :=
                        S.fst.associator ψ.left F₁ ≪≫
                          S.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                            (S.fst.associator F ψ.base).symm ≪≫
                              isoWhiskerRight S.iso ψ.base ≪≫
                                S.snd.associator G ψ.base ≪≫
                                  S.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                    (S.snd.associator ψ.right G₁).symm },
                  map := fun {x y} f ↦ { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ },
                  map_id := ⋯, map_comp := ⋯ }.obj
              S).fst.map
        f ≫
      η.left.app (S.fst.obj y) =
    η.left.app (S.fst.obj x) ≫
      ({
                  obj := fun S ↦
                    { fst := S.fst ⋙ ψ'.left, snd := S.snd ⋙ ψ'.right,
                      iso :=
                        S.fst.associator ψ'.left F₁ ≪≫
                          S.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                            (S.fst.associator F ψ'.base).symm ≪≫
                              isoWhiskerRight S.iso ψ'.base ≪≫
                                S.snd.associator G ψ'.base ≪≫
                                  S.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                    (S.snd.associator ψ'.right G₁).symm },
                  map := fun {x y} f ↦
                    { fst := whiskerRight f.fst ψ'.left, snd := whiskerRight f.snd ψ'.right, w := ⋯ },
                  map_id := ⋯, map_comp := ⋯ }.obj
              S).fst.map
        f

Tactic:
by simp

Goal state after: