mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: case right.right
R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ (((Functor.const (Discrete WalkingPair)).obj (of R (↑M × ↑N))).map { down := { down := ⋯ } } ≫
      Discrete.casesOn { as := WalkingPair.right } fun j ↦
        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N))) =
    (Discrete.casesOn { as := WalkingPair.right } fun j ↦
        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N))) ≫
      (pair M N).map { down := { down := ⋯ } }

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: case left
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
⊢ ↟((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right }))) ≫
      { pt := of R (↑M × ↑N),
              π :=
                {
                  app := fun j ↦
                    Discrete.casesOn j fun j ↦
                      WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                  naturality := ⋯ } }.π.app
        { as := WalkingPair.left } =
    s.π.app { as := WalkingPair.left }

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: case right
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
⊢ ↟((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right }))) ≫
      { pt := of R (↑M × ↑N),
              π :=
                {
                  app := fun j ↦
                    Discrete.casesOn j fun j ↦
                      WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                  naturality := ⋯ } }.π.app
        { as := WalkingPair.right } =
    s.π.app { as := WalkingPair.right }

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b) =
    K.ι (J.fst b) ≫ I.fst b

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.left (J.snd b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.snd b) =
    K.ι (J.snd b) ≫ I.snd b

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R (↑M × ↑N),
        π :=
          {
            app := fun j ↦
              Discrete.casesOn j fun j ↦ WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
            naturality := ⋯ } }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        { pt := of R (↑M × ↑N),
                π :=
                  {
                    app := fun j ↦
                      Discrete.casesOn j fun j ↦
                        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
⊢ m = ↟((Hom.hom (m ≫ ↟(LinearMap.fst R ↑M ↑N))).prod (Hom.hom (m ≫ ↟(LinearMap.snd R ↑M ↑N))))

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
x y : ↑s.1
⊢ (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) x + (ConcreteCategory.hom (s.π.app { as := j })) y) =
    (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) x) + fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) y

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
r : R
x : ↑s.1
⊢ (fun j ↦ r • (ConcreteCategory.hom (s.π.app { as := j })) x) =
    (RingHom.id R) r • fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Cone (Discrete.functor f)
m : s.pt ⟶ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j ↦ ↟(LinearMap.proj j.as) }.pt
w :
  ∀ (j : Discrete J),
    m ≫ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j ↦ ↟(LinearMap.proj j.as) }.π.app j = s.π.app j
x : ↑s.pt
j : J
⊢ (Hom.hom m) x j = (Hom.hom (lift f s)) x j

Tactic:
exact congr_arg (fun g : s.pt ⟶ f j => (g : s.pt → f j) x) (w ⟨j⟩)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a)) = I.fst a ≫ K.π (J.fst a)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.snd a) ≫ K.ι.app (WalkingMultispan.right (J.snd a)) = I.snd a ≫ K.π (J.snd a)

Tactic:
rfl

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

Goal state before:
pp: case «0»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
⊢ (isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app ((fun i ↦ i) ⟨0, ⋯⟩) = eqToHom ⋯

Tactic:
rfl

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

Goal state before:
pp: case «1»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
⊢ (isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app ((fun i ↦ i) ⟨1, ⋯⟩) = eqToHom ⋯

Tactic:
rfl

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

Goal state before:
pp: case zero.succ.zero.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
hj : 0 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨0 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : ⟨0 + 1, hj⟩ ≤ ⟨k + 1 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨k + 1 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0 + 1, hj⟩ hij ≫ map F f ⟨0 + 1, hj⟩ ⟨k + 1 + 1, hk⟩ hjk

Tactic:
rfl

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
⊢ IsIso (reflectorAdjunction R).toMonad.μ

Tactic:
by
  dsimp
  infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
⊢ IsIso (coreflectorAdjunction R).toComonad.δ

Tactic:
by
  dsimp
  infer_instance

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : J.L
⊢ equalizer.ι I.fstPiMap I.sndPiMap ≫ Pi.π I.left a =
    Fork.ι (limit.cone (parallelPair I.fstPiMap I.sndPiMap)) ≫ Fan.proj (limit.cone (Discrete.functor I.left)) a

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : J.R
⊢ Sigma.ι I.right b ≫ coequalizer.π I.fstSigmaMap I.sndSigmaMap =
    Cofan.inj (colimit.cocone (Discrete.functor I.right)) b ≫
      Cofork.π (colimit.cocone (parallelPair I.fstSigmaMap I.sndSigmaMap))

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
j : J
⊢ (T.toFunctor ⋙ T.toFunctor).map (c.π.app j) ≫ T.map (D.obj j).a ≫ (D.obj j).a =
    T.map (T.map (c.π.app j)) ≫ T.map (D.obj j).a ≫ (D.obj j).a

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after: