awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
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; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ 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; 𝓘(𝕜, 𝕜), 𝕜⟯)
have 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; 𝓘(𝕜, 𝕜), 𝕜⟯)
Tactic: simp only [commutator_apply, coe_add, Pi.add_apply, map_add]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
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
⊢ ⁅X, X⁆ = 0
have 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; 𝓘(𝕜, 𝕜), 𝕜⟯)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
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; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((⁅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; 𝓘(𝕜, 𝕜), 𝕜⟯)
have h₁ : Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (0 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
  ((0 : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
Tactic: simp only [commutator_apply, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
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
⊢ ⁅X, ⁅Y, Z⁆⁆ = ⁅⁅X, Y⁆, Z⁆ + ⁅Y, ⁅X, Z⁆⁆
have 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; 𝓘(𝕜, 𝕜), 𝕜⟯)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
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
⊢ ⁅Y, r • Z⁆ = r • ⁅Y, Z⁆
have 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; 𝓘(𝕜, 𝕜), 𝕜⟯)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LieGroup (hypothesis)
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
⊢ LieGroup I m G
have this : ContMDiffMul I m G
Tactic: have : ContMDiffMul I m G := ContMDiffMul.of_le hmn
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LieGroup (goal)
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
⊢ LieGroup I 0 G
have contMDiff_inv : ContMDiff I I (M' := G) 0 fun (a : G) ↦ a⁻¹
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LieGroup (goal)
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 I I (M' := G) 0 fun (a : G) ↦ a⁻¹
have contMDiff_inv : Continuous (Y := G) fun (a : G) ↦ a⁻¹
Tactic: rw [contMDiff_zero_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LieGroup (goal)
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₀
have 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₀
Tactic: simp_rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LieGroup (goal)
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₀
have 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₀
Tactic: simp_rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LieGroup (goal)
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
have 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
Tactic: simp_rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LieGroup (goal)
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
have 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)⁻¹
Tactic: simp_rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LieGroup (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜
hx : x ≠ 0
⊢ ContMDiffAt 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜) n Inv.inv x
have rw : ContDiffAt 𝕜 n Inv.inv x
Tactic: rw [contMDiffAt_iff_contDiffAt]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LieGroup (hypothesis)
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
⊢ ContMDiffInv₀ I 0 G
have this : T1Space G
Tactic: have : T1Space G := I.t1Space G
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LieGroup (goal)
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
⊢ ContMDiffInv₀ I 0 G
have contMDiffAt_inv₀ : ∀ ⦃x : G⦄, x ≠ 0 → ContMDiffAt I I (M' := G) 0 (fun (y : G) ↦ y⁻¹) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LieGroup (goal)
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}ᶜ
have rw : ContinuousOn (Y := G) (fun (x : G) ↦ x⁻¹) {0}ᶜ
Tactic: rw [contMDiffOn_zero_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LieGroup (hypothesis)
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
⊢ ∀ ⦃x : G⦄, x ≠ 0 → ContMDiffAt I I (M' := G) 0 (fun (y : G) ↦ y⁻¹) x
have A : 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₀
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LieGroup (hypothesis)
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
⊢ ContMDiffAt I I (M' := G) 0 (fun (y : G) ↦ y⁻¹) x
have this₁ : 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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LieGroup (goal)
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 I I (M' := G) 0 (fun (y : G) ↦ y⁻¹) x
have contMDiffAt_inv₀ : {0}ᶜ ∈ nhds x
Tactic: apply ContMDiffWithinAt.contMDiffAt this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (hypothesis)
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
⊢ ContMDiffMul I m G
have this : IsManifold I m G
Tactic: have : IsManifold I m G := IsManifold.of_le hmn
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
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
⊢ ContMDiffMul I 0 G
have contMDiff_mul : ContMDiff (I.prod I) I (M' := G) 0 fun (p : G × G) ↦ p.1 * p.2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
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 (I.prod I) I (M' := G) 0 fun (p : G × G) ↦ p.1 * p.2
have contMDiff_mul : Continuous (Y := G) fun (p : G × G) ↦ p.1 * p.2
Tactic: rw [contMDiff_zero_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
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_8
inst_4 : Semigroup G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I ∞ G
g h : G
⊢ Eq (α := C^∞⟮I, G; I, G⟯) (𝑳 I (g * h)) (ContMDiffMap.comp (𝑳 I g) (𝑳 I h))
have h₁ : ∀ (x : G), Eq (α := G) ((𝑳 I (g * h) : (a : G) → G) x : G) ((ContMDiffMap.comp (𝑳 I g) (𝑳 I h) : (a : G) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
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_8
inst_4 : Semigroup G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I ∞ G
g h : G
⊢ Eq (α := C^∞⟮I, G; I, G⟯) (𝑹 I (g * h)) (ContMDiffMap.comp (𝑹 I h) (𝑹 I g))
have h₁ : ∀ (x : G), Eq (α := G) ((𝑹 I (g * h) : (a : G) → G) x : G) ((ContMDiffMap.comp (𝑹 I h) (𝑹 I g) : (a : G) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
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 : Monoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
H' : Type u_5
inst_8 : TopologicalSpace H'
E' : Type u_6
inst_9 : NormedAddCommGroup E'
inst_10 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst_11 : Monoid G'
inst_12 : TopologicalSpace G'
inst_13 : ChartedSpace H' G'
inst_14 : ContMDiffMul I' n G'
f g : ContMDiffMonoidMorphism I I' n G G'
h :
  Eq (α := (a : G) → G') ((fun (a : ContMDiffMonoidMorphism I I' n G G') ↦ (↑a.toMonoidHom : OneHom G G').toFun) f)
    ((fun (a : ContMDiffMonoidMorphism I I' n G G') ↦ (↑a.toMonoidHom : OneHom G G').toFun) g)
⊢ f = g
have mk : ∀ (toMonoidHom : G →* G') (contMDiff_toFun : ContMDiff I I' n (↑toMonoidHom : OneHom G G').toFun)
  (h :
    Eq (α := (a : G) → G')
      ((fun (a : ContMDiffMonoidMorphism I I' n G G') ↦ (↑a.toMonoidHom : OneHom G G').toFun)
        { toMonoidHom := toMonoidHom, contMDiff_toFun := contMDiff_toFun })
      ((fun (a : ContMDiffMonoidMorphism I I' n G G') ↦ (↑a.toMonoidHom : OneHom G G').toFun) g)),
  { toMonoidHom := toMonoidHom, contMDiff_toFun := contMDiff_toFun : ContMDiffMonoidMorphism I I' n G G' } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
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 : Monoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
H' : Type u_5
inst_8 : TopologicalSpace H'
E' : Type u_6
inst_9 : NormedAddCommGroup E'
inst_10 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst_11 : Monoid G'
inst_12 : TopologicalSpace G'
inst_13 : ChartedSpace H' G'
inst_14 : ContMDiffMul I' n G'
g : ContMDiffMonoidMorphism I I' n G G'
toMonoidHom : G →* G'
contMDiff_toFun : ContMDiff I I' n (↑toMonoidHom : OneHom G G').toFun
h :
  Eq (α := (a : G) → G')
    ((fun (a : ContMDiffMonoidMorphism I I' n G G') ↦ (↑a.toMonoidHom : OneHom G G').toFun)
      { toMonoidHom := toMonoidHom, contMDiff_toFun := contMDiff_toFun })
    ((fun (a : ContMDiffMonoidMorphism I I' n G G') ↦ (↑a.toMonoidHom : OneHom G G').toFun) g)
⊢ { toMonoidHom := toMonoidHom, contMDiff_toFun := contMDiff_toFun : ContMDiffMonoidMorphism I I' n G G' } = g
have mk : ∀ (toMonoidHom_1 : G →* G') (contMDiff_toFun_1 : ContMDiff I I' n (↑toMonoidHom_1 : OneHom G G').toFun)
  (h :
    Eq (α := (a : G) → G')
      ((fun (a : ContMDiffMonoidMorphism I I' n G G') ↦ (↑a.toMonoidHom : OneHom G G').toFun)
        { toMonoidHom := toMonoidHom, contMDiff_toFun := contMDiff_toFun })
      ((fun (a : ContMDiffMonoidMorphism I I' n G G') ↦ (↑a.toMonoidHom : OneHom G G').toFun)
        { toMonoidHom := toMonoidHom_1, contMDiff_toFun := contMDiff_toFun_1 })),
  { toMonoidHom := toMonoidHom, contMDiff_toFun := contMDiff_toFun : ContMDiffMonoidMorphism I I' n G G' } =
    { toMonoidHom := toMonoidHom_1, contMDiff_toFun := contMDiff_toFun_1 }
Tactic: cases g
Cleared hypotheses: g, h