mathlib-initiative/mathlib-tactics huggingface dataset:
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)
m : t.pt ⟶ s.swap.pt
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
w : m ≫ s.swap.π.app { as := WalkingPair.swap WalkingPair.left } = t.π.app { as := WalkingPair.swap WalkingPair.left }
⊢ m ≫ s.π.app { as := WalkingPair.left } = (BinaryFan.swap t).π.app { as := WalkingPair.left }

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)
m : t.pt ⟶ s.swap.pt
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
w : m ≫ s.swap.π.app { as := WalkingPair.swap WalkingPair.right } = t.π.app { as := WalkingPair.swap WalkingPair.right }
⊢ m ≫ s.π.app { as := WalkingPair.right } = (BinaryFan.swap t).π.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
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)
m : t.pt ⟶ s.swap.pt
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
w : m ≫ s.swap.π.app { as := WalkingPair.swap WalkingPair.left } = t.π.app { as := WalkingPair.swap WalkingPair.left }
⊢ m ≫ s.π.app { as := WalkingPair.left } = (BinaryFan.swap t).π.app { as := WalkingPair.left }

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)
m : t.pt ⟶ s.swap.pt
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
w : m ≫ s.swap.π.app { as := WalkingPair.swap WalkingPair.right } = t.π.app { as := WalkingPair.swap WalkingPair.right }
⊢ m ≫ s.π.app { as := WalkingPair.right } = (BinaryFan.swap t).π.app { as := WalkingPair.right }
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 }

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:
<;>

Goal state after:
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 }

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 }
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 : StructuredArrow L R
⊢ ((map₂ α β).obj X).hom ≫ R'.map (e₁.app X.right).hom = ((map₂ α' β').obj X).hom

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:
· subst hα
    simp [dsimp% congr($(hβ).app X.right)]
  · 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

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:
<;>

Goal state after:
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

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
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case h₀
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
m : s.pt ⟶ t.pt
h₁ : m ≫ t.snd = s.fst
h₂ : m ≫ t.fst = s.snd
⊢ m ≫ t.fst = ht.lift s.flip ≫ t.fst

pp: case h₁
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
m : s.pt ⟶ t.pt
h₁ : m ≫ t.snd = s.fst
h₂ : m ≫ t.fst = s.snd
⊢ m ≫ t.snd = ht.lift s.flip ≫ t.snd

Tactic:
<;>

Goal state after:
case h₀
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
m : s.pt ⟶ t.pt
h₁ : m ≫ t.snd = s.fst
h₂ : m ≫ t.fst = s.snd
⊢ m ≫ t.fst = ht.lift s.flip ≫ t.fst

case h₁
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
m : s.pt ⟶ t.pt
h₁ : m ≫ t.snd = s.fst
h₂ : m ≫ t.fst = s.snd
⊢ m ≫ t.snd = ht.lift s.flip ≫ t.snd
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)

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:
<;>

Goal state after:
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)

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)
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

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)

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:
<;>

Goal state after:
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

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)

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)
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''

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:
<;>

Goal state after:
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''

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''
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

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:
<;>

Goal state after:
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

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
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case none.none.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (span f g).map (𝟙 none) ≫ f ≫ inl = (f ≫ inl) ≫ 𝟙 W

pp: case none.some.left.init
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ f ≫ inl = (f ≫ inl) ≫ 𝟙 W

pp: case none.some.right.init
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ g ≫ inr = (f ≫ inl) ≫ 𝟙 W

pp: case some.left.some.left.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (span f g).map (𝟙 (some WalkingPair.left)) ≫ inl = inl ≫ 𝟙 W

pp: case some.right.some.right.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (span f g).map (𝟙 (some WalkingPair.right)) ≫ inr = inr ≫ 𝟙 W

Tactic:
<;>

Goal state after:
case none.none.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (span f g).map (𝟙 none) ≫ f ≫ inl = (f ≫ inl) ≫ 𝟙 W

case none.some.left.init
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ f ≫ inl = (f ≫ inl) ≫ 𝟙 W

case none.some.right.init
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ g ≫ inr = (f ≫ inl) ≫ 𝟙 W

