awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
x : M
s : Set M
n : WithTop ℕ∞
hf : ContMDiffWithinAt I I' n f s x
hn : n ≠ 0
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 ∈ (↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩ range (↑I : H → E)
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E) ⊆
    (↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → 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 ∈ (↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩ range (↑I : H → E)
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
h : ContinuousWithinAt f s x
⊢ writtenInExtChartAt I I'' x
      (g ∘ f) =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f
have _ : f ∘ (↑(extChartAt I x).symm : E → M) ⁻¹' (extChartAt I' (f x)).source ⊆
  {x_1 : E |
    (fun (x_2 : E) ↦
        writtenInExtChartAt I I'' x (g ∘ f) x_2 =
          (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) x_2)
      x_1}
Tactic: apply
    @Filter.mem_of_superset _ _ (f ∘ (extChartAt I x).symm ⁻¹' (extChartAt I' (f x)).source) _
      (extChartAt_preimage_mem_nhdsWithin
        (h.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds _)))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
h : ContinuousWithinAt f s x
⊢ f ∘ (↑(extChartAt I x).symm : E → M) ⁻¹' (extChartAt I' (f x)).source ⊆
    {x_1 : E |
      (fun (x_2 : E) ↦
          writtenInExtChartAt I I'' x (g ∘ f) x_2 =
            (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) x_2)
        x_1}
have mfld_set_tac : ∀ ⦃my_y : E⦄,
  my_y ∈ f ∘ (↑(extChartAt I x).symm : E → M) ⁻¹' (extChartAt I' (f x)).source →
    Membership.mem (γ := Set E)
      {x_1 : E |
        (fun (x_2 : E) ↦
            writtenInExtChartAt I I'' x (g ∘ f) x_2 =
              (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) x_2)
          x_1}
      my_y
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
h : ContinuousWithinAt f s x
mfld_set_tac mfld_set_tac₁ mfld_set_tac₂ :
  ∀ ⦃my_y : E⦄,
    my_y ∈ f ∘ (↑(extChartAt I x).symm : E → M) ⁻¹' (extChartAt I' (f x)).source →
      Membership.mem (γ := Set E)
        {x_1 : E |
          (fun (x_2 : E) ↦
              writtenInExtChartAt I I'' x (g ∘ f) x_2 =
                (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) x_2)
            x_1}
        my_y
⊢ f ∘ (↑(extChartAt I x).symm : E → M) ⁻¹' (extChartAt I' (f x)).source ⊆
    {x_1 : E |
      (fun (x_2 : E) ↦
          writtenInExtChartAt I I'' x (g ∘ f) x_2 =
            (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) x_2)
        x_1}
have mfld_set_tac₃ : ∀ ⦃my_y : E⦄,
  f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) my_y)) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source →
    Membership.mem (γ := Set E)
      {x_1 : E |
        (fun (x_2 : E) ↦
            writtenInExtChartAt I I'' x (g ∘ f) x_2 =
              (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) x_2)
          x_1}
      my_y
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
⊢ Eq (α := (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f univ) (mfderiv I I' f)
have h : ∀ (x : M),
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f univ x) (mfderiv I I' f x)
Tactic: ext x : 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
x : M
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f univ x) (mfderiv I I' f x)
have h : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
  (if MDifferentiableWithinAt I I' f univ x then
    fderivWithin 𝕜
      (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
        f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
      (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
  else 0)
  (if MDifferentiableAt I I' f x then
    fderivWithin 𝕜
      (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
        f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
      (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
  else 0)
Tactic: simp only [mfderivWithin, mfderiv, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
x : M
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (if MDifferentiableWithinAt I I' f univ x then
      fderivWithin 𝕜
        (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
          f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
        (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
    else 0)
    (if MDifferentiableAt I I' f x then
      fderivWithin 𝕜
        (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
          f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
        (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
    else 0)
have h : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
  (if MDifferentiableAt I I' f x then
    fderivWithin 𝕜
      (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
        f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
      (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
  else 0)
  (if MDifferentiableAt I I' f x then
    fderivWithin 𝕜
      (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
        f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
      (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
  else 0)
Tactic: rw [mdifferentiableWithinAt_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
inst_11 : Subsingleton E
x : M
⊢ MDifferentiableAt I I' f x
have this : Subsingleton H
Tactic: have : Subsingleton H := I.injective.subsingleton
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
inst_11 : Subsingleton E
x : M
this : Subsingleton H
⊢ MDifferentiableAt I I' f x
have this₁ : DiscreteTopology M
Tactic: have : DiscreteTopology M := discreteTopology H M
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
inst_11 : Subsingleton E
x : M
this_1 : Subsingleton H
this : DiscreteTopology M
⊢ MDifferentiableAt I I' f x
have simp : DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: simp only [mdifferentiableAt_iff, continuous_of_discreteTopology.continuousAt, true_and]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
x : M
s : Set M
hf :
  Injective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(mfderivWithin I I' f s x) : (a : TangentSpace I x) → TangentSpace I' (f x))
⊢ MDifferentiableWithinAt I I' f s x
have a : Nontrivial E
Tactic: nontriviality E
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
x : M
s : Set M
hf :
  Injective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(mfderivWithin I I' f s x) : (a : TangentSpace I x) → TangentSpace I' (f x))
h : Nontrivial E
⊢ MDifferentiableWithinAt I I' f s x
have this : Nontrivial.{u_2} (TangentSpace I x)
Tactic: have : Nontrivial (TangentSpace I x) := inferInstanceAs (Nontrivial E)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
x : M
s : Set M
hf :
  Injective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(mfderivWithin I I' f s x) : (a : TangentSpace I x) → TangentSpace I' (f x))
h : Nontrivial E
this : Nontrivial.{u_2} (TangentSpace I x)
⊢ MDifferentiableWithinAt I I' f s x
have contrapose : ∀ (hf : ¬MDifferentiableWithinAt I I' f s x),
  ¬Injective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
      (⇑(mfderivWithin I I' f s x) : (a : TangentSpace I x) → TangentSpace I' (f x))
Tactic: contrapose hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
x : M
s : Set M
h : Nontrivial E
this : Nontrivial.{u_2} (TangentSpace I x)
hf : ¬MDifferentiableWithinAt I I' f s x
⊢ ¬Injective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
      (⇑(mfderivWithin I I' f s x) : (a : TangentSpace I x) → TangentSpace I' (f x))
have rw : ¬Injective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑0 : (a : TangentSpace I x) → TangentSpace I' (f x))
Tactic: rw [mfderivWithin_zero_of_not_mdifferentiableWithinAt hf]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
x : M
f : M → M'
hf :
  Injective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(mfderiv I I' f x) : (a : TangentSpace I x) → TangentSpace I' (f x))
⊢ MDifferentiableAt I I' f x
have hf₁ : Injective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
  (⇑(mfderivWithin I I' f univ x) : (a : TangentSpace I x) → TangentSpace I' (f x))
Tactic: simp only [← mdifferentiableWithinAt_univ, ← mfderivWithin_univ] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
x : M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : HasMFDerivAt I I' f x f'
⊢ MDifferentiableAt I I' f x
have rw : ContinuousAt f x ∧
  DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: rw [mdifferentiableAt_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
x : M
f₀' f₁' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h₀ : HasMFDerivAt I I' f x f₀'
h₁ : HasMFDerivAt I I' f x f₁'
⊢ f₀' = f₁'
have h₂ : HasMFDerivWithinAt I I' f univ x f₀'
Tactic: rw [← hasMFDerivWithinAt_univ] at h₀ h₁
Cleared hypotheses: h₀, h₁
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
x : M
f₀' f₁' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h₀ : HasMFDerivAt I I' f x f₀'
h₁ : HasMFDerivAt I I' f x f₁'
h₂ : HasMFDerivWithinAt I I' f univ x f₀'
⊢ f₀' = f₁'
have h₃ : HasMFDerivWithinAt I I' f univ x f₁'
Tactic: rw [← hasMFDerivWithinAt_univ] at h₀ h₁
Cleared hypotheses: h₀, h₁
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
x : M
s t : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : t ∈ 𝓝[s] x
⊢ HasMFDerivWithinAt I I' f (s ∩ t) x f' ↔ HasMFDerivWithinAt I I' f s x f'
have rw : (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈
  𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
Tactic: rw [HasMFDerivWithinAt, HasMFDerivWithinAt, extChartAt_preimage_inter_eq,
    hasFDerivWithinAt_inter', continuousWithinAt_inter' h]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
x : M
s t : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : t ∈ 𝓝 x
⊢ HasMFDerivWithinAt I I' f (s ∩ t) x f' ↔ HasMFDerivWithinAt I I' f s x f'
have rw : (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
Tactic: rw [HasMFDerivWithinAt, HasMFDerivWithinAt, extChartAt_preimage_inter_eq, hasFDerivWithinAt_inter,
    continuousWithinAt_inter h]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
f : M → M'
x : M
s t : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
hs : HasMFDerivWithinAt I I' f s x f'
ht : HasMFDerivWithinAt I I' f t x f'
⊢ HasMFDerivWithinAt I I' f (s ∪ t) x f'
have left : ContinuousWithinAt f (s ∪ t) x
Tactic: constructor