awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this_1 : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst] s
ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
this : IsOpen[inst] ((↑f : H → H) ⁻¹' s ∩ f.source)
⊢ (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ (e.target ∩ (↑e.symm : H → M) ⁻¹' e'.source) =
    e.target ∩ ((↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ (↑e.symm : H → M) ⁻¹' e'.source)

Tactic:
have A : e' ∘ e.symm ⁻¹' s ∩ (e.target ∩ e.symm ⁻¹' e'.source) =
          e.target ∩ (e' ∘ e.symm ⁻¹' s ∩ e.symm ⁻¹' e'.source) := by
        rw [← inter_assoc, ← inter_assoc]
        congr 1
        exact inter_comm _ _
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this_1 : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst] s
ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
this : IsOpen[inst] ((↑f : H → H) ⁻¹' s ∩ f.source)
A :
  (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ (e.target ∩ (↑e.symm : H → M) ⁻¹' e'.source) =
    e.target ∩ ((↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ (↑e.symm : H → M) ⁻¹' e'.source)
⊢ IsOpen[inst] (e.target ∩ e.invFun ⁻¹' ((↑e' : M → H) ⁻¹' s ∩ e'.source))

Tactic:
simpa [f, PartialEquiv.trans_source, preimage_inter, preimage_comp.symm, A] using this

Premises used: Set.preimage_inter, PartialEquiv.trans_source, Set.preimage_comp, Eq.symm
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
x : M
simp : ∃ (i : PartialEquiv M H) (h : i ∈ c.atlas), c.openPartialHomeomorph (c.chartAt x) ⋯ = c.openPartialHomeomorph i ⋯
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H))
    (⋃ (e : PartialEquiv M H), ⋃ (he : e ∈ c.atlas), {c.openPartialHomeomorph e he})
    (c.openPartialHomeomorph (c.chartAt x) ⋯)

Tactic:
simp only [mem_iUnion, mem_singleton_iff]

Premises used: Set.mem_iUnion, Set.mem_singleton_iff
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
x : M
⊢ ∃ (i : PartialEquiv M H) (h : i ∈ c.atlas), c.openPartialHomeomorph (c.chartAt x) ⋯ = c.openPartialHomeomorph i ⋯

Tactic:
⟨c.chartAt x, c.chart_mem_atlas x, rfl⟩

Premises used: ChartedSpaceCore.chart_mem_atlas, ChartedSpaceCore.chartAt, Exists.intro, rfl
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
x : M
⊢ ∃ (i : PartialEquiv M H) (h : i ∈ c.atlas), c.openPartialHomeomorph (c.chartAt x) ⋯ = c.openPartialHomeomorph i ⋯

Tactic:
exact ⟨c.chartAt x, c.chart_mem_atlas x, rfl⟩
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
⊢ range (↑I : H → E) = univ

Tactic:
have hI : range I = univ := ModelWithCorners.Boundaryless.range_eq_univ
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
rw : 𝓝[univ] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
rw₁ rw₂ : 𝓝 ((↑e : M → E) c) = 𝓝 ((↑e : M → E) c)
⊢ 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)

Tactic:
rw [hI, nhdsWithin_univ]

Premises used: nhdsWithin_univ
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
⊢ 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)

Tactic:
have H₁ : 𝓝[range I] (e c) = 𝓝 (e c) := by rw [hI, nhdsWithin_univ]
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
rw :
  map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) =
    map (↑(extChartAt I c).symm : E → M) (𝓝[range (↑I : H → E)] (↑(extChartAt I c) : M → E) c)
rw₁ rw₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = map (↑(extChartAt I c).symm : E → M) (𝓝 ((↑e : M → E) c))
⊢ map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c

Tactic:
rw [← map_extChartAt_symm_nhdsWithin_range (I := I) c, H₁]

Premises used: map_extChartAt_symm_nhdsWithin_range
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
⊢ map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c

Tactic:
have H₂ : map e.symm (𝓝 (e c)) = 𝓝 c := by
    rw [← map_extChartAt_symm_nhdsWithin_range (I := I) c, H₁]
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
rw : ∀ᶠ (a : E) in 𝓝 ((↑e : M → E) c), ‖f ((↑e.symm : E → M) a)‖ = ‖f c‖
⊢ ∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖

