[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : LocallyConstant X Y
inst✝¹ : Monoid Y
inst✝ : ContinuousMul Y
⊢ ↑1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : LocallyConstant X Y
inst✝¹ : Monoid Y
inst✝ : ContinuousMul Y
a✝ : X
⊢ ↑↑1 a✝ = ↑1 a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : LocallyConstant X Y
inst✝¹ : Monoid Y
inst✝ : ContinuousMul Y
x y : LocallyConstant X Y
⊢ OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : LocallyConstant X Y
inst✝¹ : Monoid Y
inst✝ : ContinuousMul Y
x y : LocallyConstant X Y
a✝ : X
⊢ ↑(OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y)) a✝ =
    ↑(OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y)
      a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid Y
inst✝² : Module R Y
inst✝¹ : ContinuousAdd Y
inst✝ : ContinuousConstSMul R Y
x y : LocallyConstant X Y
⊢ ↑(x + y) = ↑x + ↑y
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid Y
inst✝² : Module R Y
inst✝¹ : ContinuousAdd Y
inst✝ : ContinuousConstSMul R Y
x y : LocallyConstant X Y
a✝ : X
⊢ ↑↑(x + y) a✝ = ↑(↑x + ↑y) a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid Y
inst✝² : Module R Y
inst✝¹ : ContinuousAdd Y
inst✝ : ContinuousConstSMul R Y
x : R
y : LocallyConstant X Y
⊢ AddHom.toFun { toFun := toContinuousMap, map_add' := (_ : ∀ (x y : LocallyConstant X Y), ↑(x + y) = ↑x + ↑y) }
      (x • y) =
    ↑(RingHom.id R) x •
      AddHom.toFun { toFun := toContinuousMap, map_add' := (_ : ∀ (x y : LocallyConstant X Y), ↑(x + y) = ↑x + ↑y) } y
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid Y
inst✝² : Module R Y
inst✝¹ : ContinuousAdd Y
inst✝ : ContinuousConstSMul R Y
x : R
y : LocallyConstant X Y
a✝ : X
⊢ ↑(AddHom.toFun { toFun := toContinuousMap, map_add' := (_ : ∀ (x y : LocallyConstant X Y), ↑(x + y) = ↑x + ↑y) }
          (x • y))
      a✝ =
    ↑(↑(RingHom.id R) x •
          AddHom.toFun { toFun := toContinuousMap, map_add' := (_ : ∀ (x y : LocallyConstant X Y), ↑(x + y) = ↑x + ↑y) }
            y)
      a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
⊢ ↑1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
a✝ : X
⊢ ↑↑1 a✝ = ↑1 a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
x y : LocallyConstant X Y
⊢ OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
x y : LocallyConstant X Y
a✝ : X
⊢ ↑(OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y)) a✝ =
    ↑(OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y)
      a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : LocallyConstant X Y),
                OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
      0 =
    0
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
a✝ : X
⊢ ↑(OneHom.toFun
          (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : LocallyConstant X Y),
                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
          0)
      a✝ =
    ↑0 a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
x y : LocallyConstant X Y
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : LocallyConstant X Y),
                OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
      (x + y) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : LocallyConstant X Y),
                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
        x +
      OneHom.toFun
        (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : LocallyConstant X Y),
                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
        y
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
x y : LocallyConstant X Y
a✝ : X
⊢ ↑(OneHom.toFun
          (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : LocallyConstant X Y),
                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
          (x + y))
      a✝ =
    ↑(OneHom.toFun
            (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : LocallyConstant X Y),
                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
            x +
          OneHom.toFun
            (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : LocallyConstant X Y),
                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
            y)
      a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
r : R
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              { toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : LocallyConstant X Y),
                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (x y : LocallyConstant X Y),
                              OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : LocallyConstant X Y),
                  OneHom.toFun
                      (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : LocallyConstant X Y),
                                OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                      (x + y) =
                    OneHom.toFun
                        (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : LocallyConstant X Y),
                                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                        x +
                      OneHom.toFun
                        (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : LocallyConstant X Y),
                                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                        y) })
      (↑(algebraMap R (LocallyConstant X Y)) r) =
    ↑(algebraMap R C(X, Y)) r
[PROOFSTEP]
ext x
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
r : R
x : X
⊢ ↑(OneHom.toFun
          (↑↑{
                toMonoidHom :=
                  { toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (x y : LocallyConstant X Y),
                          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                            OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                              OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) },
                map_zero' :=
                  (_ :
                    OneHom.toFun
                        (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : LocallyConstant X Y),
                                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                        0 =
                      0),
                map_add' :=
                  (_ :
                    ∀ (x y : LocallyConstant X Y),
                      OneHom.toFun
                          (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x y : LocallyConstant X Y),
                                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                          (x + y) =
                        OneHom.toFun
                            (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : LocallyConstant X Y),
                                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                            x +
                          OneHom.toFun
                            (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : LocallyConstant X Y),
                                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                            y) })
          (↑(algebraMap R (LocallyConstant X Y)) r))
      x =
    ↑(↑(algebraMap R C(X, Y)) r) x
[PROOFSTEP]
simp [Algebra.smul_def]
