awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
A : Type u_10
inst_14 : NormedRing A
inst_15 : NormedAlgebra 𝕜 A
inst_16 : ContMDiffRing 𝓘(𝕜, A) n A
c₁ c₂ : 𝕜
x : N
⊢ Eq.{u_10 + 1} (α := A)
    ((Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
            (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) (c₁ * c₂)) ⋯ :
          (a : N) → A)
        x :
      A)
    ((HMul.hMul (α := C^n⟮I, N; 𝓘(𝕜, A), A⟯)
            (Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
              (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) c₁) ⋯)
            (Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
              (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) c₂) ⋯) :
          (a : N) → A)
        x :
      A)

Tactic:
(algebraMap 𝕜 A).map_mul _ _

Premises used: Algebra.algebraMap, RingHom.map_mul
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
A : Type u_10
inst_14 : NormedRing A
inst_15 : NormedAlgebra 𝕜 A
inst_16 : ContMDiffRing 𝓘(𝕜, A) n A
c₁ c₂ : 𝕜
x : N
⊢ Eq.{u_10 + 1} (α := A)
    ((Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
            (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) (c₁ * c₂)) ⋯ :
          (a : N) → A)
        x :
      A)
    ((HMul.hMul (α := C^n⟮I, N; 𝓘(𝕜, A), A⟯)
            (Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
              (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) c₁) ⋯)
            (Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
              (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) c₂) ⋯) :
          (a : N) → A)
        x :
      A)

Tactic:
exact (algebraMap 𝕜 A).map_mul _ _

Premises used: Algebra.algebraMap, RingHom.map_mul
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
A : Type u_10
inst_14 : NormedRing A
inst_15 : NormedAlgebra 𝕜 A
inst_16 : ContMDiffRing 𝓘(𝕜, A) n A
h :
  ∀ (x : N),
    Eq.{u_10 + 1} (α := A)
      ((Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f) (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) 0) ⋯ :
            (a : N) → A)
          x :
        A)
      ((0 : (a : N) → A) x : A)
⊢ Eq (α := C^n⟮I, N; 𝓘(𝕜, A), A⟯)
    (Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f) (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) 0) ⋯) 0

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
A : Type u_10
inst_14 : NormedRing A
inst_15 : NormedAlgebra 𝕜 A
inst_16 : ContMDiffRing 𝓘(𝕜, A) n A
x : N
⊢ Eq.{u_10 + 1} (α := A)
    ((Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f) (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) 0) ⋯ :
          (a : N) → A)
        x :
      A)
    ((0 : (a : N) → A) x : A)

Tactic:
(algebraMap 𝕜 A).map_zero

Premises used: Algebra.algebraMap, RingHom.map_zero
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
A : Type u_10
inst_14 : NormedRing A
inst_15 : NormedAlgebra 𝕜 A
inst_16 : ContMDiffRing 𝓘(𝕜, A) n A
x : N
⊢ Eq.{u_10 + 1} (α := A)
    ((Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f) (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) 0) ⋯ :
          (a : N) → A)
        x :
      A)
    ((0 : (a : N) → A) x : A)

Tactic:
exact (algebraMap 𝕜 A).map_zero

Premises used: Algebra.algebraMap, RingHom.map_zero
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
A : Type u_10
inst_14 : NormedRing A
inst_15 : NormedAlgebra 𝕜 A
inst_16 : ContMDiffRing 𝓘(𝕜, A) n A
c₁ c₂ : 𝕜
h :
  ∀ (x : N),
    Eq.{u_10 + 1} (α := A)
      ((Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
              (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) (c₁ + c₂)) ⋯ :
            (a : N) → A)
          x :
        A)
      ((HAdd.hAdd (α := C^n⟮I, N; 𝓘(𝕜, A), A⟯)
              (Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
                (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) c₁) ⋯)
              (Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
                (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) c₂) ⋯) :
            (a : N) → A)
          x :
        A)
