awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Tangent (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
e_g :
  Eq (α := E' →L[𝕜] E')
    (fderivWithin 𝕜
        ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x₀)) : OpenPartialHomeomorph M' H') I') : M' → E') ∘
          (↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I').symm : E' → M'))
        (range (↑I' : H' → E'))
        ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I') : M' → E') (g x)) :
      E' →L[𝕜] E')
    (mfderiv% (↑(extChartAt I' (g x₀)) : M' → E') (g x) :
      TangentSpace I' (g x) →L[𝕜] TangentSpace 𝓘(𝕜, E') ((↑(extChartAt I' (g x₀)) : M' → E') (g x)))
⊢ Eq (α := E →L[𝕜] E')
    (fderivWithin 𝕜
          ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x₀)) : OpenPartialHomeomorph M' H') I') : M' → E') ∘
            (↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I').symm : E' → M'))
          (range (↑I' : H' → E'))
          ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I') : M' → E') (g x)) ∘SL
        ϕ x ∘SL
          VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M)
            (achart H (f x₀)) (achart H (f x)) (f x) :
      E →L[𝕜] E')
    (mfderiv% (↑(extChartAt I' (g x₀)) : M' → E') (g x) ∘SL
        ϕ x ∘SL
          mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I (f x₀)).symm : E → M) (range (↑I : H → E))
            ((↑(extChartAt I (f x₀)) : M → E) (f x)) :
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜)
        (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x)))
        (TangentSpace 𝓘(𝕜, E') ((↑(extChartAt I' (g x₀)) : M' → E') (g x))))
have e_f : VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H (f x₀))
    (achart H (f x)) (f x) =
  mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I (f x₀)).symm : E → M) (range (↑I : H → E))
    ((↑(extChartAt I (f x₀)) : M → E) (f x))
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Tangent (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
⊢ Eq (α := E' →L[𝕜] E')
    (fderivWithin 𝕜
        ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x₀)) : OpenPartialHomeomorph M' H') I') : M' → E') ∘
          (↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I').symm : E' → M'))
        (range (↑I' : H' → E'))
        ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I') : M' → E') (g x)) :
      E' →L[𝕜] E')
    (mfderiv% (↑(extChartAt I' (g x₀)) : M' → E') (g x) :
      TangentSpace I' (g x) →L[𝕜] TangentSpace 𝓘(𝕜, E') ((↑(extChartAt I' (g x₀)) : M' → E') (g x)))
have this : MDiffAt (↑(extChartAt I' (g x₀)) : M' → E') (g x)
Tactic: have : MDiffAt (extChartAt I' (g x₀)) (g x) := mdifferentiableAt_extChartAt hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Tangent (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
⊢ VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H (f x₀))
      (achart H (f x)) (f x) =
    mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I (f x₀)).symm : E → M) (range (↑I : H → E))
      ((↑(extChartAt I (f x₀)) : M → E) (f x))
have e_f : VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H (f x₀))
    (achart H (f x)) (f x) =
  if MDiffAt[range (↑I : H → E)] (↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x)) then
    fderivWithin 𝕜
      ((↑(extChartAt I ((↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x)))) : M → E) ∘
        (↑(extChartAt I (f x₀)).symm : E → M) ∘
          (↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E))
      ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E) ⁻¹' range (↑I : H → E))
      ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))) : E → E)
        ((↑(extChartAt I (f x₀)) : M → E) (f x)))
  else 0
Tactic: simp only [mfderivWithin, writtenInExtChartAt, modelWithCornersSelf_coe, range_id, inter_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Tangent (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
⊢ VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H (f x₀))
      (achart H (f x)) (f x) =
    if MDiffAt[range (↑I : H → E)] (↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x)) then
      fderivWithin 𝕜
        ((↑(extChartAt I ((↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x)))) : M → E) ∘
          (↑(extChartAt I (f x₀)).symm : E → M) ∘
            (↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E))
        ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E) ⁻¹' range (↑I : H → E))
        ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))) : E → E)
          ((↑(extChartAt I (f x₀)) : M → E) (f x)))
    else 0
have e_f : VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H (f x₀))
    (achart H (f x)) (f x) =
  fderivWithin 𝕜
    ((↑(extChartAt I ((↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x)))) : M → E) ∘
      (↑(extChartAt I (f x₀)).symm : E → M) ∘
        (↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E))
    ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E) ⁻¹' range (↑I : H → E))
    ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))) : E → E) ((↑(extChartAt I (f x₀)) : M → E) (f x)))
Tactic: rw [if_pos]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Tangent (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
e_f :
  VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H (f x₀))
      (achart H (f x)) (f x) =
    fderivWithin 𝕜
      ((↑(extChartAt I ((↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x)))) : M → E) ∘
        (↑(extChartAt I (f x₀)).symm : E → M) ∘
          (↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E))
      ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E) ⁻¹' range (↑I : H → E))
      ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))) : E → E)
        ((↑(extChartAt I (f x₀)) : M → E) (f x)))
⊢ VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H (f x₀))
      (achart H (f x)) (f x) =
    if MDiffAt[range (↑I : H → E)] (↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x)) then
      fderivWithin 𝕜
        ((↑(extChartAt I ((↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x)))) : M → E) ∘
          (↑(extChartAt I (f x₀)).symm : E → M) ∘
            (↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E))
        ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E) ⁻¹' range (↑I : H → E))
        ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))) : E → E)
          ((↑(extChartAt I (f x₀)) : M → E) (f x)))
    else 0
have e_f₁ : MDiffAt[range (↑I : H → E)] (↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x))
Tactic: rw [if_pos]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Tangent (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
⊢ MDiffAt[range (↑I : H → E)] (↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x))
have e_f : (↑(extChartAt I (f x₀)) : M → E) (f x) ∈ (extChartAt I (f x₀)).target
Tactic: apply mdifferentiableWithinAt_extChartAt_symm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Tangent (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
⊢ (↑(extChartAt I (f x₀)) : M → E) (f x) ∈ (extChartAt I (f x₀)).target
have e_f : f x ∈ (extChartAt I (f x₀)).source
Tactic: apply (extChartAt I (f x₀)).map_source
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
⊢ UniqueMDiffWithinAt I' (f '' s) (f x)
have this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
Tactic: have := hs.inter' <| hf.1 (extChartAt_source_mem_nhds (I := I') (f x))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
⊢ UniqueMDiffWithinAt I' (f '' s) (f x)
have refine : (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E) ⊆
  (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
Tactic: refine (((hf.2.mono ?sub1).uniqueDiffWithinAt this hd).mono ?sub2).congr_pt ?pt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
refine :
  (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E) ⊆
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
⊢ UniqueMDiffWithinAt I' (f '' s) (f x)
have refine₁ : writtenInExtChartAt I I' x f ''
    ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E)) ⊆
  (↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' f '' s ∩ range (↑I' : H' → E')
Tactic: refine (((hf.2.mono ?sub1).uniqueDiffWithinAt this hd).mono ?sub2).congr_pt ?pt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
refine :
  (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E) ⊆
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
refine₁ :
  writtenInExtChartAt I I' x f ''
      ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E)) ⊆
    (↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' f '' s ∩ range (↑I' : H' → E')
⊢ UniqueMDiffWithinAt I' (f '' s) (f x)
have refine₂ : writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) = (↑(extChartAt I' (f x)) : M' → E') (f x)
Tactic: refine (((hf.2.mono ?sub1).uniqueDiffWithinAt this hd).mono ?sub2).congr_pt ?pt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E) ⊆
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
have mfld_set_tac : ∀ ⦃my_y : E⦄,
  my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E) →
    my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
mfld_set_tac mfld_set_tac₁ mfld_set_tac₂ :
  ∀ ⦃my_y : E⦄,
    my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E) →
      my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E) ⊆
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
have mfld_set_tac₃ : ∀ ⦃my_y : E⦄,
  ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) my_y) ∈ s ∧
        f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) my_y)) ∈
          (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∧
      my_y ∈ range (↑I : H → E) →
    my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
⊢ writtenInExtChartAt I I' x f ''
      ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E)) ⊆
    (↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' f '' s ∩ range (↑I' : H' → E')
have case : ∀ (y : E) (hys : (↑(extChartAt I x).symm : E → M) y ∈ s)
  (hfy : (↑(extChartAt I x).symm : E → M) y ∈ f ⁻¹' (extChartAt I' (f x)).source),
  writtenInExtChartAt I I' x f y ∈ (↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' f '' s ∩ range (↑I' : H' → E')
Tactic: case sub2 =>
    rintro _ ⟨y, ⟨⟨hys, hfy⟩, -⟩, rfl⟩
    exact ⟨⟨_, hys, ((extChartAt I' (f x)).left_inv hfy).symm⟩, mem_range_self _⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
e : OpenPartialHomeomorph M M'
he : OpenPartialHomeomorph.MDifferentiable I I' e
hx : x ∈ e.source
⊢ UniqueMDiffWithinAt I' (e.target ∩ (↑e.symm : M' → M) ⁻¹' s) ((↑e : M → M') x)
have rw : UniqueMDiffWithinAt I' ((↑e : M → M') '' (s ∩ e.source)) ((↑e : M → M') x)
Tactic: rw [← e.image_source_inter_eq', inter_comm]