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 : ℕ∞ω
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:
exact one_smul 𝕜 (f x)

Premises used: one_smul, 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 : ℕ∞ω
V : Type u_10
inst_14 : NormedAddCommGroup V
inst_15 : NormedSpace 𝕜 V
r : C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
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)
⊢ HSMul.hSMul (β := C^n⟮I, N; 𝓘(𝕜, V), V⟯) r 0 = 0

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
r : C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
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:
smul_zero _

Premises used: smul_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 : ℕ∞ω
V : Type u_10
inst_14 : NormedAddCommGroup V
inst_15 : NormedSpace 𝕜 V
r : C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
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:
exact smul_zero _

Premises used: smul_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 : ℕ∞ω
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⟯
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)
⊢ c • (f + g) = c • f + c • 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 : ℕ∞ω
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⟯
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:
smul_add (c x) (f x) (g x)

Premises used: DFunLike.coe, smul_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 : ℕ∞ω
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⟯
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:
exact smul_add (c x) (f x) (g x)

Premises used: DFunLike.coe, smul_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 : ℕ∞ω
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₁ • f + c₂ • f : (a : N) → V) x : V)
⊢ (c₁ + c₂) • f = c₁ • f + 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₁ • f + c₂ • f : (a : N) → V) x : V)

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

Premises used: add_smul, 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 : ℕ∞ω
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₁ • f + c₂ • f : (a : N) → V) x : V)

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

Premises used: add_smul, 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 : ℕ∞ω
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; 𝓘(𝕜, 𝕜), 𝕜⟯) 0 f : (a : N) → V) x : V)
      ((0 : (a : N) → V) x : V)
⊢ HSMul.hSMul (α := C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯) 0 f = 0

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; 𝓘(𝕜, 𝕜), 𝕜⟯) 0 f : (a : N) → V) x : V) ((0 : (a : N) → V) x : V)

Tactic:
zero_smul _ _

Premises used: zero_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⟯
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:
exact zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.Geometry.Manifold.Algebra.Structures
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
n : ℕ∞ω
I : ModelWithCorners 𝕜 E H
R : Type u_4
inst_4 : Semiring R
inst_5 : TopologicalSpace R
inst_6 : ChartedSpace H R
h : ContMDiffRing I n R
⊢ ContMDiffMul I n R

Tactic:
{ h with }