⊢ Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f) (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) (c₁ + c₂))
      ⋯ =
    HAdd.hAdd (α := C^n⟮I, N; 𝓘(𝕜, A), A⟯)
      (Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f) (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) c₁) ⋯)
      (Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f) (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) c₂) ⋯)

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
A : Type u_10
inst_14 : NormedRing A
inst_15 : NormedAlgebra 𝕜 A
inst_16 : ContMDiffRing 𝓘(𝕜, A) n A
c₁ c₂ : 𝕜
x : N
⊢ Eq.{u_10 + 1} (α := A)
    ((Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
            (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) (c₁ + c₂)) ⋯ :
          (a : N) → A)
        x :
      A)
    ((HAdd.hAdd (α := C^n⟮I, N; 𝓘(𝕜, A), A⟯)
            (Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
              (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) c₁) ⋯)
            (Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
              (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) c₂) ⋯) :
          (a : N) → A)
        x :
      A)

Tactic:
(algebraMap 𝕜 A).map_add _ _

Premises used: Algebra.algebraMap, RingHom.map_add
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
A : Type u_10
inst_14 : NormedRing A
inst_15 : NormedAlgebra 𝕜 A
inst_16 : ContMDiffRing 𝓘(𝕜, A) n A
c₁ c₂ : 𝕜
x : N
⊢ Eq.{u_10 + 1} (α := A)
    ((Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
            (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) (c₁ + c₂)) ⋯ :
          (a : N) → A)
        x :
      A)
    ((HAdd.hAdd (α := C^n⟮I, N; 𝓘(𝕜, A), A⟯)
            (Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
              (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) c₁) ⋯)
            (Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
              (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) c₂) ⋯) :
          (a : N) → A)
        x :
      A)

Tactic:
exact (algebraMap 𝕜 A).map_add _ _

Premises used: Algebra.algebraMap, RingHom.map_add
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
A : Type u_10
inst_14 : NormedRing A
inst_15 : NormedAlgebra 𝕜 A
inst_16 : ContMDiffRing 𝓘(𝕜, A) n A
c : 𝕜
f : C^n⟮I, N; 𝓘(𝕜, A), A⟯
h :
  ∀ (x : N),
    Eq.{u_10 + 1} (α := A)
      ((HMul.hMul (α := C^n⟮I, N; 𝓘(𝕜, A), A⟯) ((C : (a : 𝕜) → C^n⟮I, N; 𝓘(𝕜, A), A⟯) c : C^n⟮I, N; 𝓘(𝕜, A), A⟯) f :
            (a : N) → A)
          x :
        A)
      ((HMul.hMul (β := C^n⟮I, N; 𝓘(𝕜, A), A⟯) f ((C : (a : 𝕜) → C^n⟮I, N; 𝓘(𝕜, A), A⟯) c : C^n⟮I, N; 𝓘(𝕜, A), A⟯) :
            (a : N) → A)
          x :
        A)
⊢ HMul.hMul (α := C^n⟮I, N; 𝓘(𝕜, A), A⟯) ((C : (a : 𝕜) → C^n⟮I, N; 𝓘(𝕜, A), A⟯) c : C^n⟮I, N; 𝓘(𝕜, A), A⟯) f =
    HMul.hMul (β := C^n⟮I, N; 𝓘(𝕜, A), A⟯) f ((C : (a : 𝕜) → C^n⟮I, N; 𝓘(𝕜, A), A⟯) c : C^n⟮I, N; 𝓘(𝕜, A), A⟯)

Tactic:
ext x
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
A : Type u_10
inst_14 : NormedRing A
inst_15 : NormedAlgebra 𝕜 A
inst_16 : ContMDiffRing 𝓘(𝕜, A) n A
c : 𝕜
f : C^n⟮I, N; 𝓘(𝕜, A), A⟯
x : N
⊢ Eq.{u_10 + 1} (α := A)
    ((HMul.hMul (α := C^n⟮I, N; 𝓘(𝕜, A), A⟯) ((C : (a : 𝕜) → C^n⟮I, N; 𝓘(𝕜, A), A⟯) c : C^n⟮I, N; 𝓘(𝕜, A), A⟯) f :
          (a : N) → A)
        x :
      A)
    ((HMul.hMul (β := C^n⟮I, N; 𝓘(𝕜, A), A⟯) f ((C : (a : 𝕜) → C^n⟮I, N; 𝓘(𝕜, A), A⟯) c : C^n⟮I, N; 𝓘(𝕜, A), A⟯) :
          (a : N) → A)
        x :
      A)

