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
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) ≫ fst = 𝟙 (X ⨯ Y) ≫ fst

Tactic:
simp

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

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) ≫ snd = 𝟙 (X ⨯ Y) ≫ snd

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ lift fst snd ≫ snd = 𝟙 (X ⨯ Y) ≫ snd

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ map h k) ≫ fst = lift (f ≫ h) (g ≫ k) ≫ fst

Tactic:
simp

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

Goal state before:
pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ map h k) ≫ snd = lift (f ≫ h) (g ≫ k) ≫ snd

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift fst snd ≫ map g g' = map g g'

Tactic:
simp

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

Tactic:
simp

Goal state after:
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) ≫ snd = map (f ≫ h) (g ≫ k) ≫ snd

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A B X Y : C
f : A ⟶ B
g : X ⟶ Y
inst✝ : HasLimitsOfShape (Discrete WalkingPair) C
⊢ map (𝟙 X) f ≫ map g (𝟙 B) = map g (𝟙 A) ≫ map (𝟙 Y) f

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 W : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasBinaryProduct X W
inst✝¹ : HasBinaryProduct Z W
inst✝ : HasBinaryProduct Y W
⊢ map (f ≫ g) (𝟙 W) = map f (𝟙 W) ≫ map g (𝟙 W)

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 W : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasBinaryProduct W X
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct W Z
⊢ map (𝟙 W) (f ≫ g) = map (𝟙 W) f ≫ map (𝟙 W) 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 : C
f : X ⟶ Y
inst✝¹ : HasBinaryProduct X X
inst✝ : HasBinaryProduct Y Y
⊢ diag X ≫ map f f = f ≫ diag 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 : C
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (X ⨯ Y) (X ⨯ Y)
⊢ diag (X ⨯ Y) ≫ map fst snd = 𝟙 (X ⨯ Y)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasLimitsOfShape (Discrete WalkingPair) C
X X' Y Y' : C
g : X ⟶ Y
g' : X' ⟶ Y'
⊢ diag (X ⨯ X') ≫ map (fst ≫ g) (snd ≫ g') = map g g'

Tactic:
simp

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

Tactic:
simp

Goal state after:
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
⊢ inr ≫ desc g h ≫ f = inr ≫ desc (g ≫ f) (h ≫ f)

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 : C
inst✝ : HasBinaryCoproduct X X
f : X ⟶ Y
⊢ codiag X ≫ f = desc f f

Tactic:
simp

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

Tactic:
simp

Goal state after:
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
⊢ inr ≫ map (𝟙 X) (𝟙 Y) = inr ≫ 𝟙 (X ⨿ Y)

Tactic:
simp

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

Tactic:
simp

Goal state after:
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
⊢ inr ≫ desc inl inr = inr ≫ 𝟙 (X ⨿ Y)

Tactic:
simp

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

Tactic:
simp

Goal state after:
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
⊢ inr ≫ map h k ≫ desc f g = inr ≫ desc (h ≫ f) (k ≫ g)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
inst✝¹ : HasBinaryCoproduct W Y
inst✝ : HasBinaryCoproduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ map g g' ≫ desc inl inr = map g g'

Tactic:
simp

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

Tactic:
simp

