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

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryProduct A₁ B₁
inst✝¹ : HasBinaryProduct A₂ B₂
inst✝ : HasBinaryProduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ (map f g ≫ map h k) ≫ fst = map (f ≫ h) (g ≫ k) ≫ fst

pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryProduct A₁ B₁
inst✝¹ : HasBinaryProduct A₂ B₂
inst✝ : HasBinaryProduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ (map f g ≫ map h k) ≫ snd = map (f ≫ h) (g ≫ k) ≫ snd

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝³ : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryProduct A₁ B₁
inst✝¹ : HasBinaryProduct A₂ B₂
inst✝ : HasBinaryProduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ (map f g ≫ map h k) ≫ fst = map (f ≫ h) (g ≫ k) ≫ fst

case h₂
C : Type u
inst✝³ : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryProduct A₁ B₁
inst✝¹ : HasBinaryProduct A₂ B₂
inst✝ : HasBinaryProduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ (map f g ≫ map h k) ≫ snd = map (f ≫ h) (g ≫ k) ≫ snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
V W X Y : C
inst✝ : HasBinaryCoproduct X Y
f : V ⟶ W
g : X ⟶ V
h : Y ⟶ V
⊢ inl ≫ desc g h ≫ f = inl ≫ desc (g ≫ f) (h ≫ f)

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
V W X Y : C
inst✝ : HasBinaryCoproduct X Y
f : V ⟶ W
g : X ⟶ V
h : Y ⟶ V
⊢ inr ≫ desc g h ≫ f = inr ≫ desc (g ≫ f) (h ≫ f)

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
V W X Y : C
inst✝ : HasBinaryCoproduct X Y
f : V ⟶ W
g : X ⟶ V
h : Y ⟶ V
⊢ inl ≫ desc g h ≫ f = inl ≫ desc (g ≫ f) (h ≫ f)

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
V W X Y : C
inst✝ : HasBinaryCoproduct X Y
f : V ⟶ W
g : X ⟶ V
h : Y ⟶ V
⊢ inr ≫ desc g h ≫ f = inr ≫ desc (g ≫ f) (h ≫ f)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inl ≫ map (𝟙 X) (𝟙 Y) = inl ≫ 𝟙 (X ⨿ Y)

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inr ≫ map (𝟙 X) (𝟙 Y) = inr ≫ 𝟙 (X ⨿ Y)

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inl ≫ map (𝟙 X) (𝟙 Y) = inl ≫ 𝟙 (X ⨿ Y)

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inr ≫ map (𝟙 X) (𝟙 Y) = inr ≫ 𝟙 (X ⨿ Y)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inl ≫ desc inl inr = inl ≫ 𝟙 (X ⨿ Y)

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inr ≫ desc inl inr = inr ≫ 𝟙 (X ⨿ Y)

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inl ≫ desc inl inr = inl ≫ 𝟙 (X ⨿ Y)

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inr ≫ desc inl inr = inr ≫ 𝟙 (X ⨿ Y)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
S T U V W : C
inst✝¹ : HasBinaryCoproduct U W
inst✝ : HasBinaryCoproduct T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ inl ≫ map h k ≫ desc f g = inl ≫ desc (h ≫ f) (k ≫ g)

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
S T U V W : C
inst✝¹ : HasBinaryCoproduct U W
inst✝ : HasBinaryCoproduct T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ inr ≫ map h k ≫ desc f g = inr ≫ desc (h ≫ f) (k ≫ g)

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
S T U V W : C
inst✝¹ : HasBinaryCoproduct U W
inst✝ : HasBinaryCoproduct T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ inl ≫ map h k ≫ desc f g = inl ≫ desc (h ≫ f) (k ≫ g)

case h₂
C : Type u
inst✝² : Category.{v, u} C
S T U V W : C
inst✝¹ : HasBinaryCoproduct U W
inst✝ : HasBinaryCoproduct T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ inr ≫ map h k ≫ desc f g = inr ≫ desc (h ≫ f) (k ≫ g)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryCoproduct A₁ B₁
inst✝¹ : HasBinaryCoproduct A₂ B₂
inst✝ : HasBinaryCoproduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ inl ≫ map f g ≫ map h k = inl ≫ map (f ≫ h) (g ≫ k)

pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryCoproduct A₁ B₁
inst✝¹ : HasBinaryCoproduct A₂ B₂
inst✝ : HasBinaryCoproduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ inr ≫ map f g ≫ map h k = inr ≫ map (f ≫ h) (g ≫ k)

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝³ : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryCoproduct A₁ B₁
inst✝¹ : HasBinaryCoproduct A₂ B₂
inst✝ : HasBinaryCoproduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ inl ≫ map f g ≫ map h k = inl ≫ map (f ≫ h) (g ≫ k)

case h₂
C : Type u
inst✝³ : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryCoproduct A₁ B₁
inst✝¹ : HasBinaryCoproduct A₂ B₂
inst✝ : HasBinaryCoproduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ inr ≫ map f g ≫ map h k = inr ≫ map (f ≫ h) (g ≫ k)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.obj none = (cospan (F.map inl) (F.map inr)).obj none

