awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact (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
-- 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 ι
f : SmoothBumpCovering ι I M
⊢ Injective (α := M) (β := ι → E × ℝ) (⇑(f.embeddingPiTangent (s := univ)) : (a : M) → ι → E × ℝ)

Tactic:
injOn_univ.1 f.embeddingPiTangent_injOn

Premises used: SmoothBumpCovering.embeddingPiTangent_injOn, Iff.mp, Set.injOn_univ
-- 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
set :
  let 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)
⊢ Eq (α := TangentSpace I x →L[ℝ] E)
    (ContinuousLinearMap.comp (M₂ := (i : ι) → E × ℝ)
        (ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E × ℝ) (f.ind (s := s) x hx) :
          ((i : ι) → E × ℝ) →L[ℝ] E)
        (mfderiv% (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) x :
          TangentSpace I x →L[ℝ]
            TangentSpace (E := ι → E × ℝ) 𝓘(ℝ, ι → E × ℝ) (M := ι → E × ℝ)
              ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) x : ι → E × ℝ)) :
      TangentSpace I x →L[ℝ] E)
    (mfderiv% (↑(chartAt H (f.c (s := s) (f.ind (s := s) x hx))) : M → H) x :
      TangentSpace I x →L[ℝ] TangentSpace I ((↑(chartAt H (f.c (s := s) (f.ind (s := s) x hx))) : M → H) x))

Tactic:
set L :=
    (ContinuousLinearMap.fst ℝ E ℝ).comp
      (@ContinuousLinearMap.proj ℝ _ ι (fun _ => E × ℝ) _ _ (fun _ => inferInstance) (f.ind x hx))

Premises used: ContinuousLinearMap.comp, Real, ContinuousLinearMap.proj, ContinuousLinearMap.fst, 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
L : ((i : ι) → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E × ℝ) (f.ind (s := s) x hx)
⊢ Ne (α := ℕ∞ω) ∞ 0

Tactic:
simp
-- 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
L : ((i : ι) → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E × ℝ) (f.ind (s := s) x hx)
⊢ 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
-- 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
L : ((i : ι) → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E × ℝ) (f.ind (s := s) x hx)
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))
⊢ Eq (α :=
    TangentSpace I x →L[ℝ]
      TangentSpace 𝓘(ℝ, 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))
    (mfderiv% (↑(chartAt H (f.c (s := s) (f.ind (s := s) x hx))) : M → H) x)

Tactic:
hasMFDerivAt_unique this _

Premises used: hasMFDerivAt_unique
-- 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
L : ((i : ι) → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E × ℝ) (f.ind (s := s) x hx)
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))
convert_2 :
  HasMFDerivAt I 𝓘(ℝ, E) (M' := E)
    (comp (β := (i : ι) → E × ℝ) (⇑L : (a : (i : ι) → E × ℝ) → E)
      (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ))
    x (mfderiv% (↑(chartAt H (f.c (s := s) (f.ind (s := s) x hx))) : M → H) x)
⊢ 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)

Tactic:
convert! hasMFDerivAt_unique this _

Premises used: hasMFDerivAt_unique
-- 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
L : ((i : ι) → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E × ℝ) (f.ind (s := s) x hx)
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))
⊢ HasMFDerivAt I 𝓘(ℝ, E) (M' := E)
    (comp (β := (i : ι) → E × ℝ) (⇑L : (a : (i : ι) → E × ℝ) → E)
      (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ))
    x (mfderiv% (↑(chartAt H (f.c (s := s) (f.ind (s := s) x hx))) : M → H) x)

Tactic:
(hasMFDerivAt_extChartAt (f.mem_chartAt_ind_source x hx)).congr_of_eventuallyEq ?_

Premises used: hasMFDerivAt_extChartAt, SmoothBumpCovering.mem_chartAt_ind_source, HasMFDerivAt.congr_of_eventuallyEq
-- 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
L : ((i : ι) → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E × ℝ) (f.ind (s := s) x hx)
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))
convert_2 :
  comp (β := (i : ι) → E × ℝ) (⇑L : (a : (i : ι) → E × ℝ) → E)
      (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) =ᶠ[𝓝 x]
    (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E)
