[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring Y
inst✝ : Algebra R Y
⊢ ∀ (r : R) (x : (fun x => LocallyConstant X Y) r),
    ↑(RingHom.comp constRingHom (algebraMap R Y)) r * x = x * ↑(RingHom.comp constRingHom (algebraMap R Y)) r
[PROOFSTEP]
intros
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring Y
inst✝ : Algebra R Y
r✝ : R
x✝ : LocallyConstant X Y
⊢ ↑(RingHom.comp constRingHom (algebraMap R Y)) r✝ * x✝ = x✝ * ↑(RingHom.comp constRingHom (algebraMap R Y)) r✝
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring Y
inst✝ : Algebra R Y
r✝ : R
x✝¹ : LocallyConstant X Y
x✝ : X
⊢ ↑(↑(RingHom.comp constRingHom (algebraMap R Y)) r✝ * x✝¹) x✝ =
    ↑(x✝¹ * ↑(RingHom.comp constRingHom (algebraMap R Y)) r✝) x✝
[PROOFSTEP]
exact Algebra.commutes' _ _
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring Y
inst✝ : Algebra R Y
⊢ ∀ (r : R) (x : (fun x => LocallyConstant X Y) r), r • x = ↑(RingHom.comp constRingHom (algebraMap R Y)) r * x
[PROOFSTEP]
intros
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring Y
inst✝ : Algebra R Y
r✝ : R
x✝ : LocallyConstant X Y
⊢ r✝ • x✝ = ↑(RingHom.comp constRingHom (algebraMap R Y)) r✝ * x✝
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring Y
inst✝ : Algebra R Y
r✝ : R
x✝¹ : LocallyConstant X Y
x✝ : X
⊢ ↑(r✝ • x✝¹) x✝ = ↑(↑(RingHom.comp constRingHom (algebraMap R Y)) r✝ * x✝¹) x✝
[PROOFSTEP]
exact Algebra.smul_def' _ _
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
R : Type u_3
inst✝¹ : TopologicalSpace Y
Z : Type ?u.139413
inst✝ : Mul Z
f : X → Y
hf : Continuous f
r s : LocallyConstant Y Z
⊢ comap f (r * s) = comap f r * comap f s
[PROOFSTEP]
ext x
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
R : Type u_3
inst✝¹ : TopologicalSpace Y
Z : Type ?u.139413
inst✝ : Mul Z
f : X → Y
hf : Continuous f
r s : LocallyConstant Y Z
x : X
⊢ ↑(comap f (r * s)) x = ↑(comap f r * comap f s) x
[PROOFSTEP]
simp [hf]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
R : Type u_3
inst✝¹ : TopologicalSpace Y
Z : Type ?u.141527
inst✝ : MulOneClass Z
f : X → Y
hf : Continuous f
⊢ comap f 1 = 1
[PROOFSTEP]
ext x
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
R : Type u_3
inst✝¹ : TopologicalSpace Y
Z : Type ?u.141527
inst✝ : MulOneClass Z
f : X → Y
hf : Continuous f
x : X
⊢ ↑(comap f 1) x = ↑1 x
[PROOFSTEP]
simp [hf]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
R✝ : Type u_3
inst✝³ : TopologicalSpace Y
Z : Type ?u.147135
R : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid Z
inst✝ : Module R Z
f : X → Y
hf : Continuous f
r : R
s : LocallyConstant Y Z
⊢ AddHom.toFun
      { toFun := comap f,
        map_add' :=
          (_ :
            ∀ (x y : LocallyConstant Y Z),
              ↑(comapAddMonoidHom f hf) (x + y) = ↑(comapAddMonoidHom f hf) x + ↑(comapAddMonoidHom f hf) y) }
      (r • s) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := comap f,
          map_add' :=
            (_ :
              ∀ (x y : LocallyConstant Y Z),
                ↑(comapAddMonoidHom f hf) (x + y) = ↑(comapAddMonoidHom f hf) x + ↑(comapAddMonoidHom f hf) y) }
        s
[PROOFSTEP]
ext x
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
R✝ : Type u_3
inst✝³ : TopologicalSpace Y
Z : Type ?u.147135
R : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid Z
inst✝ : Module R Z
f : X → Y
hf : Continuous f
r : R
s : LocallyConstant Y Z
x : X
⊢ ↑(AddHom.toFun
          { toFun := comap f,
            map_add' :=
              (_ :
                ∀ (x y : LocallyConstant Y Z),
                  ↑(comapAddMonoidHom f hf) (x + y) = ↑(comapAddMonoidHom f hf) x + ↑(comapAddMonoidHom f hf) y) }
          (r • s))
      x =
    ↑(↑(RingHom.id R) r •
          AddHom.toFun
            { toFun := comap f,
              map_add' :=
                (_ :
                  ∀ (x y : LocallyConstant Y Z),
                    ↑(comapAddMonoidHom f hf) (x + y) = ↑(comapAddMonoidHom f hf) x + ↑(comapAddMonoidHom f hf) y) }
            s)
      x
[PROOFSTEP]
simp [hf]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
R✝ : Type u_3
inst✝³ : TopologicalSpace Y
Z : Type ?u.155777
R : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring Z
inst✝ : Algebra R Z
f : X → Y
hf : Continuous f
r : R
⊢ OneHom.toFun (↑↑(comapRingHom f hf)) (↑(algebraMap R (LocallyConstant Y Z)) r) =
    ↑(algebraMap R (LocallyConstant X Z)) r
[PROOFSTEP]
ext x
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
R✝ : Type u_3
inst✝³ : TopologicalSpace Y
Z : Type ?u.155777
R : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring Z
inst✝ : Algebra R Z
f : X → Y
hf : Continuous f
r : R
x : X
⊢ ↑(OneHom.toFun (↑↑(comapRingHom f hf)) (↑(algebraMap R (LocallyConstant Y Z)) r)) x =
    ↑(↑(algebraMap R (LocallyConstant X Z)) r) x
[PROOFSTEP]
simp [hf]
