[GOAL]
𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : SmoothMul I' G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : SmoothMul I'' G''
φ : G' →* G''
hφ : Smooth I' I'' ↑φ
⊢ (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : SmoothMul I' G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : SmoothMul I'' G''
φ : G' →* G''
hφ : Smooth I' I'' ↑φ
x✝ : N
⊢ ↑((fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1) x✝ = ↑1 x✝
[PROOFSTEP]
show φ 1 = 1
[GOAL]
case h
𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : SmoothMul I' G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : SmoothMul I'' G''
φ : G' →* G''
hφ : Smooth I' I'' ↑φ
x✝ : N
⊢ ↑φ 1 = 1
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : SmoothMul I' G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : SmoothMul I'' G''
φ : G' →* G''
hφ : Smooth I' I'' ↑φ
f g : C^⊤⟮I, N; I', G'⟯
⊢ OneHom.toFun
      { toFun := fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) },
        map_one' :=
          (_ : (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1 = 1) }
      (f * g) =
    OneHom.toFun
        { toFun := fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) },
          map_one' :=
            (_ : (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1 = 1) }
        f *
      OneHom.toFun
        { toFun := fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) },
          map_one' :=
            (_ : (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1 = 1) }
        g
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : SmoothMul I' G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : SmoothMul I'' G''
φ : G' →* G''
hφ : Smooth I' I'' ↑φ
f g : C^⊤⟮I, N; I', G'⟯
x : N
⊢ ↑(OneHom.toFun
          { toFun := fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) },
            map_one' :=
              (_ : (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1 = 1) }
          (f * g))
      x =
    ↑(OneHom.toFun
            { toFun := fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) },
              map_one' :=
                (_ :
                  (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1 = 1) }
            f *
          OneHom.toFun
            { toFun := fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) },
              map_one' :=
                (_ :
                  (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1 = 1) }
            g)
      x
