mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none.none.id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (span f g ⋙ F).map (WidePushoutShape.Hom.id none) ≫
      (Option.casesOn none (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f) (F.map g)).map (WidePushoutShape.Hom.id none)

Tactic:
simp

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

Goal state before:
pp: case none.some.left.init
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (span f g ⋙ F).map (init WalkingPair.left) ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f) (F.map g)).map (init WalkingPair.left)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X x✝ : Over A
⊢ Hom.left ({ app := fun g ↦ homMk (coprod.map (Hom.left (𝟙 X)) (𝟙 g.left)) ⋯, naturality := ⋯ }.app x✝) =
    Hom.left ((𝟙 X.coprodObj).app x✝)

Tactic:
simp

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

Goal state before:
pp: case none.some.right.init
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (span f g ⋙ F).map (init WalkingPair.right) ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f) (F.map g)).map (init WalkingPair.right)

Tactic:
simp

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

Goal state before:
pp: case some.left.some.left.id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (span f g ⋙ F).map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f) (F.map g)).map (WidePushoutShape.Hom.id (some WalkingPair.left))

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X✝ Y✝ Z✝ : Over A
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : Over A
⊢ Hom.left ({ app := fun g_1 ↦ homMk (coprod.map (Hom.left (f ≫ g)) (𝟙 g_1.left)) ⋯, naturality := ⋯ }.app x✝) =
    Hom.left
      (({ app := fun g ↦ homMk (coprod.map (Hom.left f) (𝟙 g.left)) ⋯, naturality := ⋯ } ≫
            { app := fun g_1 ↦ homMk (coprod.map (Hom.left g) (𝟙 g_1.left)) ⋯, naturality := ⋯ }).app
        x✝)

Tactic:
simp

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

Goal state before:
pp: case some.right.some.right.id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (span f g ⋙ F).map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f) (F.map g)).map (WidePushoutShape.Hom.id (some WalkingPair.right))

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryFan X Y
hc : IsLimit c
x✝ : BinaryCofan (op X) (op Y)
⊢ (c.fst.op ≫ (hc.lift x✝.unop).op).unop = x✝.inl.unop

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryFan X Y
hc : IsLimit c
x✝ : BinaryCofan (op X) (op Y)
⊢ (c.snd.op ≫ (hc.lift x✝.unop).op).unop = x✝.inr.unop

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryCofan X Y
hc : IsColimit c
x✝ : BinaryFan (op X) (op Y)
⊢ ((hc.desc x✝.unop).op ≫ c.inl.op).unop = x✝.fst.unop

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryCofan X Y
hc : IsColimit c
x✝ : BinaryFan (op X) (op Y)
⊢ ((hc.desc x✝.unop).op ≫ c.inr.op).unop = x✝.snd.unop

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryFan (op X) (op Y)
hc : IsLimit c
x✝ : BinaryCofan X Y
⊢ (c.fst.unop ≫ (hc.lift x✝.op).unop).op = x✝.inl.op

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryFan (op X) (op Y)
hc : IsLimit c
x✝ : BinaryCofan X Y
⊢ (c.snd.unop ≫ (hc.lift x✝.op).unop).op = x✝.inr.op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : S ⟶ T.obj Y
⊢ mk f = mk ((mk f).hom ≫ T.map (𝟙 Y))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : StructuredArrow S T
g : f.right ⟶ Y'
g' : Y' ⟶ Y''
⊢ mk ((mk (f.hom ≫ T.map g)).hom ≫ T.map g') = mk (f.hom ≫ T.map (g ≫ g'))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : S ⟶ T.obj Y
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ mk ((mk (f ≫ T.map g)).hom ≫ T.map g') = mk ((mk f).hom ≫ T.map (g ≫ g'))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : S ⟶ T.obj Y
⊢ mk f = mk (f ≫ T.map (𝟙 Y))

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryCofan (op X) (op Y)
hc : IsColimit c
x✝ : BinaryFan X Y
⊢ ((hc.desc x✝.op).unop ≫ c.inl.unop).op = x✝.fst.op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
Y : C
T : C ⥤ D
f : S ⟶ T.obj Y
⊢ mkPostcomp f (𝟙 Y) = eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : S ⟶ T.obj Y
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ mk ((f ≫ T.map g) ≫ T.map g') = mk (f ≫ T.map (g ≫ g'))

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryCofan (op X) (op Y)
hc : IsColimit c
x✝ : BinaryFan X Y
⊢ ((hc.desc x✝.op).unop ≫ c.inr.unop).op = x✝.snd.op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
Y Y' Y'' : C
T : C ⥤ D
f : S ⟶ T.obj Y
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ mkPostcomp f (g ≫ g') = mkPostcomp f g ≫ mkPostcomp (f ≫ T.map g) g' ≫ eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
⊢ I.lift (BinaryFan.swap t) ≫ s.swap.π.app { as := WalkingPair.left } = t.π.app { as := WalkingPair.left }

Tactic:
simp

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

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
⊢ I.lift (BinaryFan.swap t) ≫ s.swap.π.app { as := WalkingPair.right } = t.π.app { as := WalkingPair.right }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
f : StructuredArrow S T
⊢ (map (𝟙 S)).obj (mk f.hom) = mk f.hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
T : C ⥤ D
f : S ⟶ S'
f' : S' ⟶ S''
h : StructuredArrow S'' T
⊢ (map (f ≫ f')).obj (mk h.hom) = (map f).obj ((map f').obj (mk h.hom))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A✝ B✝ : StructuredArrow S T
f : A✝ ⟶ B✝
t : IsIso ((proj S T).map f)
⊢ f ≫ homMk (inv ((proj S T).map f)) ⋯ = 𝟙 A✝ ∧ homMk (inv ((proj S T).map f)) ⋯ ≫ f = 𝟙 B✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: case left
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
inst✝¹ : T.Full
inst✝ : T.Faithful
c : Cocone (Functor.empty (StructuredArrow (T.obj Y) T))
m : (asEmptyCocone (mk (𝟙 (T.obj Y)))).pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{1}), (asEmptyCocone (mk (𝟙 (T.obj Y)))).ι.app j ≫ m = c.ι.app j
⊢ m.left = (homMk (T.preimage c.pt.hom) ⋯).left

