Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
x✝¹ x✝ : WalkingReflexivePair
f : x✝¹ ⟶ x✝
⊢ (F.map f ≫
      match x✝ with
      | zero => e₀
      | one => e₁) =
    (match x✝¹ with
      | zero => e₀
      | one => e₁) ≫
      G.map f

Tactic:
cases f

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ (F.map left ≫
      match zero with
      | zero => e₀
      | one => e₁) =
    (match one with
      | zero => e₀
      | one => e₁) ≫
      G.map left

case right
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ (F.map right ≫
      match zero with
      | zero => e₀
      | one => e₁) =
    (match one with
      | zero => e₀
      | one => e₁) ≫
      G.map right

case reflexion
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ (F.map reflexion ≫
      match one with
      | zero => e₀
      | one => e₁) =
    (match zero with
      | zero => e₀
      | one => e₁) ≫
      G.map reflexion

case leftCompReflexion
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ (F.map leftCompReflexion ≫
      match one with
      | zero => e₀
      | one => e₁) =
    (match one with
      | zero => e₀
      | one => e₁) ≫
      G.map leftCompReflexion

case rightCompReflexion
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ (F.map rightCompReflexion ≫
      match one with
      | zero => e₀
      | one => e₁) =
    (match one with
      | zero => e₀
      | one => e₁) ≫
      G.map rightCompReflexion

case id
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
x✝ : WalkingReflexivePair
⊢ (F.map (Hom.id x✝) ≫
      match x✝ with
      | zero => e₀
      | one => e₁) =
    (match x✝ with
      | zero => e₀
      | one => e₁) ≫
      G.map (Hom.id x✝)