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
⊢ Injective (α := TangentSpace I x) (β :=
    TangentSpace (E := ι → E × ℝ) 𝓘(ℝ, ι → E × ℝ) (M := ι → E × ℝ)
      ((f.embeddingPiTangent (s := s) : (a : M) → ι → E × ℝ) x : ι → E × ℝ))
    (⇑(mfderiv% (⇑(f.embeddingPiTangent (s := s)) : (a : M) → ι → E × ℝ) x) :
      (a : TangentSpace I x) → TangentSpace 𝓘(ℝ, ι → E × ℝ) ((f.embeddingPiTangent : (a : M) → ι → E × ℝ) x))

Tactic:
LinearMap.ker_eq_bot.1 (f.embeddingPiTangent_ker_mfderiv x hx)

Premises used: LinearMap.ker_eq_bot, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, Iff.mp
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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
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))
⊢ ∃ (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 ι

Premises used: nonempty_fintype
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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))

Tactic:
⟨_, eEF ∘ f.embeddingPiTangent,
    eEF.toDiffeomorph.contMDiff.comp f.embeddingPiTangent.contMDiff,
    eEF.injective.comp f.embeddingPiTangent_injective, fun x => ?_⟩

Premises used: ContMDiff.comp, Function.comp, ContinuousLinearEquiv.injective, SmoothBumpCovering.embeddingPiTangent, ContMDiffMap.contMDiff, ContinuousLinearEquiv.toDiffeomorph, Function.Injective.comp, And.intro, SmoothBumpCovering.embeddingPiTangent_injective, Exists.intro, Diffeomorph.contMDiff, DFunLike.coe
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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) ⋯
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))
⊢ ∃ (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:
refine ⟨_, eEF ∘ f.embeddingPiTangent,
    eEF.toDiffeomorph.contMDiff.comp f.embeddingPiTangent.contMDiff,
    eEF.injective.comp f.embeddingPiTangent_injective, fun x => ?_⟩
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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
⊢ Ne (α := ℕ∞ω) ∞ 0

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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
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))
⊢ 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:
rw [mfderiv_comp _ eEF.differentiableAt.mdifferentiableAt
      (f.embeddingPiTangent.contMDiff.mdifferentiableAt (by simp)),
    eEF.mfderiv_eq]

Premises used: mfderiv_comp, ContinuousLinearEquiv.differentiableAt, SmoothBumpCovering.embeddingPiTangent, ContMDiffMap.contMDiff, ContinuousLinearEquiv.mfderiv_eq, DifferentiableAt.mdifferentiableAt, ContMDiff.mdifferentiableAt
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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.{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:
eEF.injective.comp (f.embeddingPiTangent_injective_mfderiv _ trivial)

Premises used: trivial, ContinuousLinearEquiv.injective, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, Function.Injective.comp, TangentSpace
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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.{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:
exact eEF.injective.comp (f.embeddingPiTangent_injective_mfderiv _ trivial)

Premises used: trivial, ContinuousLinearEquiv.injective, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, Function.Injective.comp
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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
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))
⊢ ∃ (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, -⟩

Premises used: isClosed_univ, SmoothBumpCovering.exists_isSubordinate, Filter.univ_mem
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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
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))
⊢ ∃ (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
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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 ι
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))
⊢ ∃ (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⟩

Premises used: SmoothBumpCovering.exists_immersion_euclidean
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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)
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:
⟨n, e, hsmooth, hsmooth.continuous.isClosedEmbedding hinj, hinj_mfderiv⟩

Premises used: ContMDiff.continuous, Continuous.isClosedEmbedding, And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.WhitneyEmbedding
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)
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:
exact ⟨n, e, hsmooth, hsmooth.continuous.isClosedEmbedding hinj, hinj_mfderiv⟩
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
P : Type u_3
n : ℕ
inst : NeZero n
poly : Polygon P n
h : poly.HasNondegenerateEdges
by_contra! : ∀ (hlt : n < 2), False
⊢ 2 ≤ n

Tactic:
by_contra! hlt
-- Module: Mathlib.Geometry.Polygon.Basic
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
1 : ∀ [NeZero (R := ℕ) 1] {poly : Polygon P 1} (h : poly.HasNondegenerateEdges) (hlt : LT.lt (α := ℕ) 1 2), False
⊢ False

Tactic:
interval_cases n
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
P : Type u_3
n : ℕ
inst : NeZero (R := ℕ) 0
poly : Polygon P 0
h : poly.HasNondegenerateEdges
hlt : LT.lt (α := ℕ) 0 2
⊢ False

Tactic:
simp_all only [neZero_zero_iff_false]

Premises used: neZero_zero_iff_false
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
P : Type u_3
n : ℕ
inst : NeZero (R := ℕ) 1
poly : Polygon P 1
h : poly.HasNondegenerateEdges
hlt : LT.lt (α := ℕ) 1 2
⊢ poly.vertices 0 = poly.vertices ((finRotate 1 : (a : Fin 1) → Fin 1) 0)

Tactic:
simp
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
P : Type u_3
n : ℕ
inst : NeZero (R := ℕ) 1
poly : Polygon P 1
h : poly.HasNondegenerateEdges
hlt : LT.lt (α := ℕ) 1 2
⊢ False

Tactic:
exact h 0 (by simp)

Premises used: OfNat.ofNat
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
n : ℕ
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AddTorsor V P
inst_4 : PartialOrder R
poly : Polygon P n
i : Fin n
⊢ edgeSet R poly i = image.{u_1, u_3} (α := R) (⇑(edgePath R poly i) : (a : R) → P) (Icc 0 1)

Tactic:
rfl

Premises used: affineSegment, Polygon.edgeSet, rfl
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
n : ℕ
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AddTorsor V P
inst_4 : NeZero n
inst_5 : Nontrivial R
poly : Polygon P n
h : HasNondegenerateVertices R poly
obtain :
  ∀ (m : ℕ) [inst_6 : NeZero m.succ] {poly : Polygon P m.succ} (h : HasNondegenerateVertices R poly),
    poly.HasNondegenerateEdges
⊢ poly.HasNondegenerateEdges

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne n)

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl, NeZero.ne
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AddTorsor V P
inst_4 : Nontrivial R
m : ℕ
inst_5 : NeZero m.succ
poly : Polygon P m.succ
h : HasNondegenerateVertices R poly
i : Fin m.succ
⊢ Ne (α := Fin 3) 0 1

Tactic:
decide
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AddTorsor V P
inst_4 : Nontrivial R
m : ℕ
inst_5 : NeZero m.succ
poly : Polygon P m.succ
h : HasNondegenerateVertices R poly
i : Fin m.succ
⊢ poly.vertices i ≠ poly.vertices ((finRotate m.succ : (a : Fin m.succ) → Fin m.succ) i)

Tactic:
simpa using (h i).injective.ne (by decide : (0 : Fin 3) ≠ 1)

Premises used: Function.Injective.ne, AffineIndependent.injective
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
n : ℕ
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AddTorsor V P
inst_4 : NeZero n
inst_5 : Nontrivial R
poly : Polygon P n
h : HasNondegenerateVertices R poly
⊢ 2 ≤ n

Tactic:
have := h.hasNondegenerateEdges.two_le
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
n : ℕ
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AddTorsor V P
inst_4 : NeZero n
inst_5 : Nontrivial R
poly : Polygon P n
h : HasNondegenerateVertices R poly
this : 2 ≤ n
by_contra! : ∀ (hlt : n < 3), False
⊢ 3 ≤ n

Tactic:
by_contra! hlt
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
n : ℕ
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AddTorsor V P
inst_4 : NeZero n
inst_5 : Nontrivial R
poly : Polygon P n
h : HasNondegenerateVertices R poly
this : 2 ≤ n
hlt : n < 3
2 :
  ∀ [inst_6 : NeZero (R := ℕ) 2] {poly : Polygon P 2} (h : HasNondegenerateVertices R poly) (this : LE.le (α := ℕ) 2 2)
    (hlt : LT.lt (α := ℕ) 2 3), False
⊢ False

Tactic:
interval_cases n
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
n : ℕ
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AddTorsor V P
inst_4 : Nontrivial R
inst_5 : NeZero (R := ℕ) 2
poly : Polygon P 2
h : HasNondegenerateVertices R poly
this : LE.le (α := ℕ) 2 2
hlt : LT.lt (α := ℕ) 2 3
⊢ Ne (α := Fin 3) 0 2

Tactic:
decide
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
n : ℕ
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AddTorsor V P
inst_4 : Nontrivial R
inst_5 : NeZero (R := ℕ) 2
poly : Polygon P 2
h : HasNondegenerateVertices R poly
this : LE.le (α := ℕ) 2 2
hlt : LT.lt (α := ℕ) 2 3
⊢ ![poly.vertices 0, poly.vertices (HAdd.hAdd (α := Fin 2) 0 1), poly.vertices (HAdd.hAdd (α := Fin 2) 0 2)] 0 =
    ![poly.vertices 0, poly.vertices (HAdd.hAdd (α := Fin 2) 0 1), poly.vertices (HAdd.hAdd (α := Fin 2) 0 2)] 2

Tactic:
simp
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
n : ℕ
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AddTorsor V P
inst_4 : Nontrivial R
inst_5 : NeZero (R := ℕ) 2
poly : Polygon P 2
h : HasNondegenerateVertices R poly
this : LE.le (α := ℕ) 2 2
hlt : LT.lt (α := ℕ) 2 3
⊢ False

Tactic:
exact (h 0).injective.ne (by decide : (0 : Fin 3) ≠ 2) (by simp)

Premises used: Function.Injective.ne, AffineIndependent.injective, OfNat.ofNat