Tactic:
rw [← H₂, eventually_map]

Premises used: Filter.eventually_map
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
⊢ e.target ∈ 𝓝 ((↑e : M → E) c)

Tactic:
have : e.target ∈ 𝓝 (e c) := H₁ ▸ extChartAt_target_mem_nhdsWithin c
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
h : ∀ (y : E) (hyt : y ∈ e.target) (hy₂ : MDiffAt f ((↑e.symm : E → M) y)), DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y
⊢ ∀ᶠ (y : E) in 𝓝 ((↑e : M → E) c), DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y

Tactic:
filter_upwards [this, Tendsto.eventually H₂.le hd] with y hyt hy₂

Premises used: Eq.le, Filter.Tendsto.eventually
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
y : E
hyt : y ∈ e.target
hy₂ : MDiffAt f ((↑e.symm : E → M) y)
rw : (↑e.symm : E → M) y ∈ (extChartAt I c).source
⊢ (↑e.symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source

Tactic:
rw [← extChartAt_source I c]

Premises used: extChartAt_source
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
y : E
hyt : y ∈ e.target
hy₂ : MDiffAt f ((↑e.symm : E → M) y)
⊢ (↑e.symm : E → M) y ∈ (extChartAt I c).source

Tactic:
(extChartAt I c).map_target hyt

Premises used: PartialEquiv.map_target, extChartAt, Set.Mem
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
y : E
hyt : y ∈ e.target
hy₂ : MDiffAt f ((↑e.symm : E → M) y)
⊢ (↑e.symm : E → M) y ∈ (extChartAt I c).source

Tactic:
exact (extChartAt I c).map_target hyt

Premises used: PartialEquiv.map_target, extChartAt
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
y : E
hyt : y ∈ e.target
hy₂ : MDiffAt f ((↑e.symm : E → M) y)
⊢ (↑e.symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source

Tactic:
have hys : e.symm y ∈ (chartAt H c).source := by
      rw [← extChartAt_source I c]
      exact (extChartAt I c).map_target hyt
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
y : E
hyt : y ∈ e.target
hy₂ : MDiffAt f ((↑e.symm : E → M) y)
hys : (↑e.symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
⊢ Membership.mem (γ := Set F) (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv (chartAt F 0)))
    (f ((↑e.symm : E → M) y))

Tactic:
have hfy : f (e.symm y) ∈ (chartAt F (0 : F)).source := mem_univ _
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
y : E
hyt : y ∈ e.target
hy₂ : MDiffAt f ((↑e.symm : E → M) y)
hys : (↑e.symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
hfy :
  Membership.mem (γ := Set F) (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv (chartAt F 0)))
    (f ((↑e.symm : E → M) y))
⊢ ContinuousAt f ((↑e.symm : E → M) y) ∧
    DifferentiableAt ℂ ((↑(extChartAt 𝓘(ℂ, F) 0) : F → F) ∘ f ∘ (↑(extChartAt I c).symm : E → M)) y

Tactic:
rw [mdifferentiableAt_iff_of_mem_source hys hfy, hI, differentiableWithinAt_univ,
      e.right_inv hyt] at hy₂

Premises used: PartialEquiv.right_inv, mdifferentiableAt_iff_of_mem_source, differentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
y : E
hyt : y ∈ e.target
hy₂ : MDiffAt f ((↑e.symm : E → M) y)
hys : (↑e.symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
hfy :
  Membership.mem (γ := Set F) (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv (chartAt F 0)))
    (f ((↑e.symm : E → M) y))
hy₃ :
  ContinuousAt f ((↑e.symm : E → M) y) ∧
    DifferentiableAt ℂ ((↑(extChartAt 𝓘(ℂ, F) 0) : F → F) ∘ f ∘ (↑(extChartAt I c).symm : E → M)) y
⊢ (↑e.symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source

Tactic:
rw [mdifferentiableAt_iff_of_mem_source hys hfy, hI, differentiableWithinAt_univ,
      e.right_inv hyt] at hy₂

Premises used: PartialEquiv.right_inv, mdifferentiableAt_iff_of_mem_source, differentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
y : E
hyt : y ∈ e.target
hy₂ : MDiffAt f ((↑e.symm : E → M) y)
hys : (↑e.symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
hfy :
  Membership.mem (γ := Set F) (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv (chartAt F 0)))
    (f ((↑e.symm : E → M) y))
hy₃ :
  ContinuousAt f ((↑e.symm : E → M) y) ∧
    DifferentiableAt ℂ ((↑(extChartAt 𝓘(ℂ, F) 0) : F → F) ∘ f ∘ (↑(extChartAt I c).symm : E → M)) y
hys₁ : (↑e.symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
⊢ Membership.mem (γ := Set F) (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv (chartAt F 0)))
    (f ((↑e.symm : E → M) y))

Tactic:
rw [mdifferentiableAt_iff_of_mem_source hys hfy, hI, differentiableWithinAt_univ,
      e.right_inv hyt] at hy₂

Premises used: PartialEquiv.right_inv, mdifferentiableAt_iff_of_mem_source, differentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
y : E
hyt : y ∈ e.target
hy₂ :
  ContinuousAt f ((↑e.symm : E → M) y) ∧
    DifferentiableAt ℂ ((↑(extChartAt 𝓘(ℂ, F) 0) : F → F) ∘ f ∘ (↑(extChartAt I c).symm : E → M)) y
hys : (↑e.symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
hfy :
  Membership.mem (γ := Set F) (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv (chartAt F 0)))
    (f ((↑e.symm : E → M) y))
⊢ DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y

Tactic:
hy₂.2

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
y : E
hyt : y ∈ e.target
hy₂ :
  ContinuousAt f ((↑e.symm : E → M) y) ∧
    DifferentiableAt ℂ ((↑(extChartAt 𝓘(ℂ, F) 0) : F → F) ∘ f ∘ (↑(extChartAt I c).symm : E → M)) y
hys : (↑e.symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
hfy :
  Membership.mem (γ := Set F) (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv (chartAt F 0)))
    (f ((↑e.symm : E → M) y))
⊢ DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y

Tactic:
exact hy₂.2

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
⊢ ∀ᶠ (y : E) in 𝓝 ((↑e : M → E) c), DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y

Tactic:
replace hd : ∀ᶠ y in 𝓝 (e c), DifferentiableAt ℂ (f ∘ e.symm) y := by
    have : e.target ∈ 𝓝 (e c) := H₁ ▸ extChartAt_target_mem_nhdsWithin c
    filter_upwards [this, Tendsto.eventually H₂.le hd] with y hyt hy₂
    have hys : e.symm y ∈ (chartAt H c).source := by
      rw [← extChartAt_source I c]
      exact (extChartAt I c).map_target hyt
    have hfy : f (e.symm y) ∈ (chartAt F (0 : F)).source := mem_univ _
    rw [mdifferentiableAt_iff_of_mem_source hys hfy, hI, differentiableWithinAt_univ,
      e.right_inv hyt] at hy₂
    exact hy₂.2
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
hd : ∀ᶠ (y : E) in 𝓝 ((↑e : M → E) c), DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y
⊢ ∀ᶠ (y : E) in 𝓝 ((↑e : M → E) c), ‖(f ∘ (↑e.symm : E → M)) y‖ = ‖(f ∘ (↑e.symm : E → M)) ((↑e : M → E) c)‖

Tactic:
norm_eventually_eq_of_isLocalMax hd _

Premises used: Complex.norm_eventually_eq_of_isLocalMax
-- Module: Mathlib.Geometry.Manifold.Complex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
hd : ∀ᶠ (y : E) in 𝓝 ((↑e : M → E) c), DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y
h : ∀ (x : E), f c = (f ∘ (↑e.symm : E → M)) ((↑e : M → E) c)
convert! : IsLocalMax (norm ∘ f ∘ (↑e.symm : E → M)) ((↑e : M → E) c)
⊢ ∀ᶠ (a : E) in 𝓝 ((↑e : M → E) c), ‖f ((↑e.symm : E → M) a)‖ = ‖f c‖

Tactic:
convert! norm_eventually_eq_of_isLocalMax hd _

Premises used: Complex.norm_eventually_eq_of_isLocalMax