awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
inst_11 : CompleteSpace E
inst_12 : IsManifold I 1 M
inst_13 : IsManifold I' 1 M'
hV :
  ContMDiffAt I' (I'.prod 𝓘(𝕜, E')) (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M') ↦ ⟨x, V x⟩) (f x₀)
hf : ContMDiffAt I I' n f x₀
hf' : IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderiv% f x₀)
hmn : m + 1 ≤ n
hV₁ :
  ContMDiffWithinAt I' (I'.prod 𝓘(𝕜, E')) (M' := Bundle.TotalSpace.{u_7, u_6, u_6} (B := M') E' (TangentSpace I')) m
    (fun (x : M') ↦ ⟨x, V x⟩) univ (f x₀)
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, mpullback I I' f V x⟩) x₀
have hf₁ : ContMDiffWithinAt I I' n f univ x₀
Tactic: simp only [← contMDiffWithinAt_univ] at hV hf hf' ⊢
Cleared hypotheses: hV, hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
m n : ℕ∞ω
inst_6 : CompleteSpace E
inst_7 : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, V x⟩) s x
hs : UniqueMDiffOn I s
hx : x ∈ s
hmn : m + 1 ≤ n
hm : m ≠ ∞
⊢ ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
      Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m
      (fun (x_1 : E) ↦ ⟨x_1, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_1⟩)
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) y)
have T : {x_1 : E |
    (fun (x' : E) ↦
        ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
          Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m
          (fun (x_2 : E) ↦ ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2⟩)
          ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) x')
      x_1} ∈
  𝓝[(extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x
Tactic: have T := nhdsWithin_mono _ (subset_insert _ _)
    ((contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin hm).1
      (contMDiffWithinAt_mpullbackWithin_extChartAt_symm hV hs hx hmn))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
m n : ℕ∞ω
inst_6 : CompleteSpace E
inst_7 : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, V x⟩) s x
hs : UniqueMDiffOn I s
hx : x ∈ s
hmn : m + 1 ≤ n
hm : m ≠ ∞
T :
  {x_1 : E |
      (fun (x' : E) ↦
          ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
            Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m
            (fun (x_2 : E) ↦
              ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2⟩)
            ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) x')
        x_1} ∈
    𝓝[(extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x
⊢ ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
      Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m
      (fun (x_1 : E) ↦ ⟨x_1, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_1⟩)
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) y)
have A : (↑(extChartAt I x) : M → E) ⁻¹'
    {x_1 : E |
      (fun (x' : E) ↦
          ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
            Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m
            (fun (x_2 : E) ↦
              ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2⟩)
            ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) x')
        x_1} ∈
  𝓝[(↑(extChartAt I x) : M → E) ⁻¹' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)] x
Tactic: have A := (continuousAt_extChartAt (I := I) x).continuousWithinAt.preimage_mem_nhdsWithin'' T rfl
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
m n : ℕ∞ω
inst_6 : CompleteSpace E
inst_7 : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, V x⟩) s x
hs : UniqueMDiffOn I s
hx : x ∈ s
hmn : m + 1 ≤ n
hm : m ≠ ∞
T :
  {x_1 : E |
      (fun (x' : E) ↦
          ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
            Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m
            (fun (x_2 : E) ↦
              ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2⟩)
            ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) x')
        x_1} ∈
    𝓝[(extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x
A :
  (↑(extChartAt I x) : M → E) ⁻¹'
      {x_1 : E |
        (fun (x' : E) ↦
            ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
              Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m
              (fun (x_2 : E) ↦
                ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2⟩)
              ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) x')
          x_1} ∈
    𝓝[(↑(extChartAt I x) : M → E) ⁻¹' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)] x
⊢ ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
      Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m
      (fun (x_1 : E) ↦ ⟨x_1, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_1⟩)
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) y)
have apply : (↑(extChartAt I x) : M → E) ⁻¹' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ∈ 𝓝[s] x
Tactic: apply (nhdsWithin_le_iff.2 _) A
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
m n : ℕ∞ω
inst_6 : CompleteSpace E
inst_7 : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, V x⟩) s x
hs : UniqueMDiffOn I s
hx : x ∈ s
hmn : m + 1 ≤ n
hm : m ≠ ∞
T :
  {x_1 : E |
      (fun (x' : E) ↦
          ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
            Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m
            (fun (x_2 : E) ↦
              ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2⟩)
            ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) x')
        x_1} ∈
    𝓝[(extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x
A :
  (↑(extChartAt I x) : M → E) ⁻¹'
      {x_1 : E |
        (fun (x' : E) ↦
            ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
              Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m
              (fun (x_2 : E) ↦
                ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2⟩)
              ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) x')
          x_1} ∈
    𝓝[(↑(extChartAt I x) : M → E) ⁻¹' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)] x
⊢ (↑(extChartAt I x) : M → E) ⁻¹' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ∈ 𝓝[s] x
have h : ∀ (y : M) (hy : y ∈ s) (h'y : y ∈ (extChartAt I x).source),
  y ∈ (↑(extChartAt I x) : M → E) ⁻¹' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)
Tactic: filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds (extChartAt_source_mem_nhds (I := I) x)]
    with y hy h'y
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
m n : ℕ∞ω
inst_6 : CompleteSpace E
inst_7 : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m
    (fun (x : M) ↦ ⟨x, V x⟩) s x
hs : UniqueMDiffOn I s
hx : x ∈ s
hmn : m + 1 ≤ n
hm : m ≠ ∞
T :
  {x_1 : E |
      (fun (x' : E) ↦
          ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
            Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m
            (fun (x_2 : E) ↦
              ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2⟩)
            ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) x')
        x_1} ∈
    𝓝[(extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x
A :
  (↑(extChartAt I x) : M → E) ⁻¹'
      {x_1 : E |
        (fun (x' : E) ↦
            ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
              Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m
              (fun (x_2 : E) ↦
                ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2⟩)
              ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) x')
          x_1} ∈
    𝓝[(↑(extChartAt I x) : M → E) ⁻¹' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)] x
y : M
hy : y ∈ s
h'y : y ∈ (extChartAt I x).source
⊢ y ∈ (↑(extChartAt I x) : M → E) ⁻¹' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)
have h'y₁ : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
Tactic: simp only [mfld_simps] at hy h'y
Cleared hypotheses: h'y
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
inst_6 : IsManifold I 1 M
V : (x : M) → TangentSpace I x
⊢ V =ᶠ[𝓝[s] x]
    mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
have a : {x_1 : M |
    (fun (x_2 : M) ↦
        V x_2 =
          mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))) x_2)
      x_1} ∈
  𝓝 x
Tactic: apply nhdsWithin_le_nhds
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
inst_6 : IsManifold I 1 M
V : (x : M) → TangentSpace I x
⊢ {x_1 : M |
      (fun (x_2 : M) ↦
          V x_2 =
            mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
              (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))) x_2)
        x_1} ∈
    𝓝 x
have h : ∀ (y : M) (hy : y ∈ (extChartAt I x).source),
  V y =
    mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))) y
Tactic: filter_upwards [extChartAt_source_mem_nhds (I := I) x] with y hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
inst_6 : IsManifold I 1 M
V : (x : M) → TangentSpace I x
y : M
hy : y ∈ (extChartAt I x).source
⊢ V y =
    mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))) y
have A : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y) = y
Tactic: have A : (extChartAt I x).symm (extChartAt I x y) = y := (extChartAt I x).left_inv hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
inst_6 : IsManifold I 1 M
V : (x : M) → TangentSpace I x
y : M
hy : y ∈ (extChartAt I x).source
A : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y) = y
⊢ V y =
    mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))) y
have h : V y = (inverse (ContinuousLinearMap.id 𝕜 (TangentSpace I y)) : (a : TangentSpace I y) → TangentSpace I y) (V y)
Tactic: rw [mpullback_apply, mpullbackWithin_apply,
    ← (isInvertible_mfderiv_extChartAt hy).inverse_comp_apply_of_right,
    mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt' hy, A]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (hypothesis)
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type uH
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
h_1 : y ∈ s
h :
  Eq (α := ι → E × ℝ) ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) x : ι → E × ℝ)
    ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) y : ι → E × ℝ)
