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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝[≠] (↑(extChartAt I x) : M → E) x]
    (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
have apply : (↑(extChartAt I x).symm : E → M) ⁻¹' u ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ) ∩
    {(↑(extChartAt I x) : M → E) x}ᶜ ⊆
  {x_1 : E |
    (fun (x_2 : E) ↦
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) x_2 =
          ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)) x_2)
      x_1}
Tactic: apply mem_nhdsWithin_iff_exists_mem_nhds_inter.2
    ⟨_, Filter.inter_mem ((continuousAt_extChartAt_symm x).preimage_mem_nhds u_mem) B, ?_⟩
-- 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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
hz : z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' u ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ)
h'z : Membership.mem (γ := Set E) {(↑(extChartAt I x) : M → E) x}ᶜ z
⊢ Membership.mem (γ := Set E)
    {x_1 : E |
      (fun (x_2 : E) ↦
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) x_2 =
            ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)) x_2)
        x_1}
    z
have simp : ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) z ↔
  ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)) z
Tactic: simp only [eq_iff_iff, mem_setOf_eq]
-- 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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
hz : z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' u ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ)
h'z : Membership.mem (γ := Set E) {(↑(extChartAt I x) : M → E) x}ᶜ z
⊢ z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ↔
    z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
have pos : ∀ (hIz : z ∈ range (↑I : H → E)),
  z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ↔
    z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
Tactic: by_cases hIz : z ∈ range I
-- 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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
hz : z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' u ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ)
h'z : Membership.mem (γ := Set E) {(↑(extChartAt I x) : M → E) x}ᶜ z
pos :
  ∀ (hIz : z ∈ range (↑I : H → E)),
    z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ↔
      z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
⊢ z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ↔
    z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
have neg : ∀ (hIz : z ∉ range (↑I : H → E)),
  z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ↔
    z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
Tactic: by_cases hIz : z ∈ range I
-- 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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
hz : z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' u ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ)
h'z : Membership.mem (γ := Set E) {(↑(extChartAt I x) : M → E) x}ᶜ z
hIz : z ∈ range (↑I : H → E)
⊢ z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ↔
    z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
have pos : ∀ (hz : (↑(extChartAt I x).symm : E → M) z ∈ u ∧ z ∈ (extChartAt I x).target),
  (↑(extChartAt I x).symm : E → M) z ∈ s ↔ (↑(extChartAt I x).symm : E → M) z ∈ t
Tactic: simp only [mem_inter_iff, mem_preimage, mem_union, mem_compl_iff, hIz, not_true_eq_false,
      or_false, and_true] at hz ⊢
Cleared hypotheses: hz
-- 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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
h'z : Membership.mem (γ := Set E) {(↑(extChartAt I x) : M → E) x}ᶜ z
hIz : z ∈ range (↑I : H → E)
hz : (↑(extChartAt I x).symm : E → M) z ∈ u ∧ z ∈ (extChartAt I x).target
⊢ (↑(extChartAt I x).symm : E → M) z ∈ s ↔ (↑(extChartAt I x).symm : E → M) z ∈ t
have pos : ((↑(extChartAt I x).symm : E → M) z ∈ s) = ((↑(extChartAt I x).symm : E → M) z ∈ t)
Tactic: rw [← eq_iff_iff]
-- 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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
h'z : Membership.mem (γ := Set E) {(↑(extChartAt I x) : M → E) x}ᶜ z
hIz : z ∈ range (↑I : H → E)
hz : (↑(extChartAt I x).symm : E → M) z ∈ u ∧ z ∈ (extChartAt I x).target
⊢ ((↑(extChartAt I x).symm : E → M) z ∈ s) = ((↑(extChartAt I x).symm : E → M) z ∈ t)
have apply : Membership.mem (γ := Set M) {x}ᶜ ((↑(extChartAt I x).symm : E → M) z)
Tactic: apply hu ⟨hz.1, ?_⟩
-- 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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
h'z : Membership.mem (γ := Set E) {(↑(extChartAt I x) : M → E) x}ᶜ z
hIz : z ∈ range (↑I : H → E)
hz : (↑(extChartAt I x).symm : E → M) z ∈ u ∧ z ∈ (extChartAt I x).target
⊢ Membership.mem (γ := Set M) {x}ᶜ ((↑(extChartAt I x).symm : E → M) z)
have h'z₁ : ¬z = (↑(extChartAt I x) : M → E) x
Tactic: push _ ∈ _ at h'z ⊢
Cleared hypotheses: h'z
-- 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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
hIz : z ∈ range (↑I : H → E)
hz : (↑(extChartAt I x).symm : E → M) z ∈ u ∧ z ∈ (extChartAt I x).target
h'z : ¬z = (↑(extChartAt I x) : M → E) x
⊢ ¬(↑(extChartAt I x).symm : E → M) z = x
have rw : ¬(↑(extChartAt I x) : M → E) x = z
Tactic: rw [eq_comm, (extChartAt I x).eq_symm_apply (by simp) hz.2]
-- 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 t : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ HasMFDerivWithinAt I I' f s x f' ↔ HasMFDerivWithinAt I I' f t x f'
have this : T1Space M
Tactic: have : T1Space M := I.t1Space 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'
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))
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ ContinuousWithinAt f s x ∧
      HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x) ↔
    ContinuousWithinAt f t x ∧
      HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x)
have refine_1 : ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x
Tactic: refine and_congr ?_ ?_
-- 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))
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
refine_1 : ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x
⊢ ContinuousWithinAt f s x ∧
      HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x) ↔
    ContinuousWithinAt f t x ∧
      HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x)
have refine_2 : HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x) ↔
  HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)
Tactic: refine and_congr ?_ ?_
-- 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))
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x) ↔
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
have refine_2 : (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝[≠] (↑(extChartAt I x) : M → E) x]
  (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
Tactic: apply hasFDerivWithinAt_congr_set' (extChartAt I x x)
-- 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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ MDifferentiableWithinAt I I' f s x ↔ MDifferentiableWithinAt I I' f t x
have simp : (∃ (f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))),
    HasMFDerivWithinAt I I' f s x f') ↔
  ∃ (f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))),
    HasMFDerivWithinAt I I' f t x f'
Tactic: simp only [mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt]
-- 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
h : s =ᶠ[𝓝 x] t
⊢ MDifferentiableWithinAt I I' f s x ↔ MDifferentiableWithinAt I I' f t x
have simp : (∃ (f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))),
    HasMFDerivWithinAt I I' f s x f') ↔
  ∃ (f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))),
    HasMFDerivWithinAt I I' f t x f'
Tactic: simp only [mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt]
-- 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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f s x) (mfderivWithin I I' f t x)
have pos : ∀ (hx : MDifferentiableWithinAt I I' f s x),
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f s x) (mfderivWithin I I' f t x)
Tactic: by_cases hx : MDifferentiableWithinAt I I' f s x
-- 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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
pos :
  ∀ (hx : MDifferentiableWithinAt I I' f s x),
    Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
      (mfderivWithin I I' f s x) (mfderivWithin I I' f t x)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f s x) (mfderivWithin I I' f t x)
have neg : ∀ (hx : ¬MDifferentiableWithinAt I I' f s x),
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f s x) (mfderivWithin I I' f t x)
Tactic: by_cases hx : MDifferentiableWithinAt I I' f s x
-- 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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
hx : MDifferentiableWithinAt I I' f s x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f s x) (mfderivWithin I I' f t x)
have pos : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
  (fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x))
  (fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x))
Tactic: simp only [mfderivWithin, hx, (mdifferentiableWithinAt_congr_set' y h).1 hx, ↓reduceIte]
-- 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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
hx : MDifferentiableWithinAt I I' f s x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x))
    (fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x))
have pos : (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝[≠] (↑(extChartAt I x) : M → E) x]
  (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
Tactic: apply fderivWithin_congr_set' (extChartAt I x x)
-- 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 f₁ : M → M'
x : M
s : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : HasMFDerivWithinAt I I' f s x f'
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ HasMFDerivWithinAt I I' f₁ s x f'
have refine : HasFDerivWithinAt (writtenInExtChartAt I I' x f₁) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
  ((↑(extChartAt I x) : M → E) x)
Tactic: refine ⟨ContinuousWithinAt.congr_of_eventuallyEq h.1 h₁ hx, ?_⟩
-- 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 f₁ : M → M'
x : M
s : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : HasMFDerivWithinAt I I' f s x f'
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f₁) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)
have h₂ : writtenInExtChartAt I I' x
    f₁ =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
  writtenInExtChartAt I I' x f
Tactic: apply HasFDerivWithinAt.congr_of_eventuallyEq h.2