awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
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
apply : (↑(extChartAt I x) : M → E) ⁻¹' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ∈ 𝓝[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)

Tactic:
apply (nhdsWithin_le_iff.2 _) A

Premises used: Iff.mpr, nhdsWithin_le_iff
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
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
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)
⊢ (↑(extChartAt I x) : M → E) ⁻¹' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ∈ 𝓝[s] x

Tactic:
filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds (extChartAt_source_mem_nhds (I := I) x)]
    with y hy h'y

Premises used: extChartAt_source_mem_nhds, nhdsWithin_le_nhds, self_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
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 ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
simp only [mfld_simps] at hy h'y
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
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 ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ y ∈ (↑(extChartAt I x) : M → E) ⁻¹' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)

Tactic:
simp [hy, h'y]
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
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
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
⊢ 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)))

Tactic:
apply nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
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
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
⊢ {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:
filter_upwards [extChartAt_source_mem_nhds (I := I) x] with y hy

Premises used: extChartAt_source_mem_nhds
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
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
⊢ (↑(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
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
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
h : V y = (inverse (ContinuousLinearMap.id 𝕜 (TangentSpace I y)) : (a : TangentSpace I y) → TangentSpace I y) (V 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

Tactic:
rw [mpullback_apply, mpullbackWithin_apply,
    ← (isInvertible_mfderiv_extChartAt hy).inverse_comp_apply_of_right,
    mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt' hy, A]

Premises used: VectorField.mpullback_apply, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt', ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_right, VectorField.mpullbackWithin_apply, isInvertible_mfderiv_extChartAt
-- Module: Mathlib.Geometry.Manifold.VectorField.Pullback
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 = (inverse (ContinuousLinearMap.id 𝕜 (TangentSpace I y)) : (a : TangentSpace I y) → TangentSpace I y) (V y)

Tactic:
simp only [ContinuousLinearMap.inverse_id, ContinuousLinearMap.coe_id', id_eq]

Premises used: ContinuousLinearMap.coe_id', ContinuousLinearMap.inverse_id, id_eq
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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
⊢ Eq (α := (a : M) → ι → E × ℝ) (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) fun (x : M) (i : ι) ↦
    ((↑(f.toFun (s := s) i) : M → ℝ) x • (↑(extChartAt I (f.c (s := s) i)) : M → E) x,
      (↑(f.toFun (s := s) i) : M → ℝ) x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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
_ :
  y ∈ s →
    Eq (α := ι → E × ℝ) ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) x : ι → E × ℝ)
        ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) y : ι → E × ℝ) →
      x = y
⊢ y ∈ s →
    Eq (α := ι → E × ℝ) ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) x : ι → E × ℝ)
        ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) y : ι → E × ℝ) →
      x = y

Tactic:
_
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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_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

Premises used: funext_iff, SmoothBumpCovering.embeddingPiTangent_coe
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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)
⊢ (↑(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))

Premises used: Prod.mk_inj, Iff.mp, SmoothBumpCovering.ind
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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
⊢ (↑(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))

Premises used: Prod.mk_inj, Iff.mp, SmoothBumpCovering.ind
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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
⊢ 1 = (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) y

Tactic:
rw [f.apply_ind x hx] at h₂

Premises used: SmoothBumpCovering.apply_ind
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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
⊢ (↑(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₁

Premises used: one_smul, SmoothBumpCovering.apply_ind
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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
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
⊢ 1 = (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) y

Tactic:
rw [← h₂, f.apply_ind x hx, one_smul, one_smul] at h₁

Premises used: one_smul, SmoothBumpCovering.apply_ind
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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
⊢ 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
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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
this : y ∈ (extChartAt I (f.c (s := s) (f.ind (s := s) x hx))).source
⊢ x = y

Tactic:
(extChartAt I (f.c _)).injOn (f.mem_extChartAt_ind_source x hx) this h₁

Premises used: extChartAt, SmoothBumpCovering.c, PartialEquiv.injOn, SmoothBumpCovering.mem_extChartAt_ind_source