LeftInvariantDerivation.left_invariant'

theorem LeftInvariantDerivation.left_invariant' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {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 : SmoothMul I G] (g : G) (X : LeftInvariantDerivation I G), (hfdifferential ⋯) ((Derivation.evalAt 1) ↑X) = (Derivation.evalAt g) ↑X

This is a premature version of the left invariant lemma, which is recommended to be used in its `left_invariant` form. The theorem states that for any non-trivially normed field `𝕜`, normed add commutative group `E`, topological spaces `H` and `G`, and a model with corners `I` on `𝕜`, `E`, and `H`, if `G` is a charted space with respect to `H`, and `G` has a monoid structure that allows for smooth multiplication, then for any element `g` in `G` and any left-invariant derivation `X` on `I` and `G`, the differential of `h` evaluated at `1` and applied on `X` equals the differential of `h` evaluated at `g` and applied on `X`.

More concisely: For any non-trivially normed field 𝕜, normed add commutative group E, topological spaces H and G, and a model with corners I on 𝕜, E, and H, if G is a charted space with respect to H and has a smooth multiplication, then for any element g in G, and any left-invariant derivation X on I and G, the differential of any function h from I to H evaluated at g is equal to the evaluation of the differential of h at 1 and the action of g on X.