⊢ HasMFDerivAt I 𝓘(ℝ, E) (M' := E)
    (comp (β := (i : ι) → E × ℝ) (⇑L : (a : (i : ι) → E × ℝ) → E)
      (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ))
    x (mfderiv% (↑(chartAt H (f.c (s := s) (f.ind (s := s) x hx))) : M → H) x)

Tactic:
refine (hasMFDerivAt_extChartAt (f.mem_chartAt_ind_source x hx)).congr_of_eventuallyEq ?_

Premises used: hasMFDerivAt_extChartAt, SmoothBumpCovering.mem_chartAt_ind_source, HasMFDerivAt.congr_of_eventuallyEq
-- 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
L : ((i : ι) → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E × ℝ) (f.ind (s := s) x hx)
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))
⊢ comp (β := (i : ι) → E × ℝ) (⇑L : (a : (i : ι) → E × ℝ) → E)
      (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) =ᶠ[𝓝 x]
    (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E)

Tactic:
(f.eventuallyEq_one x hx).mono fun y hy => ?_

Premises used: Filter.EventuallyEq, SmoothBumpCovering.eventuallyEq_one, Filter.Eventually.mono
-- 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
L : ((i : ι) → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E × ℝ) (f.ind (s := s) x hx)
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))
convert_2 :
  ∀ (y : M) (hy : (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) y = 1 y),
    comp (β := (i : ι) → E × ℝ) (⇑L : (a : (i : ι) → E × ℝ) → E)
        (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) y =
      (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) y
⊢ comp (β := (i : ι) → E × ℝ) (⇑L : (a : (i : ι) → E × ℝ) → E)
      (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) =ᶠ[𝓝 x]
    (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E)

Tactic:
refine (f.eventuallyEq_one x hx).mono fun y hy => ?_

Premises used: SmoothBumpCovering.eventuallyEq_one, Filter.Eventually.mono
-- 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
L : ((i : ι) → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E × ℝ) (f.ind (s := s) x hx)
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))
y : M
hy : (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) y = 1 y
convert_2 :
  (↑(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 =
    (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) y
⊢ comp (β := (i : ι) → E × ℝ) (⇑L : (a : (i : ι) → E × ℝ) → E) (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ)
      y =
    (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) y

Tactic:
simp only [L, embeddingPiTangent_coe, ContinuousLinearMap.coe_comp', (· ∘ ·),
    ContinuousLinearMap.coe_fst', ContinuousLinearMap.proj_apply]

Premises used: ContinuousLinearMap.coe_comp', ContinuousLinearMap.proj_apply, Function.comp, ContinuousLinearMap.coe_fst', 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
L : ((i : ι) → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E × ℝ) (f.ind (s := s) x hx)
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))
y : M
hy : (↑(f.toFun (s := s) (f.ind (s := s) x hx)) : M → ℝ) y = 1 y
convert_2 :
  HSMul.hSMul (α := ℝ) (1 y) ((↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) y) =
    (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) y
convert_2₁ :
  HSMul.hSMul (α := ℝ) 1 ((↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) y) =
    (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) y
convert_2₂ convert_2₃ :
  (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) 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 → ℝ) y •
      (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) y =
    (↑(extChartAt I (f.c (s := s) (f.ind (s := s) x hx))) : M → E) y

Tactic:
rw [hy, Pi.one_apply, one_smul]

Premises used: Pi.one_apply, one_smul
-- 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
h :
  LE.le (α := Submodule ℝ (TangentSpace I x))
    (LinearMap.ker (M₂ :=
      TangentSpace (E := ι → E × ℝ) 𝓘(ℝ, ι → E × ℝ) (M := ι → E × ℝ)
        ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) x : ι → E × ℝ))
      (↑(mfderiv% (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) x) :
        TangentSpace I x →ₗ[ℝ] TangentSpace 𝓘(ℝ, ι → E × ℝ) ((f.embeddingPiTangent : (a : M) → ι → E × ℝ) x)))
    ⊥
⊢ Eq (α := Submodule ℝ (TangentSpace I x))
    (LinearMap.ker (M₂ :=
      TangentSpace (E := ι → E × ℝ) 𝓘(ℝ, ι → E × ℝ) (M := ι → E × ℝ)
        ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) x : ι → E × ℝ))
      (↑(mfderiv% (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) x) :
        TangentSpace I x →ₗ[ℝ] TangentSpace 𝓘(ℝ, ι → E × ℝ) ((f.embeddingPiTangent : (a : M) → ι → E × ℝ) x)))
    ⊥

Tactic:
apply bot_unique

