awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (goal)
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[ℝ] 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 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)
Tactic: convert! hasMFDerivAt_unique this _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (goal)
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)
have 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)
Tactic: refine (hasMFDerivAt_extChartAt (f.mem_chartAt_ind_source x hx)).congr_of_eventuallyEq ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (goal)
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)
have 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
Tactic: refine (f.eventuallyEq_one x hx).mono fun y hy => ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (goal)
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
⊢ 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
have 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
Tactic: simp only [L, embeddingPiTangent_coe, ContinuousLinearMap.coe_comp', (· ∘ ·),
    ContinuousLinearMap.coe_fst', ContinuousLinearMap.proj_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (goal)
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
⊢ (↑(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
have 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
Tactic: rw [hy, Pi.one_apply, one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (goal)
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
⊢ (↑(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
have 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
Tactic: rw [hy, Pi.one_apply, one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (goal)
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
⊢ (↑(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
have 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
Tactic: rw [hy, Pi.one_apply, one_smul]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (goal)
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
⊢ 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)))
    ⊥
have 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)))
  ⊥
Tactic: apply bot_unique
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (goal)
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)))
    ⊥
have 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)))
Tactic: rw [← (mdifferentiable_chart (f.c (f.ind x hx))).ker_mfderiv_eq_bot
      (f.mem_chartAt_ind_source x hx),
    ← comp_embeddingPiTangent_mfderiv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (goal)
Goal:
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
ι : Type u_1
inst_8 : Finite ι
f : SmoothBumpCovering ι I M
⊢ ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)),
    ContMDiff I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) ∞ e ∧
      Injective e ∧
        ∀ (x : M),
          Injective (α := TangentSpace I x) (β := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) (e x))
            (⇑(mfderiv% e x) : (a : TangentSpace I x) → TangentSpace (𝓡 n) (e x))
have intro : ∀ (val : Fintype ι),
  ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)),
    ContMDiff I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) ∞ e ∧
      Injective e ∧
        ∀ (x : M),
          Injective (α := TangentSpace I x) (β := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) (e x))
            (⇑(mfderiv% e x) : (a : TangentSpace I x) → TangentSpace (𝓡 n) (e x))
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (goal)
Goal:
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
ι : Type u_1
inst_8 : Finite ι
f : SmoothBumpCovering ι I M
val : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
this_1 : IsNoetherian.{0, uE} ℝ (E × ℝ) := ⋯
this : FiniteDimensional ℝ (ι → E × ℝ) := ⋯
eEF : (ι → E × ℝ) ≃L[ℝ] F := ContinuousLinearEquiv.ofFinrankEq (𝕜 := ℝ) (E := ι → E × ℝ) (F := F) ⋯
⊢ ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)),
    ContMDiff I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) ∞ e ∧
      Injective e ∧
        ∀ (x : M),
          Injective (α := TangentSpace I x) (β := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) (e x))
            (⇑(mfderiv% e x) : (a : TangentSpace I x) → TangentSpace (𝓡 n) (e x))
have intro : ∀ (x : M),
  Injective (α := TangentSpace I x) (β :=
    TangentSpace (E := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))) (𝓡 finrank ℝ (ι → E × ℝ)) (M :=
      EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ))))
      (comp (β := ι → E × ℝ) (⇑eEF : (a : ι → E × ℝ) → F) (⇑(f.embeddingPiTangent (s := univ)) : (a : M) → ι → E × ℝ)
        x))
    (⇑(mfderiv%
            (comp (β := ι → E × ℝ) (⇑eEF : (a : ι → E × ℝ) → F)
              (⇑(f.embeddingPiTangent (s := univ)) : (a : M) → ι → E × ℝ))
          x) :
      (a : TangentSpace I x) →
        TangentSpace (𝓡 finrank ℝ (ι → E × ℝ))
          (((⇑eEF : (a : ι → E × ℝ) → F) ∘ (⇑f.embeddingPiTangent : (a : M) → ι → E × ℝ)) x))
