Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case one.zero.leftCompReflexion
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ { left := { as := PUnit.unit }, right := zero, hom := leftCompReflexion } ∈ p

pp: case one.zero.rightCompReflexion
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ { left := { as := PUnit.unit }, right := zero, hom := rightCompReflexion } ∈ p

pp: case one.zero.id
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ { left := { as := PUnit.unit }, right := zero,
      hom := Hom.id ((Functor.fromPUnit WalkingReflexivePair.one).obj { as := PUnit.unit }) } ∈
    p

pp: case one.one.left
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ { left := { as := PUnit.unit }, right := one, hom := left } ∈ p

pp: case one.one.right
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ { left := { as := PUnit.unit }, right := one, hom := right } ∈ p

Tactic:
· exact (h₂ (StructuredArrow.homMk .left)).2 hₗ

Goal state after:
case one.zero.rightCompReflexion
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ { left := { as := PUnit.unit }, right := zero, hom := rightCompReflexion } ∈ p

case one.zero.id
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ { left := { as := PUnit.unit }, right := zero,
      hom := Hom.id ((Functor.fromPUnit WalkingReflexivePair.one).obj { as := PUnit.unit }) } ∈
    p

case one.one.left
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ { left := { as := PUnit.unit }, right := one, hom := left } ∈ p

case one.one.right
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ { left := { as := PUnit.unit }, right := one, hom := right } ∈ p