pp: case some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.obj (some WalkingPair.left) = (cospan (F.map inl) (F.map inr)).obj (some WalkingPair.left)

pp: case some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.obj (some WalkingPair.right) = (cospan (F.map inl) (F.map inr)).obj (some WalkingPair.right)

Tactic:
<;>

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.obj none = (cospan (F.map inl) (F.map inr)).obj none

case some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.obj (some WalkingPair.left) = (cospan (F.map inl) (F.map inr)).obj (some WalkingPair.left)

case some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.obj (some WalkingPair.right) = (cospan (F.map inl) (F.map inr)).obj (some WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct (⊤_ C) P
⊢ (snd ≫ lift (terminal.from P) (𝟙 P)) ≫ fst = 𝟙 ((⊤_ C) ⨯ P) ≫ fst

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct (⊤_ C) P
⊢ (snd ≫ lift (terminal.from P) (𝟙 P)) ≫ snd = 𝟙 ((⊤_ C) ⨯ P) ≫ snd

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct (⊤_ C) P
⊢ (snd ≫ lift (terminal.from P) (𝟙 P)) ≫ fst = 𝟙 ((⊤_ C) ⨯ P) ≫ fst

case h₂
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct (⊤_ C) P
⊢ (snd ≫ lift (terminal.from P) (𝟙 P)) ≫ snd = 𝟙 ((⊤_ C) ⨯ P) ≫ snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct P (⊤_ C)
⊢ (fst ≫ lift (𝟙 P) (terminal.from P)) ≫ fst = 𝟙 (P ⨯ ⊤_ C) ≫ fst

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct P (⊤_ C)
⊢ (fst ≫ lift (𝟙 P) (terminal.from P)) ≫ snd = 𝟙 (P ⨯ ⊤_ C) ≫ snd

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct P (⊤_ C)
⊢ (fst ≫ lift (𝟙 P) (terminal.from P)) ≫ fst = 𝟙 (P ⨯ ⊤_ C) ≫ fst

case h₂
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct P (⊤_ C)
⊢ (fst ≫ lift (𝟙 P) (terminal.from P)) ≫ snd = 𝟙 (P ⨯ ⊤_ C) ≫ snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ ((associator X (⊤_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom) ≫ fst = map (rightUnitor X).hom (𝟙 Y) ≫ fst

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ ((associator X (⊤_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom) ≫ snd = map (rightUnitor X).hom (𝟙 Y) ≫ snd

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ ((associator X (⊤_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom) ≫ fst = map (rightUnitor X).hom (𝟙 Y) ≫ fst

case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ ((associator X (⊤_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom) ≫ snd = map (rightUnitor X).hom (𝟙 Y) ≫ snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inl ≫ desc (initial.to P) (𝟙 P) ≫ inr = inl ≫ 𝟙 ((⊥_ C) ⨿ P)

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inr ≫ desc (initial.to P) (𝟙 P) ≫ inr = inr ≫ 𝟙 ((⊥_ C) ⨿ P)

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inl ≫ desc (initial.to P) (𝟙 P) ≫ inr = inl ≫ 𝟙 ((⊥_ C) ⨿ P)

case h₂
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inr ≫ desc (initial.to P) (𝟙 P) ≫ inr = inr ≫ 𝟙 ((⊥_ C) ⨿ P)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none.none.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (WidePullbackShape.Hom.id none) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id none)

pp: case some.left.none.term
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (term WalkingPair.left) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (term WalkingPair.left)

pp: case some.left.some.left.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id (some WalkingPair.left))

pp: case some.right.none.term
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (term WalkingPair.right) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (term WalkingPair.right)

pp: case some.right.some.right.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id (some WalkingPair.right))

Tactic:
<;>

Goal state after:
case none.none.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (WidePullbackShape.Hom.id none) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id none)

case some.left.none.term
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (term WalkingPair.left) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (term WalkingPair.left)

case some.left.some.left.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id (some WalkingPair.left))

case some.right.none.term
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (term WalkingPair.right) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (term WalkingPair.right)

case some.right.some.right.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id (some WalkingPair.right))
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inl ≫ desc (𝟙 P) (initial.to P) ≫ inl = inl ≫ 𝟙 (P ⨿ ⊥_ C)

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inr ≫ desc (𝟙 P) (initial.to P) ≫ inl = inr ≫ 𝟙 (P ⨿ ⊥_ C)

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inl ≫ desc (𝟙 P) (initial.to P) ≫ inl = inl ≫ 𝟙 (P ⨿ ⊥_ C)

case h₂
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inr ≫ desc (𝟙 P) (initial.to P) ≫ inl = inr ≫ 𝟙 (P ⨿ ⊥_ C)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.obj none = (span (F.map fst) (F.map snd)).obj none

pp: case some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.obj (some WalkingPair.left) = (span (F.map fst) (F.map snd)).obj (some WalkingPair.left)

pp: case some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.obj (some WalkingPair.right) = (span (F.map fst) (F.map snd)).obj (some WalkingPair.right)

Tactic:
<;>

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.obj none = (span (F.map fst) (F.map snd)).obj none

case some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.obj (some WalkingPair.left) = (span (F.map fst) (F.map snd)).obj (some WalkingPair.left)

case some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.obj (some WalkingPair.right) = (span (F.map fst) (F.map snd)).obj (some WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ inl ≫ inl ≫ (associator X (⊥_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom = inl ≫ inl ≫ map (rightUnitor X).hom (𝟙 Y)

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ inr ≫ (associator X (⊥_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom = inr ≫ map (rightUnitor X).hom (𝟙 Y)

Tactic:
<;>

Goal state after:
case h₁.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ inl ≫ inl ≫ (associator X (⊥_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom = inl ≫ inl ≫ map (rightUnitor X).hom (𝟙 Y)

case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ inr ≫ (associator X (⊥_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom = inr ≫ map (rightUnitor X).hom (𝟙 Y)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none.none.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (WidePushoutShape.Hom.id none) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id none)

pp: case none.some.left.init
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (init WalkingPair.left) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (init WalkingPair.left)

pp: case none.some.right.init
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (init WalkingPair.right) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (init WalkingPair.right)

pp: case some.left.some.left.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id (some WalkingPair.left))

pp: case some.right.some.right.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id (some WalkingPair.right))

Tactic:
<;>

Goal state after:
case none.none.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (WidePushoutShape.Hom.id none) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id none)

case none.some.left.init
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (init WalkingPair.left) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (init WalkingPair.left)

case none.some.right.init
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (init WalkingPair.right) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (init WalkingPair.right)

case some.left.some.left.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id (some WalkingPair.left))

case some.right.some.right.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id (some WalkingPair.right))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).obj none ≅ (cospan (F.map f) (F.map g)).obj none

pp: case some.left
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).obj (some WalkingPair.left) ≅ (cospan (F.map f) (F.map g)).obj (some WalkingPair.left)

pp: case some.right
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).obj (some WalkingPair.right) ≅ (cospan (F.map f) (F.map g)).obj (some WalkingPair.right)

Tactic:
<;>

Goal state after:
case none
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).obj none ≅ (cospan (F.map f) (F.map g)).obj none

case some.left
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).obj (some WalkingPair.left) ≅ (cospan (F.map f) (F.map g)).obj (some WalkingPair.left)

case some.right
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).obj (some WalkingPair.right) ≅ (cospan (F.map f) (F.map g)).obj (some WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
E : Type u₃
inst✝⁴ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
A B : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))
inst✝ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)
⊢ prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd) ≫ prod.fst =
    (G.map (prod.lift (F.map prod.fst) (F.map prod.snd)) ≫ prod.lift (G.map prod.fst) (G.map prod.snd)) ≫ prod.fst