Goal state after:
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₃
⊢ inr ≫ map f g ≫ map h k = inr ≫ map (f ≫ h) (g ≫ k)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A B X Y : C
f : A ⟶ B
g : X ⟶ Y
inst✝ : HasColimitsOfShape (Discrete WalkingPair) C
⊢ map (𝟙 X) f ≫ map g (𝟙 B) = map g (𝟙 A) ≫ map (𝟙 Y) f

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 W : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasBinaryCoproduct Z W
inst✝¹ : HasBinaryCoproduct Y W
inst✝ : HasBinaryCoproduct X W
⊢ map (f ≫ g) (𝟙 W) = map f (𝟙 W) ≫ map g (𝟙 W)

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 W : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasBinaryCoproduct W X
inst✝¹ : HasBinaryCoproduct W Y
inst✝ : HasBinaryCoproduct W Z
⊢ map (𝟙 W) (f ≫ g) = map (𝟙 W) f ≫ map (𝟙 W) 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 : C
f : X ⟶ Y
inst✝¹ : HasBinaryCoproduct X X
inst✝ : HasBinaryCoproduct Y Y
⊢ map f f ≫ codiag Y = codiag X ≫ f

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 : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)
⊢ map inl inr ≫ codiag (X ⨿ Y) = 𝟙 (X ⨿ Y)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape (Discrete WalkingPair) C
X X' Y Y' : C
g : X ⟶ Y
g' : X' ⟶ Y'
⊢ map (g ≫ inl) (g' ≫ inr) ≫ codiag (Y ⨿ Y') = 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
inst✝ : HasBinaryProducts C
W X Y Z : C
f : X ⟶ Y
g : Z ⟶ W
⊢ prod.map f g ≫ (prod.braiding Y W).hom = (prod.braiding X Z).hom ≫ prod.map g f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryProducts C
W X Y Z : C
⊢ map (associator W X Y).hom (𝟙 Z) ≫ (associator W (X ⨯ Y) Z).hom ≫ map (𝟙 W) (associator X Y Z).hom =
    (associator (W ⨯ X) Y Z).hom ≫ (associator W X (Y ⨯ Z)).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryProducts C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ map (map f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom = (associator X₁ X₂ X₃).hom ≫ map f₁ (map f₂ f₃)

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 : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct (⊤_ C) P
⊢ lift (terminal.from P) (𝟙 P) ≫ snd = 𝟙 P

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 : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct P (⊤_ C)
⊢ lift (𝟙 P) (terminal.from P) ≫ fst = 𝟙 P

Tactic:
simp

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

Tactic:
simp

Goal state after:
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) ≫ snd = map (rightUnitor X).hom (𝟙 Y) ≫ snd

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
W X Y Z : C
⊢ map (associator W X Y).hom (𝟙 Z) ≫ (associator W (X ⨿ Y) Z).hom ≫ map (𝟙 W) (associator X Y Z).hom =
    (associator (W ⨿ X) Y Z).hom ≫ (associator W X (Y ⨿ Z)).hom

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
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ map (map f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom = (associator X₁ X₂ X₃).hom ≫ map f₁ (map f₂ f₃)

Tactic:
simp

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

Tactic:
simp

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

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

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

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 : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inr ≫ desc (initial.to P) (𝟙 P) = 𝟙 P

Tactic:
simp

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

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

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

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

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

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 : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inl ≫ desc (𝟙 P) (initial.to P) = 𝟙 P

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 : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
f : X ⟶ Y
⊢ map f (𝟙 (⊥_ C)) ≫ (rightUnitor Y).hom = (rightUnitor X).hom ≫ f

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
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:
simp

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

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
F : WalkingSpan ⥤ C
⊢ F.map (init WalkingPair.left) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (init WalkingPair.left)

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
F : WalkingSpan ⥤ C
⊢ F.map (init WalkingPair.right) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).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
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))

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

Goal state after:
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (WidePullbackShape.Hom.id none) ≫
      (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (WidePullbackShape.Hom.id none)

Tactic:
simp

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

Goal state before:
pp: case some.left.none.term
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).map (term WalkingPair.left) ≫
      (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (term WalkingPair.left)

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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (WidePullbackShape.Hom.id (some WalkingPair.left))

Tactic:
simp

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

Goal state before:
pp: case some.right.none.term
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).map (term WalkingPair.right) ≫
      (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (term WalkingPair.right)

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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (WidePullbackShape.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
D : Type u₂
inst✝³ : Category.{w, u₂} D
F : C ⥤ D
A B : C
inst✝² : HasBinaryCoproduct A B
inst✝¹ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝ : IsIso (coprodComparison F A B)
⊢ F.map coprod.inl ≫ inv (coprodComparison F A B) = coprod.inl

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{w, u₂} D
F : C ⥤ D
A B : C
inst✝² : HasBinaryCoproduct A B
inst✝¹ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝ : IsIso (coprodComparison F A B)
⊢ F.map coprod.inr ≫ inv (coprodComparison F A B) = coprod.inr

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✝ : Over A
k : X✝ ⟶ Y✝
g : Over A
⊢ coprod.map (Hom.left k) (𝟙 g.left) ≫ (Y✝.coprodObj.obj g).hom = (X✝.coprodObj.obj g).hom

Tactic:
by
        dsimp; rw [coprod.map_desc, Category.id_comp, Over.w k]

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✝ : Over A
k✝ : X✝ ⟶ Y✝
f g : Over A
k : f ⟶ g
⊢ Hom.left (X✝.coprodObj.map k ≫ homMk (coprod.map (Hom.left k✝) (𝟙 g.left)) ⋯) =
    Hom.left (homMk (coprod.map (Hom.left k✝) (𝟙 f.left)) ⋯ ≫ Y✝.coprodObj.map k)

Tactic:
simp

Goal state after: