awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group 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 : LieGroup I n G
f : M → G
x₀ : M
hf : ContMDiffAt I' I n f x₀
⊢ 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)⁻¹) x₀

Tactic:
(contMDiff_inv I n).contMDiffAt.comp x₀ hf

Premises used: contMDiff_inv, ContMDiff.contMDiffAt, ContMDiffAt.comp
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group 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 : LieGroup I n G
f : M → G
s : Set M
hf : ContMDiffOn I' I n f s
⊢ 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 ↦ (hf x hx).inv

Premises used: ContMDiffWithinAt.inv, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group 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 : LieGroup I n G
f : M → G
hf : ContMDiff I' I n f
⊢ 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 ↦ (hf x).inv

Premises used: ContMDiffAt.inv, ContMDiff
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group 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 : LieGroup 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₀
simp_rw : 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 * (g x)⁻¹) s x₀
⊢ 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 / g x) s x₀

Tactic:
simp_rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group 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 : LieGroup 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.{u_1, u_5, u_6, u_7, u_3, u_2, u_4} I' I (M' := G) n (fun (x : M) ↦ f x * (g x)⁻¹) s x₀

Tactic:
hf.mul hg.inv

Premises used: ContMDiffWithinAt.inv, ContMDiffWithinAt.mul
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group 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 : LieGroup 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.{u_1, u_5, u_6, u_7, u_3, u_2, u_4} I' I (M' := G) n (fun (x : M) ↦ f x * (g x)⁻¹) s x₀

Tactic:
exact hf.mul hg.inv

Premises used: ContMDiffWithinAt.inv, ContMDiffWithinAt.mul
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group 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 : LieGroup I n G
f g : M → G
x₀ : M
hf : ContMDiffAt I' I n f x₀
hg : ContMDiffAt I' I n g x₀
simp_rw : 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 * (g x)⁻¹) x₀
⊢ 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 / g x) x₀

Tactic:
simp_rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group 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 : LieGroup I n G
f g : M → G
x₀ : M
hf : ContMDiffAt I' I n f x₀
hg : ContMDiffAt I' I n g x₀
⊢ 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 * (g x)⁻¹) x₀

Tactic:
hf.mul hg.inv

Premises used: ContMDiffAt.inv, ContMDiffAt.mul
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group 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 : LieGroup I n G
f g : M → G
x₀ : M
hf : ContMDiffAt I' I n f x₀
hg : ContMDiffAt I' I n g x₀
⊢ 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 * (g x)⁻¹) x₀

Tactic:
exact hf.mul hg.inv

Premises used: ContMDiffAt.inv, ContMDiffAt.mul
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group 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 : LieGroup I n G
f g : M → G
s : Set M
hf : ContMDiffOn I' I n f s
hg : ContMDiffOn I' I n g s
simp_rw : 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 * (g x)⁻¹) s
⊢ 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 / g x) s

Tactic:
simp_rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group 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 : LieGroup 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.{u_1, u_5, u_6, u_7, u_3, u_2, u_4} I' I (M' := G) n (fun (x : M) ↦ f x * (g x)⁻¹) s

Tactic:
hf.mul hg.inv

Premises used: ContMDiffOn.mul, ContMDiffOn.inv
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group 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 : LieGroup 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.{u_1, u_5, u_6, u_7, u_3, u_2, u_4} I' I (M' := G) n (fun (x : M) ↦ f x * (g x)⁻¹) s

Tactic:
exact hf.mul hg.inv

Premises used: ContMDiffOn.mul, ContMDiffOn.inv
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group 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 : LieGroup I n G
f g : M → G
hf : ContMDiff I' I n f
hg : ContMDiff I' I n g
simp_rw : 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 * (g x)⁻¹
⊢ 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 / g x

Tactic:
simp_rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group 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 : LieGroup I n G
f g : M → G
hf : ContMDiff I' I n f
hg : ContMDiff I' I n g
⊢ 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 * (g x)⁻¹

Tactic:
hf.mul hg.inv

Premises used: ContMDiff.inv, ContMDiff.mul
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group 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 : LieGroup I n G
f g : M → G
hf : ContMDiff I' I n f
hg : ContMDiff I' I n g
⊢ 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 * (g x)⁻¹

Tactic:
exact hf.mul hg.inv

Premises used: ContMDiff.inv, ContMDiff.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 : Group G
inst_7 : LieGroup I n 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'
G' : Type u_7
inst_11 : TopologicalSpace G'
inst_12 : ChartedSpace H' G'
inst_13 : Group G'
inst_14 : LieGroup I' n G'
⊢ LieGroup (I.prod I') n (G × G')

Tactic:
{ ContMDiffMul.prod _ _ _ _ with contMDiff_inv := contMDiff_fst.inv.prodMk contMDiff_snd.inv }