pp: case h₂
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
E : Type u₃
inst✝⁴ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
A B : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))
inst✝ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)
⊢ prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd) ≫ prod.snd =
    (G.map (prod.lift (F.map prod.fst) (F.map prod.snd)) ≫ prod.lift (G.map prod.fst) (G.map prod.snd)) ≫ prod.snd

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
E : Type u₃
inst✝⁴ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
A B : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))
inst✝ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)
⊢ prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd) ≫ prod.fst =
    (G.map (prod.lift (F.map prod.fst) (F.map prod.snd)) ≫ prod.lift (G.map prod.fst) (G.map prod.snd)) ≫ prod.fst

case h₂
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
E : Type u₃
inst✝⁴ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
A B : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))
inst✝ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)
⊢ prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd) ≫ prod.snd =
    (G.map (prod.lift (F.map prod.fst) (F.map prod.snd)) ≫ prod.lift (G.map prod.fst) (G.map prod.snd)) ≫ prod.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none
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).obj none ≅ (span (F.map f) (F.map g)).obj none

pp: case some.left
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).obj (some WalkingPair.left) ≅ (span (F.map f) (F.map g)).obj (some WalkingPair.left)

pp: case some.right
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).obj (some WalkingPair.right) ≅ (span (F.map f) (F.map g)).obj (some WalkingPair.right)

Tactic:
<;>

Goal state after:
case none
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).obj none ≅ (span (F.map f) (F.map g)).obj none

case some.left
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).obj (some WalkingPair.left) ≅ (span (F.map f) (F.map g)).obj (some WalkingPair.left)

case some.right
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).obj (some WalkingPair.right) ≅ (span (F.map f) (F.map g)).obj (some WalkingPair.right)
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 }

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

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)
⊢ I.lift (BinaryFan.swap t) ≫ s.swap.π.app { as := WalkingPair.left } = 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)
⊢ I.lift (BinaryFan.swap t) ≫ s.swap.π.app { as := WalkingPair.right } = t.π.app { as := WalkingPair.right }