awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p ∈
    PartialEquiv.source (β := ModelProd (ModelProd H E) (ModelProd H' E'))
      (OpenPartialHomeomorph.toPartialEquiv (chartAt (ModelProd (ModelProd H E) (ModelProd H' E')) (a, b)))
⊢ Function.comp (β := E × E') Prod.snd
      (fun (x : TangentBundle I M × TangentBundle I' M') ↦
        (fderivWithin 𝕜
              (((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) ∘ fun (p : M × M') ↦
                  ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H) p.1,
                    (↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H') p.2)) ∘
                (↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H (x.1.proj (E := TangentSpace I)))).prod
                          (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (x.2.proj (E := TangentSpace I'))))).symm :
                    ModelProd H H' → M × M') ∘
                  (↑(I.prod I'.toPartialEquiv).symm : E × E' → ModelProd H H'))
              (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
              ((↑I : H → E) ((↑(chartAt H (x.1.proj (E := TangentSpace I))) : M → H) (x.1.proj (E := TangentSpace I))),
                (↑I' : H' → E')
                  ((↑(chartAt H' (x.2.proj (E := TangentSpace I'))) : M' → H') (x.2.proj (E := TangentSpace I')))) :
            (a : E × E') → E × E')
          (x.1.snd (E := TangentSpace I), x.2.snd (E := TangentSpace I')))
      p =
    ((↑(trivializationAt E' (TangentSpace I') (b.proj (E := TangentSpace I'))) :
          TotalSpace E' (TangentSpace I') → M' × E')
        p.2).2
have hp₁ : p.1.proj (E := TangentSpace I) ∈
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
  p.2.proj (E := TangentSpace I') ∈
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
Tactic: simp only [prodChartedSpace_chartAt, OpenPartialHomeomorph.prod_toPartialEquiv,
      PartialEquiv.prod_source, Set.mem_prod, TangentBundle.mem_chart_source_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
⊢ DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
have apply : ContDiffWithinAt 𝕜 1 φ (range (↑I' : H' → E'))
  ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
Tactic: apply ContDiffWithinAt.differentiableWithinAt _ one_ne_zero
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
⊢ ContDiffWithinAt 𝕜 1 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
have hy : (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))) ∈
  ((extChartAt I' (p.2.proj (E := TangentSpace I'))).symm ≫ extChartAt I' (b.proj (E := TangentSpace I'))).source
Tactic: apply contDiffWithinAt_ext_coord_change
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
D0 :
  DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
      ((↑I : H → E) ((↑(chartAt H (w.proj (E := TangentSpace I))) : M → H) (w.proj (E := TangentSpace I))),
        (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
φ' : (x : E) → E :=
  fun (x : E) ↦
    (↑I : H → E)
      ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H (p.1.proj (E := TangentSpace I)))) : H → M) ((↑I.symm : E → H) x)))
⊢ DifferentiableWithinAt 𝕜 φ' (range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))))
have apply : ContDiffWithinAt 𝕜 1 φ' (range (↑I : H → E))
  ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))))
Tactic: apply ContDiffWithinAt.differentiableWithinAt _ one_ne_zero
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
D0 :
  DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
      ((↑I : H → E) ((↑(chartAt H (w.proj (E := TangentSpace I))) : M → H) (w.proj (E := TangentSpace I))),
        (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
φ' : (x : E) → E :=
  fun (x : E) ↦
    (↑I : H → E)
      ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H (p.1.proj (E := TangentSpace I)))) : H → M) ((↑I.symm : E → H) x)))
⊢ ContDiffWithinAt 𝕜 1 φ' (range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))))
have hy : (↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))) ∈
  ((extChartAt I (p.1.proj (E := TangentSpace I))).symm ≫ extChartAt I (a.proj (E := TangentSpace I))).source
Tactic: apply contDiffWithinAt_ext_coord_change
-- Lean 4 proof step from Mathlib.Geometry.Manifold.DerivationBundle (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
x : M
k : 𝕜
f : C^∞⟮I, M; 𝕜⟯⟨x⟩
h : 𝕜
⊢ (k • f) • h = k • f • h
have rw : HMul.hMul (α := 𝕜) ((k • f : (a : M) → 𝕜) x : 𝕜) h = k • f • h
Tactic: rw [smul_def, smul_def, ContMDiffMap.coe_smul, Pi.smul_apply, smul_eq_mul, smul_eq_mul,
      mul_assoc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.DerivationBundle (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
x : M
k : 𝕜
f : C^∞⟮I, M; 𝕜⟯⟨x⟩
h : 𝕜
rw : HMul.hMul (α := 𝕜) ((k • f : (a : M) → 𝕜) x : 𝕜) h = k • f • h
⊢ (k • f) • h = k • f • h
have rw₁ : HMul.hMul (α := 𝕜) ((k • f : (a : M) → 𝕜) x : 𝕜) h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
Tactic: rw [smul_def, smul_def, ContMDiffMap.coe_smul, Pi.smul_apply, smul_eq_mul, smul_eq_mul,
      mul_assoc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.DerivationBundle (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
x : M
k : 𝕜
f : C^∞⟮I, M; 𝕜⟯⟨x⟩
h : 𝕜
rw : HMul.hMul (α := 𝕜) ((k • f : (a : M) → 𝕜) x : 𝕜) h = k • f • h
rw₁ : HMul.hMul (α := 𝕜) ((k • f : (a : M) → 𝕜) x : 𝕜) h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
⊢ (k • f) • h = k • f • h
have rw₂ : HSMul.hSMul (β := (a : M) → 𝕜) k (⇑f : (a : M) → 𝕜) x * h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
Tactic: rw [smul_def, smul_def, ContMDiffMap.coe_smul, Pi.smul_apply, smul_eq_mul, smul_eq_mul,
      mul_assoc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.DerivationBundle (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
x : M
k : 𝕜
f : C^∞⟮I, M; 𝕜⟯⟨x⟩
h : 𝕜
rw : HMul.hMul (α := 𝕜) ((k • f : (a : M) → 𝕜) x : 𝕜) h = k • f • h
rw₁ : HMul.hMul (α := 𝕜) ((k • f : (a : M) → 𝕜) x : 𝕜) h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
rw₂ : HSMul.hSMul (β := (a : M) → 𝕜) k (⇑f : (a : M) → 𝕜) x * h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
⊢ (k • f) • h = k • f • h
have rw₃ : HSMul.hSMul (β := 𝕜) k ((f : (a : M) → 𝕜) x : 𝕜) * h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
Tactic: rw [smul_def, smul_def, ContMDiffMap.coe_smul, Pi.smul_apply, smul_eq_mul, smul_eq_mul,
      mul_assoc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.DerivationBundle (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
x : M
k : 𝕜
f : C^∞⟮I, M; 𝕜⟯⟨x⟩
h : 𝕜
rw : HMul.hMul (α := 𝕜) ((k • f : (a : M) → 𝕜) x : 𝕜) h = k • f • h
rw₁ : HMul.hMul (α := 𝕜) ((k • f : (a : M) → 𝕜) x : 𝕜) h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
rw₂ : HSMul.hSMul (β := (a : M) → 𝕜) k (⇑f : (a : M) → 𝕜) x * h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
rw₃ : HSMul.hSMul (β := 𝕜) k ((f : (a : M) → 𝕜) x : 𝕜) * h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
⊢ (k • f) • h = k • f • h
have rw₄ : HMul.hMul (β := 𝕜) k ((f : (a : M) → 𝕜) x : 𝕜) * h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
Tactic: rw [smul_def, smul_def, ContMDiffMap.coe_smul, Pi.smul_apply, smul_eq_mul, smul_eq_mul,
      mul_assoc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.DerivationBundle (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
x : M
k : 𝕜
f : C^∞⟮I, M; 𝕜⟯⟨x⟩
h : 𝕜
rw : HMul.hMul (α := 𝕜) ((k • f : (a : M) → 𝕜) x : 𝕜) h = k • f • h
rw₁ : HMul.hMul (α := 𝕜) ((k • f : (a : M) → 𝕜) x : 𝕜) h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
rw₂ : HSMul.hSMul (β := (a : M) → 𝕜) k (⇑f : (a : M) → 𝕜) x * h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
rw₃ : HSMul.hSMul (β := 𝕜) k ((f : (a : M) → 𝕜) x : 𝕜) * h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
rw₄ : HMul.hMul (β := 𝕜) k ((f : (a : M) → 𝕜) x : 𝕜) * h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
⊢ (k • f) • h = k • f • h
have rw₅ : HMul.hMul (β := 𝕜) k ((f : (a : M) → 𝕜) x : 𝕜) * h = k * HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
Tactic: rw [smul_def, smul_def, ContMDiffMap.coe_smul, Pi.smul_apply, smul_eq_mul, smul_eq_mul,
      mul_assoc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.DerivationBundle (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
x : M
k : 𝕜
f : C^∞⟮I, M; 𝕜⟯⟨x⟩
h : 𝕜
rw : HMul.hMul (α := 𝕜) ((k • f : (a : M) → 𝕜) x : 𝕜) h = k • f • h
rw₁ : HMul.hMul (α := 𝕜) ((k • f : (a : M) → 𝕜) x : 𝕜) h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
rw₂ : HSMul.hSMul (β := (a : M) → 𝕜) k (⇑f : (a : M) → 𝕜) x * h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
rw₃ : HSMul.hSMul (β := 𝕜) k ((f : (a : M) → 𝕜) x : 𝕜) * h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
rw₄ : HMul.hMul (β := 𝕜) k ((f : (a : M) → 𝕜) x : 𝕜) * h = k • HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
rw₅ : HMul.hMul (β := 𝕜) k ((f : (a : M) → 𝕜) x : 𝕜) * h = k * HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
⊢ (k • f) • h = k • f • h
have rw₆ : k * HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h = k * HMul.hMul (α := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) h
Tactic: rw [smul_def, smul_def, ContMDiffMap.coe_smul, Pi.smul_apply, smul_eq_mul, smul_eq_mul,
      mul_assoc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.DerivationBundle (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f_1 : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : (f : (a : M) → M') x = y
v : PointDerivation I x
g g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp (g + g') f) =
    HAdd.hAdd (α := 𝕜) (β := 𝕜) ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
      ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜)
have rw : (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f + ContMDiffMap.comp g' f) =
  HAdd.hAdd (α := 𝕜) (β := 𝕜) ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
    ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜)
Tactic: rw [ContMDiffMap.add_comp, Derivation.map_add]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.DerivationBundle (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f_1 : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : (f : (a : M) → M') x = y
v : PointDerivation I x
g g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
rw :
  (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f + ContMDiffMap.comp g' f) =
    HAdd.hAdd (α := 𝕜) (β := 𝕜) ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
      ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜)
⊢ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp (g + g') f) =
    HAdd.hAdd (α := 𝕜) (β := 𝕜) ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
      ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜)
have rw₁ : HAdd.hAdd (α := 𝕜) (β := 𝕜) ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
    ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜) =
  HAdd.hAdd (α := 𝕜) (β := 𝕜) ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
    ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜)
Tactic: rw [ContMDiffMap.add_comp, Derivation.map_add]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.DerivationBundle (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f_1 : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : (f : (a : M) → M') x = y
v : PointDerivation I x
k : 𝕜
g : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp (k • g) f) =
    HSMul.hSMul (α := 𝕜) (β := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) k : 𝕜)
      ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
have dsimp : (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp (k • g) f) =
  HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.DerivationBundle (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f_1 : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : (f : (a : M) → M') x = y
v : PointDerivation I x
k : 𝕜
g : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp (k • g) f) =
    HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
have rw : (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (k • ContMDiffMap.comp g f) =
  HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
Tactic: rw [ContMDiffMap.smul_comp, Derivation.map_smul, smul_eq_mul]