awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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 : ℕ∞ω
G' : Type u_10
inst_14 : Monoid G'
inst_15 : TopologicalSpace G'
inst_16 : ChartedSpace H' G'
inst_17 : ContMDiffMul I' n G'
G'' : Type u_11
inst_18 : Monoid G''
inst_19 : TopologicalSpace G''
inst_20 : ChartedSpace H'' G''
inst_21 : ContMDiffMul I'' n G''
φ : G' →* G''
hφ : ContMDiff.{u_1, u_3, u_5, u_10, u_7, u_8, u_11} I' (M := G') I'' (M' := G'') n (⇑φ : (a : G') → G'')
f g : C^n⟮I, N; I', G'⟯
x : N
⊢ Eq.{u_11 + 1} (α := G'')
    ((Subtype.mk (p := fun (f : N → G'') ↦ ContMDiff I I'' n f)
            (Function.comp.{u_6 + 1, u_10 + 1, u_11 + 1} (β := G') (⇑φ : (a : G') → G'') (⇑(f * g) : (a : N) → G')) ⋯ :
          (a : N) → G'')
        x :
      G'')
    ((Subtype.mk (p := fun (f : N → G'') ↦ ContMDiff I I'' n f)
              (Function.comp.{u_6 + 1, u_10 + 1, u_11 + 1} (β := G') (⇑φ : (a : G') → G'') (⇑f : (a : N) → G')) ⋯ *
            Subtype.mk (p := fun (f : N → G'') ↦ ContMDiff I I'' n f)
              (Function.comp.{u_6 + 1, u_10 + 1, u_11 + 1} (β := G') (⇑φ : (a : G') → G'') (⇑g : (a : N) → G')) ⋯ :
          (a : N) → G'')
        x :
      G'')
have h : (φ : (a : G') → G'') (HMul.hMul (α := G') (β := G') ((f : (a : N) → G') x : G') ((g : (a : N) → G') x : G')) =
  HMul.hMul (α := G'') (β := G'') ((φ : (a : G') → G'') ((f : (a : N) → G') x : G') : G'')
    ((φ : (a : G') → G'') ((g : (a : N) → G') x : G') : G'')
Tactic: change φ (f x * g x) = φ (f x) * φ (g x)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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 : ℕ∞ω
G : Type u_10
inst_14 : Group G
inst_15 : TopologicalSpace G
inst_16 : ChartedSpace H' G
inst_17 : LieGroup I' n G
f g : C^n⟮I, N; I', G⟯
⊢ f / g = f * Subtype.mk (p := fun (f : N → G) ↦ ContMDiff I I' n f) (fun (x : N) ↦ ((g : (a : N) → G) x)⁻¹) ⋯
have h : ∀ (x : N),
  Eq.{u_10 + 1} (α := G) ((f / g : (a : N) → G) x : G)
    ((f * Subtype.mk (p := fun (f : N → G) ↦ ContMDiff I I' n f) (fun (x : N) ↦ ((g : (a : N) → G) x)⁻¹) sorry :
          (a : N) → G)
        x :
      G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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 : ℕ∞ω
G : Type u_10
inst_14 : Group G
inst_15 : TopologicalSpace G
inst_16 : ChartedSpace H' G
inst_17 : LieGroup I' n G
a : C^n⟮I, N; I', G⟯
⊢ Subtype.mk (p := fun (f : N → G) ↦ ContMDiff I I' n f) (fun (x : N) ↦ ((a : (a : N) → G) x)⁻¹) ⋯ * a = 1
have h : ∀ (x : N),
  Eq.{u_10 + 1} (α := G)
    ((Subtype.mk (p := fun (f : N → G) ↦ ContMDiff I I' n f) (fun (x : N) ↦ ((a : (a : N) → G) x)⁻¹) sorry * a :
          (a : N) → G)
        x :
      G)
    ((1 : (a : N) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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 : ℕ∞ω
R : Type u_10
inst_14 : Semiring R
inst_15 : TopologicalSpace R
inst_16 : ChartedSpace H' R
inst_17 : ContMDiffRing I' n R
a : C^n⟮I, N; I', R⟯
⊢ 0 * a = 0
have h : ∀ (x : N), Eq.{u_10 + 1} (α := R) ((0 * a : (a : N) → R) x : R) ((0 : (a : N) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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 : ℕ∞ω
R : Type u_10
inst_14 : Semiring R
inst_15 : TopologicalSpace R
inst_16 : ChartedSpace H' R
inst_17 : ContMDiffRing I' n R
a : C^n⟮I, N; I', R⟯
⊢ a * 0 = 0
have h : ∀ (x : N), Eq.{u_10 + 1} (α := R) ((a * 0 : (a : N) → R) x : R) ((0 : (a : N) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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 : ℕ∞ω
R : Type u_10
inst_14 : Semiring R
inst_15 : TopologicalSpace R
inst_16 : ChartedSpace H' R
inst_17 : ContMDiffRing I' n R
a b c : C^n⟮I, N; I', R⟯
⊢ a * (b + c) = a * b + a * c
have h : ∀ (x : N), Eq.{u_10 + 1} (α := R) ((a * (b + c) : (a : N) → R) x : R) ((a * b + a * c : (a : N) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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 : ℕ∞ω
R : Type u_10
inst_14 : Semiring R
inst_15 : TopologicalSpace R
inst_16 : ChartedSpace H' R
inst_17 : ContMDiffRing I' n R
a b c : C^n⟮I, N; I', R⟯
⊢ (a + b) * c = a * c + b * c
have h : ∀ (x : N), Eq.{u_10 + 1} (α := R) (((a + b) * c : (a : N) → R) x : R) ((a * c + b * c : (a : N) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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
⊢ 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) 1) ⋯) 1
have 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) 1) sorry :
          (a : N) → A)
        x :
      A)
    ((1 : (a : N) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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₂ : 𝕜
⊢ Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f) (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) (c₁ * c₂))
      ⋯ =
    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₂) ⋯)
have 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₂)) sorry :
          (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₁) sorry)
            (Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
              (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) c₂) sorry) :
          (a : N) → A)
        x :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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
⊢ 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
have 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) sorry :
          (a : N) → A)
        x :
      A)
    ((0 : (a : N) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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₂ : 𝕜
⊢ 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₂) ⋯)
have 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₂)) sorry :
          (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₁) sorry)
            (Subtype.mk (p := fun (f : N → A) ↦ ContMDiff I 𝓘(𝕜, A) n f)
              (fun (x : N) ↦ (algebraMap 𝕜 A : (a : 𝕜) → A) c₂) sorry) :
          (a : N) → A)
        x :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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⟯
⊢ 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⟯)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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⟯
⊢ 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
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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⟯
⊢ (c₁ * c₂) • f = c₁ • c₂ • f
have h : ∀ (x : N), Eq.{u_10 + 1} (α := V) (((c₁ * c₂) • f : (a : N) → V) x : V) ((c₁ • c₂ • f : (a : N) → V) x : V)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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⟯
⊢ HSMul.hSMul (α := C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯) 1 f = f
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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
r : C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ HSMul.hSMul (β := C^n⟮I, N; 𝓘(𝕜, V), V⟯) r 0 = 0
have h : ∀ (x : N),
  Eq.{u_10 + 1} (α := V) ((HSMul.hSMul (β := C^n⟮I, N; 𝓘(𝕜, V), V⟯) r 0 : (a : N) → V) x : V) ((0 : (a : N) → V) x : V)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f g : C^n⟮I, N; 𝓘(𝕜, V), V⟯
⊢ c • (f + g) = c • f + c • g
have h : ∀ (x : N), Eq.{u_10 + 1} (α := V) ((c • (f + g) : (a : N) → V) x : V) ((c • f + c • g : (a : N) → V) x : V)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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⟯
⊢ (c₁ + c₂) • f = c₁ • f + c₂ • f
have h : ∀ (x : N), Eq.{u_10 + 1} (α := V) (((c₁ + c₂) • f : (a : N) → V) x : V) ((c₁ • f + c₂ • f : (a : N) → V) x : V)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (goal)
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⟯
⊢ HSMul.hSMul (α := C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯) 0 f = 0
have h : ∀ (x : N),
  Eq.{u_10 + 1} (α := V) ((HSMul.hSMul (α := C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯) 0 f : (a : N) → V) x : V) ((0 : (a : N) → V) x : V)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Structures (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) 𝓘(𝕜, 𝕜) (M' := 𝕜) n fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2
have rw : (Continuous (Y := 𝕜) fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2) ∧
  ∀ (x : 𝕜 × 𝕜) (y : 𝕜),
    ContDiffOn 𝕜 n
      ((↑(extChartAt 𝓘(𝕜, 𝕜) y) : 𝕜 → 𝕜) ∘
        (fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2) ∘ (↑(extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).symm : 𝕜 × 𝕜 → 𝕜 × 𝕜))
      ((extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).target ∩
        (↑(extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).symm : 𝕜 × 𝕜 → 𝕜 × 𝕜) ⁻¹'
          (fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2) ⁻¹' (extChartAt 𝓘(𝕜, 𝕜) y).source)
Tactic: rw [contMDiff_iff]