Tactic:
simp

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ R.lift (BinaryFan.assocInv P t) ≫ (BinaryFan.assoc Q s).π.app { as := WalkingPair.left } =
    t.π.app { as := WalkingPair.left }

Tactic:
simp

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

Goal state before:
pp: case right.left
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ (R.lift (BinaryFan.assocInv P t) ≫ (BinaryFan.assoc Q s).π.app { as := WalkingPair.right }) ≫
      sYZ.π.app { as := WalkingPair.left } =
    t.π.app { as := WalkingPair.right } ≫ sYZ.π.app { as := WalkingPair.left }

Tactic:
simp

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

Goal state before:
pp: case right.right
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ (R.lift (BinaryFan.assocInv P t) ≫ (BinaryFan.assoc Q s).π.app { as := WalkingPair.right }) ≫
      sYZ.π.app { as := WalkingPair.right } =
    t.π.app { as := WalkingPair.right } ≫ sYZ.π.app { as := WalkingPair.right }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
S✝ S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
S : C
F : B ⥤ C
G : C ⥤ D
inst✝ : G.Faithful
X✝ Y✝ : StructuredArrow S F
f : (post S F G).obj X✝ ⟶ (post S F G).obj Y✝
⊢ (post S F G).map (homMk (Hom.right f) ⋯) = f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
S✝ S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
S : C
F : B ⥤ C
G : C ⥤ D
inst✝ : G.Full
h : StructuredArrow (G.obj S) (F ⋙ G)
⊢ ((post S F G).obj (mk (G.preimage h.hom))).hom ≫
      (F ⋙ G).map (Iso.refl ((post S F G).obj (mk (G.preimage h.hom))).right).hom =
    h.hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F : C ⥤ A
G : D ⥤ B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : L' ⟶ G'.obj L
β' : R ⋙ G' ⟶ F' ⋙ R'
hα : α = α' ≫ e₂.inv.app L
hβ : β ≫ Functor.whiskerRight e₁.hom R' = R.whiskerLeft e₂.hom ≫ β'
⊢ ∀ {X Y : StructuredArrow L R} (f : X ⟶ Y),
    (map₂ α β).map f ≫ (isoMk (e₁.app Y.right) ⋯).hom = (isoMk (e₁.app X.right) ⋯).hom ≫ (map₂ α' β').map f