Tactic: refine ⟨_, eEF ∘ f.embeddingPiTangent,
    eEF.toDiffeomorph.contMDiff.comp f.embeddingPiTangent.contMDiff,
    eEF.injective.comp f.embeddingPiTangent_injective, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (goal)
Goal:
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
ι : Type u_1
inst_8 : Finite ι
f : SmoothBumpCovering ι I M
val : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
this_1 : IsNoetherian.{0, uE} ℝ (E × ℝ) := ⋯
this : FiniteDimensional ℝ (ι → E × ℝ) := ⋯
eEF : (ι → E × ℝ) ≃L[ℝ] F := ContinuousLinearEquiv.ofFinrankEq (𝕜 := ℝ) (E := ι → E × ℝ) (F := F) ⋯
x : M
⊢ Injective (α := TangentSpace I x) (β :=
    TangentSpace (E := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))) (𝓡 finrank ℝ (ι → E × ℝ)) (M :=
      EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ))))
      (comp (β := ι → E × ℝ) (⇑eEF : (a : ι → E × ℝ) → F) (⇑(f.embeddingPiTangent (s := univ)) : (a : M) → ι → E × ℝ)
        x))
    (⇑(mfderiv%
            (comp (β := ι → E × ℝ) (⇑eEF : (a : ι → E × ℝ) → F)
              (⇑(f.embeddingPiTangent (s := univ)) : (a : M) → ι → E × ℝ))
          x) :
      (a : TangentSpace I x) →
        TangentSpace (𝓡 finrank ℝ (ι → E × ℝ))
          (((⇑eEF : (a : ι → E × ℝ) → F) ∘ (⇑f.embeddingPiTangent : (a : M) → ι → E × ℝ)) x))
have intro : Injective.{uE + 1, 1} (α := TangentSpace I x) (β :=
  TangentSpace (E := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))) (𝓡 finrank ℝ (ι → E × ℝ)) (M :=
    EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ))))
    (comp (β := ι → E × ℝ) (⇑eEF : (a : ι → E × ℝ) → F) (⇑(f.embeddingPiTangent (s := univ)) : (a : M) → ι → E × ℝ) x))
  (⇑((↑eEF : (ι → E × ℝ) →L[ℝ] F).comp (σ₁₂ := RingHom.id ℝ)
        (mfderiv% (⇑(f.embeddingPiTangent (s := univ)) : (a : M) → ι → E × ℝ) x)) :
    (a : TangentSpace I x) →
      TangentSpace (𝓡 finrank ℝ (ι → E × ℝ))
        (((⇑eEF : (a : ι → E × ℝ) → F) ∘ (⇑f.embeddingPiTangent : (a : M) → ι → E × ℝ)) x))
Tactic: rw [mfderiv_comp _ eEF.differentiableAt.mdifferentiableAt
      (f.embeddingPiTangent.contMDiff.mdifferentiableAt (by simp)),
    eEF.mfderiv_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (goal)
Goal:
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 : CompactSpace M
⊢ ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)),
    ContMDiff I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) ∞ e ∧
      IsClosedEmbedding e ∧
        ∀ (x : M),
          Injective (α := TangentSpace I x) (β := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) (e x))
            (⇑(mfderiv% e x) : (a : TangentSpace I x) → TangentSpace (𝓡 n) (e x))
have rcases : ∀ (ι : Type uM) (f : SmoothBumpCovering ι I M),
  ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)),
    ContMDiff I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) ∞ e ∧
      IsClosedEmbedding e ∧
        ∀ (x : M),
          Injective (α := TangentSpace I x) (β := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) (e x))
            (⇑(mfderiv% e x) : (a : TangentSpace I x) → TangentSpace (𝓡 n) (e x))
Tactic: rcases SmoothBumpCovering.exists_isSubordinate I isClosed_univ fun (x : M) _ => univ_mem with
    ⟨ι, f, -⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (goal)
