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 : ℕ∞ω
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:
exact div_eq_mul_inv _ _

Premises used: div_eq_mul_inv
-- 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
a : C^n⟮I, N; I', G⟯
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)⁻¹) ⋯ * a :
            (a : N) → G)
          x :
        G)
      ((1 : (a : N) → G) x : G)
⊢ Subtype.mk (p := fun (f : N → G) ↦ ContMDiff I I' n f) (fun (x : N) ↦ ((a : (a : N) → G) x)⁻¹) ⋯ * a = 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 : Group G
inst_15 : TopologicalSpace G
inst_16 : ChartedSpace H' G
inst_17 : LieGroup I' n G
a : C^n⟮I, N; I', G⟯
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)⁻¹) ⋯ * a :
          (a : N) → G)
        x :
      G)
    ((1 : (a : N) → G) x : G)

Tactic:
inv_mul_cancel _

Premises used: inv_mul_cancel
-- 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
a : C^n⟮I, N; I', G⟯
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)⁻¹) ⋯ * a :
          (a : N) → G)
        x :
      G)
    ((1 : (a : N) → G) x : G)

Tactic:
exact inv_mul_cancel _

Premises used: inv_mul_cancel
-- 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 : Group G
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H' G
inst_12 : LieGroup I' n G
f : C^n⟮I, N; I', G⟯
⊢ Eq (α := (a : N) → G) (⇑f⁻¹ : (a : N) → G) (⇑f : (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
n : ℕ∞ω
G : Type u_10
inst_9 : Group G
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H' G
inst_12 : LieGroup I' n G
f g : C^n⟮I, N; I', G⟯
⊢ (⇑(f / g) : (a : N) → G) = HDiv.hDiv (α := (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 : ℕ∞ω
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⟯
h : ∀ (x : N), Eq.{u_10 + 1} (α := R) ((0 * a : (a : N) → R) x : R) ((0 : (a : N) → R) x : R)
⊢ 0 * a = 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 : ℕ∞ω
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⟯
x : N
⊢ Eq.{u_10 + 1} (α := R) ((0 * a : (a : N) → R) x : R) ((0 : (a : N) → R) x : R)

Tactic:
zero_mul _

Premises used: MulZeroClass.zero_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 : ℕ∞ω
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⟯
x : N
⊢ Eq.{u_10 + 1} (α := R) ((0 * a : (a : N) → R) x : R) ((0 : (a : N) → R) x : R)

Tactic:
exact zero_mul _

Premises used: MulZeroClass.zero_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 : ℕ∞ω
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⟯
h : ∀ (x : N), Eq.{u_10 + 1} (α := R) ((a * 0 : (a : N) → R) x : R) ((0 : (a : N) → R) x : R)
⊢ 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 : ℕ∞ω
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⟯
x : N
⊢ Eq.{u_10 + 1} (α := R) ((a * 0 : (a : N) → R) x : R) ((0 : (a : N) → R) x : R)

Tactic:
mul_zero _

Premises used: MulZeroClass.mul_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 : ℕ∞ω
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⟯
x : N
⊢ Eq.{u_10 + 1} (α := R) ((a * 0 : (a : N) → R) x : R) ((0 : (a : N) → R) x : R)

Tactic:
exact mul_zero _

Premises used: MulZeroClass.mul_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 : ℕ∞ω
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⟯
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)
⊢ a * (b + c) = a * b + 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 : ℕ∞ω
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⟯
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:
left_distrib _ _ _

Premises used: left_distrib
-- 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 : ℕ∞ω
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⟯
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:
exact left_distrib _ _ _

Premises used: left_distrib
-- 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 : ℕ∞ω
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⟯
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)
⊢ (a + b) * c = a * c + b * 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 : ℕ∞ω
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⟯
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:
right_distrib _ _ _

Premises used: right_distrib
-- 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 : ℕ∞ω
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⟯
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:
exact right_distrib _ _ _

Premises used: right_distrib
-- 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
n : ℕ∞ω
V : Type u_10
inst_6 : NormedAddCommGroup V
inst_7 : NormedSpace 𝕜 V
r : 𝕜
f : C^n⟮I, N; 𝓘(𝕜, V), V⟯
⊢ (⇑(r • f) : (a : N) → V) = HSMul.hSMul (β := (a : N) → V) r (⇑f : (a : N) → V)

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
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
r : 𝕜
g : C^n⟮I'', N'; 𝓘(𝕜, V), V⟯
h : C^n⟮I, N; I'', N'⟯
⊢ (r • g).comp h = r • 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 : ℕ∞ω
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) 1) ⋯ :
            (a : N) → A)
          x :
        A)
      ((1 : (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) 1) ⋯) 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 : ℕ∞ω
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) 1) ⋯ :
          (a : N) → A)
        x :
      A)
    ((1 : (a : N) → A) x : A)

Tactic:
(algebraMap 𝕜 A).map_one

Premises used: Algebra.algebraMap, RingHom.map_one
-- 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) 1) ⋯ :
          (a : N) → A)
        x :
      A)
    ((1 : (a : N) → A) x : A)

Tactic:
exact (algebraMap 𝕜 A).map_one

Premises used: Algebra.algebraMap, RingHom.map_one
-- 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)
      ((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)
⊢ 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₂) ⋯)

Tactic:
ext