awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Inv G
inst_7 : Zero G
E' : Type u_5
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_6
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
f : M → G
inst_13 : ContinuousInv₀ G
this_1 : T1Space G
A : ContMDiffOn I I (M' := G) 0 (fun (x : G) ↦ x⁻¹) {0}ᶜ
x : G
hx : x ≠ 0
this : ContMDiffWithinAt I I (M' := G) 0 (fun (x : G) ↦ x⁻¹) {0}ᶜ x
⊢ {0}ᶜ ∈ nhds x

Tactic:
exact IsOpen.mem_nhds isOpen_compl_singleton hx

Premises used: isOpen_compl_singleton, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Inv G
inst_7 : Zero G
E' : Type u_5
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_6
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
f : M → G
inst_13 : ContMDiffInv₀ I 2 G
⊢ ContMDiffInv₀ I 1 G

Tactic:
ContMDiffInv₀.of_le one_le_two

Premises used: one_le_two, ContMDiffInv₀.of_le
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Inv G
inst_7 : Zero G
inst_8 : ContMDiffInv₀ I n G
x : G
hx : x ≠ 0
⊢ ContMDiffAt I I (M' := G) n (fun (y : G) ↦ y⁻¹) x

Tactic:
ContMDiffInv₀.contMDiffAt_inv₀ hx

Premises used: ContMDiffInv₀.contMDiffAt_inv₀
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Inv G
inst_7 : Zero G
inst_8 : ContMDiffInv₀ I n G
⊢ ContinuousInv₀ G

Tactic:
{ continuousAt_inv₀ := fun _ hx ↦ (contMDiffAt_inv₀ (I := I) (n := n) hx).continuousAt }

Premises used: ContinuousInv₀.mk, ContMDiffAt.continuousAt, contMDiffAt_inv₀
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Inv G
inst_7 : Zero G
inst_8 : ContMDiffInv₀ I n G
⊢ ContMDiffOn I (M := G) I n Inv.inv {0}ᶜ

Tactic:
fun _x hx ↦ (contMDiffAt_inv₀ hx).contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, contMDiffAt_inv₀, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Inv G
inst_7 : Zero G
E' : Type u_5
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_6
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
f : M → G
inst_13 : ContMDiffInv₀ I n G
s : Set M
a : M
hf : ContMDiffWithinAt I' I n f s a
ha : f a ≠ 0
⊢ ContMDiffWithinAt.{u_1, u_5, u_6, u_7, u_3, u_2, u_4} I' I (M' := G) n (fun (x : M) ↦ (f x)⁻¹) s a

Tactic:
(contMDiffAt_inv₀ ha).comp_contMDiffWithinAt a hf

Premises used: ContMDiffAt.comp_contMDiffWithinAt, contMDiffAt_inv₀
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Inv G
inst_7 : Zero G
E' : Type u_5
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_6
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
f : M → G
inst_13 : ContMDiffInv₀ I n G
a : M
hf : ContMDiffAt I' I n f a
ha : f a ≠ 0
⊢ ContMDiffAt.{u_1, u_5, u_6, u_7, u_3, u_2, u_4} I' I (M' := G) n (fun (x : M) ↦ (f x)⁻¹) a

Tactic:
(contMDiffAt_inv₀ ha).comp a hf

Premises used: contMDiffAt_inv₀, ContMDiffAt.comp
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Inv G
inst_7 : Zero G
E' : Type u_5
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_6
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
f : M → G
inst_13 : ContMDiffInv₀ I n G
hf : ContMDiff I' I n f
h0 : ∀ (x : M), f x ≠ 0
⊢ ContMDiff.{u_1, u_5, u_6, u_7, u_3, u_2, u_4} I' I (M' := G) n fun (x : M) ↦ (f x)⁻¹

Tactic:
fun x ↦ ContMDiffAt.inv₀ (hf x) (h0 x)

Premises used: ContMDiff, ContMDiffAt.inv₀
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Inv G
inst_7 : Zero G
E' : Type u_5
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_6
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
f : M → G
inst_13 : ContMDiffInv₀ I n G
s : Set M
hf : ContMDiffOn I' I n f s
h0 : ∀ x ∈ s, f x ≠ 0
⊢ ContMDiffOn.{u_1, u_5, u_6, u_7, u_3, u_2, u_4} I' I (M' := G) n (fun (x : M) ↦ (f x)⁻¹) s

Tactic:
fun x hx ↦ ContMDiffWithinAt.inv₀ (hf x hx) (h0 x hx)

