Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case 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
Z✝ : WalkingReflexivePair
g : zero ⟶ Z✝
⊢ (match one, Z✝, Hom.left ≫ g 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 one, zero, 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) ≫
      match zero, Z✝, g 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

pp: case 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
Z✝ : WalkingReflexivePair
g : zero ⟶ Z✝
⊢ (match one, Z✝, Hom.right ≫ g 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 one, zero, 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) ≫
      match zero, Z✝, g 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

pp: case 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
Z✝ : WalkingReflexivePair
g : one ⟶ Z✝
⊢ (match zero, Z✝, Hom.reflexion ≫ g 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 zero, one, 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) ≫
      match one, Z✝, g 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

pp: case 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
Z✝ : WalkingReflexivePair
g : one ⟶ Z✝
⊢ (match one, Z✝, Hom.leftCompReflexion ≫ g 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 one, 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) ≫
      match one, Z✝, g 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

pp: case 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
Z✝ : WalkingReflexivePair
g : one ⟶ Z✝
⊢ (match one, Z✝, Hom.rightCompReflexion ≫ g 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 one, 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) ≫
      match one, Z✝, g 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

pp: case 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✝ Z✝ : WalkingReflexivePair
g : X✝ ⟶ Z✝
⊢ (match X✝, Z✝, Hom.id X✝ ≫ g 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✝, 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✝, Z✝, g 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

Tactic:
<;>

Goal state after:
case 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
Z✝ : WalkingReflexivePair
g : zero ⟶ Z✝
⊢ (match one, Z✝, Hom.left ≫ g 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 one, zero, 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) ≫
      match zero, Z✝, g 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

case 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
Z✝ : WalkingReflexivePair
g : zero ⟶ Z✝
⊢ (match one, Z✝, Hom.right ≫ g 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 one, zero, 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) ≫
      match zero, Z✝, g 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

case 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
Z✝ : WalkingReflexivePair
g : one ⟶ Z✝
⊢ (match zero, Z✝, Hom.reflexion ≫ g 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 zero, one, 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) ≫
      match one, Z✝, g 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

case 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
Z✝ : WalkingReflexivePair
g : one ⟶ Z✝
⊢ (match one, Z✝, Hom.leftCompReflexion ≫ g 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 one, 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) ≫
      match one, Z✝, g 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

case 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
Z✝ : WalkingReflexivePair
g : one ⟶ Z✝
⊢ (match one, Z✝, Hom.rightCompReflexion ≫ g 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 one, 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) ≫
      match one, Z✝, g 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

case 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✝ Z✝ : WalkingReflexivePair
g : X✝ ⟶ Z✝
⊢ (match X✝, Z✝, Hom.id X✝ ≫ g 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✝, 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✝, Z✝, g 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