awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (↑I : H → E) ×ˢ range (↑I' : H' → E')) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
D0 :
  DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
      ((↑I : H → E) ((↑(chartAt H (w.proj (E := TangentSpace I))) : M → H) (w.proj (E := TangentSpace I))),
        (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
⊢ DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))),
        (↑I' : H' → E')
          ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I')))).2

Tactic:
D0

Premises used: ModelWithCorners.toFun'
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (↑I : H → E) ×ˢ range (↑I' : H' → E')) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
D0 :
  DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
      ((↑I : H → E) ((↑(chartAt H (w.proj (E := TangentSpace I))) : M → H) (w.proj (E := TangentSpace I))),
        (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
⊢ DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))),
        (↑I' : H' → E')
          ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I')))).2

Tactic:
exact D0
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (↑I : H → E) ×ˢ range (↑I' : H' → E')) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
D0 :
  DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
      ((↑I : H → E) ((↑(chartAt H (w.proj (E := TangentSpace I))) : M → H) (w.proj (E := TangentSpace I))),
        (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
⊢ Eq.{u_5 + 1} (α := E')
    ((fderivWithin 𝕜 φ (range (↑I' : H' → E'))
              ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))),
                  (↑I' : H' → E')
                    ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H')
                      (p.2.proj (E := TangentSpace I')))).2 ∘SL
            fderivWithin 𝕜 Prod.snd (range (↑I : H → E) ×ˢ range (↑I' : H' → E'))
              ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))),
                (↑I' : H' → E')
                  ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I')))) :
          (a : E × E') → E')
        (p.1.snd (E := TangentSpace I), p.2.snd (E := TangentSpace I')) :
      E')
    ((fderivWithin 𝕜 φ (range (↑I' : H' → E'))
            ((↑I' : H' → E')
              ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I')))) :
          (a : E') → E')
        (p.2.snd (E := TangentSpace I')) :
      E')

Tactic:
simp [fderivWithin_snd, U]

Premises used: fderivWithin_snd
-- Module: Mathlib.Geometry.Manifold.ContMDiffMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_4
inst_5 : TopologicalSpace H
H' : Type u_5
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f : C^n⟮I, M; I', M'⟯
⊢ ContMDiff.{u_1, u_2, u_4, u_6, u_3, u_5, u_7} I (M := M) I' (M' := M') n (⇑f : (a : M) → M')

Tactic:
f.prop

Premises used: Subtype.prop
-- Module: Mathlib.Geometry.Manifold.ContMDiffMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_4
inst_5 : TopologicalSpace H
H' : Type u_5
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f : M → M'
hf : ContMDiff I I' n f
⊢ (⇑(Subtype.mk (p := fun (f : M → M') ↦ ContMDiff I I' n f) f hf) : (a : M) → M') = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.ContMDiffMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_4
inst_5 : TopologicalSpace H
H' : Type u_5
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : C^n⟮I, M; I', M'⟯
h : Eq (α := (a : M) → M') (⇑f : (a : M) → M') (⇑g : (a : M) → M')
⊢ f = g

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Geometry.Manifold.ContMDiffMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_4
inst_5 : TopologicalSpace H
H' : Type u_5
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : C^n⟮I, M; I', M'⟯
h : ∀ (x : M), Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') x : M') ((g : (a : M) → M') x : M')
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Geometry.Manifold.ContMDiffMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_4
inst_5 : TopologicalSpace H
H' : Type u_5
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
n : ℕ∞ω
f : C^n⟮I', M'; I'', M''⟯
g : C^n⟮I, M; I', M'⟯
x : M
⊢ Eq.{u_10 + 1} (α := M'') ((f.comp g : (a : M) → M'') x : M'') ((f : (a : M') → M'') ((g : (a : M) → M') x : M') : M'')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.DerivationBundle
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
⊢ Algebra 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Manifold.DerivationBundle
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
⊢ IsScalarTower 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Manifold.DerivationBundle
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
x : M
⊢ IsScalarTower 𝕜 C^∞⟮I, M; 𝕜⟯⟨x⟩ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯

Tactic:
IsScalarTower.right

Premises used: IsScalarTower.right, PointedContMDiffMap
-- Module: Mathlib.Geometry.Manifold.DerivationBundle
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
f : C^∞⟮I, M; 𝕜⟯⟨x⟩
k : 𝕜
⊢ f • k = HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) k

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.DerivationBundle
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
x : M
k : 𝕜
f : C^∞⟮I, M; 𝕜⟯⟨x⟩
h : 𝕜
rw : HMul.hMul (α := 𝕜) ((k • f : (a : M) → 𝕜) x : 𝕜) h = k • f • h
rw₁ : HMul.hMul (α := 𝕜) ((k • f : (a : M) → 𝕜) x : 𝕜) h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
rw₂ : HSMul.hSMul (β := (a : M) → 𝕜) k (⇑f : (a : M) → 𝕜) x * h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
rw₃ : HSMul.hSMul (β := 𝕜) k ((f : (a : M) → 𝕜) x : 𝕜) * h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
rw₄ : HMul.hMul (β := 𝕜) k ((f : (a : M) → 𝕜) x : 𝕜) * h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
rw₅ : HMul.hMul (β := 𝕜) k ((f : (a : M) → 𝕜) x : 𝕜) * h = k * HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
rw₆ rw₇ : k * HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h = k * HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
⊢ (k • f) • h = k • f • h

Tactic:
rw [smul_def, smul_def, ContMDiffMap.coe_smul, Pi.smul_apply, smul_eq_mul, smul_eq_mul,
      mul_assoc]

Premises used: mul_assoc, PointedContMDiffMap.smul_def, ContMDiffMap.coe_smul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Geometry.Manifold.DerivationBundle
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
x : M
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((evalAt x : (a : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I x) X :
            PointDerivation I x) :
          (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜)
        f :
      𝕜)
    ((((X : (a : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯) : (a : M) → 𝕜) x : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.DerivationBundle
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f_1 : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : (f : (a : M) → M') x = y
v : PointDerivation I x
g g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
rw :
  (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f + ContMDiffMap.comp g' f) =
    HAdd.hAdd (α := 𝕜) (β := 𝕜) ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
      ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜)
rw₁ rw₂ :
  HAdd.hAdd (α := 𝕜) (β := 𝕜) ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
      ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜) =
    HAdd.hAdd (α := 𝕜) (β := 𝕜) ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
      ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜)
⊢ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp (g + g') f) =
    HAdd.hAdd (α := 𝕜) (β := 𝕜) ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
      ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜)

Tactic:
rw [ContMDiffMap.add_comp, Derivation.map_add]

Premises used: ContMDiffMap.add_comp, Derivation.map_add
-- Module: Mathlib.Geometry.Manifold.DerivationBundle
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f_1 : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : (f : (a : M) → M') x = y
v : PointDerivation I x
k : 𝕜
g : C^∞⟮I', M'; 𝕜⟯⟨y⟩
dsimp :
  (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp (k • g) f) =
    HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
⊢ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp (k • g) f) =
    HSMul.hSMul (α := 𝕜) (β := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) k : 𝕜)
      ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)

Tactic:
dsimp
-- Module: Mathlib.Geometry.Manifold.DerivationBundle
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f_1 : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : (f : (a : M) → M') x = y
v : PointDerivation I x
k : 𝕜
g : C^∞⟮I', M'; 𝕜⟯⟨y⟩
rw :
  (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (k • ContMDiffMap.comp g f) =
    HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
rw₁ :
  HSMul.hSMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜) =
    HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
rw₂ rw₃ :
  HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜) =
    HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
⊢ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp (k • g) f) =
    HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)

Tactic:
rw [ContMDiffMap.smul_comp, Derivation.map_smul, smul_eq_mul]

Premises used: ContMDiffMap.smul_comp, Derivation.map_smul, smul_eq_mul
-- Module: Mathlib.Geometry.Manifold.DerivationBundle
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f_1 : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : (f : (a : M) → M') x = y
v : PointDerivation I x
g g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
dsimp :
  (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp (g * g') f) =
    HSMul.hSMul (β := 𝕜) g ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜) +
      HSMul.hSMul (β := 𝕜) g' ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
⊢ ({ toFun := fun (g : C^∞⟮I', M'; 𝕜⟯⟨y⟩) ↦ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f), map_add' := ⋯,
          map_smul' := ⋯ } :
        (a : C^∞⟮I', M'; 𝕜⟯⟨y⟩) → 𝕜)
      (g * g') =
    HSMul.hSMul (β := 𝕜) g
        (({ toFun := fun (g : C^∞⟮I', M'; 𝕜⟯⟨y⟩) ↦ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f),
                map_add' := ⋯, map_smul' := ⋯ : C^∞⟮I', M'; 𝕜⟯⟨y⟩ →ₗ[𝕜] 𝕜 } :
              (a : C^∞⟮I', M'; 𝕜⟯⟨y⟩) → 𝕜)
            g' :
          𝕜) +
      HSMul.hSMul (β := 𝕜) g'
        (({ toFun := fun (g : C^∞⟮I', M'; 𝕜⟯⟨y⟩) ↦ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f),
                map_add' := ⋯, map_smul' := ⋯ : C^∞⟮I', M'; 𝕜⟯⟨y⟩ →ₗ[𝕜] 𝕜 } :
              (a : C^∞⟮I', M'; 𝕜⟯⟨y⟩) → 𝕜)
            g :
          𝕜)

Tactic:
dsimp
-- Module: Mathlib.Geometry.Manifold.DerivationBundle
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f_1 : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : (f : (a : M) → M') x = y
v : PointDerivation I x
g g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
rw :
  HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : M') → 𝕜) y : 𝕜)
        ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜) +
      HMul.hMul (α := 𝕜) (β := 𝕜) ((g' : (a : M') → 𝕜) y : 𝕜)
        ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜) =
    HSMul.hSMul (β := 𝕜) g ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜) +
      HSMul.hSMul (β := 𝕜) g' ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
⊢ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp (g * g') f) =
    HSMul.hSMul (β := 𝕜) g ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜) +
      HSMul.hSMul (β := 𝕜) g' ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)

Tactic:
rw [ContMDiffMap.mul_comp, Derivation.leibniz,
          PointedContMDiffMap.smul_def, ContMDiffMap.comp_apply,
          PointedContMDiffMap.smul_def, ContMDiffMap.comp_apply, h]

Premises used: PointedContMDiffMap.smul_def, Derivation.leibniz, ContMDiffMap.mul_comp, ContMDiffMap.comp_apply
-- Module: Mathlib.Geometry.Manifold.DerivationBundle
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f_1 : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : (f : (a : M) → M') x = y
v : PointDerivation I x
g g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : M') → 𝕜) y : 𝕜)
        ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜) +
      HMul.hMul (α := 𝕜) (β := 𝕜) ((g' : (a : M') → 𝕜) y : 𝕜)
        ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜) =
    HSMul.hSMul (β := 𝕜) g ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜) +
      HSMul.hSMul (β := 𝕜) g' ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)

Tactic:
norm_cast