Goal:
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 : CompactSpace M
ι : Type uM
f : SmoothBumpCovering ι I M
⊢ ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)),
    ContMDiff I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) ∞ e ∧
      IsClosedEmbedding e ∧
        ∀ (x : M),
          Injective (α := TangentSpace I x) (β := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) (e x))
            (⇑(mfderiv% e x) : (a : TangentSpace I x) → TangentSpace (𝓡 n) (e x))
have haveI : ∀ (this : Fintype ι),
  ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)),
    ContMDiff I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) ∞ e ∧
      IsClosedEmbedding e ∧
        ∀ (x : M),
          Injective (α := TangentSpace I x) (β := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) (e x))
            (⇑(mfderiv% e x) : (a : TangentSpace I x) → TangentSpace (𝓡 n) (e x))
Tactic: haveI := f.fintype
-- Lean 4 proof step from Mathlib.Geometry.Manifold.WhitneyEmbedding (goal)
Goal:
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 : CompactSpace M
ι : Type uM
f : SmoothBumpCovering ι I M
this : Fintype ι
⊢ ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)),
    ContMDiff I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) ∞ e ∧
      IsClosedEmbedding e ∧
        ∀ (x : M),
          Injective (α := TangentSpace I x) (β := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) (e x))
            (⇑(mfderiv% e x) : (a : TangentSpace I x) → TangentSpace (𝓡 n) (e x))
have rcases : ∀ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)) (hsmooth : ContMDiff I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) ∞ e)
  (hinj : Injective e)
  (hinj_mfderiv :
    ∀ (x : M),
      Injective (α := TangentSpace I x) (β := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) (e x))
        (⇑(mfderiv% e x) : (a : TangentSpace I x) → TangentSpace (𝓡 n) (e x))),
  ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)),
    ContMDiff I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) ∞ e ∧
      IsClosedEmbedding e ∧
        ∀ (x : M),
          Injective (α := TangentSpace I x) (β := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) (e x))
            (⇑(mfderiv% e x) : (a : TangentSpace I x) → TangentSpace (𝓡 n) (e x))
Tactic: rcases f.exists_immersion_euclidean with ⟨n, e, hsmooth, hinj, hinj_mfderiv⟩
-- Lean 4 proof step from Mathlib.Geometry.Polygon.Basic (goal)
Goal:
P : Type u_3
n : ℕ
inst : NeZero n
poly : Polygon P n
h : poly.HasNondegenerateEdges
⊢ 2 ≤ n
have by_contra! : ∀ (hlt : n < 2), False
Tactic: by_contra! hlt
-- Lean 4 proof step from Mathlib.Geometry.Polygon.Basic (goal)
Goal:
P : Type u_3
n : ℕ
inst : NeZero n
poly : Polygon P n
h : poly.HasNondegenerateEdges
hlt : n < 2
⊢ False
have 0 : ∀ [NeZero (R := ℕ) 0] {poly : Polygon P 0} (h : poly.HasNondegenerateEdges) (hlt : LT.lt (α := ℕ) 0 2), False
Tactic: interval_cases n
Cleared hypotheses: inst, poly, h, hlt
-- Lean 4 proof step from Mathlib.Geometry.Polygon.Basic (goal)
Goal:
P : Type u_3
n : ℕ
inst : NeZero n
poly : Polygon P n
h : poly.HasNondegenerateEdges
hlt : n < 2
0 : ∀ [NeZero (R := ℕ) 0] {poly : Polygon P 0} (h : poly.HasNondegenerateEdges) (hlt : LT.lt (α := ℕ) 0 2), False
⊢ False
have 1 : ∀ [NeZero (R := ℕ) 1] {poly : Polygon P 1} (h : poly.HasNondegenerateEdges) (hlt : LT.lt (α := ℕ) 1 2), False
Tactic: interval_cases n
Cleared hypotheses: inst, poly, h, hlt