Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case left.reflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.left ≫ Hom.reflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f ≫ s

pp: case left.id
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.left ≫ Hom.id zero with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f

pp: case right.reflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.right ≫ Hom.reflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g ≫ s

pp: case right.id
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.right ≫ Hom.id zero with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g

pp: case reflexion.left
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match zero, zero, Hom.reflexion ≫ Hom.left with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    𝟙 B

pp: case reflexion.right
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match zero, zero, Hom.reflexion ≫ Hom.right with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    𝟙 B

pp: case reflexion.leftCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match zero, one, Hom.reflexion ≫ Hom.leftCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    s

pp: case reflexion.rightCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match zero, one, Hom.reflexion ≫ Hom.rightCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    s

pp: case reflexion.id
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match zero, one, Hom.reflexion ≫ Hom.id one with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    s

pp: case leftCompReflexion.left
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.leftCompReflexion ≫ Hom.left with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f

pp: case leftCompReflexion.right
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.leftCompReflexion ≫ Hom.right with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f

pp: case leftCompReflexion.leftCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.leftCompReflexion ≫ Hom.leftCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f ≫ s

pp: case leftCompReflexion.rightCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.leftCompReflexion ≫ Hom.rightCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f ≫ s

pp: case leftCompReflexion.id
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.leftCompReflexion ≫ Hom.id one with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f ≫ s

pp: case rightCompReflexion.left
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.rightCompReflexion ≫ Hom.left with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g

pp: case rightCompReflexion.right
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.rightCompReflexion ≫ Hom.right with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g

pp: case rightCompReflexion.leftCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.rightCompReflexion ≫ Hom.leftCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g ≫ s

pp: case rightCompReflexion.rightCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.rightCompReflexion ≫ Hom.rightCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g ≫ s

pp: case rightCompReflexion.id
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.rightCompReflexion ≫ Hom.id one with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g ≫ s

pp: case id.left
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.id one ≫ Hom.left with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f

pp: case id.right
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.id one ≫ Hom.right with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g

pp: case id.reflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match zero, one, Hom.id zero ≫ Hom.reflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    s

pp: case id.leftCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.id one ≫ Hom.leftCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f ≫ s

pp: case id.rightCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.id one ≫ Hom.rightCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g ≫ s

pp: case id.id
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
X✝ : WalkingReflexivePair
⊢ (match X✝, X✝, Hom.id X✝ ≫ Hom.id X✝ with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    𝟙
      (match X✝ with
      | zero => B
      | one => A)

Tactic:
<;>

Goal state after:
case left.reflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.left ≫ Hom.reflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f ≫ s

case left.id
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.left ≫ Hom.id zero with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f

case right.reflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.right ≫ Hom.reflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g ≫ s

case right.id
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.right ≫ Hom.id zero with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g

case reflexion.left
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match zero, zero, Hom.reflexion ≫ Hom.left with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    𝟙 B

case reflexion.right
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match zero, zero, Hom.reflexion ≫ Hom.right with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    𝟙 B

case reflexion.leftCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match zero, one, Hom.reflexion ≫ Hom.leftCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    s

case reflexion.rightCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match zero, one, Hom.reflexion ≫ Hom.rightCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    s

case reflexion.id
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match zero, one, Hom.reflexion ≫ Hom.id one with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    s

case leftCompReflexion.left
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.leftCompReflexion ≫ Hom.left with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f

case leftCompReflexion.right
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.leftCompReflexion ≫ Hom.right with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f

case leftCompReflexion.leftCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.leftCompReflexion ≫ Hom.leftCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f ≫ s

case leftCompReflexion.rightCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.leftCompReflexion ≫ Hom.rightCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f ≫ s

case leftCompReflexion.id
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.leftCompReflexion ≫ Hom.id one with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f ≫ s

case rightCompReflexion.left
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.rightCompReflexion ≫ Hom.left with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g

case rightCompReflexion.right
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.rightCompReflexion ≫ Hom.right with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g

case rightCompReflexion.leftCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.rightCompReflexion ≫ Hom.leftCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g ≫ s

case rightCompReflexion.rightCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.rightCompReflexion ≫ Hom.rightCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g ≫ s

case rightCompReflexion.id
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.rightCompReflexion ≫ Hom.id one with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g ≫ s

case id.left
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.id one ≫ Hom.left with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f

case id.right
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, zero, Hom.id one ≫ Hom.right with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g

case id.reflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match zero, one, Hom.id zero ≫ Hom.reflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    s

case id.leftCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.id one ≫ Hom.leftCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f ≫ s

case id.rightCompReflexion
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (match one, one, Hom.id one ≫ Hom.rightCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g ≫ s

case id.id
C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
X✝ : WalkingReflexivePair
⊢ (match X✝, X✝, Hom.id X✝ ≫ Hom.id X✝ with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    𝟙
      (match X✝ with
      | zero => B
      | one => A)