[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : ℕ∞
⊢ Algebra 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
[PROOFSTEP]
infer_instance
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : ℕ∞
⊢ IsScalarTower 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
[PROOFSTEP]
infer_instance
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : ℕ∞
x : M
k : 𝕜
f : C^⊤⟮I, M; 𝕜⟯⟨x⟩
h : 𝕜
⊢ (k • f) • h = k • f • h
[PROOFSTEP]
rw [smul_def, smul_def, SmoothMap.coe_smul, Pi.smul_apply, smul_eq_mul, smul_eq_mul, mul_assoc]
[GOAL]
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞
X Y : Derivation 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ g✝ : C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^⊤⟮I, M; I', M'⟯
x : M
y : M'
h : ↑f x = y
v : PointDerivation I x
g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩
⊢ (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
    (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g'
[PROOFSTEP]
dsimp
[GOAL]
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞
X Y : Derivation 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ g✝ : C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^⊤⟮I, M; I', M'⟯
x : M
y : M'
h : ↑f x = y
v : PointDerivation I x
g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩
⊢ ↑v (ContMDiffMap.comp (g + g') f) = ↑v (ContMDiffMap.comp g f) + ↑v (ContMDiffMap.comp g' f)
[PROOFSTEP]
rw [SmoothMap.add_comp, Derivation.map_add]
[GOAL]
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞
X Y : Derivation 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ g✝ : C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^⊤⟮I, M; I', M'⟯
x : M
y : M'
h : ↑f x = y
v : PointDerivation I x
k : 𝕜
g : C^⊤⟮I', M'; 𝕜⟯⟨y⟩
⊢ AddHom.toFun
      { toFun := fun g => ↑v (ContMDiffMap.comp g f),
        map_add' :=
          (_ :
            ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
              (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') }
      (k • g) =
    ↑(RingHom.id 𝕜) k •
      AddHom.toFun
        { toFun := fun g => ↑v (ContMDiffMap.comp g f),
          map_add' :=
            (_ :
              ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                  (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') }
        g
[PROOFSTEP]
dsimp
[GOAL]
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞
X Y : Derivation 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ g✝ : C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^⊤⟮I, M; I', M'⟯
x : M
y : M'
h : ↑f x = y
v : PointDerivation I x
k : 𝕜
g : C^⊤⟮I', M'; 𝕜⟯⟨y⟩
⊢ ↑v (ContMDiffMap.comp (k • g) f) = k * ↑v (ContMDiffMap.comp g f)
[PROOFSTEP]
rw [SmoothMap.smul_comp, Derivation.map_smul, smul_eq_mul]
[GOAL]
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞
X Y : Derivation 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ g✝ : C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^⊤⟮I, M; I', M'⟯
x : M
y : M'
h : ↑f x = y
v : PointDerivation I x
g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩
⊢ ↑{
          toAddHom :=
            { toFun := fun g => ↑v (ContMDiffMap.comp g f),
              map_add' :=
                (_ :
                  ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                    (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                      (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') },
          map_smul' :=
            (_ :
              ∀ (k : 𝕜) (g : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                AddHom.toFun
                    { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                      map_add' :=
                        (_ :
                          ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                            (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                              (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') }
                    (k • g) =
                  ↑(RingHom.id 𝕜) k •
                    AddHom.toFun
                      { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                        map_add' :=
                          (_ :
                            ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                              (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                                (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') }
                      g) }
      (g * g') =
    g •
        ↑{
              toAddHom :=
                { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                  map_add' :=
                    (_ :
                      ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                        (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                          (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') },
              map_smul' :=
                (_ :
                  ∀ (k : 𝕜) (g : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                    AddHom.toFun
                        { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                          map_add' :=
                            (_ :
                              ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                                (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                                  (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') }
                        (k • g) =
                      ↑(RingHom.id 𝕜) k •
                        AddHom.toFun
                          { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                            map_add' :=
                              (_ :
                                ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                                  (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                                    (fun g => ↑v (ContMDiffMap.comp g f)) g +
                                      (fun g => ↑v (ContMDiffMap.comp g f)) g') }
                          g) }
          g' +
      g' •
        ↑{
              toAddHom :=
                { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                  map_add' :=
                    (_ :
                      ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                        (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                          (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') },
              map_smul' :=
                (_ :
                  ∀ (k : 𝕜) (g : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                    AddHom.toFun
                        { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                          map_add' :=
                            (_ :
                              ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                                (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                                  (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') }
                        (k • g) =
                      ↑(RingHom.id 𝕜) k •
                        AddHom.toFun
                          { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                            map_add' :=
                              (_ :
                                ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                                  (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                                    (fun g => ↑v (ContMDiffMap.comp g f)) g +
                                      (fun g => ↑v (ContMDiffMap.comp g f)) g') }
                          g) }
          g
[PROOFSTEP]
dsimp
[GOAL]
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞
X Y : Derivation 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ g✝ : C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^⊤⟮I, M; I', M'⟯
x : M
y : M'
h : ↑f x = y
v : PointDerivation I x
g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩
⊢ ↑v (ContMDiffMap.comp (g * g') f) = g • ↑v (ContMDiffMap.comp g' f) + g' • ↑v (ContMDiffMap.comp g f)
[PROOFSTEP]
rw [SmoothMap.mul_comp, Derivation.leibniz, PointedSmoothMap.smul_def, ContMDiffMap.comp_apply,
  PointedSmoothMap.smul_def, ContMDiffMap.comp_apply, h]
[GOAL]
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞
X Y : Derivation 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ g✝ : C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^⊤⟮I, M; I', M'⟯
x : M
y : M'
h : ↑f x = y
v : PointDerivation I x
g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩
⊢ ↑g y * ↑v (ContMDiffMap.comp g' f) + ↑g' y * ↑v (ContMDiffMap.comp g f) =
    g • ↑v (ContMDiffMap.comp g' f) + g' • ↑v (ContMDiffMap.comp g f)
[PROOFSTEP]
norm_cast
