[GOAL]
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
⊢ IsLimit (limitCone F)
[PROOFSTEP]
refine'
  IsLimit.ofFaithful (forget (AlgebraCat R))
    (Types.limitConeIsLimit.{v, w} _)
      -- Porting note: in mathlib3 the function term
            -- `fun v => ⟨fun j => ((forget (AlgebraCat R)).mapCone s).π.app j v`
            -- was provided by unification, and the last argument `(fun s => _)` was `(fun s => rfl)`.
    (fun s => ⟨⟨⟨⟨fun v => ⟨fun j => ((forget (AlgebraCat R)).mapCone s).π.app j v, _⟩, _⟩, _⟩, _, _⟩, _⟩) (fun s => _)
[GOAL]
case refine'_1
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
v : ↑s.pt
⊢ (fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v) ∈ Functor.sections (F ⋙ forget (AlgebraCatMax R))
[PROOFSTEP]
intro j j' f
[GOAL]
case refine'_1
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
v : ↑s.pt
j j' : J
f : j ⟶ j'
⊢ (F ⋙ forget (AlgebraCatMax R)).map f ((fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v) j) =
    (fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v) j'
[PROOFSTEP]
exact FunLike.congr_fun (Cone.w s f) v
[GOAL]
case refine'_2
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
⊢ (fun v =>
        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
          property := (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
      1 =
    1
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case refine'_2.a
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
⊢ ↑((fun v =>
          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
            property := (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
        1) =
    ↑1
[PROOFSTEP]
ext j
[GOAL]
case refine'_2.a.h
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
j : J
⊢ ↑((fun v =>
            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
              property :=
                (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
          1)
      j =
    ↑1 j
[PROOFSTEP]
simp [forget_map_eq_coe, AlgHom.map_one, Functor.mapCone_π_app]
[GOAL]
case refine'_2.a.h
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
j : J
⊢ 1 = ↑1 j
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
⊢ ∀ (x y : ↑s.pt),
    OneHom.toFun
        {
          toFun := fun v =>
            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
              property :=
                (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
          map_one' :=
            (_ :
              (fun v =>
                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                      property :=
                        (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                  1 =
                1) }
        (x * y) =
      OneHom.toFun
          {
            toFun := fun v =>
              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                property :=
                  (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
            map_one' :=
              (_ :
                (fun v =>
                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                        property :=
                          (_ :
                            ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                    1 =
                  1) }
          x *
        OneHom.toFun
          {
            toFun := fun v =>
              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                property :=
                  (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
            map_one' :=
              (_ :
                (fun v =>
                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                        property :=
                          (_ :
                            ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                    1 =
                  1) }
          y
[PROOFSTEP]
intro x y
[GOAL]
case refine'_3
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
x y : ↑s.pt
⊢ OneHom.toFun
      {
        toFun := fun v =>
          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
            property := (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
        map_one' :=
          (_ :
            (fun v =>
                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                    property :=
                      (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                1 =
              1) }
      (x * y) =
    OneHom.toFun
        {
          toFun := fun v =>
            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
              property :=
                (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
          map_one' :=
            (_ :
              (fun v =>
                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                      property :=
                        (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                  1 =
                1) }
        x *
      OneHom.toFun
        {
          toFun := fun v =>
            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
              property :=
                (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
          map_one' :=
            (_ :
              (fun v =>
                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                      property :=
                        (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                  1 =
                1) }
        y
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case refine'_3.a
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
x y : ↑s.pt
⊢ ↑(OneHom.toFun
        {
          toFun := fun v =>
            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
              property :=
                (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
          map_one' :=
            (_ :
              (fun v =>
                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                      property :=
                        (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                  1 =
                1) }
        (x * y)) =
    ↑(OneHom.toFun
          {
            toFun := fun v =>
              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                property :=
                  (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
            map_one' :=
              (_ :
                (fun v =>
                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                        property :=
                          (_ :
                            ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                    1 =
                  1) }
          x *
        OneHom.toFun
          {
            toFun := fun v =>
              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                property :=
                  (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
            map_one' :=
              (_ :
                (fun v =>
                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                        property :=
                          (_ :
                            ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                    1 =
                  1) }
          y)
[PROOFSTEP]
ext j
[GOAL]
case refine'_3.a.h
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
x y : ↑s.pt
j : J
⊢ ↑(OneHom.toFun
          {
            toFun := fun v =>
              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                property :=
                  (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
            map_one' :=
              (_ :
                (fun v =>
                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                        property :=
                          (_ :
                            ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                    1 =
                  1) }
          (x * y))
      j =
    ↑(OneHom.toFun
            {
              toFun := fun v =>
                { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                  property :=
                    (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
              map_one' :=
                (_ :
                  (fun v =>
                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                          property :=
                            (_ :
                              ∀ {j j' : J} (f : j ⟶ j'),
                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                      1 =
                    1) }
            x *
          OneHom.toFun
            {
              toFun := fun v =>
                { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                  property :=
                    (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
              map_one' :=
                (_ :
                  (fun v =>
                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                          property :=
                            (_ :
                              ∀ {j j' : J} (f : j ⟶ j'),
                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                      1 =
                    1) }
            y)
      j
[PROOFSTEP]
simp [forget_map_eq_coe, AlgHom.map_mul, Functor.mapCone_π_app]
[GOAL]
case refine'_3.a.h
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
x y : ↑s.pt
j : J
⊢ ↑(NatTrans.app s.π j) x * ↑(NatTrans.app s.π j) y =
    ↑({ val := fun j => ↑(NatTrans.app s.π j) x,
            property :=
              (_ : (fun x => x ∈ Functor.sections (F ⋙ forget (AlgebraCatMax R))) fun j => ↑(NatTrans.app s.π j) x) } *
          { val := fun j => ↑(NatTrans.app s.π j) y,
            property :=
              (_ : (fun x => x ∈ Functor.sections (F ⋙ forget (AlgebraCatMax R))) fun j => ↑(NatTrans.app s.π j) y) })
      j
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            {
              toFun := fun v =>
                { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                  property :=
                    (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
              map_one' :=
                (_ :
                  (fun v =>
                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                          property :=
                            (_ :
                              ∀ {j j' : J} (f : j ⟶ j'),
                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                      1 =
                    1) },
          map_mul' :=
            (_ :
              ∀ (x y : ↑s.pt),
                OneHom.toFun
                    {
                      toFun := fun v =>
                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                          property :=
                            (_ :
                              ∀ {j j' : J} (f : j ⟶ j'),
                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                      map_one' :=
                        (_ :
                          (fun v =>
                                { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                              1 =
                            1) }
                    (x * y) =
                  OneHom.toFun
                      {
                        toFun := fun v =>
                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                        map_one' :=
                          (_ :
                            (fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                1 =
                              1) }
                      x *
                    OneHom.toFun
                      {
                        toFun := fun v =>
                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                        map_one' :=
                          (_ :
                            (fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                1 =
                              1) }
                      y) })
      0 =
    0
[PROOFSTEP]
simp [forget_map_eq_coe, AlgHom.map_zero, Functor.mapCone_π_app]
[GOAL]
case refine'_4
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
⊢ { val := fun j => 0, property := (_ : (fun x => x ∈ Functor.sections (F ⋙ forget (AlgebraCatMax R))) fun j => 0) } = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_5
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
⊢ ∀ (x y : ↑s.pt),
    OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun v =>
                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                    property :=
                      (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                map_one' :=
                  (_ :
                    (fun v =>
                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑s.pt),
                  OneHom.toFun
                      {
                        toFun := fun v =>
                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                        map_one' :=
                          (_ :
                            (fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                1 =
                              1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun v =>
                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                              property :=
                                (_ :
                                  ∀ {j j' : J} (f : j ⟶ j'),
                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                          map_one' :=
                            (_ :
                              (fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                  1 =
                                1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun v =>
                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                              property :=
                                (_ :
                                  ∀ {j j' : J} (f : j ⟶ j'),
                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                          map_one' :=
                            (_ :
                              (fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                  1 =
                                1) }
                        y) })
        (x + y) =
      OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun v =>
                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                      property :=
                        (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                  map_one' :=
                    (_ :
                      (fun v =>
                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                              property :=
                                (_ :
                                  ∀ {j j' : J} (f : j ⟶ j'),
                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                          1 =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ↑s.pt),
                    OneHom.toFun
                        {
                          toFun := fun v =>
                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                              property :=
                                (_ :
                                  ∀ {j j' : J} (f : j ⟶ j'),
                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                          map_one' :=
                            (_ :
                              (fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                  1 =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun v =>
                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                            map_one' :=
                              (_ :
                                (fun v =>
                                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                        property :=
                                          (_ :
                                            ∀ {j j' : J} (f : j ⟶ j'),
                                              ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                    1 =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun v =>
                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                            map_one' :=
                              (_ :
                                (fun v =>
                                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                        property :=
                                          (_ :
                                            ∀ {j j' : J} (f : j ⟶ j'),
                                              ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                    1 =
                                  1) }
                          y) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun v =>
                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                      property :=
                        (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                  map_one' :=
                    (_ :
                      (fun v =>
                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                              property :=
                                (_ :
                                  ∀ {j j' : J} (f : j ⟶ j'),
                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                          1 =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ↑s.pt),
                    OneHom.toFun
                        {
                          toFun := fun v =>
                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                              property :=
                                (_ :
                                  ∀ {j j' : J} (f : j ⟶ j'),
                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                          map_one' :=
                            (_ :
                              (fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                  1 =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun v =>
                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                            map_one' :=
                              (_ :
                                (fun v =>
                                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                        property :=
                                          (_ :
                                            ∀ {j j' : J} (f : j ⟶ j'),
                                              ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                    1 =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun v =>
                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                            map_one' :=
                              (_ :
                                (fun v =>
                                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                        property :=
                                          (_ :
                                            ∀ {j j' : J} (f : j ⟶ j'),
                                              ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                    1 =
                                  1) }
                          y) })
          y
[PROOFSTEP]
intro x y
[GOAL]
case refine'_5
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
x y : ↑s.pt
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            {
              toFun := fun v =>
                { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                  property :=
                    (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
              map_one' :=
                (_ :
                  (fun v =>
                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                          property :=
                            (_ :
                              ∀ {j j' : J} (f : j ⟶ j'),
                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                      1 =
                    1) },
          map_mul' :=
            (_ :
              ∀ (x y : ↑s.pt),
                OneHom.toFun
                    {
                      toFun := fun v =>
                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                          property :=
                            (_ :
                              ∀ {j j' : J} (f : j ⟶ j'),
                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                      map_one' :=
                        (_ :
                          (fun v =>
                                { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                              1 =
                            1) }
                    (x * y) =
                  OneHom.toFun
                      {
                        toFun := fun v =>
                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                        map_one' :=
                          (_ :
                            (fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                1 =
                              1) }
                      x *
                    OneHom.toFun
                      {
                        toFun := fun v =>
                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                        map_one' :=
                          (_ :
                            (fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                1 =
                              1) }
                      y) })
      (x + y) =
    OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun v =>
                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                    property :=
                      (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                map_one' :=
                  (_ :
                    (fun v =>
                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑s.pt),
                  OneHom.toFun
                      {
                        toFun := fun v =>
                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                        map_one' :=
                          (_ :
                            (fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                1 =
                              1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun v =>
                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                              property :=
                                (_ :
                                  ∀ {j j' : J} (f : j ⟶ j'),
                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                          map_one' :=
                            (_ :
                              (fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                  1 =
                                1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun v =>
                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                              property :=
                                (_ :
                                  ∀ {j j' : J} (f : j ⟶ j'),
                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                          map_one' :=
                            (_ :
                              (fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                  1 =
                                1) }
                        y) })
        x +
      OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun v =>
                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                    property :=
                      (_ : ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                map_one' :=
                  (_ :
                    (fun v =>
                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑s.pt),
                  OneHom.toFun
                      {
                        toFun := fun v =>
                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                        map_one' :=
                          (_ :
                            (fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                1 =
                              1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun v =>
                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                              property :=
                                (_ :
                                  ∀ {j j' : J} (f : j ⟶ j'),
                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                          map_one' :=
                            (_ :
                              (fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                  1 =
                                1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun v =>
                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                              property :=
                                (_ :
                                  ∀ {j j' : J} (f : j ⟶ j'),
                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                          map_one' :=
                            (_ :
                              (fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                  1 =
                                1) }
                        y) })
        y
[PROOFSTEP]
simp [forget_map_eq_coe, AlgHom.map_add, Functor.mapCone_π_app]
[GOAL]
case refine'_5
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
x y : ↑s.pt
⊢ { val := fun j => ↑(NatTrans.app s.π j) x + ↑(NatTrans.app s.π j) y,
      property :=
        (_ :
          (fun x => x ∈ Functor.sections (F ⋙ forget (AlgebraCatMax R))) fun j =>
            ↑(NatTrans.app s.π j) x + ↑(NatTrans.app s.π j) y) } =
    { val := fun j => ↑(NatTrans.app s.π j) x,
        property :=
          (_ : (fun x => x ∈ Functor.sections (F ⋙ forget (AlgebraCatMax R))) fun j => ↑(NatTrans.app s.π j) x) } +
      { val := fun j => ↑(NatTrans.app s.π j) y,
        property :=
          (_ : (fun x => x ∈ Functor.sections (F ⋙ forget (AlgebraCatMax R))) fun j => ↑(NatTrans.app s.π j) y) }
[PROOFSTEP]
rfl
[GOAL]
case refine'_6
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
⊢ ∀ (r : R),
    OneHom.toFun
        (↑↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    {
                      toFun := fun v =>
                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                          property :=
                            (_ :
                              ∀ {j j' : J} (f : j ⟶ j'),
                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                      map_one' :=
                        (_ :
                          (fun v =>
                                { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                              1 =
                            1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : ↑s.pt),
                        OneHom.toFun
                            {
                              toFun := fun v =>
                                { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                              map_one' :=
                                (_ :
                                  (fun v =>
                                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                          property :=
                                            (_ :
                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                      1 =
                                    1) }
                            (x * y) =
                          OneHom.toFun
                              {
                                toFun := fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                map_one' :=
                                  (_ :
                                    (fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                        1 =
                                      1) }
                              x *
                            OneHom.toFun
                              {
                                toFun := fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                map_one' :=
                                  (_ :
                                    (fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                        1 =
                                      1) }
                              y) },
              map_zero' :=
                (_ :
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            {
                              toFun := fun v =>
                                { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                              map_one' :=
                                (_ :
                                  (fun v =>
                                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                          property :=
                                            (_ :
                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                      1 =
                                    1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : ↑s.pt),
                                OneHom.toFun
                                    {
                                      toFun := fun v =>
                                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                          property :=
                                            (_ :
                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                      map_one' :=
                                        (_ :
                                          (fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                              1 =
                                            1) }
                                    (x * y) =
                                  OneHom.toFun
                                      {
                                        toFun := fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                        map_one' :=
                                          (_ :
                                            (fun v =>
                                                  {
                                                    val := fun j =>
                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                    property :=
                                                      (_ :
                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                            ↑(NatTrans.app s.π j') v) })
                                                1 =
                                              1) }
                                      x *
                                    OneHom.toFun
                                      {
                                        toFun := fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                        map_one' :=
                                          (_ :
                                            (fun v =>
                                                  {
                                                    val := fun j =>
                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                    property :=
                                                      (_ :
                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                            ↑(NatTrans.app s.π j') v) })
                                                1 =
                                              1) }
                                      y) })
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x y : ↑s.pt),
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                map_one' :=
                                  (_ :
                                    (fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                        1 =
                                      1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : ↑s.pt),
                                  OneHom.toFun
                                      {
                                        toFun := fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                        map_one' :=
                                          (_ :
                                            (fun v =>
                                                  {
                                                    val := fun j =>
                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                    property :=
                                                      (_ :
                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                            ↑(NatTrans.app s.π j') v) })
                                                1 =
                                              1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        y) })
                        (x + y) =
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                {
                                  toFun := fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                  map_one' :=
                                    (_ :
                                      (fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                          1 =
                                        1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x y : ↑s.pt),
                                    OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        (x * y) =
                                      OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          x *
                                        OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          y) })
                          x +
                        OneHom.toFun
                          (↑{
                              toOneHom :=
                                {
                                  toFun := fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                  map_one' :=
                                    (_ :
                                      (fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                          1 =
                                        1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x y : ↑s.pt),
                                    OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        (x * y) =
                                      OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          x *
                                        OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          y) })
                          y) })
        (↑(algebraMap R ↑s.pt) r) =
      ↑(algebraMap R ↑(limitCone F).pt) r
[PROOFSTEP]
intro r
[GOAL]
case refine'_6
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
r : R
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              {
                toOneHom :=
                  {
                    toFun := fun v =>
                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                        property :=
                          (_ :
                            ∀ {j j' : J} (f : j ⟶ j'), ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                    map_one' :=
                      (_ :
                        (fun v =>
                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                            1 =
                          1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : ↑s.pt),
                      OneHom.toFun
                          {
                            toFun := fun v =>
                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                            map_one' :=
                              (_ :
                                (fun v =>
                                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                        property :=
                                          (_ :
                                            ∀ {j j' : J} (f : j ⟶ j'),
                                              ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                    1 =
                                  1) }
                          (x * y) =
                        OneHom.toFun
                            {
                              toFun := fun v =>
                                { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                              map_one' :=
                                (_ :
                                  (fun v =>
                                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                          property :=
                                            (_ :
                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                      1 =
                                    1) }
                            x *
                          OneHom.toFun
                            {
                              toFun := fun v =>
                                { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                              map_one' :=
                                (_ :
                                  (fun v =>
                                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                          property :=
                                            (_ :
                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                      1 =
                                    1) }
                            y) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          {
                            toFun := fun v =>
                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                            map_one' :=
                              (_ :
                                (fun v =>
                                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                        property :=
                                          (_ :
                                            ∀ {j j' : J} (f : j ⟶ j'),
                                              ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                    1 =
                                  1) },
                        map_mul' :=
                          (_ :
                            ∀ (x y : ↑s.pt),
                              OneHom.toFun
                                  {
                                    toFun := fun v =>
                                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                        property :=
                                          (_ :
                                            ∀ {j j' : J} (f : j ⟶ j'),
                                              ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                    map_one' :=
                                      (_ :
                                        (fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                            1 =
                                          1) }
                                  (x * y) =
                                OneHom.toFun
                                    {
                                      toFun := fun v =>
                                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                          property :=
                                            (_ :
                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                      map_one' :=
                                        (_ :
                                          (fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                              1 =
                                            1) }
                                    x *
                                  OneHom.toFun
                                    {
                                      toFun := fun v =>
                                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                          property :=
                                            (_ :
                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                      map_one' :=
                                        (_ :
                                          (fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                              1 =
                                            1) }
                                    y) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : ↑s.pt),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            {
                              toFun := fun v =>
                                { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                              map_one' :=
                                (_ :
                                  (fun v =>
                                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                          property :=
                                            (_ :
                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                      1 =
                                    1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : ↑s.pt),
                                OneHom.toFun
                                    {
                                      toFun := fun v =>
                                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                          property :=
                                            (_ :
                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                      map_one' :=
                                        (_ :
                                          (fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                              1 =
                                            1) }
                                    (x * y) =
                                  OneHom.toFun
                                      {
                                        toFun := fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                        map_one' :=
                                          (_ :
                                            (fun v =>
                                                  {
                                                    val := fun j =>
                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                    property :=
                                                      (_ :
                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                            ↑(NatTrans.app s.π j') v) })
                                                1 =
                                              1) }
                                      x *
                                    OneHom.toFun
                                      {
                                        toFun := fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                        map_one' :=
                                          (_ :
                                            (fun v =>
                                                  {
                                                    val := fun j =>
                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                    property :=
                                                      (_ :
                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                            ↑(NatTrans.app s.π j') v) })
                                                1 =
                                              1) }
                                      y) })
                      (x + y) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                map_one' :=
                                  (_ :
                                    (fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                        1 =
                                      1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : ↑s.pt),
                                  OneHom.toFun
                                      {
                                        toFun := fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                        map_one' :=
                                          (_ :
                                            (fun v =>
                                                  {
                                                    val := fun j =>
                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                    property :=
                                                      (_ :
                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                            ↑(NatTrans.app s.π j') v) })
                                                1 =
                                              1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        y) })
                        x +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                map_one' :=
                                  (_ :
                                    (fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                        1 =
                                      1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : ↑s.pt),
                                  OneHom.toFun
                                      {
                                        toFun := fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                        map_one' :=
                                          (_ :
                                            (fun v =>
                                                  {
                                                    val := fun j =>
                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                    property :=
                                                      (_ :
                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                            ↑(NatTrans.app s.π j') v) })
                                                1 =
                                              1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        y) })
                        y) })
      (↑(algebraMap R ↑s.pt) r) =
    ↑(algebraMap R ↑(limitCone F).pt) r
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case refine'_6.a
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
r : R
⊢ ↑(OneHom.toFun
        (↑↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    {
                      toFun := fun v =>
                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                          property :=
                            (_ :
                              ∀ {j j' : J} (f : j ⟶ j'),
                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                      map_one' :=
                        (_ :
                          (fun v =>
                                { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                              1 =
                            1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : ↑s.pt),
                        OneHom.toFun
                            {
                              toFun := fun v =>
                                { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                              map_one' :=
                                (_ :
                                  (fun v =>
                                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                          property :=
                                            (_ :
                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                      1 =
                                    1) }
                            (x * y) =
                          OneHom.toFun
                              {
                                toFun := fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                map_one' :=
                                  (_ :
                                    (fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                        1 =
                                      1) }
                              x *
                            OneHom.toFun
                              {
                                toFun := fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                map_one' :=
                                  (_ :
                                    (fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                        1 =
                                      1) }
                              y) },
              map_zero' :=
                (_ :
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            {
                              toFun := fun v =>
                                { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                              map_one' :=
                                (_ :
                                  (fun v =>
                                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                          property :=
                                            (_ :
                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                      1 =
                                    1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : ↑s.pt),
                                OneHom.toFun
                                    {
                                      toFun := fun v =>
                                        { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                          property :=
                                            (_ :
                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                      map_one' :=
                                        (_ :
                                          (fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                              1 =
                                            1) }
                                    (x * y) =
                                  OneHom.toFun
                                      {
                                        toFun := fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                        map_one' :=
                                          (_ :
                                            (fun v =>
                                                  {
                                                    val := fun j =>
                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                    property :=
                                                      (_ :
                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                            ↑(NatTrans.app s.π j') v) })
                                                1 =
                                              1) }
                                      x *
                                    OneHom.toFun
                                      {
                                        toFun := fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                        map_one' :=
                                          (_ :
                                            (fun v =>
                                                  {
                                                    val := fun j =>
                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                    property :=
                                                      (_ :
                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                            ↑(NatTrans.app s.π j') v) })
                                                1 =
                                              1) }
                                      y) })
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x y : ↑s.pt),
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                map_one' :=
                                  (_ :
                                    (fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                        1 =
                                      1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : ↑s.pt),
                                  OneHom.toFun
                                      {
                                        toFun := fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                        map_one' :=
                                          (_ :
                                            (fun v =>
                                                  {
                                                    val := fun j =>
                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                    property :=
                                                      (_ :
                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                            ↑(NatTrans.app s.π j') v) })
                                                1 =
                                              1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        y) })
                        (x + y) =
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                {
                                  toFun := fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                  map_one' :=
                                    (_ :
                                      (fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                          1 =
                                        1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x y : ↑s.pt),
                                    OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        (x * y) =
                                      OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          x *
                                        OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          y) })
                          x +
                        OneHom.toFun
                          (↑{
                              toOneHom :=
                                {
                                  toFun := fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                  map_one' :=
                                    (_ :
                                      (fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                          1 =
                                        1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x y : ↑s.pt),
                                    OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        (x * y) =
                                      OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          x *
                                        OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          y) })
                          y) })
        (↑(algebraMap R ↑s.pt) r)) =
    ↑(↑(algebraMap R ↑(limitCone F).pt) r)
[PROOFSTEP]
ext j
[GOAL]
case refine'_6.a.h
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
r : R
j : J
⊢ ↑(OneHom.toFun
          (↑↑{
                toMonoidHom :=
                  {
                    toOneHom :=
                      {
                        toFun := fun v =>
                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                        map_one' :=
                          (_ :
                            (fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                1 =
                              1) },
                    map_mul' :=
                      (_ :
                        ∀ (x y : ↑s.pt),
                          OneHom.toFun
                              {
                                toFun := fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                map_one' :=
                                  (_ :
                                    (fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                        1 =
                                      1) }
                              (x * y) =
                            OneHom.toFun
                                {
                                  toFun := fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                  map_one' :=
                                    (_ :
                                      (fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                          1 =
                                        1) }
                                x *
                              OneHom.toFun
                                {
                                  toFun := fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                  map_one' :=
                                    (_ :
                                      (fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                          1 =
                                        1) }
                                y) },
                map_zero' :=
                  (_ :
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                map_one' :=
                                  (_ :
                                    (fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                        1 =
                                      1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : ↑s.pt),
                                  OneHom.toFun
                                      {
                                        toFun := fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                        map_one' :=
                                          (_ :
                                            (fun v =>
                                                  {
                                                    val := fun j =>
                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                    property :=
                                                      (_ :
                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                            ↑(NatTrans.app s.π j') v) })
                                                1 =
                                              1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        y) })
                        0 =
                      0),
                map_add' :=
                  (_ :
                    ∀ (x y : ↑s.pt),
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                {
                                  toFun := fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                  map_one' :=
                                    (_ :
                                      (fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                          1 =
                                        1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x y : ↑s.pt),
                                    OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        (x * y) =
                                      OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          x *
                                        OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          y) })
                          (x + y) =
                        OneHom.toFun
                            (↑{
                                toOneHom :=
                                  {
                                    toFun := fun v =>
                                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                        property :=
                                          (_ :
                                            ∀ {j j' : J} (f : j ⟶ j'),
                                              ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                    map_one' :=
                                      (_ :
                                        (fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                            1 =
                                          1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : ↑s.pt),
                                      OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          (x * y) =
                                        OneHom.toFun
                                            {
                                              toFun := fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                              map_one' :=
                                                (_ :
                                                  (fun v =>
                                                        {
                                                          val := fun j =>
                                                            NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                          property :=
                                                            (_ :
                                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                                ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                  ↑(NatTrans.app s.π j') v) })
                                                      1 =
                                                    1) }
                                            x *
                                          OneHom.toFun
                                            {
                                              toFun := fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                              map_one' :=
                                                (_ :
                                                  (fun v =>
                                                        {
                                                          val := fun j =>
                                                            NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                          property :=
                                                            (_ :
                                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                                ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                  ↑(NatTrans.app s.π j') v) })
                                                      1 =
                                                    1) }
                                            y) })
                            x +
                          OneHom.toFun
                            (↑{
                                toOneHom :=
                                  {
                                    toFun := fun v =>
                                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                        property :=
                                          (_ :
                                            ∀ {j j' : J} (f : j ⟶ j'),
                                              ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                    map_one' :=
                                      (_ :
                                        (fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                            1 =
                                          1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : ↑s.pt),
                                      OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          (x * y) =
                                        OneHom.toFun
                                            {
                                              toFun := fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                              map_one' :=
                                                (_ :
                                                  (fun v =>
                                                        {
                                                          val := fun j =>
                                                            NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                          property :=
                                                            (_ :
                                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                                ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                  ↑(NatTrans.app s.π j') v) })
                                                      1 =
                                                    1) }
                                            x *
                                          OneHom.toFun
                                            {
                                              toFun := fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                              map_one' :=
                                                (_ :
                                                  (fun v =>
                                                        {
                                                          val := fun j =>
                                                            NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                          property :=
                                                            (_ :
                                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                                ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                  ↑(NatTrans.app s.π j') v) })
                                                      1 =
                                                    1) }
                                            y) })
                            y) })
          (↑(algebraMap R ↑s.pt) r))
      j =
    ↑(↑(algebraMap R ↑(limitCone F).pt) r) j
[PROOFSTEP]
exact (s.π.app j).commutes r
[GOAL]
case refine'_7
R : Type u
inst✝¹ : CommRing R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AlgebraCatMax R
s : Cone F
⊢ (forget (AlgebraCat R)).map
      ((fun s =>
          {
            toRingHom :=
              {
                toMonoidHom :=
                  {
                    toOneHom :=
                      {
                        toFun := fun v =>
                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                        map_one' :=
                          (_ :
                            (fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                1 =
                              1) },
                    map_mul' :=
                      (_ :
                        ∀ (x y : ↑s.pt),
                          OneHom.toFun
                              {
                                toFun := fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                map_one' :=
                                  (_ :
                                    (fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                        1 =
                                      1) }
                              (x * y) =
                            OneHom.toFun
                                {
                                  toFun := fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                  map_one' :=
                                    (_ :
                                      (fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                          1 =
                                        1) }
                                x *
                              OneHom.toFun
                                {
                                  toFun := fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                  map_one' :=
                                    (_ :
                                      (fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                          1 =
                                        1) }
                                y) },
                map_zero' :=
                  (_ :
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun v =>
                                  { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                map_one' :=
                                  (_ :
                                    (fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                        1 =
                                      1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : ↑s.pt),
                                  OneHom.toFun
                                      {
                                        toFun := fun v =>
                                          { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                            property :=
                                              (_ :
                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                  ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                        map_one' :=
                                          (_ :
                                            (fun v =>
                                                  {
                                                    val := fun j =>
                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                    property :=
                                                      (_ :
                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                            ↑(NatTrans.app s.π j') v) })
                                                1 =
                                              1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        y) })
                        0 =
                      0),
                map_add' :=
                  (_ :
                    ∀ (x y : ↑s.pt),
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                {
                                  toFun := fun v =>
                                    { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                  map_one' :=
                                    (_ :
                                      (fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                          1 =
                                        1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x y : ↑s.pt),
                                    OneHom.toFun
                                        {
                                          toFun := fun v =>
                                            { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                              property :=
                                                (_ :
                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                    ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                          map_one' :=
                                            (_ :
                                              (fun v =>
                                                    {
                                                      val := fun j =>
                                                        NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                      property :=
                                                        (_ :
                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                              ↑(NatTrans.app s.π j') v) })
                                                  1 =
                                                1) }
                                        (x * y) =
                                      OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          x *
                                        OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          y) })
                          (x + y) =
                        OneHom.toFun
                            (↑{
                                toOneHom :=
                                  {
                                    toFun := fun v =>
                                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                        property :=
                                          (_ :
                                            ∀ {j j' : J} (f : j ⟶ j'),
                                              ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                    map_one' :=
                                      (_ :
                                        (fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                            1 =
                                          1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : ↑s.pt),
                                      OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          (x * y) =
                                        OneHom.toFun
                                            {
                                              toFun := fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                              map_one' :=
                                                (_ :
                                                  (fun v =>
                                                        {
                                                          val := fun j =>
                                                            NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                          property :=
                                                            (_ :
                                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                                ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                  ↑(NatTrans.app s.π j') v) })
                                                      1 =
                                                    1) }
                                            x *
                                          OneHom.toFun
                                            {
                                              toFun := fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                              map_one' :=
                                                (_ :
                                                  (fun v =>
                                                        {
                                                          val := fun j =>
                                                            NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                          property :=
                                                            (_ :
                                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                                ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                  ↑(NatTrans.app s.π j') v) })
                                                      1 =
                                                    1) }
                                            y) })
                            x +
                          OneHom.toFun
                            (↑{
                                toOneHom :=
                                  {
                                    toFun := fun v =>
                                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                        property :=
                                          (_ :
                                            ∀ {j j' : J} (f : j ⟶ j'),
                                              ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                    map_one' :=
                                      (_ :
                                        (fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                            1 =
                                          1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : ↑s.pt),
                                      OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          (x * y) =
                                        OneHom.toFun
                                            {
                                              toFun := fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                              map_one' :=
                                                (_ :
                                                  (fun v =>
                                                        {
                                                          val := fun j =>
                                                            NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                          property :=
                                                            (_ :
                                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                                ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                  ↑(NatTrans.app s.π j') v) })
                                                      1 =
                                                    1) }
                                            x *
                                          OneHom.toFun
                                            {
                                              toFun := fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                              map_one' :=
                                                (_ :
                                                  (fun v =>
                                                        {
                                                          val := fun j =>
                                                            NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                          property :=
                                                            (_ :
                                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                                ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                  ↑(NatTrans.app s.π j') v) })
                                                      1 =
                                                    1) }
                                            y) })
                            y) },
            commutes' :=
              (_ :
                ∀ (r : R),
                  OneHom.toFun
                      (↑↑{
                            toMonoidHom :=
                              {
                                toOneHom :=
                                  {
                                    toFun := fun v =>
                                      { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                        property :=
                                          (_ :
                                            ∀ {j j' : J} (f : j ⟶ j'),
                                              ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                    map_one' :=
                                      (_ :
                                        (fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) })
                                            1 =
                                          1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : ↑s.pt),
                                      OneHom.toFun
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) }
                                          (x * y) =
                                        OneHom.toFun
                                            {
                                              toFun := fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                              map_one' :=
                                                (_ :
                                                  (fun v =>
                                                        {
                                                          val := fun j =>
                                                            NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                          property :=
                                                            (_ :
                                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                                ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                  ↑(NatTrans.app s.π j') v) })
                                                      1 =
                                                    1) }
                                            x *
                                          OneHom.toFun
                                            {
                                              toFun := fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                              map_one' :=
                                                (_ :
                                                  (fun v =>
                                                        {
                                                          val := fun j =>
                                                            NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                          property :=
                                                            (_ :
                                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                                ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                  ↑(NatTrans.app s.π j') v) })
                                                      1 =
                                                    1) }
                                            y) },
                            map_zero' :=
                              (_ :
                                OneHom.toFun
                                    (↑{
                                        toOneHom :=
                                          {
                                            toFun := fun v =>
                                              { val := fun j => NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                property :=
                                                  (_ :
                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                      ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                            map_one' :=
                                              (_ :
                                                (fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) })
                                                    1 =
                                                  1) },
                                        map_mul' :=
                                          (_ :
                                            ∀ (x y : ↑s.pt),
                                              OneHom.toFun
                                                  {
                                                    toFun := fun v =>
                                                      {
                                                        val := fun j =>
                                                          NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                        property :=
                                                          (_ :
                                                            ∀ {j j' : J} (f : j ⟶ j'),
                                                              ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                ↑(NatTrans.app s.π j') v) },
                                                    map_one' :=
                                                      (_ :
                                                        (fun v =>
                                                              {
                                                                val := fun j =>
                                                                  NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j
                                                                    v,
                                                                property :=
                                                                  (_ :
                                                                    ∀ {j j' : J} (f : j ⟶ j'),
                                                                      ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                        ↑(NatTrans.app s.π j') v) })
                                                            1 =
                                                          1) }
                                                  (x * y) =
                                                OneHom.toFun
                                                    {
                                                      toFun := fun v =>
                                                        {
                                                          val := fun j =>
                                                            NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                          property :=
                                                            (_ :
                                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                                ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                  ↑(NatTrans.app s.π j') v) },
                                                      map_one' :=
                                                        (_ :
                                                          (fun v =>
                                                                {
                                                                  val := fun j =>
                                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j
                                                                      v,
                                                                  property :=
                                                                    (_ :
                                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                                        ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                          ↑(NatTrans.app s.π j') v) })
                                                              1 =
                                                            1) }
                                                    x *
                                                  OneHom.toFun
                                                    {
                                                      toFun := fun v =>
                                                        {
                                                          val := fun j =>
                                                            NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                          property :=
                                                            (_ :
                                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                                ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                  ↑(NatTrans.app s.π j') v) },
                                                      map_one' :=
                                                        (_ :
                                                          (fun v =>
                                                                {
                                                                  val := fun j =>
                                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j
                                                                      v,
                                                                  property :=
                                                                    (_ :
                                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                                        ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                          ↑(NatTrans.app s.π j') v) })
                                                              1 =
                                                            1) }
                                                    y) })
                                    0 =
                                  0),
                            map_add' :=
                              (_ :
                                ∀ (x y : ↑s.pt),
                                  OneHom.toFun
                                      (↑{
                                          toOneHom :=
                                            {
                                              toFun := fun v =>
                                                {
                                                  val := fun j =>
                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                  property :=
                                                    (_ :
                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                        ↑(NatTrans.app s.π j ≫ F.map f) v = ↑(NatTrans.app s.π j') v) },
                                              map_one' :=
                                                (_ :
                                                  (fun v =>
                                                        {
                                                          val := fun j =>
                                                            NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                          property :=
                                                            (_ :
                                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                                ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                  ↑(NatTrans.app s.π j') v) })
                                                      1 =
                                                    1) },
                                          map_mul' :=
                                            (_ :
                                              ∀ (x y : ↑s.pt),
                                                OneHom.toFun
                                                    {
                                                      toFun := fun v =>
                                                        {
                                                          val := fun j =>
                                                            NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                          property :=
                                                            (_ :
                                                              ∀ {j j' : J} (f : j ⟶ j'),
                                                                ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                  ↑(NatTrans.app s.π j') v) },
                                                      map_one' :=
                                                        (_ :
                                                          (fun v =>
                                                                {
                                                                  val := fun j =>
                                                                    NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j
                                                                      v,
                                                                  property :=
                                                                    (_ :
                                                                      ∀ {j j' : J} (f : j ⟶ j'),
                                                                        ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                          ↑(NatTrans.app s.π j') v) })
                                                              1 =
                                                            1) }
                                                    (x * y) =
                                                  OneHom.toFun
                                                      {
                                                        toFun := fun v =>
                                                          {
                                                            val := fun j =>
                                                              NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                            property :=
                                                              (_ :
                                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                                  ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                    ↑(NatTrans.app s.π j') v) },
                                                        map_one' :=
                                                          (_ :
                                                            (fun v =>
                                                                  {
                                                                    val := fun j =>
                                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π
                                                                        j v,
                                                                    property :=
                                                                      (_ :
                                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                            ↑(NatTrans.app s.π j') v) })
                                                                1 =
                                                              1) }
                                                      x *
                                                    OneHom.toFun
                                                      {
                                                        toFun := fun v =>
                                                          {
                                                            val := fun j =>
                                                              NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                            property :=
                                                              (_ :
                                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                                  ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                    ↑(NatTrans.app s.π j') v) },
                                                        map_one' :=
                                                          (_ :
                                                            (fun v =>
                                                                  {
                                                                    val := fun j =>
                                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π
                                                                        j v,
                                                                    property :=
                                                                      (_ :
                                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                            ↑(NatTrans.app s.π j') v) })
                                                                1 =
                                                              1) }
                                                      y) })
                                      (x + y) =
                                    OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              {
                                                toFun := fun v =>
                                                  {
                                                    val := fun j =>
                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                    property :=
                                                      (_ :
                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                            ↑(NatTrans.app s.π j') v) },
                                                map_one' :=
                                                  (_ :
                                                    (fun v =>
                                                          {
                                                            val := fun j =>
                                                              NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                            property :=
                                                              (_ :
                                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                                  ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                    ↑(NatTrans.app s.π j') v) })
                                                        1 =
                                                      1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑s.pt),
                                                  OneHom.toFun
                                                      {
                                                        toFun := fun v =>
                                                          {
                                                            val := fun j =>
                                                              NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                            property :=
                                                              (_ :
                                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                                  ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                    ↑(NatTrans.app s.π j') v) },
                                                        map_one' :=
                                                          (_ :
                                                            (fun v =>
                                                                  {
                                                                    val := fun j =>
                                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π
                                                                        j v,
                                                                    property :=
                                                                      (_ :
                                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                            ↑(NatTrans.app s.π j') v) })
                                                                1 =
                                                              1) }
                                                      (x * y) =
                                                    OneHom.toFun
                                                        {
                                                          toFun := fun v =>
                                                            {
                                                              val := fun j =>
                                                                NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                              property :=
                                                                (_ :
                                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                                    ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                      ↑(NatTrans.app s.π j') v) },
                                                          map_one' :=
                                                            (_ :
                                                              (fun v =>
                                                                    {
                                                                      val := fun j =>
                                                                        NatTrans.app
                                                                          ((forget (AlgebraCat R)).mapCone s).π j v,
                                                                      property :=
                                                                        (_ :
                                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                              ↑(NatTrans.app s.π j') v) })
                                                                  1 =
                                                                1) }
                                                        x *
                                                      OneHom.toFun
                                                        {
                                                          toFun := fun v =>
                                                            {
                                                              val := fun j =>
                                                                NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                              property :=
                                                                (_ :
                                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                                    ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                      ↑(NatTrans.app s.π j') v) },
                                                          map_one' :=
                                                            (_ :
                                                              (fun v =>
                                                                    {
                                                                      val := fun j =>
                                                                        NatTrans.app
                                                                          ((forget (AlgebraCat R)).mapCone s).π j v,
                                                                      property :=
                                                                        (_ :
                                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                              ↑(NatTrans.app s.π j') v) })
                                                                  1 =
                                                                1) }
                                                        y) })
                                        x +
                                      OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              {
                                                toFun := fun v =>
                                                  {
                                                    val := fun j =>
                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                    property :=
                                                      (_ :
                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                            ↑(NatTrans.app s.π j') v) },
                                                map_one' :=
                                                  (_ :
                                                    (fun v =>
                                                          {
                                                            val := fun j =>
                                                              NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                            property :=
                                                              (_ :
                                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                                  ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                    ↑(NatTrans.app s.π j') v) })
                                                        1 =
                                                      1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑s.pt),
                                                  OneHom.toFun
                                                      {
                                                        toFun := fun v =>
                                                          {
                                                            val := fun j =>
                                                              NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                            property :=
                                                              (_ :
                                                                ∀ {j j' : J} (f : j ⟶ j'),
                                                                  ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                    ↑(NatTrans.app s.π j') v) },
                                                        map_one' :=
                                                          (_ :
                                                            (fun v =>
                                                                  {
                                                                    val := fun j =>
                                                                      NatTrans.app ((forget (AlgebraCat R)).mapCone s).π
                                                                        j v,
                                                                    property :=
                                                                      (_ :
                                                                        ∀ {j j' : J} (f : j ⟶ j'),
                                                                          ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                            ↑(NatTrans.app s.π j') v) })
                                                                1 =
                                                              1) }
                                                      (x * y) =
                                                    OneHom.toFun
                                                        {
                                                          toFun := fun v =>
                                                            {
                                                              val := fun j =>
                                                                NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                              property :=
                                                                (_ :
                                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                                    ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                      ↑(NatTrans.app s.π j') v) },
                                                          map_one' :=
                                                            (_ :
                                                              (fun v =>
                                                                    {
                                                                      val := fun j =>
                                                                        NatTrans.app
                                                                          ((forget (AlgebraCat R)).mapCone s).π j v,
                                                                      property :=
                                                                        (_ :
                                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                              ↑(NatTrans.app s.π j') v) })
                                                                  1 =
                                                                1) }
                                                        x *
                                                      OneHom.toFun
                                                        {
                                                          toFun := fun v =>
                                                            {
                                                              val := fun j =>
                                                                NatTrans.app ((forget (AlgebraCat R)).mapCone s).π j v,
                                                              property :=
                                                                (_ :
                                                                  ∀ {j j' : J} (f : j ⟶ j'),
                                                                    ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                      ↑(NatTrans.app s.π j') v) },
                                                          map_one' :=
                                                            (_ :
                                                              (fun v =>
                                                                    {
                                                                      val := fun j =>
                                                                        NatTrans.app
                                                                          ((forget (AlgebraCat R)).mapCone s).π j v,
                                                                      property :=
                                                                        (_ :
                                                                          ∀ {j j' : J} (f : j ⟶ j'),
                                                                            ↑(NatTrans.app s.π j ≫ F.map f) v =
                                                                              ↑(NatTrans.app s.π j') v) })
                                                                  1 =
                                                                1) }
                                                        y) })
                                        y) })
                      (↑(algebraMap R ↑s.pt) r) =
                    ↑(algebraMap R ↑(limitCone F).pt) r) })
        s) =
    IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (AlgebraCat R))) ((forget (AlgebraCat R)).mapCone s)
[PROOFSTEP]
rfl