⊢ x = y
have h₁ : ∀ (x_1 : ι),
  ((↑(f.toFun (s := s) x_1) : M → ℝ) x • (↑(extChartAt I (f.c (s := s) x_1)) : M → E) x,
      (↑(f.toFun (s := s) x_1) : M → ℝ) x) =
    ((↑(f.toFun (s := s) x_1) : M → ℝ) y • (↑(extChartAt I (f.c (s := s) x_1)) : M → E) y,
      (↑(f.toFun (s := s) x_1) : M → ℝ) y)
Tactic: simp only [embeddingPiTangent_coe, funext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (hypothesis)
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type uH
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
h_1 : y ∈ s
h :
  ∀ (x_1 : ι),
    ((↑(f.toFun (s := s) x_1) : M → ℝ) x • (↑(extChartAt I (f.c (s := s) x_1)) : M → E) x,
        (↑(f.toFun (s := s) x_1) : M → ℝ) x) =
      ((↑(f.toFun (s := s) x_1) : M → ℝ) y • (↑(extChartAt I (f.c (s := s) x_1)) : M → E) y,
        (↑(f.toFun (s := s) x_1) : M → ℝ) y)
⊢ x = y
have h₁ : (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) x •
    (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) x =
  (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) y •
    (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) y
Tactic: obtain ⟨h₁, h₂⟩ := Prod.mk_inj.1 (h (f.ind x hx))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (hypothesis)
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type uH
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
h_1 : y ∈ s
h :
  ∀ (x_1 : ι),
    ((↑(f.toFun (s := s) x_1) : M → ℝ) x • (↑(extChartAt I (f.c (s := s) x_1)) : M → E) x,
        (↑(f.toFun (s := s) x_1) : M → ℝ) x) =
      ((↑(f.toFun (s := s) x_1) : M → ℝ) y • (↑(extChartAt I (f.c (s := s) x_1)) : M → E) y,
        (↑(f.toFun (s := s) x_1) : M → ℝ) y)
h₁ :
  (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) x •
      (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) x =
    (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) y •
      (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) y
⊢ x = y
have h₂ : (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) x = (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) y
Tactic: obtain ⟨h₁, h₂⟩ := Prod.mk_inj.1 (h (f.ind x hx))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (hypothesis)
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type uH
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
h_1 : y ∈ s
h :
  ∀ (x_1 : ι),
    ((↑(f.toFun (s := s) x_1) : M → ℝ) x • (↑(extChartAt I (f.c (s := s) x_1)) : M → E) x,
        (↑(f.toFun (s := s) x_1) : M → ℝ) x) =
      ((↑(f.toFun (s := s) x_1) : M → ℝ) y • (↑(extChartAt I (f.c (s := s) x_1)) : M → E) y,
        (↑(f.toFun (s := s) x_1) : M → ℝ) y)
h₁ :
  (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) x •
      (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) x =
    (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) y •
      (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) y
h₂ : (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) x = (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) y
⊢ x = y
have h₃ : 1 = (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) y
Tactic: rw [f.apply_ind x hx] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (hypothesis)
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type uH
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
h_1 : y ∈ s
h :
  ∀ (x_1 : ι),
    ((↑(f.toFun (s := s) x_1) : M → ℝ) x • (↑(extChartAt I (f.c (s := s) x_1)) : M → E) x,
        (↑(f.toFun (s := s) x_1) : M → ℝ) x) =
      ((↑(f.toFun (s := s) x_1) : M → ℝ) y • (↑(extChartAt I (f.c (s := s) x_1)) : M → E) y,
        (↑(f.toFun (s := s) x_1) : M → ℝ) y)
h₁ :
  (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) x •
      (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) x =
    (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) y •
      (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) y
h₂ : 1 = (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) y
⊢ x = y
have h₃ : (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) x =
  (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) y
Tactic: rw [← h₂, f.apply_ind x hx, one_smul, one_smul] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (hypothesis)
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type uH
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
h_1 : y ∈ s
h :
  ∀ (x_1 : ι),
    ((↑(f.toFun (s := s) x_1) : M → ℝ) x • (↑(extChartAt I (f.c (s := s) x_1)) : M → E) x,
        (↑(f.toFun (s := s) x_1) : M → ℝ) x) =
      ((↑(f.toFun (s := s) x_1) : M → ℝ) y • (↑(extChartAt I (f.c (s := s) x_1)) : M → E) y,
        (↑(f.toFun (s := s) x_1) : M → ℝ) y)
h₁ :
  (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) x =
    (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) y
h₂ : 1 = (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) y
⊢ x = y
have this : y ∈ (extChartAt I (f.c (s := s) (f.ind (s := s) x hx))).source
Tactic: have := f.mem_extChartAt_source_of_eq_one h₂.symm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (hypothesis)
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type uH
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
L : ((i : ι) → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E × ℝ) (f.ind (s := s) x hx)
⊢ Eq (α := TangentSpace I x →L[ℝ] E)
    (L.comp (σ₁₂ := RingHom.id ℝ) (mfderiv% (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) x))
    (mfderiv% (↑(chartAt H (f.c (s := s) (f.ind (s := s) x hx))) : M → H) x)
have this : HasMFDerivAt I 𝓘(ℝ, E) (M' := E)
  (comp (β := (i : ι) → E × ℝ) (⇑L : (a : (i : ι) → E × ℝ) → E)
    (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ))
  x (L.comp (σ₁₂ := RingHom.id ℝ) (mfderiv% (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) x))
Tactic: have := L.hasMFDerivAt.comp x
    (f.embeddingPiTangent.contMDiff.mdifferentiableAt (by simp)).hasMFDerivAt