Tactic:
Algebra.commutes' _ _

Premises used: Algebra.commutes'
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
A : Type u_10
inst_14 : NormedRing A
inst_15 : NormedAlgebra 𝕜 A
inst_16 : ContMDiffRing 𝓘(𝕜, A) n A
c : 𝕜
f : C^n⟮I, N; 𝓘(𝕜, A), A⟯
x : N
⊢ Eq.{u_10 + 1} (α := A)
    ((HMul.hMul (α := C^n⟮I, N; 𝓘(𝕜, A), A⟯) ((C : (a : 𝕜) → C^n⟮I, N; 𝓘(𝕜, A), A⟯) c : C^n⟮I, N; 𝓘(𝕜, A), A⟯) f :
          (a : N) → A)
        x :
      A)
    ((HMul.hMul (β := C^n⟮I, N; 𝓘(𝕜, A), A⟯) f ((C : (a : 𝕜) → C^n⟮I, N; 𝓘(𝕜, A), A⟯) c : C^n⟮I, N; 𝓘(𝕜, A), A⟯) :
          (a : N) → A)
        x :
      A)

Tactic:
exact Algebra.commutes' _ _

Premises used: Algebra.commutes'
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
A : Type u_10
inst_14 : NormedRing A
inst_15 : NormedAlgebra 𝕜 A
inst_16 : ContMDiffRing 𝓘(𝕜, A) n A
c : 𝕜
f : C^n⟮I, N; 𝓘(𝕜, A), A⟯
h :
  ∀ (x : N),
    Eq.{u_10 + 1} (α := A) ((c • f : (a : N) → A) x : A)
      ((HMul.hMul (α := C^n⟮I, N; 𝓘(𝕜, A), A⟯) ((C : (a : 𝕜) → C^n⟮I, N; 𝓘(𝕜, A), A⟯) c : C^n⟮I, N; 𝓘(𝕜, A), A⟯) f :
            (a : N) → A)
          x :
        A)
⊢ c • f = HMul.hMul (α := C^n⟮I, N; 𝓘(𝕜, A), A⟯) ((C : (a : 𝕜) → C^n⟮I, N; 𝓘(𝕜, A), A⟯) c : C^n⟮I, N; 𝓘(𝕜, A), A⟯) f

Tactic:
ext x
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
A : Type u_10
inst_14 : NormedRing A
inst_15 : NormedAlgebra 𝕜 A
inst_16 : ContMDiffRing 𝓘(𝕜, A) n A
c : 𝕜
f : C^n⟮I, N; 𝓘(𝕜, A), A⟯
x : N
⊢ Eq.{u_10 + 1} (α := A) ((c • f : (a : N) → A) x : A)
    ((HMul.hMul (α := C^n⟮I, N; 𝓘(𝕜, A), A⟯) ((C : (a : 𝕜) → C^n⟮I, N; 𝓘(𝕜, A), A⟯) c : C^n⟮I, N; 𝓘(𝕜, A), A⟯) f :
          (a : N) → A)
        x :
      A)

Tactic:
Algebra.smul_def' _ _