Premises used: ContMDiffWithinAt.inv₀, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : GroupWithZero G
inst_7 : ContMDiffInv₀ I n G
inst_8 : ContMDiffMul I n G
E' : Type u_5
inst_9 : NormedAddCommGroup E'
inst_10 : NormedSpace 𝕜 E'
H' : Type u_6
inst_11 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
f g : M → G
s : Set M
a : M
hf : ContMDiffWithinAt I' I n f s a
hg : ContMDiffWithinAt I' I n g s a
h₀ : g a ≠ 0
⊢ ContMDiffWithinAt I' I n (f / g) s a

Tactic:
simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

Premises used: div_eq_mul_inv, ContMDiffWithinAt.inv₀, ContMDiffWithinAt.mul
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : GroupWithZero G
inst_7 : ContMDiffInv₀ I n G
inst_8 : ContMDiffMul I n G
E' : Type u_5
inst_9 : NormedAddCommGroup E'
inst_10 : NormedSpace 𝕜 E'
H' : Type u_6
inst_11 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
f g : M → G
s : Set M
hf : ContMDiffOn I' I n f s
hg : ContMDiffOn I' I n g s
h₀ : ∀ x ∈ s, g x ≠ 0
⊢ ContMDiffOn I' I n (f / g) s

Tactic:
simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

Premises used: ContMDiffOn.mul, div_eq_mul_inv, ContMDiffOn.inv₀
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : GroupWithZero G
inst_7 : ContMDiffInv₀ I n G
inst_8 : ContMDiffMul I n G
E' : Type u_5
inst_9 : NormedAddCommGroup E'
inst_10 : NormedSpace 𝕜 E'
H' : Type u_6
inst_11 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
f g : M → G
a : M
hf : ContMDiffAt I' I n f a
hg : ContMDiffAt I' I n g a
h₀ : g a ≠ 0
⊢ ContMDiffAt I' I n (f / g) a

Tactic:
simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

Premises used: div_eq_mul_inv, ContMDiffAt.inv₀, ContMDiffAt.mul
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : GroupWithZero G
inst_7 : ContMDiffInv₀ I n G
inst_8 : ContMDiffMul I n G
E' : Type u_5
inst_9 : NormedAddCommGroup E'
inst_10 : NormedSpace 𝕜 E'
H' : Type u_6
inst_11 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
f g : M → G
hf : ContMDiff I' I n f
hg : ContMDiff I' I n g
h₀ : ∀ (x : M), g x ≠ 0
⊢ ContMDiff I' I n (f / g)

Tactic:
simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

Premises used: ContMDiff.mul, div_eq_mul_inv, ContMDiff.inv₀
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
m n : ℕ∞ω
hmn : m ≤ n
h : ContMDiffMul I n G
⊢ IsManifold I m G

Tactic:
have : IsManifold I m G := IsManifold.of_le hmn
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
m n : ℕ∞ω
hmn : m ≤ n
h : ContMDiffMul I n G
this : IsManifold I m G
⊢ ContMDiffMul I m G

Tactic:
⟨h.contMDiff_mul.of_le hmn⟩

Premises used: ContMDiffMul.contMDiff_mul, ContMDiffMul.mk, ContMDiff.of_le
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
m n : ℕ∞ω
hmn : m ≤ n
h : ContMDiffMul I n G
this : IsManifold I m G
⊢ ContMDiffMul I m G

Tactic:
exact ⟨h.contMDiff_mul.of_le hmn⟩
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H' M
a : ℕ∞ω
inst_12 : ContMDiffMul I ∞ G
h : ENat.LEInfty a
⊢ ContMDiffMul I a G

Tactic:
ContMDiffMul.of_le h.out

Premises used: ContMDiffMul.of_le, ENat.LEInfty.out
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H' M
a : ℕ∞ω
inst_12 : ContMDiffMul I ω G
⊢ ContMDiffMul I a G

Tactic:
ContMDiffMul.of_le le_top

Premises used: ContMDiffMul.of_le, le_top
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H' M
inst_12 : ContinuousMul G
contMDiff_mul : ContMDiff (I.prod I) I (M' := G) 0 fun (p : G × G) ↦ p.1 * p.2
⊢ ContMDiffMul I 0 G

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H' M
inst_12 : ContinuousMul G
contMDiff_mul : Continuous (Y := G) fun (p : G × G) ↦ p.1 * p.2
⊢ ContMDiff (I.prod I) I (M' := G) 0 fun (p : G × G) ↦ p.1 * p.2

Tactic:
rw [contMDiff_zero_iff]

Premises used: contMDiff_zero_iff
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H' M
inst_12 : ContinuousMul G
⊢ Continuous (Y := G) fun (p : G × G) ↦ p.1 * p.2

Tactic:
continuous_mul

Premises used: continuous_mul
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H' M
inst_12 : ContinuousMul G
⊢ Continuous (Y := G) fun (p : G × G) ↦ p.1 * p.2

Tactic:
exact continuous_mul

Premises used: continuous_mul
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H' M
inst_12 : ContMDiffMul I 2 G
⊢ ContMDiffMul I 1 G

Tactic:
ContMDiffMul.of_le one_le_two

Premises used: ContMDiffMul.of_le, one_le_two
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
⊢ ContMDiff (I.prod I) I (M' := G) n fun (p : G × G) ↦ p.1 * p.2

Tactic:
ContMDiffMul.contMDiff_mul

Premises used: ContMDiffMul.contMDiff_mul
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
⊢ ContinuousMul G

Tactic:
⟨(contMDiff_mul I n).continuous⟩

Premises used: contMDiff_mul, ContMDiff.continuous, ContinuousMul.mk
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H' M
inst_12 : ContMDiffMul I n G
f g : M → G
s : Set M
x : M
hf : ContMDiffWithinAt I' I n f s x
hg : ContMDiffWithinAt I' I n g s x
⊢ ContMDiffWithinAt I' I n (f * g) s x

Tactic:
(contMDiff_mul I n).contMDiffAt.comp_contMDiffWithinAt x (hf.prodMk hg)

Premises used: contMDiff_mul, ContMDiffWithinAt.prodMk, ContMDiff.contMDiffAt, ContMDiffAt.comp_contMDiffWithinAt
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H' M
inst_12 : ContMDiffMul I n G
f g : M → G
x : M
hf : ContMDiffAt I' I n f x
hg : ContMDiffAt I' I n g x
⊢ ContMDiffAt I' I n (f * g) x

Tactic:
hf.mul hg

Premises used: ContMDiffAt, ContMDiffWithinAt.mul
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H' M
inst_12 : ContMDiffMul I n G
f g : M → G
s : Set M
hf : ContMDiffOn I' I n f s
hg : ContMDiffOn I' I n g s
⊢ ContMDiffOn I' I n (f * g) s

Tactic:
fun x hx ↦ (hf x hx).mul (hg x hx)

Premises used: ContMDiffWithinAt.mul, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H' M
inst_12 : ContMDiffMul I n G
f g : M → G
hf : ContMDiff I' I n f
hg : ContMDiff I' I n g
⊢ ContMDiff I' I n (f * g)

Tactic:
fun x ↦ (hf x).mul (hg x)

Premises used: ContMDiff, ContMDiffAt.mul
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
a : G
⊢ ContMDiff I I (M' := G) n fun (x : G) ↦ a * x

Tactic:
contMDiff_const.mul contMDiff_id

Premises used: ContMDiff.mul, contMDiff_const, contMDiff_id
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
a b : G
⊢ ContMDiffAt I I (M' := G) n (fun (x : G) ↦ a * x) b

Tactic:
contMDiff_mul_left.contMDiffAt

Premises used: contMDiff_mul_left, ContMDiff.contMDiffAt
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
a : G
⊢ ContMDiff I I (M' := G) n fun (x : G) ↦ x * a

Tactic:
contMDiff_id.mul contMDiff_const

Premises used: ContMDiff.mul, contMDiff_const, contMDiff_id
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
n : ℕ∞ω
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
a b : G
⊢ ContMDiffAt I I (M' := G) n (fun (x : G) ↦ x * a) b

Tactic:
contMDiff_mul_right.contMDiffAt

Premises used: contMDiff_mul_right, ContMDiff.contMDiffAt
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I 1 G
a : G
⊢ MDiff fun (x : G) ↦ a * x

Tactic:
contMDiff_mul_left.mdifferentiable one_ne_zero

Premises used: contMDiff_mul_left, ContMDiff.mdifferentiable, one_ne_zero
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I 1 G
a b : G
⊢ (MDiffAt fun (x : G) ↦ a * x) b

Tactic:
contMDiffAt_mul_left.mdifferentiableAt one_ne_zero

Premises used: ContMDiffAt.mdifferentiableAt, contMDiffAt_mul_left, one_ne_zero
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I 1 G
a : G
⊢ MDiff fun (x : G) ↦ x * a

Tactic:
contMDiff_mul_right.mdifferentiable one_ne_zero

Premises used: contMDiff_mul_right, ContMDiff.mdifferentiable, one_ne_zero