Premises used: ContMDiffMul.prod, ContMDiff.inv, LieGroup.mk, contMDiff_snd, contMDiff_fst, ContMDiff.prodMk
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜
hx : x ≠ 0
rw : ContDiffAt 𝕜 n Inv.inv x
⊢ ContMDiffAt 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜) n Inv.inv x

Tactic:
rw [contMDiffAt_iff_contDiffAt]

Premises used: contMDiffAt_iff_contDiffAt
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜
hx : x ≠ 0
⊢ ContDiffAt 𝕜 n Inv.inv x

Tactic:
contDiffAt_inv 𝕜 hx

Premises used: contDiffAt_inv
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜
hx : x ≠ 0
⊢ ContDiffAt 𝕜 n Inv.inv x

Tactic:
exact contDiffAt_inv 𝕜 hx

Premises used: contDiffAt_inv
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Inv G
inst_7 : Zero G
m n : ℕ∞ω
hmn : m ≤ n
h : ContMDiffInv₀ I n G
⊢ ContMDiffInv₀ I m G

Tactic:
⟨fun x hx ↦ (h.contMDiffAt_inv₀ hx).of_le hmn⟩

Premises used: ContMDiffInv₀.mk, ContMDiffInv₀.contMDiffAt_inv₀, ContMDiffAt.of_le
-- Module: Mathlib.Geometry.Manifold.Algebra.LieGroup
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 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Inv G
inst_7 : Zero G
m n : ℕ∞ω
hmn : m ≤ n
h : ContMDiffInv₀ I n G
⊢ ContMDiffInv₀ I m G

Tactic:
exact ⟨fun x hx ↦ (h.contMDiffAt_inv₀ hx).of_le hmn⟩
-- 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
a : ℕ∞ω
inst_13 : ContMDiffInv₀ I ∞ G
h : ENat.LEInfty a
⊢ ContMDiffInv₀ I a G

Tactic:
ContMDiffInv₀.of_le h.out

Premises used: ENat.LEInfty.out, 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
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
a : ℕ∞ω
inst_13 : ContMDiffInv₀ I ω G
⊢ ContMDiffInv₀ I a G

Tactic:
ContMDiffInv₀.of_le le_top

Premises used: le_top, 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
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
⊢ T1Space G

Tactic:
have : T1Space G := I.t1Space G
-- 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 : T1Space G
contMDiffAt_inv₀ : ∀ ⦃x : G⦄, x ≠ 0 → ContMDiffAt I I (M' := G) 0 (fun (y : G) ↦ y⁻¹) x
⊢ ContMDiffInv₀ I 0 G

Tactic:
constructor
-- 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 : T1Space G
rw : ContinuousOn (Y := G) (fun (x : G) ↦ x⁻¹) {0}ᶜ
⊢ ContMDiffOn I I (M' := G) 0 (fun (x : G) ↦ x⁻¹) {0}ᶜ

Tactic:
rw [contMDiffOn_zero_iff]

Premises used: contMDiffOn_zero_iff
-- 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 : T1Space G
⊢ ContinuousOn (Y := G) (fun (x : G) ↦ x⁻¹) {0}ᶜ

Tactic:
continuousOn_inv₀

Premises used: continuousOn_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 : ContinuousInv₀ G
this : T1Space G
⊢ ContinuousOn (Y := G) (fun (x : G) ↦ x⁻¹) {0}ᶜ

Tactic:
exact continuousOn_inv₀

Premises used: continuousOn_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 : ContinuousInv₀ G
this : T1Space G
⊢ ContMDiffOn I I (M' := G) 0 (fun (x : G) ↦ x⁻¹) {0}ᶜ

Tactic:
have A : CMDiff[{0}ᶜ] 0 (fun (x : G) ↦ x⁻¹) := by
    rw [contMDiffOn_zero_iff]
    exact continuousOn_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 : ContinuousInv₀ G
this : T1Space G
A : ContMDiffOn I I (M' := G) 0 (fun (x : G) ↦ x⁻¹) {0}ᶜ
x : G
hx : x ≠ 0
⊢ ContMDiffWithinAt I I (M' := G) 0 (fun (x : G) ↦ x⁻¹) {0}ᶜ x

Tactic:
have : ContMDiffWithinAt I I 0 (fun (x : G) ↦ x⁻¹) {0}ᶜ x := A x hx
-- 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
contMDiffAt_inv₀ : {0}ᶜ ∈ nhds x
⊢ ContMDiffAt I I (M' := G) 0 (fun (y : G) ↦ y⁻¹) x

Tactic:
apply ContMDiffWithinAt.contMDiffAt this

Premises used: ContMDiffWithinAt.contMDiffAt
-- 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:
IsOpen.mem_nhds isOpen_compl_singleton hx

Premises used: isOpen_compl_singleton, IsOpen.mem_nhds