Premises used: ContMDiffMul.mk, ContMDiffRing.contMDiff_mul
-- Module: Mathlib.Geometry.Manifold.Algebra.Structures
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
n : ℕ∞ω
I : ModelWithCorners 𝕜 E H
R : Type u_4
inst_4 : Ring R
inst_5 : TopologicalSpace R
inst_6 : ChartedSpace H R
inst_7 : ContMDiffRing I n R
⊢ ContMDiff I I (M' := R) n fun (a : R) ↦ -a

Tactic:
simpa only [neg_one_mul] using contMDiff_mul_left (G := R) (a := -1)

Premises used: contMDiff_mul_left, neg_one_mul
-- Module: Mathlib.Geometry.Manifold.Algebra.Structures
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
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)
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) 𝓘(𝕜, 𝕜) (M' := 𝕜) n fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2

Tactic:
rw [contMDiff_iff]

Premises used: contMDiff_iff
-- Module: Mathlib.Geometry.Manifold.Algebra.Structures
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
⊢ (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:
⟨continuous_mul, fun x y => ?_⟩

Premises used: continuous_mul, And.intro
-- Module: Mathlib.Geometry.Manifold.Algebra.Structures
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
refine :
  ∀ (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)
⊢ (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:
refine ⟨continuous_mul, fun x y => ?_⟩
-- Module: Mathlib.Geometry.Manifold.Algebra.Structures
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜 × 𝕜
y : 𝕜
simp : ContDiffOn 𝕜 (F := 𝕜) n (fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2) Set.univ
⊢ 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:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.Algebra.Structures
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜 × 𝕜
y : 𝕜
rw : ContDiff 𝕜 (F := 𝕜) n fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2
⊢ ContDiffOn 𝕜 (F := 𝕜) n (fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2) Set.univ

Tactic:
rw [contDiffOn_univ]

Premises used: contDiffOn_univ
-- Module: Mathlib.Geometry.Manifold.Algebra.Structures
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜 × 𝕜
y : 𝕜
⊢ ContDiff 𝕜 (F := 𝕜) n fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2

Tactic:
contDiff_mul

Premises used: contDiff_mul
-- Module: Mathlib.Geometry.Manifold.Algebra.Structures
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜 × 𝕜
y : 𝕜
⊢ ContDiff 𝕜 (F := 𝕜) n fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2

Tactic:
exact contDiff_mul

Premises used: contDiff_mul
-- Module: Mathlib.Geometry.Manifold.Algebra.Structures
Goal:
𝕜 : Type u_1
R : Type u_2
E : Type u_3
H : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace H
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : ChartedSpace H R
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
inst_6 : Semiring R
inst_7 : ContMDiffRing I n R
⊢ IsTopologicalSemiring R

Tactic:
{ continuousMul_of_contMDiffMul I n, continuousAdd_of_contMDiffAdd I n with }

Premises used: continuousMul_of_contMDiffMul, continuousAdd_of_contMDiffAdd, IsTopologicalSemiring.mk
-- Module: Mathlib.Geometry.Manifold.Bordism
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
M : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I k M
inst_10 : CompactSpace M
inst_11 : BoundarylessManifold I M
s : SingularManifold.{u_7, u_1, u_4, u_5} X k I
⊢ IsManifold.{0, u_4, u_5, u_7} I k s.M

Tactic:
s.isManifold

Premises used: SingularManifold.isManifold
-- Module: Mathlib.Geometry.Manifold.Bordism
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
M : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I k M
inst_10 : CompactSpace M
inst_11 : BoundarylessManifold I M
s : SingularManifold.{u_7, u_1, u_4, u_5} X k I
⊢ CompactSpace.{u_7} s.M

Tactic:
s.compactSpace

Premises used: SingularManifold.compactSpace
-- Module: Mathlib.Geometry.Manifold.Bordism
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
M : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I k M
inst_10 : CompactSpace M
inst_11 : BoundarylessManifold I M
s : SingularManifold.{u_7, u_1, u_4, u_5} X k I
⊢ BoundarylessManifold.{0, u_4, u_5, u_7} I s.M

Tactic:
s.boundaryless

Premises used: SingularManifold.boundaryless
-- Module: Mathlib.Geometry.Manifold.Bordism
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : TopologicalSpace H
I : ModelWithCorners ℝ E H
s : SingularManifold.{u_7, u_1, u_4, u_5} X k I
φ : X → Y
hφ : Continuous φ
⊢ (s.map hφ).f = φ ∘ s.f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.Bordism
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : TopologicalSpace H
I : ModelWithCorners ℝ E H
s : SingularManifold.{u_7, u_1, u_4, u_5} X k I
φ : X → Y
hφ : Continuous φ
⊢ (s.map hφ).M = s.M

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.Bordism
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
s : SingularManifold.{u_7, u_1, u_4, u_5} X k I
φ : X → Y
ψ : Y → Z
hφ : Continuous φ
hψ : Continuous ψ
⊢ ((s.map hφ).map hψ).f = (ψ ∘ φ) ∘ s.f

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Geometry.Manifold.Bordism
Goal:
X : Type u_1
inst : TopologicalSpace X
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
M : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : IsManifold I k M
inst_8 : CompactSpace M
inst_9 : BoundarylessManifold I M
s : SingularManifold.{u_9, u_1, u_4, u_5} X k I
φ : M → s.M
hφ : Continuous φ
⊢ (s.comap hφ).M = M

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.Bordism
Goal:
X : Type u_1
inst : TopologicalSpace X
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
M : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : IsManifold I k M
inst_8 : CompactSpace M
inst_9 : BoundarylessManifold I M
s : SingularManifold.{u_9, u_1, u_4, u_5} X k I
φ : M → s.M
hφ : Continuous φ
⊢ (s.comap hφ).f = s.f ∘ φ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.Bordism
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
M_1 : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : TopologicalSpace H
I_1 : ModelWithCorners ℝ E H
inst_7 : TopologicalSpace M_1
inst_8 : ChartedSpace H M_1
inst_9 : IsManifold I_1 k M_1
inst_10 : CompactSpace M_1
inst_11 : BoundarylessManifold I_1 M_1
E' : Type u_7
H' : Type u_8
inst_12 : NormedAddCommGroup E'
inst_13 : NormedSpace ℝ E'
inst_14 : TopologicalSpace H'
M : Type u
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
I : ModelWithCorners ℝ E H
inst_17 : IsManifold I k M
inst_18 : IsEmpty M
rw : ∀ (x : M), ContinuousAt.{u, u_1} (Y := X) (fun (x : M) ↦ ⋯.elim) x
⊢ Continuous.{u, u_1} (Y := X) fun (x : M) ↦ ⋯.elim

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt