awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst_4 : TopologicalSpace H'
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst_7 : TopologicalSpace H''
E'' : Type u_7
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H G
M : Type u_9
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace H'' N
n : ℕ∞ω
h : ContMDiff (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, E)) (M := 𝕜 × E) (E' := 𝕜 × E) 𝓘(𝕜, 𝕜 × E) n id
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, E)) 𝓘(𝕜, E) (M' := E) n fun (p : 𝕜 × E) ↦ p.1 • p.2

Tactic:
exact contDiff_smul.contMDiff.comp h

Premises used: ContMDiff.comp, ContDiff.contMDiff, contDiff_smul
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst_4 : TopologicalSpace H'
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst_7 : TopologicalSpace H''
E'' : Type u_7
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H G
M : Type u_9
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace H'' N
inst_16 : CompleteSpace E
n : ℕ∞ω
rw :
  ContMDiff (E := (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) (M := (E →L[𝕜] E) × E) (E' :=
    (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) n id
⊢ ContMDiff (E := (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) (M := (E →L[𝕜] E) × E) (E' :=
    (E →L[𝕜] E) × E) 𝓘(𝕜, (E →L[𝕜] E) × E) n id

Tactic:
rw [contMDiff_prod_module_iff, ← contMDiff_prod_iff]

Premises used: contMDiff_prod_iff, contMDiff_prod_module_iff
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst_4 : TopologicalSpace H'
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst_7 : TopologicalSpace H''
E'' : Type u_7
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H G
M : Type u_9
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace H'' N
inst_16 : CompleteSpace E
n : ℕ∞ω
⊢ ContMDiff (E := (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) (M := (E →L[𝕜] E) × E) (E' :=
    (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) n id

Tactic:
contMDiff_id

Premises used: contMDiff_id
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst_4 : TopologicalSpace H'
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst_7 : TopologicalSpace H''
E'' : Type u_7
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H G
M : Type u_9
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace H'' N
inst_16 : CompleteSpace E
n : ℕ∞ω
⊢ ContMDiff (E := (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) (M := (E →L[𝕜] E) × E) (E' :=
    (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) n id

Tactic:
exact contMDiff_id

Premises used: contMDiff_id
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst_4 : TopologicalSpace H'
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst_7 : TopologicalSpace H''
E'' : Type u_7
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H G
M : Type u_9
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace H'' N
inst_16 : CompleteSpace E
n : ℕ∞ω
⊢ ContMDiff (E := (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) (M := (E →L[𝕜] E) × E) (E' :=
    (E →L[𝕜] E) × E) 𝓘(𝕜, (E →L[𝕜] E) × E) n id

Tactic:
have h : ContMDiff (𝓘(𝕜, E →L[𝕜] E).prod 𝓘(𝕜, E)) 𝓘(𝕜, (E →L[𝕜] E) × E) n
        (@id ((E →L[𝕜] E) × E)) := by
      rw [contMDiff_prod_module_iff, ← contMDiff_prod_iff]; exact contMDiff_id
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst_4 : TopologicalSpace H'
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst_7 : TopologicalSpace H''
E'' : Type u_7
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H G
M : Type u_9
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace H'' N
inst_16 : CompleteSpace E
n : ℕ∞ω
h :
  ContMDiff (E := (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) (M := (E →L[𝕜] E) × E) (E' :=
    (E →L[𝕜] E) × E) 𝓘(𝕜, (E →L[𝕜] E) × E) n id
⊢ ContMDiff (E := (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) 𝓘(𝕜, E) (M' := E) n
    fun (p : (E →L[𝕜] E) × E) ↦ p.1 • p.2

Tactic:
isBoundedBilinearMap_apply.contDiff.contMDiff.comp h

Premises used: ContMDiff.comp, IsBoundedBilinearMap.contDiff, ContDiff.contMDiff
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst_4 : TopologicalSpace H'
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst_7 : TopologicalSpace H''
E'' : Type u_7
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H G
M : Type u_9
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace H'' N
inst_16 : CompleteSpace E
n : ℕ∞ω
h :
  ContMDiff (E := (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) (M := (E →L[𝕜] E) × E) (E' :=
    (E →L[𝕜] E) × E) 𝓘(𝕜, (E →L[𝕜] E) × E) n id
⊢ ContMDiff (E := (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) 𝓘(𝕜, E) (M' := E) n
    fun (p : (E →L[𝕜] E) × E) ↦ p.1 • p.2

Tactic:
exact isBoundedBilinearMap_apply.contDiff.contMDiff.comp h

Premises used: ContMDiff.comp, IsBoundedBilinearMap.contDiff, ContDiff.contMDiff
-- 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
n : ℕ∞ω
G : Type u_10
inst_9 : Mul G
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H' G
inst_12 : ContMDiffMul I' n G
f g : C^n⟮I, N; I', G⟯
⊢ (⇑(f * g) : (a : N) → G) = HMul.hMul (α := (a : N) → G) (⇑f : (a : N) → G) (⇑g : (a : N) → G)

Tactic:
rfl

Premises used: 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 : ℕ∞ω
G : Type u_10
inst_14 : Mul G
inst_15 : TopologicalSpace G
inst_16 : ChartedSpace H' G
inst_17 : ContMDiffMul I' n G
f g : C^n⟮I'', N'; I', G⟯
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
n : ℕ∞ω
G : Type u_10
inst_9 : One G
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H' G
⊢ Eq (α := (a : N) → G) (⇑1 : (a : N) → G) 1

Tactic:
rfl

Premises used: 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
n_1 : ℕ∞ω
G : Type u_10
inst_9 : Monoid G
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H' G
inst_12 : ContMDiffMul I' n_1 G
f : C^n_1⟮I, N; I', G⟯
n : ℕ
⊢ (⇑(f ^ n) : (a : N) → G) = HPow.hPow (α := (a : N) → G) (⇑f : (a : N) → G) n

Tactic:
rfl

Premises used: 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 : ℕ∞ω
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'')
h :
  ∀ (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'') (⇑1 : (a : N) → G')) ⋯ :
            (a : N) → G'')
          x :
        G'')
      ((1 : (a : N) → G'') x : G'')
⊢ Eq (α := C^n⟮I, N; I'', 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'') (⇑1 : (a : N) → G')) ⋯)
    1

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 : ℕ∞ω
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'')
x : N
h : Eq.{u_11 + 1} (α := G'') ((φ : (a : G') → G'') 1 : G'') (1 : G'')
⊢ 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'') (⇑1 : (a : N) → G')) ⋯ :
          (a : N) → G'')
        x :
      G'')
    ((1 : (a : N) → G'') x : G'')

Tactic:
change φ 1 = 1

Premises used: OfNat.ofNat, DFunLike.coe
-- 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 : ℕ∞ω
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'')
x : N
⊢ Eq.{u_11 + 1} (α := G'') ((φ : (a : G') → G'') 1 : G'') (1 : G'')

Tactic:
simp
-- 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 : ℕ∞ω
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'⟯
h :
  ∀ (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'')
⊢ 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')) ⋯ =
    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')) ⋯

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 : ℕ∞ω
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
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'')
⊢ 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'')

Tactic:
change φ (f x * g x) = φ (f x) * φ (g x)

Premises used: HMul.hMul, DFunLike.coe
-- 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 : ℕ∞ω
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
⊢ (φ : (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:
simp
-- 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 : ℕ∞ω
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⟯
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)⁻¹) ⋯ :
            (a : N) → G)
          x :
        G)
⊢ f / g = f * Subtype.mk (p := fun (f : N → G) ↦ ContMDiff I I' n f) (fun (x : N) ↦ ((g : (a : N) → G) x)⁻¹) ⋯

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 : ℕ∞ω
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⟯
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)⁻¹) ⋯ :
          (a : N) → G)
        x :
      G)

Tactic:
div_eq_mul_inv _ _

Premises used: div_eq_mul_inv