Premises used: Algebra.smul_def'
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
A : Type u_10
inst_14 : NormedRing A
inst_15 : NormedAlgebra 𝕜 A
inst_16 : ContMDiffRing 𝓘(𝕜, A) n A
c : 𝕜
f : C^n⟮I, N; 𝓘(𝕜, A), A⟯
x : N
⊢ Eq.{u_10 + 1} (α := A) ((c • f : (a : N) → A) x : A)
    ((HMul.hMul (α := C^n⟮I, N; 𝓘(𝕜, A), A⟯) ((C : (a : 𝕜) → C^n⟮I, N; 𝓘(𝕜, A), A⟯) c : C^n⟮I, N; 𝓘(𝕜, A), A⟯) f :
          (a : N) → A)
        x :
      A)

Tactic:
exact Algebra.smul_def' _ _

Premises used: Algebra.smul_def'
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
N : Type u_6
inst_4 : TopologicalSpace N
inst_5 : ChartedSpace H N
E'' : Type u_7
inst_6 : NormedAddCommGroup E''
inst_7 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_8 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_9 : TopologicalSpace N'
inst_10 : ChartedSpace H'' N'
n : ℕ∞ω
V : Type u_10
inst_11 : NormedAddCommGroup V
inst_12 : NormedSpace 𝕜 V
f : C^n⟮I'', N'; 𝓘(𝕜, 𝕜), 𝕜⟯
g : C^n⟮I'', N'; 𝓘(𝕜, V), V⟯
h : C^n⟮I, N; I'', N'⟯
⊢ (f • g).comp h = f.comp h • g.comp h

Tactic:
rfl

Premises used: ContMDiffMap.comp, rfl
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
V : Type u_10
inst_14 : NormedAddCommGroup V
inst_15 : NormedSpace 𝕜 V
c₁ c₂ : C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^n⟮I, N; 𝓘(𝕜, V), V⟯
h : ∀ (x : N), Eq.{u_10 + 1} (α := V) (((c₁ * c₂) • f : (a : N) → V) x : V) ((c₁ • c₂ • f : (a : N) → V) x : V)
⊢ (c₁ * c₂) • f = c₁ • c₂ • f

Tactic:
ext x
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
V : Type u_10
inst_14 : NormedAddCommGroup V
inst_15 : NormedSpace 𝕜 V
c₁ c₂ : C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^n⟮I, N; 𝓘(𝕜, V), V⟯
x : N
⊢ Eq.{u_10 + 1} (α := V) (((c₁ * c₂) • f : (a : N) → V) x : V) ((c₁ • c₂ • f : (a : N) → V) x : V)

Tactic:
mul_smul (c₁ x) (c₂ x) (f x)

Premises used: DFunLike.coe, SemigroupAction.mul_smul
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
V : Type u_10
inst_14 : NormedAddCommGroup V
inst_15 : NormedSpace 𝕜 V
c₁ c₂ : C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^n⟮I, N; 𝓘(𝕜, V), V⟯
x : N
⊢ Eq.{u_10 + 1} (α := V) (((c₁ * c₂) • f : (a : N) → V) x : V) ((c₁ • c₂ • f : (a : N) → V) x : V)

Tactic:
exact mul_smul (c₁ x) (c₂ x) (f x)

Premises used: DFunLike.coe, SemigroupAction.mul_smul
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
V : Type u_10
inst_14 : NormedAddCommGroup V
inst_15 : NormedSpace 𝕜 V
f : C^n⟮I, N; 𝓘(𝕜, V), V⟯
h :
  ∀ (x : N),
    Eq.{u_10 + 1} (α := V) ((HSMul.hSMul (α := C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯) 1 f : (a : N) → V) x : V)
      ((f : (a : N) → V) x : V)
⊢ HSMul.hSMul (α := C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯) 1 f = f

Tactic:
ext x
-- Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
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
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
V : Type u_10
inst_14 : NormedAddCommGroup V
inst_15 : NormedSpace 𝕜 V
f : C^n⟮I, N; 𝓘(𝕜, V), V⟯
x : N
⊢ Eq.{u_10 + 1} (α := V) ((HSMul.hSMul (α := C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯) 1 f : (a : N) → V) x : V) ((f : (a : N) → V) x : V)

Tactic:
one_smul 𝕜 (f x)

Premises used: one_smul, DFunLike.coe