mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case leftCompReflexion.id.rightCompReflexion
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.rightCompReflexion =
    Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.rightCompReflexion)

Tactic:
rfl

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

Goal state before:
pp: case leftCompReflexion.id.id
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp (Hom.id one) =
    Hom.leftCompReflexion.comp ((Hom.id one).comp (Hom.id one))

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.left.reflexion
⊢ (Hom.rightCompReflexion.comp Hom.left).comp Hom.reflexion = Hom.rightCompReflexion.comp (Hom.left.comp Hom.reflexion)

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.left.id
⊢ (Hom.rightCompReflexion.comp Hom.left).comp (Hom.id zero) = Hom.rightCompReflexion.comp (Hom.left.comp (Hom.id zero))

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.right.reflexion
⊢ (Hom.rightCompReflexion.comp Hom.right).comp Hom.reflexion =
    Hom.rightCompReflexion.comp (Hom.right.comp Hom.reflexion)

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.right.id
⊢ (Hom.rightCompReflexion.comp Hom.right).comp (Hom.id zero) =
    Hom.rightCompReflexion.comp (Hom.right.comp (Hom.id zero))

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.leftCompReflexion.left
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.left =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.left)

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.leftCompReflexion.right
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.right =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.right)

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.leftCompReflexion.leftCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.leftCompReflexion.rightCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.leftCompReflexion.id
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp (Hom.id one) =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp (Hom.id one))

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.rightCompReflexion.left
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.left =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.left)

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.rightCompReflexion.right
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.right =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.right)

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.rightCompReflexion.leftCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.rightCompReflexion.rightCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.rightCompReflexion.id
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp (Hom.id one) =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp (Hom.id one))

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.id.left
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.left = Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.left)

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.id.right
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.right = Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.right)

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.id.leftCompReflexion
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.leftCompReflexion =
    Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.leftCompReflexion)

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.id.rightCompReflexion
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.rightCompReflexion =
    Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.rightCompReflexion)

Tactic:
rfl

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

Goal state before:
pp: case rightCompReflexion.id.id
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp (Hom.id one) =
    Hom.rightCompReflexion.comp ((Hom.id one).comp (Hom.id one))

Tactic:
rfl

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

Goal state before:
pp: case id.left.reflexion
⊢ ((Hom.id one).comp Hom.left).comp Hom.reflexion = (Hom.id one).comp (Hom.left.comp Hom.reflexion)

Tactic:
rfl

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

Goal state before:
pp: case id.left.id
⊢ ((Hom.id one).comp Hom.left).comp (Hom.id zero) = (Hom.id one).comp (Hom.left.comp (Hom.id zero))

Tactic:
rfl

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

Goal state before:
pp: case id.right.reflexion
⊢ ((Hom.id one).comp Hom.right).comp Hom.reflexion = (Hom.id one).comp (Hom.right.comp Hom.reflexion)

Tactic:
rfl

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

Goal state before:
pp: case id.right.id
⊢ ((Hom.id one).comp Hom.right).comp (Hom.id zero) = (Hom.id one).comp (Hom.right.comp (Hom.id zero))

Tactic:
rfl

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

Goal state before:
pp: case id.reflexion.left
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.left = (Hom.id zero).comp (Hom.reflexion.comp Hom.left)

Tactic:
rfl

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

Goal state before:
pp: case id.reflexion.right
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.right = (Hom.id zero).comp (Hom.reflexion.comp Hom.right)

Tactic:
rfl

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

Goal state before:
pp: case id.reflexion.leftCompReflexion
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.leftCompReflexion =
    (Hom.id zero).comp (Hom.reflexion.comp Hom.leftCompReflexion)

Tactic:
rfl

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

Goal state before:
pp: case id.reflexion.rightCompReflexion
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.rightCompReflexion =
    (Hom.id zero).comp (Hom.reflexion.comp Hom.rightCompReflexion)

Tactic:
rfl

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

Goal state before:
pp: case id.reflexion.id
⊢ ((Hom.id zero).comp Hom.reflexion).comp (Hom.id one) = (Hom.id zero).comp (Hom.reflexion.comp (Hom.id one))

Tactic:
rfl

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

Goal state before:
pp: case id.leftCompReflexion.left
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.left)

Tactic:
rfl

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

Goal state before:
pp: case id.leftCompReflexion.right
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.right)

Tactic:
rfl

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

Goal state before:
pp: case id.leftCompReflexion.leftCompReflexion
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)

Tactic:
rfl

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

Goal state before:
pp: case id.leftCompReflexion.rightCompReflexion
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)

Tactic:
rfl

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

Goal state before:
pp: case id.leftCompReflexion.id
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp (Hom.id one) =
    (Hom.id one).comp (Hom.leftCompReflexion.comp (Hom.id one))

Tactic:
rfl

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

Goal state before:
pp: case id.rightCompReflexion.left
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.left)

Tactic:
rfl

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

Goal state before:
pp: case id.rightCompReflexion.right
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.right)

Tactic:
rfl

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

Goal state before:
pp: case id.rightCompReflexion.leftCompReflexion
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)

Tactic:
rfl

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

Goal state before:
pp: case id.rightCompReflexion.rightCompReflexion
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)

Tactic:
rfl

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

Goal state before:
pp: case id.rightCompReflexion.id
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp (Hom.id one) =
    (Hom.id one).comp (Hom.rightCompReflexion.comp (Hom.id one))

Tactic:
rfl

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

Goal state before:
pp: case id.id.left
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.left = (Hom.id one).comp ((Hom.id one).comp Hom.left)

Tactic:
rfl

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

Goal state before:
pp: case id.id.right
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.right = (Hom.id one).comp ((Hom.id one).comp Hom.right)

Tactic:
rfl

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

Goal state before:
pp: case id.id.reflexion
⊢ ((Hom.id zero).comp (Hom.id zero)).comp Hom.reflexion = (Hom.id zero).comp ((Hom.id zero).comp Hom.reflexion)

Tactic:
rfl

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

Goal state before:
pp: case id.id.leftCompReflexion
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.leftCompReflexion =
    (Hom.id one).comp ((Hom.id one).comp Hom.leftCompReflexion)

Tactic:
rfl

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

Goal state before:
pp: case id.id.rightCompReflexion
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.rightCompReflexion =
    (Hom.id one).comp ((Hom.id one).comp Hom.rightCompReflexion)

Tactic:
rfl

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

Goal state before:
pp: case id.id.id
W✝ : WalkingReflexivePair
⊢ ((Hom.id W✝).comp (Hom.id W✝)).comp (Hom.id W✝) = (Hom.id W✝).comp ((Hom.id W✝).comp (Hom.id W✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
⊢ T.map (T.forget.map (s.π.app j)) ≫ (D.obj j).a = s.pt.a ≫ T.forget.map (s.π.app j)

Tactic:
apply (s.π.app j).h

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
⊢ 𝟙 (G.obj A.A) = 𝟙 (G.obj ((𝟭 D).obj A.1))

Tactic:
rfl

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

Goal state before:
pp: case left.id
⊢ (match one, zero, WalkingParallelPairHom.left ≫ WalkingParallelPairHom.id one with
    | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
    | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
    | x, .(x), WalkingParallelPairHom.id .(x) =>
      Hom.id
        (match x with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)) =
    (match one, zero, WalkingParallelPairHom.left with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) ≫
      match one, one, WalkingParallelPairHom.id one with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)

Tactic:
rfl

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

Goal state before:
pp: case right.id
⊢ (match one, zero, WalkingParallelPairHom.right ≫ WalkingParallelPairHom.id one with
    | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
    | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
    | x, .(x), WalkingParallelPairHom.id .(x) =>
      Hom.id
        (match x with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)) =
    (match one, zero, WalkingParallelPairHom.right with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) ≫
      match one, one, WalkingParallelPairHom.id one with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)

Tactic:
rfl

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

Goal state before:
pp: case id.left
⊢ (match one, zero, WalkingParallelPairHom.id zero ≫ WalkingParallelPairHom.left with
    | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
    | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
    | x, .(x), WalkingParallelPairHom.id .(x) =>
      Hom.id
        (match x with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)) =
    (match zero, zero, WalkingParallelPairHom.id zero with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) ≫
      match one, zero, WalkingParallelPairHom.left with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)

Tactic:
rfl

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

Goal state before:
pp: case id.right
⊢ (match one, zero, WalkingParallelPairHom.id zero ≫ WalkingParallelPairHom.right with
    | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
    | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
    | x, .(x), WalkingParallelPairHom.id .(x) =>
      Hom.id
        (match x with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)) =
    (match zero, zero, WalkingParallelPairHom.id zero with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) ≫
      match one, zero, WalkingParallelPairHom.right with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)

Tactic:
rfl

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

Goal state before:
pp: case id.id
X✝ : WalkingParallelPair
⊢ (match X✝, X✝, WalkingParallelPairHom.id X✝ ≫ WalkingParallelPairHom.id X✝ with
    | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
    | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
    | x, .(x), WalkingParallelPairHom.id .(x) =>
      Hom.id
        (match x with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)) =
    (match X✝, X✝, WalkingParallelPairHom.id X✝ with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) ≫
      match X✝, X✝, WalkingParallelPairHom.id X✝ with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
h₀₁ :
  Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_4 _proof_246) = Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_4 _proof_246)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_246 _proof_247) = Arrow.mk ((mk₂ f f').map' 1 2 _proof_246 _proof_247)
⊢ mk₂ f f' = mk₂ f f'

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ c.π.app ?m.162 ≫ (D ⋙ T.forget).map ?m.164 = c.π.app A ≫ (D.map f).f

pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ ?m.162 ⟶ B

pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ J

Tactic:
rfl

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

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
h : n + 1 ≤ m
f g : ComposableArrows C m
app : f.obj' n ⋯ ≅ g.obj' n ⋯
app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h
w : f.map' n (n + 1) ⋯ h ≫ app'.hom = app.hom ≫ g.map' n (n + 1) ⋯ h
⊢ g.map' n (n + 1) ⋯ h ≫ app'.inv = app.inv ≫ f.map' n (n + 1) ⋯ h

Tactic:
← cancel_epi app.hom,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
h : n + 1 ≤ m
f g : ComposableArrows C m
app : f.obj' n ⋯ ≅ g.obj' n ⋯
app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h
w : f.map' n (n + 1) ⋯ h ≫ app'.hom = app.hom ≫ g.map' n (n + 1) ⋯ h
⊢ app.hom ≫ g.map' n (n + 1) ⋯ h ≫ app'.inv = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

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

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after: