awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
hfi :
  ¬ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
⊢ Eq (α := E)
    ((ContinuousLinearMap.inverse
            (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (range (↑I : H → E))
              ((↑(extChartAt I x₀) : M → E) x₀)) :
          (a : TangentSpace I ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀))) →
            TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x₀) : M → E) x₀))
        (((ContinuousLinearMap.inverse
                (mfderivWithin I I' f s ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀))) :
              ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜)
                (TangentSpace I' (f ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀))))
                (TangentSpace I ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)))) :
            (a : TangentSpace I' (f ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)))) →
              TangentSpace I ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)))
          (W (f ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀))))) :
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x₀) : M → E) x₀))
    (0 : E)
have neg : Eq (α := E)
  (((ContinuousLinearMap.inverse
            (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (range (↑I : H → E))
              ((↑(extChartAt I x₀) : M → E) x₀)) :
          TangentSpace I x₀ →L[𝕜] TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x₀) : M → E) x₀)) :
        (a : TangentSpace I x₀) → TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x₀) : M → E) x₀))
      (((0 : ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x₀)) (TangentSpace I x₀)) :
          (a : TangentSpace I' (f x₀)) → TangentSpace I x₀)
        (W (f x₀))) :
    TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x₀) : M → E) x₀))
  (0 : E)
Tactic: rw [A, ContinuousLinearMap.inverse_of_not_isInvertible hfi]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
hfi :
  ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
⊢ CompleteSpace E'
have rcases : ∀ (M : ContinuousLinearEquiv.{u_1, u_1, u_3, u_6} (RingHom.id 𝕜) (TangentSpace I x₀) (TangentSpace I' (f x₀))),
  CompleteSpace E'
Tactic: rcases hfi with ⟨M, -⟩
Cleared hypotheses: hfi
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
hfi :
  ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
⊢ Eq (α := TangentSpace I x₀) (mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀)
    (mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀)
have this : CompleteSpace E'
Tactic: have : CompleteSpace E' := by
    rcases hfi with ⟨M, -⟩
    let M' : E ≃L[𝕜] E' := M
    exact (completeSpace_congr (e := M'.toEquiv) M'.isUniformEmbedding).1 (by assumption)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
hfi :
  ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
this : CompleteSpace E'
⊢ ∃ (u : Set M),
    IsOpen[inst_4] u ∧
      x₀ ∈ u ∧ s ∩ u ⊆ f ⁻¹' t ∧ s ∩ u ⊆ f ⁻¹' (extChartAt I' (f x₀)).source ∧ ContMDiffOn I I' 2 f (s ∩ u)
have obtain : ∀ (u : Set M) (u_open : IsOpen[inst_4] u) (x₀u : x₀ ∈ u) (hu : ContMDiffOn I I' 2 f (insert x₀ s ∩ u)),
  ∃ (u : Set M),
    IsOpen[inst_4] u ∧
      x₀ ∈ u ∧ s ∩ u ⊆ f ⁻¹' t ∧ s ∩ u ⊆ f ⁻¹' (extChartAt I' (f x₀)).source ∧ ContMDiffOn I I' 2 f (s ∩ u)
Tactic: obtain ⟨u, u_open, x₀u, hu⟩ : ∃ u, IsOpen u ∧ x₀ ∈ u ∧ CMDiff[insert x₀ s ∩ u] 2 f :=
      hf.contMDiffOn' le_rfl (by simp)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu_1 : UniqueMDiffOn I s
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
hfi :
  ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
this : CompleteSpace E'
u : Set M
u_open : IsOpen[inst_4] u
x₀u : x₀ ∈ u
hu : ContMDiffOn I I' 2 f (insert x₀ s ∩ u)
⊢ ∃ (u : Set M),
    IsOpen[inst_4] u ∧
      x₀ ∈ u ∧ s ∩ u ⊆ f ⁻¹' t ∧ s ∩ u ⊆ f ⁻¹' (extChartAt I' (f x₀)).source ∧ ContMDiffOn I I' 2 f (s ∩ u)
have this₁ : f ⁻¹' (extChartAt I' (f x₀)).source ∈ 𝓝[s] x₀
Tactic: have : f ⁻¹' (extChartAt I' (f x₀)).source ∈ 𝓝[s] x₀ :=
      hf.continuousWithinAt.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds (f x₀))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu_1 : UniqueMDiffOn I s
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
hfi :
  ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
this_1 : CompleteSpace E'
u : Set M
u_open : IsOpen[inst_4] u
x₀u : x₀ ∈ u
hu : ContMDiffOn I I' 2 f (insert x₀ s ∩ u)
this : f ⁻¹' (extChartAt I' (f x₀)).source ∈ 𝓝[s] x₀
⊢ ∃ (u : Set M),
    IsOpen[inst_4] u ∧
      x₀ ∈ u ∧ s ∩ u ⊆ f ⁻¹' t ∧ s ∩ u ⊆ f ⁻¹' (extChartAt I' (f x₀)).source ∧ ContMDiffOn I I' 2 f (s ∩ u)
have rcases : ∀ (w : Set M) (w_open : IsOpen[inst_4] w) (x₀w : x₀ ∈ w) (hw : w ∩ s ⊆ f ⁻¹' t ∩ f ⁻¹' (extChartAt I' (f x₀)).source),
  ∃ (u : Set M),
    IsOpen[inst_4] u ∧
      x₀ ∈ u ∧ s ∩ u ⊆ f ⁻¹' t ∧ s ∩ u ⊆ f ⁻¹' (extChartAt I' (f x₀)).source ∧ ContMDiffOn I I' 2 f (s ∩ u)
Tactic: rcases mem_nhdsWithin.1 (Filter.inter_mem hst this) with ⟨w, w_open, x₀w, hw⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu_1 : UniqueMDiffOn I s
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
hfi :
  ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
this_1 : CompleteSpace E'
u : Set M
u_open : IsOpen[inst_4] u
x₀u : x₀ ∈ u
hu : ContMDiffOn I I' 2 f (insert x₀ s ∩ u)
this : f ⁻¹' (extChartAt I' (f x₀)).source ∈ 𝓝[s] x₀
w : Set M
w_open : IsOpen[inst_4] w
x₀w : x₀ ∈ w
hw : w ∩ s ⊆ f ⁻¹' t ∩ f ⁻¹' (extChartAt I' (f x₀)).source
⊢ ∃ (u : Set M),
    IsOpen[inst_4] u ∧
      x₀ ∈ u ∧ s ∩ u ⊆ f ⁻¹' t ∧ s ∩ u ⊆ f ⁻¹' (extChartAt I' (f x₀)).source ∧ ContMDiffOn I I' 2 f (s ∩ u)
have refine_1 : s ∩ (u ∩ w) ⊆ f ⁻¹' t
Tactic: refine ⟨u ∩ w, u_open.inter w_open, by simp [x₀u, x₀w], ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu_1 : UniqueMDiffOn I s
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
hfi :
  ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
this_1 : CompleteSpace E'
u : Set M
u_open : IsOpen[inst_4] u
x₀u : x₀ ∈ u
hu : ContMDiffOn I I' 2 f (insert x₀ s ∩ u)
this : f ⁻¹' (extChartAt I' (f x₀)).source ∈ 𝓝[s] x₀
w : Set M
w_open : IsOpen[inst_4] w
x₀w : x₀ ∈ w
hw : w ∩ s ⊆ f ⁻¹' t ∩ f ⁻¹' (extChartAt I' (f x₀)).source
refine_1 : s ∩ (u ∩ w) ⊆ f ⁻¹' t
⊢ ∃ (u : Set M),
    IsOpen[inst_4] u ∧
      x₀ ∈ u ∧ s ∩ u ⊆ f ⁻¹' t ∧ s ∩ u ⊆ f ⁻¹' (extChartAt I' (f x₀)).source ∧ ContMDiffOn I I' 2 f (s ∩ u)
have refine_2 : s ∩ (u ∩ w) ⊆ f ⁻¹' (extChartAt I' (f x₀)).source
Tactic: refine ⟨u ∩ w, u_open.inter w_open, by simp [x₀u, x₀w], ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu_1 : UniqueMDiffOn I s
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
hfi :
  ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
this_1 : CompleteSpace E'
u : Set M
u_open : IsOpen[inst_4] u
x₀u : x₀ ∈ u
hu : ContMDiffOn I I' 2 f (insert x₀ s ∩ u)
this : f ⁻¹' (extChartAt I' (f x₀)).source ∈ 𝓝[s] x₀
w : Set M
w_open : IsOpen[inst_4] w
x₀w : x₀ ∈ w
hw : w ∩ s ⊆ f ⁻¹' t ∩ f ⁻¹' (extChartAt I' (f x₀)).source
refine_1 : s ∩ (u ∩ w) ⊆ f ⁻¹' t
refine_2 : s ∩ (u ∩ w) ⊆ f ⁻¹' (extChartAt I' (f x₀)).source
⊢ ∃ (u : Set M),
    IsOpen[inst_4] u ∧
      x₀ ∈ u ∧ s ∩ u ⊆ f ⁻¹' t ∧ s ∩ u ⊆ f ⁻¹' (extChartAt I' (f x₀)).source ∧ ContMDiffOn I I' 2 f (s ∩ u)
have refine_3 : ContMDiffOn I I' 2 f (s ∩ (u ∩ w))
Tactic: refine ⟨u ∩ w, u_open.inter w_open, by simp [x₀u, x₀w], ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu_1 : UniqueMDiffOn I s
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
hfi :
  ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
this_1 : CompleteSpace E'
u : Set M
u_open : IsOpen[inst_4] u
x₀u : x₀ ∈ u
hu : ContMDiffOn I I' 2 f (insert x₀ s ∩ u)
this : f ⁻¹' (extChartAt I' (f x₀)).source ∈ 𝓝[s] x₀
w : Set M
w_open : IsOpen[inst_4] w
x₀w : x₀ ∈ w
hw : w ∩ s ⊆ f ⁻¹' t ∩ f ⁻¹' (extChartAt I' (f x₀)).source
⊢ s ∩ (u ∩ w) ⊆ f ⁻¹' t
have apply : s ∩ (u ∩ w) ⊆ w ∩ s
Tactic: apply Subset.trans _ (hw.trans inter_subset_left)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu_1 : UniqueMDiffOn I s
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
hfi :
  ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
this_1 : CompleteSpace E'
u : Set M
u_open : IsOpen[inst_4] u
x₀u : x₀ ∈ u
hu : ContMDiffOn I I' 2 f (insert x₀ s ∩ u)
this : f ⁻¹' (extChartAt I' (f x₀)).source ∈ 𝓝[s] x₀
w : Set M
w_open : IsOpen[inst_4] w
x₀w : x₀ ∈ w
hw : w ∩ s ⊆ f ⁻¹' t ∩ f ⁻¹' (extChartAt I' (f x₀)).source
⊢ s ∩ (u ∩ w) ⊆ f ⁻¹' (extChartAt I' (f x₀)).source
have apply : s ∩ (u ∩ w) ⊆ w ∩ s
Tactic: apply Subset.trans _ (hw.trans inter_subset_right)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu_1 : UniqueMDiffOn I s
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
hfi :
  ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
this_1 : CompleteSpace E'
u : Set M
u_open : IsOpen[inst_4] u
x₀u : x₀ ∈ u
hu : ContMDiffOn I I' 2 f (insert x₀ s ∩ u)
this : f ⁻¹' (extChartAt I' (f x₀)).source ∈ 𝓝[s] x₀
w : Set M
w_open : IsOpen[inst_4] w
x₀w : x₀ ∈ w
hw : w ∩ s ⊆ f ⁻¹' t ∩ f ⁻¹' (extChartAt I' (f x₀)).source
⊢ ContMDiffOn I I' 2 f (s ∩ (u ∩ w))
have refine_3 : s ∩ (u ∩ w) ⊆ insert x₀ s ∩ u
Tactic: apply hu.mono