[PROOFSTEP]
show φ (f x * g x) = φ (f x) * φ (g x)
[GOAL]
case h
𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : SmoothMul I' G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : SmoothMul I'' G''
φ : G' →* G''
hφ : Smooth I' I'' ↑φ
f g : C^⊤⟮I, N; I', G'⟯
x : N
⊢ ↑φ (↑f x * ↑g x) = ↑φ (↑f x) * ↑φ (↑g x)
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
G : Type u_10
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H' G
inst✝ : LieGroup I' G
src✝ : Monoid C^⊤⟮I, N; I', G⟯ := monoid
f g : C^⊤⟮I, N; I', G⟯
⊢ f / g = f * g⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
G : Type u_10
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H' G
inst✝ : LieGroup I' G
src✝ : Monoid C^⊤⟮I, N; I', G⟯ := monoid
f g : C^⊤⟮I, N; I', G⟯
x✝ : N
⊢ ↑(f / g) x✝ = ↑(f * g⁻¹) x✝
[PROOFSTEP]
exact div_eq_mul_inv _ _
[GOAL]
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
G : Type u_10
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H' G
inst✝ : LieGroup I' G
src✝ : Monoid C^⊤⟮I, N; I', G⟯ := monoid
a : C^⊤⟮I, N; I', G⟯
⊢ a⁻¹ * a = 1
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
G : Type u_10
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H' G
inst✝ : LieGroup I' G
src✝ : Monoid C^⊤⟮I, N; I', G⟯ := monoid
a : C^⊤⟮I, N; I', G⟯
x✝ : N
⊢ ↑(a⁻¹ * a) x✝ = ↑1 x✝
[PROOFSTEP]
exact mul_left_inv _
[GOAL]
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a b c : C^⊤⟮I, N; I', R⟯
⊢ a * (b + c) = a * b + a * c
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a b c : C^⊤⟮I, N; I', R⟯
x✝ : N
⊢ ↑(a * (b + c)) x✝ = ↑(a * b + a * c) x✝
[PROOFSTEP]
exact left_distrib _ _ _
[GOAL]
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a b c : C^⊤⟮I, N; I', R⟯
⊢ (a + b) * c = a * c + b * c
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a b c : C^⊤⟮I, N; I', R⟯
x✝ : N
⊢ ↑((a + b) * c) x✝ = ↑(a * c + b * c) x✝
[PROOFSTEP]
exact right_distrib _ _ _
[GOAL]
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a : C^⊤⟮I, N; I', R⟯
⊢ 0 * a = 0
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a : C^⊤⟮I, N; I', R⟯
x✝ : N
⊢ ↑(0 * a) x✝ = ↑0 x✝
[PROOFSTEP]
exact zero_mul _
[GOAL]
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a : C^⊤⟮I, N; I', R⟯
⊢ a * 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a : C^⊤⟮I, N; I', R⟯
x✝ : N
⊢ ↑(a * 0) x✝ = ↑0 x✝
[PROOFSTEP]
exact mul_zero _
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
⊢ (fun c => { val := fun x => ↑(algebraMap 𝕜 A) c, property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
      1 =
    1
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
x✝ : N
⊢ ↑((fun c => { val := fun x => ↑(algebraMap 𝕜 A) c, property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
          1)
      x✝ =
    ↑1 x✝
[PROOFSTEP]
exact (algebraMap 𝕜 A).map_one
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c₁ c₂ : 𝕜
⊢ OneHom.toFun
      {
        toFun := fun c =>
          { val := fun x => ↑(algebraMap 𝕜 A) c, property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
        map_one' :=
          (_ :
            (fun c =>
                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                1 =
              1) }
      (c₁ * c₂) =
    OneHom.toFun
        {
          toFun := fun c =>
            { val := fun x => ↑(algebraMap 𝕜 A) c, property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
          map_one' :=
            (_ :
              (fun c =>
                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                  1 =
                1) }
        c₁ *
      OneHom.toFun
        {
          toFun := fun c =>
            { val := fun x => ↑(algebraMap 𝕜 A) c, property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
          map_one' :=
            (_ :
              (fun c =>
                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                  1 =
                1) }
        c₂
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c₁ c₂ : 𝕜
x✝ : N
⊢ ↑(OneHom.toFun
          {
            toFun := fun c =>
              { val := fun x => ↑(algebraMap 𝕜 A) c, property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
            map_one' :=
              (_ :
                (fun c =>
                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                    1 =
                  1) }
          (c₁ * c₂))
      x✝ =
    ↑(OneHom.toFun
            {
              toFun := fun c =>
                { val := fun x => ↑(algebraMap 𝕜 A) c,
                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
              map_one' :=
                (_ :
                  (fun c =>
                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                      1 =
                    1) }
            c₁ *
          OneHom.toFun
            {
              toFun := fun c =>
                { val := fun x => ↑(algebraMap 𝕜 A) c,
                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
              map_one' :=
                (_ :
                  (fun c =>
                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                      1 =
                    1) }
            c₂)
      x✝
[PROOFSTEP]
exact (algebraMap 𝕜 A).map_mul _ _
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            {
              toFun := fun c =>
                { val := fun x => ↑(algebraMap 𝕜 A) c,
                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
              map_one' :=
                (_ :
                  (fun c =>
                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                      1 =
                    1) },
          map_mul' :=
            (_ :
              ∀ (c₁ c₂ : 𝕜),
                OneHom.toFun
                    {
                      toFun := fun c =>
                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                      map_one' :=
                        (_ :
                          (fun c =>
                                { val := fun x => ↑(algebraMap 𝕜 A) c,
                                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                              1 =
                            1) }
                    (c₁ * c₂) =
                  OneHom.toFun
                      {
                        toFun := fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                        map_one' :=
                          (_ :
                            (fun c =>
                                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                1 =
                              1) }
                      c₁ *
                    OneHom.toFun
                      {
                        toFun := fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                        map_one' :=
                          (_ :
                            (fun c =>
                                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                1 =
                              1) }
                      c₂) })
      0 =
    0
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
x✝ : N
⊢ ↑(OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun c =>
                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                  map_one' :=
                    (_ :
                      (fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                          1 =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (c₁ c₂ : 𝕜),
                    OneHom.toFun
                        {
                          toFun := fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                          map_one' :=
                            (_ :
                              (fun c =>
                                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                  1 =
                                1) }
                        (c₁ * c₂) =
                      OneHom.toFun
                          {
                            toFun := fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                            map_one' :=
                              (_ :
                                (fun c =>
                                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                    1 =
                                  1) }
                          c₁ *
                        OneHom.toFun
                          {
                            toFun := fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                            map_one' :=
                              (_ :
                                (fun c =>
                                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                    1 =
                                  1) }
                          c₂) })
          0)
      x✝ =
    ↑0 x✝
[PROOFSTEP]
exact (algebraMap 𝕜 A).map_zero
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c₁ c₂ : 𝕜
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            {
              toFun := fun c =>
                { val := fun x => ↑(algebraMap 𝕜 A) c,
                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
              map_one' :=
                (_ :
                  (fun c =>
                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                      1 =
                    1) },
          map_mul' :=
            (_ :
              ∀ (c₁ c₂ : 𝕜),
                OneHom.toFun
                    {
                      toFun := fun c =>
                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                      map_one' :=
                        (_ :
                          (fun c =>
                                { val := fun x => ↑(algebraMap 𝕜 A) c,
                                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                              1 =
                            1) }
                    (c₁ * c₂) =
                  OneHom.toFun
                      {
                        toFun := fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                        map_one' :=
                          (_ :
                            (fun c =>
                                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                1 =
                              1) }
                      c₁ *
                    OneHom.toFun
                      {
                        toFun := fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                        map_one' :=
                          (_ :
                            (fun c =>
                                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                1 =
                              1) }
                      c₂) })
      (c₁ + c₂) =
    OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun c =>
                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                map_one' :=
                  (_ :
                    (fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (c₁ c₂ : 𝕜),
                  OneHom.toFun
                      {
                        toFun := fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                        map_one' :=
                          (_ :
                            (fun c =>
                                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                1 =
                              1) }
                      (c₁ * c₂) =
                    OneHom.toFun
                        {
                          toFun := fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                          map_one' :=
                            (_ :
                              (fun c =>
                                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                  1 =
                                1) }
                        c₁ *
                      OneHom.toFun
                        {
                          toFun := fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                          map_one' :=
                            (_ :
                              (fun c =>
                                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                  1 =
                                1) }
                        c₂) })
        c₁ +
      OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun c =>
                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                map_one' :=
                  (_ :
                    (fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (c₁ c₂ : 𝕜),
                  OneHom.toFun
                      {
                        toFun := fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                        map_one' :=
                          (_ :
                            (fun c =>
                                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                1 =
                              1) }
                      (c₁ * c₂) =
                    OneHom.toFun
                        {
                          toFun := fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                          map_one' :=
                            (_ :
                              (fun c =>
                                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                  1 =
                                1) }
                        c₁ *
                      OneHom.toFun
                        {
                          toFun := fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                          map_one' :=
                            (_ :
                              (fun c =>
                                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                  1 =
                                1) }
                        c₂) })
        c₂
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c₁ c₂ : 𝕜
x✝ : N
⊢ ↑(OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun c =>
                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                  map_one' :=
                    (_ :
                      (fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                          1 =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (c₁ c₂ : 𝕜),
                    OneHom.toFun
                        {
                          toFun := fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                          map_one' :=
                            (_ :
                              (fun c =>
                                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                  1 =
                                1) }
                        (c₁ * c₂) =
                      OneHom.toFun
                          {
                            toFun := fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                            map_one' :=
                              (_ :
                                (fun c =>
                                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                    1 =
                                  1) }
                          c₁ *
                        OneHom.toFun
                          {
                            toFun := fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                            map_one' :=
                              (_ :
                                (fun c =>
                                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                    1 =
                                  1) }
                          c₂) })
          (c₁ + c₂))
      x✝ =
    ↑(OneHom.toFun
            (↑{
                toOneHom :=
                  {
                    toFun := fun c =>
                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                    map_one' :=
                      (_ :
                        (fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                            1 =
                          1) },
                map_mul' :=
                  (_ :
                    ∀ (c₁ c₂ : 𝕜),
                      OneHom.toFun
                          {
                            toFun := fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                            map_one' :=
                              (_ :
                                (fun c =>
                                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                    1 =
                                  1) }
                          (c₁ * c₂) =
                        OneHom.toFun
                            {
                              toFun := fun c =>
                                { val := fun x => ↑(algebraMap 𝕜 A) c,
                                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                              map_one' :=
                                (_ :
                                  (fun c =>
                                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                      1 =
                                    1) }
                            c₁ *
                          OneHom.toFun
                            {
                              toFun := fun c =>
                                { val := fun x => ↑(algebraMap 𝕜 A) c,
                                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                              map_one' :=
                                (_ :
                                  (fun c =>
                                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                      1 =
                                    1) }
                            c₂) })
            c₁ +
          OneHom.toFun
            (↑{
                toOneHom :=
                  {
                    toFun := fun c =>
                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                    map_one' :=
                      (_ :
                        (fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                            1 =
                          1) },
                map_mul' :=
                  (_ :
                    ∀ (c₁ c₂ : 𝕜),
                      OneHom.toFun
                          {
                            toFun := fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                            map_one' :=
                              (_ :
                                (fun c =>
                                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                    1 =
                                  1) }
                          (c₁ * c₂) =
                        OneHom.toFun
                            {
                              toFun := fun c =>
                                { val := fun x => ↑(algebraMap 𝕜 A) c,
                                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                              map_one' :=
                                (_ :
                                  (fun c =>
                                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                      1 =
                                    1) }
                            c₁ *
                          OneHom.toFun
                            {
                              toFun := fun c =>
                                { val := fun x => ↑(algebraMap 𝕜 A) c,
                                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                              map_one' :=
                                (_ :
                                  (fun c =>
                                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                      1 =
                                    1) }
                            c₂) })
            c₂)
      x✝
[PROOFSTEP]
exact (algebraMap 𝕜 A).map_add _ _
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c : 𝕜
f : (fun x => C^⊤⟮I, N; 𝓘(𝕜, A), A⟯) c
⊢ ↑C c * f = f * ↑C c
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c : 𝕜
f : (fun x => C^⊤⟮I, N; 𝓘(𝕜, A), A⟯) c
x : N
⊢ ↑(↑C c * f) x = ↑(f * ↑C c) x
[PROOFSTEP]
exact Algebra.commutes' _ _
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c : 𝕜
f : (fun x => C^⊤⟮I, N; 𝓘(𝕜, A), A⟯) c
⊢ c • f = ↑C c * f
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c : 𝕜
f : (fun x => C^⊤⟮I, N; 𝓘(𝕜, A), A⟯) c
x : N
⊢ ↑(c • f) x = ↑(↑C c * f) x
[PROOFSTEP]
exact Algebra.smul_def' _ _
[GOAL]
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
⊢ 1 • f = f
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
x : N
⊢ ↑(1 • f) x = ↑f x
[PROOFSTEP]
exact one_smul 𝕜 (f x)
[GOAL]
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
c₁ c₂ : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
⊢ (c₁ * c₂) • f = c₁ • c₂ • f
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
c₁ c₂ : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
x : N
⊢ ↑((c₁ * c₂) • f) x = ↑(c₁ • c₂ • f) x
[PROOFSTEP]
exact mul_smul (c₁ x) (c₂ x) (f x)
[GOAL]
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
r : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ r • 0 = 0
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
r : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
x : N
⊢ ↑(r • 0) x = ↑0 x
[PROOFSTEP]
exact smul_zero _
[GOAL]
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
c : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f g : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
⊢ c • (f + g) = c • f + c • g
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
c : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f g : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
x : N
⊢ ↑(c • (f + g)) x = ↑(c • f + c • g) x
[PROOFSTEP]
exact smul_add (c x) (f x) (g x)
[GOAL]
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
c₁ c₂ : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
⊢ (c₁ + c₂) • f = c₁ • f + c₂ • f
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
c₁ c₂ : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
x : N
⊢ ↑((c₁ + c₂) • f) x = ↑(c₁ • f + c₂ • f) x
[PROOFSTEP]
exact add_smul (c₁ x) (c₂ x) (f x)
[GOAL]
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
⊢ 0 • f = 0
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
x : N
⊢ ↑(0 • f) x = ↑0 x
[PROOFSTEP]
exact zero_smul _ _
