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'
f : M → M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : 1 ≤ n
hs : UniqueMDiffOn I s
⊢ ContinuousOn (X := TangentBundle I M) (Y := TangentBundle I' M') (tangentMapWithin I I' f s)
    (TotalSpace.proj (E := TangentSpace I) ⁻¹' s)
have this : ContMDiffOn I.tangent (M := TangentBundle I M) I'.tangent (M' := TangentBundle I' M') 0 (tangentMapWithin I I' f s)
  (TotalSpace.proj (E := TangentSpace I) ⁻¹' s)
Tactic: have : CMDiff[π E (TangentSpace I) ⁻¹' s] 0 (tangentMapWithin I I' f s) :=
    hf.contMDiffOn_tangentMapWithin hmn hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m 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'
f : M → M'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiff I I' n f
hmn : m + 1 ≤ n
⊢ ContMDiff I.tangent (M := TangentBundle I M) I'.tangent (M' := TangentBundle I' M') m (tangentMap I I' f)
have rw : ∀ (hf : ContMDiffOn I I' n f univ) (hmn : m + 1 ≤ n),
  ContMDiffOn I.tangent (M := TangentBundle I M) I'.tangent (M' := TangentBundle I' M') m (tangentMap I I' f) univ
Tactic: rw [← contMDiffOn_univ] at hf ⊢
Cleared hypotheses: hf, hmn
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m 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'
f : M → M'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f univ
hmn : m + 1 ≤ n
⊢ ContMDiffOn I.tangent (M := TangentBundle I M) I'.tangent (M' := TangentBundle I' M') m (tangentMap I I' f) univ
have h : Eq (α := TangentBundle I M → TangentBundle I' M') (tangentMap I I' f) (tangentMapWithin I I' f univ)
Tactic: convert! hf.contMDiffOn_tangentMapWithin hmn uniqueMDiffOn_univ
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m 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'
f : M → M'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f univ
hmn : m + 1 ≤ n
⊢ Eq (α := TangentBundle I M → TangentBundle I' M') (tangentMap I I' f) (tangentMapWithin I I' f univ)
have h : Eq (α := TangentBundle I M → TangentBundle I' M') (tangentMap I I' f) (tangentMap I I' f)
Tactic: rw [tangentMapWithin_univ]
-- 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'
f : M → M'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiff I I' n f
hmn : 1 ≤ n
⊢ Continuous[instTopologicalSpaceTangentBundle, instTopologicalSpaceTangentBundle] (tangentMap I I' f)
have hf₁ : ContMDiffOn I I' n f univ
Tactic: rw [← contMDiffOn_univ] at hf
Cleared hypotheses: hf, hmn
-- 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'
f : M → M'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f univ
hmn : 1 ≤ n
⊢ Continuous[instTopologicalSpaceTangentBundle, instTopologicalSpaceTangentBundle] (tangentMap I I' f)
have rw : ContinuousOn (X := TangentBundle I M) (Y := TangentBundle I' M') (tangentMap I I' f) univ
Tactic: rw [← continuousOn_univ]
-- 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'
f : M → M'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f univ
hmn : 1 ≤ n
⊢ ContinuousOn (X := TangentBundle I M) (Y := TangentBundle I' M') (tangentMap I I' f) univ
have h : Eq (α := TangentBundle I M → TangentBundle I' M') (tangentMap I I' f) (tangentMapWithin I I' f univ)
Tactic: convert! hf.continuousOn_tangentMapWithin hmn uniqueMDiffOn_univ
-- 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'
f : M → M'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f univ
hmn : 1 ≤ n
⊢ Eq (α := TangentBundle I M → TangentBundle I' M') (tangentMap I I' f) (tangentMapWithin I I' f univ)
have h : Eq (α := TangentBundle I M → TangentBundle I' M') (tangentMap I I' f) (tangentMap I I' f)
Tactic: rw [tangentMapWithin_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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
Is : IsManifold I 1 M
p : TangentBundle I M
⊢ Eq (α := TangentBundle I.tangent (TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)))
    (tangentMap I I.tangent (zeroSection E (TangentSpace I)) p)
    ⟨⟨p.proj (E := TangentSpace I), 0⟩, (p.snd (E := TangentSpace I), 0)⟩
have rcases : ∀ (x : M) (v : TangentSpace I x),
  Eq (α := TangentBundle I.tangent (TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)))
    (tangentMap I I.tangent (zeroSection E (TangentSpace I)) ⟨x, v⟩)
    ⟨⟨TotalSpace.proj (F := E) (E := TangentSpace I) ⟨x, v⟩, 0⟩, (TotalSpace.snd (E := TangentSpace I) ⟨x, v⟩, 0)⟩
Tactic: rcases p with ⟨x, v⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
have hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
Tactic: apply IsOpen.mem_nhds
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
hs :
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
have hx : (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
Tactic: apply IsOpen.mem_nhds
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (hypothesis)
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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
⊢ Eq (α := TangentBundle I.tangent (TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)))
    (tangentMap I I.tangent (zeroSection E (TangentSpace I)) ⟨x, v⟩)
    ⟨⟨TotalSpace.proj (F := E) (E := TangentSpace I) ⟨x, v⟩, 0⟩, (TotalSpace.snd (E := TangentSpace I) ⟨x, v⟩, 0)⟩
have N : (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
  𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
Tactic: have N : I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (I ((chartAt H x) x)) := by
    apply IsOpen.mem_nhds
    · apply (OpenPartialHomeomorph.open_target _).preimage I.continuous_invFun
    · simp only [mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (hypothesis)
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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ Eq (α := TangentBundle I.tangent (TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)))
    (tangentMap I I.tangent (zeroSection E (TangentSpace I)) ⟨x, v⟩)
    ⟨⟨TotalSpace.proj (F := E) (E := TangentSpace I) ⟨x, v⟩, 0⟩, (TotalSpace.snd (E := TangentSpace I) ⟨x, v⟩, 0)⟩
have A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
Tactic: have A : MDiffAt (fun x ↦ TotalSpace.mk' E (x : M) (0 : TangentSpace I x)) x :=
    haveI : CMDiff 1 (zeroSection E (TangentSpace I : M → Type _)) :=
      Bundle.contMDiff_zeroSection 𝕜 (TangentSpace I : M → Type _)
    this.mdifferentiableAt one_ne_zero
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
⊢ Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) (range (↑I : H → E))
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
have rw : Eq (α := E × E)
  ((ContinuousLinearMap.prod (fderiv 𝕜 (fun (x' : E) ↦ x') ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
          (fderiv 𝕜 (fun (x' : E) ↦ 0) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))) :
        (a : E) → E × E)
      v :
    E × E)
  ((v, 0) : TangentSpace I x × E)
Tactic: rw [fderivWithin_eq_fderiv, DifferentiableAt.fderiv_prodMk]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
rw :
  Eq (α := E × E)
    ((ContinuousLinearMap.prod (fderiv 𝕜 (fun (x' : E) ↦ x') ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
            (fderiv 𝕜 (fun (x' : E) ↦ 0) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
⊢ Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) (range (↑I : H → E))
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
have hf₁ : DifferentiableAt 𝕜 (F := E) (fun (x' : E) ↦ x') ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
Tactic: rw [fderivWithin_eq_fderiv, DifferentiableAt.fderiv_prodMk]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
rw :
  Eq (α := E × E)
    ((ContinuousLinearMap.prod (fderiv 𝕜 (fun (x' : E) ↦ x') ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
            (fderiv 𝕜 (fun (x' : E) ↦ 0) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
hf₁ : DifferentiableAt 𝕜 (F := E) (fun (x' : E) ↦ x') ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) (range (↑I : H → E))
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
have hf₂ : DifferentiableAt 𝕜 (F := E) (fun (x' : E) ↦ 0) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
Tactic: rw [fderivWithin_eq_fderiv, DifferentiableAt.fderiv_prodMk]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
rw :
  Eq (α := E × E)
    ((ContinuousLinearMap.prod (fderiv 𝕜 (fun (x' : E) ↦ x') ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
            (fderiv 𝕜 (fun (x' : E) ↦ 0) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
hf₁ : DifferentiableAt 𝕜 (F := E) (fun (x' : E) ↦ x') ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
hf₂ : DifferentiableAt 𝕜 (F := E) (fun (x' : E) ↦ 0) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) (range (↑I : H → E))
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
have hs : UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
Tactic: rw [fderivWithin_eq_fderiv, DifferentiableAt.fderiv_prodMk]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
rw :
  Eq (α := E × E)
    ((ContinuousLinearMap.prod (fderiv 𝕜 (fun (x' : E) ↦ x') ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
            (fderiv 𝕜 (fun (x' : E) ↦ 0) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
hf₁ : DifferentiableAt 𝕜 (F := E) (fun (x' : E) ↦ x') ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
hf₂ : DifferentiableAt 𝕜 (F := E) (fun (x' : E) ↦ 0) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
hs : UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) (range (↑I : H → E))
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
have h : DifferentiableAt 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
Tactic: rw [fderivWithin_eq_fderiv, DifferentiableAt.fderiv_prodMk]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (hypothesis)
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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
⊢ Eq (α := TangentBundle I.tangent (TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)))
    (tangentMap I I.tangent (zeroSection E (TangentSpace I)) ⟨x, v⟩)
    ⟨⟨TotalSpace.proj (F := E) (E := TangentSpace I) ⟨x, v⟩, 0⟩, (TotalSpace.snd (E := TangentSpace I) ⟨x, v⟩, 0)⟩
have B : Eq (α := E × E)
  (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) (range (↑I : H → E))
            ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
          E →L[𝕜] E × E) :
        (a : E) → E × E)
      v :
    E × E)
  ((v, 0) : TangentSpace I x × E)
Tactic: have B : fderivWithin 𝕜 (fun x' : E ↦ (x', (0 : E))) (Set.range I) (I ((chartAt H x) x)) v
      = (v, 0) := by
    rw [fderivWithin_eq_fderiv, DifferentiableAt.fderiv_prodMk]
    · simp
    · exact differentiableAt_fun_id
    · exact differentiableAt_const _
    · exact ModelWithCorners.uniqueDiffWithinAt_image I
    · exact differentiableAt_id.prodMk (differentiableAt_const _)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) (range (↑I : H → E))
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
⊢ Eq (α := TangentBundle I.tangent (TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)))
    (tangentMap I I.tangent (zeroSection E (TangentSpace I)) ⟨x, v⟩)
    ⟨⟨TotalSpace.proj (F := E) (E := TangentSpace I) ⟨x, v⟩, 0⟩, (TotalSpace.snd (E := TangentSpace I) ⟨x, v⟩, 0)⟩
have simp : Eq (α := TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
  ((fderivWithin 𝕜
          (fun (x_1 : E) ↦
            ((↑I : H → E)
                ((↑(ChartedSpace.chartAt x) : M → H)
                  ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) x_1))),
              0))
          (range (↑I : H → E)) ((↑I : H → E) ((↑(ChartedSpace.chartAt x) : M → H) x)) :
        (a : TangentSpace I x) → TangentSpace I.tangent ⟨x, 0⟩)
      v :
    TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
  ((v, 0) : E × E)
Tactic: simp +unfoldPartialApp only [Bundle.zeroSection, tangentMap, mfderiv, A,
    if_pos, chartAt, FiberBundle.chartedSpace_chartAt, TangentBundle.trivializationAt_apply,
    Function.comp_def, map_zero, mfld_simps]