awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g h : G
r : 𝕜
X_1 Y_1 : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
h₁ :
  HAdd.hAdd (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) -
      HAdd.hAdd (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) =
    HSub.hSub (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) +
      HSub.hSub (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
⊢ Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((⁅X + Y, Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((⁅X, Z⁆ + ⁅Y, Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)

Tactic:
simp only [commutator_apply, coe_add, Pi.add_apply, map_add]

Premises used: map_add, LeftInvariantDerivation.coe_add, Pi.add_apply, LeftInvariantDerivation.commutator_apply
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g h : G
r : 𝕜
X_1 Y_1 : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ HAdd.hAdd (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) -
      HAdd.hAdd (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) =
    HSub.hSub (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) +
      HSub.hSub (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)

Tactic:
ring
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g h : G
r : 𝕜
X_1 Y_1 : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
h₁ :
  ∀ (f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯),
    Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((⁅X, Y + Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((⁅X, Y⁆ + ⁅X, Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
⊢ ⁅X, Y + Z⁆ = ⁅X, Y⁆ + ⁅X, Z⁆

Tactic:
ext1
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g h : G
r : 𝕜
X_1 Y_1 : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
h₁ :
  HAdd.hAdd (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) -
      HAdd.hAdd (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) =
    HSub.hSub (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) +
      HSub.hSub (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
⊢ Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((⁅X, Y + Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((⁅X, Y⁆ + ⁅X, Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)

Tactic:
simp only [commutator_apply, coe_add, Pi.add_apply, map_add]

Premises used: map_add, LeftInvariantDerivation.coe_add, Pi.add_apply, LeftInvariantDerivation.commutator_apply
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g h : G
r : 𝕜
X_1 Y_1 : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ HAdd.hAdd (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) -
      HAdd.hAdd (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) =
    HSub.hSub (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) +
      HSub.hSub (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)

Tactic:
ring
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g h : G
r : 𝕜
X_1 Y : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X : LeftInvariantDerivation I G
h₁ :
  ∀ (f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯),
    Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((⁅X, X⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((0 : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
⊢ ⁅X, X⁆ = 0

Tactic:
ext1
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g h : G
r : 𝕜
X_1 Y : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X : LeftInvariantDerivation I G
f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
h₁ :
  Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (0 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((0 : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
⊢ Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((⁅X, X⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((0 : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)

Tactic:
simp only [commutator_apply, sub_self]

Premises used: sub_self, LeftInvariantDerivation.commutator_apply
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g h : G
r : 𝕜
X_1 Y : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X : LeftInvariantDerivation I G
f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (0 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((0 : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g h : G
r : 𝕜
X_1 Y_1 : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
h₁ :
  ∀ (f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯),
    Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((⁅X, ⁅Y, Z⁆⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((⁅⁅X, Y⁆, Z⁆ + ⁅Y, ⁅X, Z⁆⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
⊢ ⁅X, ⁅Y, Z⁆⁆ = ⁅⁅X, Y⁆, Z⁆ + ⁅Y, ⁅X, Z⁆⁆

Tactic:
ext1
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g h : G
r_1 : 𝕜
X Y_1 : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
Y Z : LeftInvariantDerivation I G
h₁ :
  ∀ (f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯),
    Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((⁅Y, r • Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((r • ⁅Y, Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
⊢ ⁅Y, r • Z⁆ = r • ⁅Y, Z⁆

Tactic:
ext1
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g h : G
r_1 : 𝕜
X Y_1 : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
Y Z : LeftInvariantDerivation I G
f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((⁅Y, r • Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((r • ⁅Y, Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)

Tactic:
simp only [commutator_apply, map_smul, smul_sub, coe_smul, Pi.smul_apply]

Premises used: smul_sub, LeftInvariantDerivation.coe_smul, LeftInvariantDerivation.commutator_apply, map_smul, Pi.smul_apply
-- 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 : Group G
m n : ℕ∞ω
hmn : m ≤ n
h : LieGroup I n G
⊢ ContMDiffMul I m G

Tactic:
have : ContMDiffMul I m G := ContMDiffMul.of_le hmn
-- 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 : Group G
m n : ℕ∞ω
hmn : m ≤ n
h : LieGroup I n G
this : ContMDiffMul I m G
⊢ LieGroup I m G

Tactic:
⟨h.contMDiff_inv.of_le hmn⟩

Premises used: LieGroup.mk, LieGroup.contMDiff_inv, ContMDiff.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 : Group G
m n : ℕ∞ω
hmn : m ≤ n
h : LieGroup I n G
this : ContMDiffMul I m G
⊢ LieGroup I m G

Tactic:
exact ⟨h.contMDiff_inv.of_le hmn⟩
-- 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
a : ℕ∞ω
inst_12 : LieGroup I ∞ G
h : ENat.LEInfty a
⊢ LieGroup I a G

Tactic:
LieGroup.of_le h.out

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

Tactic:
LieGroup.of_le le_top

Premises used: le_top, LieGroup.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
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 : IsTopologicalGroup G
contMDiff_inv : ContMDiff I I (M' := G) 0 fun (a : G) ↦ a⁻¹
⊢ LieGroup I 0 G

Tactic:
constructor
-- 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 : IsTopologicalGroup G
contMDiff_inv : Continuous (Y := G) fun (a : G) ↦ a⁻¹
⊢ ContMDiff I I (M' := G) 0 fun (a : G) ↦ a⁻¹

Tactic:
rw [contMDiff_zero_iff]

Premises used: contMDiff_zero_iff
-- 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 : IsTopologicalGroup G
⊢ Continuous (Y := G) fun (a : G) ↦ a⁻¹

Tactic:
continuous_inv

Premises used: ContinuousInv.continuous_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 : IsTopologicalGroup G
⊢ Continuous (Y := G) fun (a : G) ↦ a⁻¹

Tactic:
exact continuous_inv

Premises used: ContinuousInv.continuous_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 2 G
⊢ LieGroup I 1 G

Tactic:
LieGroup.of_le one_le_two

Premises used: one_le_two, LieGroup.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
n : ℕ∞ω
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I n G
⊢ ContMDiff I I (M' := G) n fun (x : G) ↦ x⁻¹

Tactic:
LieGroup.contMDiff_inv

Premises used: LieGroup.contMDiff_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
inst_7 : LieGroup I n G
⊢ IsTopologicalGroup G

Tactic:
{ continuousMul_of_contMDiffMul I n with continuous_inv := (contMDiff_inv I n).continuous }

Premises used: IsTopologicalGroup.mk, continuousMul_of_contMDiffMul
-- 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
x₀ : M
hf : ContMDiffWithinAt I' I n f 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)⁻¹) s x₀

Tactic:
(contMDiff_inv I n).contMDiffAt.contMDiffWithinAt.comp x₀ hf <| Set.mapsTo_univ _ _

Premises used: ContMDiffAt.contMDiffWithinAt, Set.mapsTo_univ, contMDiff_inv, ContMDiff.contMDiffAt, ContMDiffWithinAt.comp