case some.left.some.left.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (span f g).map (𝟙 (some WalkingPair.left)) ≫ inl = inl ≫ 𝟙 W

case some.right.some.right.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ (span f g).map (𝟙 (some WalkingPair.right)) ≫ inr = inr ≫ 𝟙 W
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 ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ inl f g ≫ map f g f' g' i₂ i₃ i₁ e₁ e₂ ≫ map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄ =
    inl f g ≫ map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) ⋯ ⋯

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

Tactic:
<;>

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

case h₁
C : Type u
inst✝³ : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ inr f g ≫ map f g f' g' i₂ i₃ i₁ e₁ e₂ ≫ map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄ =
    inr f g ≫ map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) ⋯ ⋯
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 ≫ map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯ = inl f g ≫ 𝟙 (pushout f g)

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 ≫ map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯ = inr f g ≫ 𝟙 (pushout f g)

Tactic:
<;>

Goal state after:
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 ≫ map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯ = inl f g ≫ 𝟙 (pushout f g)

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 ≫ map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯ = inr f g ≫ 𝟙 (pushout f g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case h₀
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
s : PushoutCocone g f
m : t.pt ⟶ s.pt
h₁ : t.inr ≫ m = s.inl
h₂ : t.inl ≫ m = s.inr
⊢ t.inl ≫ m = t.inl ≫ ht.desc s.flip

pp: case h₁
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
s : PushoutCocone g f
m : t.pt ⟶ s.pt
h₁ : t.inr ≫ m = s.inl
h₂ : t.inl ≫ m = s.inr
⊢ t.inr ≫ m = t.inr ≫ ht.desc s.flip

Tactic:
<;>

Goal state after:
case h₀
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
s : PushoutCocone g f
m : t.pt ⟶ s.pt
h₁ : t.inr ≫ m = s.inl
h₂ : t.inl ≫ m = s.inr
⊢ t.inl ≫ m = t.inl ≫ ht.desc s.flip

case h₁
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
s : PushoutCocone g f
m : t.pt ⟶ s.pt
h₁ : t.inr ≫ m = s.inl
h₂ : t.inl ≫ m = s.inr
⊢ t.inr ≫ m = t.inr ≫ ht.desc s.flip
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 : WalkingSpan ⥤ C
t : Cocone F
⊢ ((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app none ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt).hom =
    (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app none

pp: case some.left
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingSpan ⥤ C
t : Cocone F
⊢ ((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app (some WalkingPair.left) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt).hom =
    (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app (some WalkingPair.left)

pp: case some.right
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingSpan ⥤ C
t : Cocone F
⊢ ((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app (some WalkingPair.right) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt).hom =
    (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app (some WalkingPair.right)

Tactic:
<;>

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingSpan ⥤ C
t : Cocone F
⊢ ((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app none ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt).hom =
    (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app none

case some.left
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingSpan ⥤ C
t : Cocone F
⊢ ((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app (some WalkingPair.left) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt).hom =
    (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app (some WalkingPair.left)

case some.right
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingSpan ⥤ C
t : Cocone F
⊢ ((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app (some WalkingPair.right) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt).hom =
    (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app (some WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
⊢ left.comp (id one) = left

pp: case right
⊢ right.comp (id one) = right

pp: case id
X : WalkingParallelPair
⊢ (id X).comp (id X) = id X

Tactic:
<;>

Goal state after:
case left
⊢ left.comp (id one) = left

case right
⊢ right.comp (id one) = right

case id
X : WalkingParallelPair
⊢ (id X).comp (id X) = id X
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom one Z
⊢ (left.comp g).comp h = left.comp (g.comp h)

pp: case right
Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom one Z
⊢ (right.comp g).comp h = right.comp (g.comp h)

pp: case id
X Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom X Z
⊢ ((id X).comp g).comp h = (id X).comp (g.comp h)

Tactic:
<;>

Goal state after:
case left
Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom one Z
⊢ (left.comp g).comp h = left.comp (g.comp h)

case right
Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom one Z
⊢ (right.comp g).comp h = right.comp (g.comp h)

case id
X Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom X Z
⊢ ((id X).comp g).comp h = (id X).comp (g.comp h)