awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.QuotientInter (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
set :
  #A ≤ card (α := G ⧸ H) (image (⇑(QuotientGroup.mk' H) : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
set₁ :
  let π : G →* G ⧸ H := QuotientGroup.mk' H;
  #A ≤ card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
set₂ :
  let π : G →* G ⧸ H := QuotientGroup.mk' H;
  ∑ b ∈ image (⇑π : (a : G) → G ⧸ H) A, #({a ∈ A | (π : (a : G) → G ⧸ H) a = b}) ≤
    card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
⊢ #A ≤ card (α := G ⧸ H) (image (⇑(QuotientGroup.mk' H) : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
have set₃ : let π : G →* G ⧸ H := QuotientGroup.mk' H;
∀ (a : G) (ha : a ∈ A),
  #({a_1 ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a_1 : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)}) ≤
    #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
Tactic: classical
  set π := QuotientGroup.mk' H
  rw [card_eq_sum_card_image π]
  refine sum_le_card_nsmul _ _ _ <| forall_mem_image.2 fun a ha ↦ ?_
  calc
    #{a' ∈ A | π a' = π a}
    _ ≤ #({a' ∈ A | π a' = π a}⁻¹ * {a' ∈ A | π a' = π a}) :=
      card_le_card_mul_left ⟨a⁻¹, by simpa⟩
    _ ≤ #{x ∈ A⁻¹ * A | x ∈ H} := by
      gcongr
      simp only [mul_subset_iff, mem_inv', map_inv, mem_filter, and_imp]
      rintro x hx hxa y hy hya
      refine ⟨mul_mem_mul (by simpa) hy, (QuotientGroup.eq_one_iff _).1 (?_ : π _ = _)⟩
      simp [hya, ← hxa]
    _ = #{x ∈ A ^ 2 | x ∈ H} := by simp [hAsymm, sq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
Goal:
𝕜 : 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 : ContMDiffMul I ∞ G
X Y : LeftInvariantDerivation I G
h :
  (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) =
    (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
⊢ X = Y
have mk : ∀ (toDerivation : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
  (left_invariant'' :
    ∀ (g : G),
      Eq (α := PointDerivation I g)
        ((𝒅ₕ (f := 𝑳 I g) sorry : (a : PointDerivation I 1) → PointDerivation I g)
            ((Derivation.evalAt 1 :
                (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
              toDerivation) :
          PointDerivation I g)
        ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
            toDerivation :
          PointDerivation I g))
  (h :
    (↑{ toDerivation := toDerivation, left_invariant'' := left_invariant'' : LeftInvariantDerivation I G } :
        Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) =
      (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)),
  { toDerivation := toDerivation, left_invariant'' := left_invariant'' : LeftInvariantDerivation I G } = Y
Tactic: cases X
Cleared hypotheses: X, h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
Goal:
𝕜 : 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 : ContMDiffMul I ∞ G
Y : LeftInvariantDerivation I G
toDerivation : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant'' :
  ∀ (g : G),
    Eq (α := PointDerivation I g)
      ((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I 1) → PointDerivation I g)
          ((Derivation.evalAt 1 : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
            toDerivation) :
        PointDerivation I g)
      ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
          toDerivation :
        PointDerivation I g)
h :
  (↑{ toDerivation := toDerivation, left_invariant'' := left_invariant'' : LeftInvariantDerivation I G } :
      Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) =
    (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
⊢ { toDerivation := toDerivation, left_invariant'' := left_invariant'' : LeftInvariantDerivation I G } = Y
have mk : ∀ (toDerivation_1 : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
  (left_invariant''_1 :
    ∀ (g : G),
      Eq (α := PointDerivation I g)
        ((𝒅ₕ (f := 𝑳 I g) sorry : (a : PointDerivation I 1) → PointDerivation I g)
            ((Derivation.evalAt 1 :
                (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
              toDerivation_1) :
          PointDerivation I g)
        ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
            toDerivation_1 :
          PointDerivation I g))
  (h :
    (↑{ toDerivation := toDerivation, left_invariant'' := left_invariant'' : LeftInvariantDerivation I G } :
        Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) =
      (↑{ toDerivation := toDerivation_1, left_invariant'' := left_invariant''_1 : LeftInvariantDerivation I G } :
        Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)),
  { toDerivation := toDerivation, left_invariant'' := left_invariant'' : LeftInvariantDerivation I G } =
    { toDerivation := toDerivation_1, left_invariant'' := left_invariant''_1 }
Tactic: cases Y
Cleared hypotheses: Y, h
-- 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_1 h : G
r_1 : 𝕜
X_1 Y : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : ℕ
X : LeftInvariantDerivation I G
g : G
⊢ Eq (α := PointDerivation I g)
    ((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I 1) → PointDerivation I g)
        ((Derivation.evalAt 1 : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
          (r • (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯))) :
      PointDerivation I g)
    ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
        (r • (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)) :
      PointDerivation I g)
have simp_rw : HSMul.hSMul (β := PointDerivation I g) r
    ((𝒅ₕ (f := 𝑳 I g) sorry : (a : PointDerivation I 1) → PointDerivation I g)
        ((Derivation.evalAt 1 : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
          (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)) :
      PointDerivation I g) =
  HSMul.hSMul (β := PointDerivation I g) r
    ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
        (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
      PointDerivation I g)
Tactic: simp_rw [LinearMap.map_smul_of_tower _ r, left_invariant']
-- 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_1 h : G
r_1 : 𝕜
X_1 Y : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : ℤ
X : LeftInvariantDerivation I G
g : G
⊢ Eq (α := PointDerivation I g)
    ((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I 1) → PointDerivation I g)
        ((Derivation.evalAt 1 : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
          (r • (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯))) :
      PointDerivation I g)
    ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
        (r • (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)) :
      PointDerivation I g)
have simp_rw : HSMul.hSMul (β := PointDerivation I g) r
    ((𝒅ₕ (f := 𝑳 I g) sorry : (a : PointDerivation I 1) → PointDerivation I g)
        ((Derivation.evalAt 1 : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
          (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)) :
      PointDerivation I g) =
  HSMul.hSMul (β := PointDerivation I g) r
    ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
        (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
      PointDerivation I g)
Tactic: simp_rw [LinearMap.map_smul_of_tower _ r, left_invariant']
-- 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_1 h : G
r_1 : 𝕜
X_1 Y : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
X : LeftInvariantDerivation I G
g : G
⊢ Eq (α := PointDerivation I g)
    ((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I 1) → PointDerivation I g)
        ((Derivation.evalAt 1 : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
          (r • (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯))) :
      PointDerivation I g)
    ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
        (r • (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)) :
      PointDerivation I g)
have simp : HSMul.hSMul (β := PointDerivation I g) r
    ((𝒅ₕ (f := 𝑳 I g) sorry : (a : PointDerivation I 1) → PointDerivation I g)
        ((Derivation.evalAt 1 : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
          (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)) :
      PointDerivation I g) =
  HSMul.hSMul (β := PointDerivation I g) r
    ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
        (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
      PointDerivation I g)
Tactic: simp only [LinearMap.map_smul_of_tower, map_smul]
-- 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_1 h : G
r_1 : 𝕜
X_1 Y : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
X : LeftInvariantDerivation I G
g : G
⊢ HSMul.hSMul (β := PointDerivation I g) r
      ((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I 1) → PointDerivation I g)
          ((Derivation.evalAt 1 : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
            (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)) :
        PointDerivation I g) =
    HSMul.hSMul (β := PointDerivation I g) r
      ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
          (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
        PointDerivation I g)
have rw : HSMul.hSMul (β := PointDerivation I g) r
    ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
        (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
      PointDerivation I g) =
  HSMul.hSMul (β := PointDerivation I g) r
    ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
        (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
      PointDerivation I g)
Tactic: rw [left_invariant']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
Goal:
𝕜 : 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 : ContMDiffMul I ∞ G
g h : G
X : LeftInvariantDerivation I G
⊢ Eq (α := PointDerivation I (g * h))
    ((evalAt (g * h) : (a : LeftInvariantDerivation I G) → PointDerivation I (g * h)) X : PointDerivation I (g * h))
    ((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I h) → PointDerivation I (g * h))
        ((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X) :
      PointDerivation I (g * h))
have H₁ : ∀ (f : C^∞⟮I, G; 𝕜⟯⟨g * h⟩),
  Eq.{u_1 + 1} (α := 𝕜)
    ((((evalAt (g * h) : (a : LeftInvariantDerivation I G) → PointDerivation I (g * h)) X : PointDerivation I (g * h)) :
          (a : C^∞⟮I, G; 𝕜⟯⟨g * h⟩) → 𝕜)
        f :
      𝕜)
    ((((𝒅ₕ (f := 𝑳 I g) sorry : (a : PointDerivation I h) → PointDerivation I (g * h))
              ((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X) :
            PointDerivation I (g * h)) :
          (a : C^∞⟮I, G; 𝕜⟯⟨g * h⟩) → 𝕜)
        f :
      𝕜)
Tactic: ext f
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
Goal:
𝕜 : 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 : ContMDiffMul I ∞ G
g h : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝕜⟯⟨g * h⟩
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((evalAt (g * h) : (a : LeftInvariantDerivation I G) → PointDerivation I (g * h)) X : PointDerivation I (g * h)) :
          (a : C^∞⟮I, G; 𝕜⟯⟨g * h⟩) → 𝕜)
        f :
      𝕜)
    ((((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I h) → PointDerivation I (g * h))
              ((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X) :
            PointDerivation I (g * h)) :
          (a : C^∞⟮I, G; 𝕜⟯⟨g * h⟩) → 𝕜)
        f :
      𝕜)
have H₁ : Eq.{u_1 + 1} (α := 𝕜)
  (((((𝒅 (𝑳 I g) ((𝑳 I h : (a : G) → G) 1) ∘ₗ 𝒅 (𝑳 I h) 1 :
                PointDerivation.{u_1, u_2, u_3, u_4} I (M := G) 1 →ₗ[𝕜]
                  PointDerivation I (M := G) ((𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1 : G) : G)) :
              (a : PointDerivation I 1) → PointDerivation I (((𝑳 I g).comp (𝑳 I h) : (a : G) → G) 1))
            ((evalAt 1 : (a : LeftInvariantDerivation I G) → PointDerivation I 1) X) :
          PointDerivation I (M := G) ((ContMDiffMap.comp (𝑳 I g) (𝑳 I h) : (a : G) → G) 1 : G)) :
        (a : C^∞⟮I, G; 𝕜⟯⟨((𝑳 I g).comp (𝑳 I h) : (a : G) → G) 1⟩) → 𝕜)
      f :
    𝕜)
  ((((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X : PointDerivation I h) :
        (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
      (ContMDiffMap.comp f (𝑳 I g)) :
    𝕜)
Tactic: rw [← left_invariant, hfdifferential_apply, hfdifferential_apply, L_mul, fdifferential_comp,
    fdifferential_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
Goal:
𝕜 : 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 : ContMDiffMul I ∞ G
g h : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝕜⟯⟨g * h⟩
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (((((𝒅 (𝑳 I g) ((𝑳 I h : (a : G) → G) 1) ∘ₗ 𝒅 (𝑳 I h) 1 :
                  PointDerivation.{u_1, u_2, u_3, u_4} I (M := G) 1 →ₗ[𝕜]
                    PointDerivation I (M := G) ((𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1 : G) : G)) :
                (a : PointDerivation I 1) → PointDerivation I (((𝑳 I g).comp (𝑳 I h) : (a : G) → G) 1))
              ((evalAt 1 : (a : LeftInvariantDerivation I G) → PointDerivation I 1) X) :
            PointDerivation I (M := G) ((ContMDiffMap.comp (𝑳 I g) (𝑳 I h) : (a : G) → G) 1 : G)) :
          (a : C^∞⟮I, G; 𝕜⟯⟨((𝑳 I g).comp (𝑳 I h) : (a : G) → G) 1⟩) → 𝕜)
        f :
      𝕜)
    ((((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X : PointDerivation I h) :
          (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
        (ContMDiffMap.comp f (𝑳 I g)) :
      𝕜)
have H₁ : Eq.{u_1 + 1} (α := 𝕜)
  ((((𝒅 (𝑳 I g) ((𝑳 I h : (a : G) → G) 1) :
              (a : PointDerivation I ((𝑳 I h : (a : G) → G) 1)) →
                PointDerivation I ((𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1)))
            ((𝒅 (𝑳 I h) 1 : (a : PointDerivation I 1) → PointDerivation I ((𝑳 I h : (a : G) → G) 1))
              ((evalAt 1 : (a : LeftInvariantDerivation I G) → PointDerivation I 1) X)) :
          PointDerivation I (M := G) ((𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1 : G) : G)) :
        (a : C^∞⟮I, G; 𝕜⟯⟨(𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1)⟩) → 𝕜)
      f :
    𝕜)
  ((((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X : PointDerivation I h) :
        (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
      (ContMDiffMap.comp f (𝑳 I g)) :
    𝕜)
Tactic: simp only [ContMDiffMap.comp_apply, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
Goal:
𝕜 : 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 : ContMDiffMul I ∞ G
g h : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝕜⟯⟨g * h⟩
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((𝒅 (𝑳 I g) ((𝑳 I h : (a : G) → G) 1) :
                (a : PointDerivation I ((𝑳 I h : (a : G) → G) 1)) →
                  PointDerivation I ((𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1)))
              ((𝒅 (𝑳 I h) 1 : (a : PointDerivation I 1) → PointDerivation I ((𝑳 I h : (a : G) → G) 1))
                ((evalAt 1 : (a : LeftInvariantDerivation I G) → PointDerivation I 1) X)) :
            PointDerivation I (M := G) ((𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1 : G) : G)) :
          (a : C^∞⟮I, G; 𝕜⟯⟨(𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1)⟩) → 𝕜)
        f :
      𝕜)
    ((((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X : PointDerivation I h) :
          (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
        (ContMDiffMap.comp f (𝑳 I g)) :
      𝕜)
have H₁ : Eq.{u_1 + 1} (α := 𝕜)
  ((((𝒅 (𝑳 I h) 1 : (a : PointDerivation I 1) → PointDerivation I ((𝑳 I h : (a : G) → G) 1))
            ((evalAt 1 : (a : LeftInvariantDerivation I G) → PointDerivation I 1) X) :
          PointDerivation I (M := G) ((𝑳 I h : (a : G) → G) 1 : G)) :
        (a : C^∞⟮I, G; 𝕜⟯⟨(𝑳 I h : (a : G) → G) 1⟩) → 𝕜)
      (ContMDiffMap.comp f (𝑳 I g)) :
    𝕜)
  ((((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X : PointDerivation I h) :
        (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
      (ContMDiffMap.comp f (𝑳 I g)) :
    𝕜)
Tactic: rw [fdifferential_apply, ← hfdifferential_apply (smoothLeftMul_one I h), left_invariant]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
Goal:
𝕜 : 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 : ContMDiffMul I ∞ G
g h : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝕜⟯⟨g * h⟩
H₁ :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((𝒅 (𝑳 I h) 1 : (a : PointDerivation I 1) → PointDerivation I ((𝑳 I h : (a : G) → G) 1))
              ((evalAt 1 : (a : LeftInvariantDerivation I G) → PointDerivation I 1) X) :
            PointDerivation I (M := G) ((𝑳 I h : (a : G) → G) 1 : G)) :
          (a : C^∞⟮I, G; 𝕜⟯⟨(𝑳 I h : (a : G) → G) 1⟩) → 𝕜)
        (ContMDiffMap.comp f (𝑳 I g)) :
      𝕜)
    ((((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X : PointDerivation I h) :
          (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
        (ContMDiffMap.comp f (𝑳 I g)) :
      𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((𝒅 (𝑳 I g) ((𝑳 I h : (a : G) → G) 1) :
                (a : PointDerivation I ((𝑳 I h : (a : G) → G) 1)) →
                  PointDerivation I ((𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1)))
              ((𝒅 (𝑳 I h) 1 : (a : PointDerivation I 1) → PointDerivation I ((𝑳 I h : (a : G) → G) 1))
                ((evalAt 1 : (a : LeftInvariantDerivation I G) → PointDerivation I 1) X)) :
            PointDerivation I (M := G) ((𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1 : G) : G)) :
          (a : C^∞⟮I, G; 𝕜⟯⟨(𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1)⟩) → 𝕜)
        f :
      𝕜)
    ((((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X : PointDerivation I h) :
          (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
        (ContMDiffMap.comp f (𝑳 I g)) :
      𝕜)
have H₂ : Eq.{u_1 + 1} (α := 𝕜)
  ((((𝒅ₕ (f := 𝑳 I h) sorry : (a : PointDerivation I 1) → PointDerivation I h)
            ((evalAt 1 : (a : LeftInvariantDerivation I G) → PointDerivation I 1) X) :
          PointDerivation I h) :
        (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
      (ContMDiffMap.comp f (𝑳 I g)) :
    𝕜)
  ((((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X : PointDerivation I h) :
        (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
      (ContMDiffMap.comp f (𝑳 I g)) :
    𝕜)
Tactic: rw [fdifferential_apply, ← hfdifferential_apply (smoothLeftMul_one I h), left_invariant]