Tactic:
simp

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

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z P✝ X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan s.pt X
Q : IsLimit t
⊢ (t.snd ≫
        Q.lift
          (mk (P.lift { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } })
            (𝟙 { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } }.pt))) ≫
      t.π.app { as := WalkingPair.right } =
    𝟙 t.pt ≫ t.π.app { as := WalkingPair.right }

Tactic:
simp

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z P✝ X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan X s.pt
Q : IsLimit t
⊢ (t.fst ≫ Q.lift (mk (𝟙 X) (P.lift { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } }))) ≫
      t.π.app { as := WalkingPair.left } =
    𝟙 t.pt ≫ t.π.app { as := WalkingPair.left }

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit 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:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
⊢ t.flip.flip.fst = (Iso.refl t.flip.flip.pt).hom ≫ t.fst

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
⊢ t.flip.flip.snd = (Iso.refl t.flip.flip.pt).hom ≫ t.snd

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
⊢ ∀ (s : PullbackCone g f), ht.lift s.flip ≫ t.snd = s.fst

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
⊢ ∀ (s : PullbackCone g f), ht.lift s.flip ≫ t.fst = s.snd

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback 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:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ inl f g ≫ desc h k ⋯ = h ∧ inr f g ≫ desc h k ⋯ = k

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ ∀ (s : PushoutCocone f g), pushout.inl f g ≫ pushout.desc s.inl s.inr ⋯ = s.inl

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ ∀ (s : PushoutCocone f g), pushout.inr f g ≫ pushout.desc s.inl s.inr ⋯ = s.inr

Tactic:
simp

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

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ lift (fst f g) (snd f g) ⋯ ≫ fst f g = 𝟙 (pullback f g) ≫ fst f g

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ lift (fst f g) (snd f g) ⋯ ≫ snd f g = 𝟙 (pullback f g) ≫ snd f g

Tactic:
simp

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

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ inl f g ≫ desc (inl f g) (inr f g) ⋯ = inl f g ≫ 𝟙 (pushout f g)

Tactic:
simp

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

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingCospan ⥤ C
t : Cone F
⊢ ((Cone.postcompose (diagramIsoCospan F).hom).obj t).π.app none =
    (Iso.refl ((Cone.postcompose (diagramIsoCospan F).hom).obj t).pt).hom ≫
      (mk (t.π.app WalkingCospan.left) (t.π.app WalkingCospan.right) ⋯).π.app none

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ inr f g ≫ desc (inl f g) (inr f g) ⋯ = inr f g ≫ 𝟙 (pushout f g)

Tactic:
simp

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

Goal state before:
pp: case some.left
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingCospan ⥤ C
t : Cone F
⊢ ((Cone.postcompose (diagramIsoCospan F).hom).obj t).π.app (some WalkingPair.left) =
    (Iso.refl ((Cone.postcompose (diagramIsoCospan F).hom).obj t).pt).hom ≫
      (mk (t.π.app WalkingCospan.left) (t.π.app WalkingCospan.right) ⋯).π.app (some WalkingPair.left)

Tactic:
simp

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

Goal state before:
pp: case some.right
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingCospan ⥤ C
t : Cone F
⊢ ((Cone.postcompose (diagramIsoCospan F).hom).obj t).π.app (some WalkingPair.right) =
    (Iso.refl ((Cone.postcompose (diagramIsoCospan F).hom).obj t).pt).hom ≫
      (mk (t.π.app WalkingCospan.left) (t.π.app WalkingCospan.right) ⋯).π.app (some WalkingPair.right)

Tactic:
simp

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

Goal state before:
pp: case h₀
C : Type u
inst✝³ : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPullback f g
inst✝¹ : HasPullback f' g'
inst✝ : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ (map f g f' g' i₁ i₂ i₃ e₁ e₂ ≫ map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄) ≫ fst f'' g'' =
    map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) ⋯ ⋯ ≫ fst f'' g''

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPullback f g
inst✝¹ : HasPullback f' g'
inst✝ : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ (map f g f' g' i₁ i₂ i₃ e₁ e₂ ≫ map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄) ≫ snd f'' g'' =
    map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) ⋯ ⋯ ≫ snd f'' g''

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

Tactic:
simp

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

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ map f g f g (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫ fst f g = 𝟙 (pullback f g) ≫ fst f g

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ map f g f g (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫ snd f g = 𝟙 (pullback f g) ≫ snd f g

Tactic:
simp

Goal state after: