Theorem: Super.mem_near_to_near' (Ray/Dynamics/BottcherNearM.lean)

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
⊢ (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a) ∈ s.near'
Tactic:
have h := Set.mem_of_mem_inter_right m
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h : p ∈ ↑(extChartAt (I.prod I) (0, a)) ⁻¹' {p | (p.1, p.2 - ↑(extChartAt I a) a) ∈ s.near'}
⊢ (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a) ∈ s.near'

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h : p ∈ ↑(extChartAt (I.prod I) (0, a)) ⁻¹' {p | (p.1, p.2 - ↑(extChartAt I a) a) ∈ s.near'}
⊢ (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a) ∈ s.near'
Tactic:
simp only [Set.mem_preimage, extChartAt_prod, PartialEquiv.prod_coe, extChartAt_eq_refl,
  PartialEquiv.refl_coe, id] at h
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h : (p.1, ↑(extChartAt I a) p.2) ∈ {p | (p.1, p.2 - ↑(extChartAt I a) a) ∈ s.near'}
⊢ (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a) ∈ s.near'

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h : (p.1, ↑(extChartAt I a) p.2) ∈ {p | (p.1, p.2 - ↑(extChartAt I a) a) ∈ s.near'}
⊢ (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a) ∈ s.near'
Tactic:
exact h
State after:
no goals