Premises used: bot_unique
-- 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
h :
  LE.le (α := Submodule ℝ (TangentSpace I x))
    (LinearMap.ker (M₂ :=
      TangentSpace (E := ι → E × ℝ) 𝓘(ℝ, ι → E × ℝ) (M := ι → E × ℝ)
        ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) x : ι → E × ℝ))
      (↑(mfderiv% (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) x) :
        TangentSpace I x →ₗ[ℝ] TangentSpace 𝓘(ℝ, ι → E × ℝ) ((f.embeddingPiTangent : (a : M) → ι → E × ℝ) x)))
    (LinearMap.ker
      (↑(ContinuousLinearMap.comp (M₂ := (i : ι) → E × ℝ)
            (ContinuousLinearMap.fst ℝ E ℝ ∘SL
                ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E × ℝ) (f.ind (s := s) x hx) :
              ((i : ι) → E × ℝ) →L[ℝ] E)
            (mfderiv% (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) x :
              TangentSpace I x →L[ℝ]
                TangentSpace (E := ι → E × ℝ) 𝓘(ℝ, ι → E × ℝ) (M := ι → E × ℝ)
                  ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) x : ι → E × ℝ))) :
        TangentSpace I x →ₗ[ℝ] TangentSpace I ((↑(chartAt H (f.c (f.ind x hx))) : M → H) x)))
⊢ LE.le (α := Submodule ℝ (TangentSpace I x))
    (LinearMap.ker (M₂ :=
      TangentSpace (E := ι → E × ℝ) 𝓘(ℝ, ι → E × ℝ) (M := ι → E × ℝ)
        ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) x : ι → E × ℝ))
      (↑(mfderiv% (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) x) :
        TangentSpace I x →ₗ[ℝ] TangentSpace 𝓘(ℝ, ι → E × ℝ) ((f.embeddingPiTangent : (a : M) → ι → E × ℝ) x)))
    ⊥

Tactic:
rw [← (mdifferentiable_chart (f.c (f.ind x hx))).ker_mfderiv_eq_bot
      (f.mem_chartAt_ind_source x hx),
    ← comp_embeddingPiTangent_mfderiv]

Premises used: mdifferentiable_chart, SmoothBumpCovering.c, SmoothBumpCovering.mem_chartAt_ind_source, SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, OpenPartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot, 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
⊢ LE.le (α := Submodule ℝ (TangentSpace I x))
    (LinearMap.ker (M₂ :=
      TangentSpace (E := ι → E × ℝ) 𝓘(ℝ, ι → E × ℝ) (M := ι → E × ℝ)
        ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) x : ι → E × ℝ))
      (↑(mfderiv% (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) x) :
        TangentSpace I x →ₗ[ℝ] TangentSpace 𝓘(ℝ, ι → E × ℝ) ((f.embeddingPiTangent : (a : M) → ι → E × ℝ) x)))
    (LinearMap.ker
      (↑(ContinuousLinearMap.comp (M₂ := (i : ι) → E × ℝ)
            (ContinuousLinearMap.fst ℝ E ℝ ∘SL
                ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E × ℝ) (f.ind (s := s) x hx) :
              ((i : ι) → E × ℝ) →L[ℝ] E)
            (mfderiv% (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) x :
              TangentSpace I x →L[ℝ]
                TangentSpace (E := ι → E × ℝ) 𝓘(ℝ, ι → E × ℝ) (M := ι → E × ℝ)
                  ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) x : ι → E × ℝ))) :
        TangentSpace I x →ₗ[ℝ] TangentSpace I ((↑(chartAt H (f.c (f.ind x hx))) : M → H) x)))

Tactic:
LinearMap.ker_le_ker_comp _ _

Premises used: Set.Mem, LinearMap.ker_le_ker_comp
-- 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
⊢ LE.le (α := Submodule ℝ (TangentSpace I x))
    (LinearMap.ker (M₂ :=
      TangentSpace (E := ι → E × ℝ) 𝓘(ℝ, ι → E × ℝ) (M := ι → E × ℝ)
        ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) x : ι → E × ℝ))
      (↑(mfderiv% (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) x) :
        TangentSpace I x →ₗ[ℝ] TangentSpace 𝓘(ℝ, ι → E × ℝ) ((f.embeddingPiTangent : (a : M) → ι → E × ℝ) x)))
    (LinearMap.ker
      (↑(ContinuousLinearMap.comp (M₂ := (i : ι) → E × ℝ)
            (ContinuousLinearMap.fst ℝ E ℝ ∘SL
                ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E × ℝ) (f.ind (s := s) x hx) :
              ((i : ι) → E × ℝ) →L[ℝ] E)
            (mfderiv% (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) x :
              TangentSpace I x →L[ℝ]
                TangentSpace (E := ι → E × ℝ) 𝓘(ℝ, ι → E × ℝ) (M := ι → E × ℝ)
                  ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) x : ι → E × ℝ))) :
        TangentSpace I x →ₗ[ℝ] TangentSpace I ((↑(chartAt H (f.c (f.ind x hx))) : M → H) x)))

Tactic:
exact LinearMap.ker_le_ker_comp _ _

Premises used: LinearMap.ker_le_ker_comp