Theorem: Super.fr_prop (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
c : ℂ
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r) ∧
      ∀ p ∈ (extChartAt (I.prod I) (c, a)).source,
        ↑(extChartAt (I.prod I) (c, a)) p ∈ ball (↑(extChartAt (I.prod I) (c, a)) (c, a)) r →
          f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
rcases(s.fla c).exists_ball_analyticOn with ⟨r0, r0p, fla⟩
State after:
case intro.intro
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r0)
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r) ∧
      ∀ p ∈ (extChartAt (I.prod I) (c, a)).source,
        ↑(extChartAt (I.prod I) (c, a)) p ∈ ball (↑(extChartAt (I.prod I) (c, a)) (c, a)) r →
          f p.1 p.2 ∈ (extChartAt I a).source

State before:
case intro.intro
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r0)
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r) ∧
      ∀ p ∈ (extChartAt (I.prod I) (c, a)).source,
        ↑(extChartAt (I.prod I) (c, a)) p ∈ ball (↑(extChartAt (I.prod I) (c, a)) (c, a)) r →
          f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
rcases eventually_nhds_iff.mp (s.stays_in_chart c) with ⟨t, tp, ot, ta⟩
State after:
case intro.intro.intro.intro.intro
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r) ∧
      ∀ p ∈ (extChartAt (I.prod I) (c, a)).source,
        ↑(extChartAt (I.prod I) (c, a)) p ∈ ball (↑(extChartAt (I.prod I) (c, a)) (c, a)) r →
          f p.1 p.2 ∈ (extChartAt I a).source

State before:
case intro.intro.intro.intro.intro
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r) ∧
      ∀ p ∈ (extChartAt (I.prod I) (c, a)).source,
        ↑(extChartAt (I.prod I) (c, a)) p ∈ ball (↑(extChartAt (I.prod I) (c, a)) (c, a)) r →
          f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
set ch := extChartAt II (c, a)
State after:
case intro.intro.intro.intro.intro
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r) ∧
      ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) r → f p.1 p.2 ∈ (extChartAt I a).source

State before:
case intro.intro.intro.intro.intro
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r) ∧
      ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) r → f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
set s := ch.target ∩ ch.symm ⁻¹' t
State after:
case intro.intro.intro.intro.intro
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r) ∧
      ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) r → f p.1 p.2 ∈ (extChartAt I a).source

State before:
case intro.intro.intro.intro.intro
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r) ∧
      ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) r → f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
have os : IsOpen s :=
  (continuousOn_extChartAt_symm II (c, a)).isOpen_inter_preimage
    (isOpen_extChartAt_target II (c, a)) ot
State after:
case intro.intro.intro.intro.intro
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r) ∧
      ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) r → f p.1 p.2 ∈ (extChartAt I a).source

State before:
case intro.intro.intro.intro.intro
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r) ∧
      ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) r → f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
have m : ch (c, a) ∈ s := by
  apply Set.mem_inter (mem_extChartAt_target _ _)
  rw [Set.mem_preimage, ch.left_inv (mem_extChartAt_source _ _)]
  exact ta
State after:
case intro.intro.intro.intro.intro
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r) ∧
      ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) r → f p.1 p.2 ∈ (extChartAt I a).source

State before:
case intro.intro.intro.intro.intro
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r) ∧
      ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) r → f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
rcases Metric.isOpen_iff.mp os (ch (c, a)) m with ⟨r1, r1p, rs⟩
State after:
case intro.intro.intro.intro.intro.intro.intro
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
r1 : ℝ
r1p : r1 > 0
rs : ball (↑ch (c, a)) r1 ⊆ s
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r) ∧
      ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) r → f p.1 p.2 ∈ (extChartAt I a).source

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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
⊢ ↑ch (c, a) ∈ s
Tactic:
apply Set.mem_inter (mem_extChartAt_target _ _)
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
⊢ ↑(extChartAt (I.prod I) (c, a)) (c, a) ∈ ↑ch.symm ⁻¹' t

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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
⊢ ↑(extChartAt (I.prod I) (c, a)) (c, a) ∈ ↑ch.symm ⁻¹' t
Tactic:
rw [Set.mem_preimage, ch.left_inv (mem_extChartAt_source _ _)]
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
⊢ (c, a) ∈ t

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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
⊢ (c, a) ∈ t
Tactic:
exact ta
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
r1 : ℝ
r1p : r1 > 0
rs : ball (↑ch (c, a)) r1 ⊆ s
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r) ∧
      ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) r → f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
use min r0 r1, by bound
State after:
case right
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
r1 : ℝ
r1p : r1 > 0
rs : ball (↑ch (c, a)) r1 ⊆ s
⊢ AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) (min r0 r1)) ∧
    ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) (min r0 r1) → f p.1 p.2 ∈ (extChartAt I a).source

State before:
case right
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
r1 : ℝ
r1p : r1 > 0
rs : ball (↑ch (c, a)) r1 ⊆ s
⊢ AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) (min r0 r1)) ∧
    ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) (min r0 r1) → f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
use fla.mono (Metric.ball_subset_ball (by bound))
State after:
case right
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
r1 : ℝ
r1p : r1 > 0
rs : ball (↑ch (c, a)) r1 ⊆ s
⊢ ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) (min r0 r1) → f p.1 p.2 ∈ (extChartAt I a).source

State before:
case right
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
r1 : ℝ
r1p : r1 > 0
rs : ball (↑ch (c, a)) r1 ⊆ s
⊢ ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) (min r0 r1) → f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
intro p ps pr
State after:
case right
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
r1 : ℝ
r1p : r1 > 0
rs : ball (↑ch (c, a)) r1 ⊆ s
p : ℂ × S
ps : p ∈ ch.source
pr : ↑ch p ∈ ball (↑ch (c, a)) (min r0 r1)
⊢ f p.1 p.2 ∈ (extChartAt I a).source

State before:
case right
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
r1 : ℝ
r1p : r1 > 0
rs : ball (↑ch (c, a)) r1 ⊆ s
p : ℂ × S
ps : p ∈ ch.source
pr : ↑ch p ∈ ball (↑ch (c, a)) (min r0 r1)
⊢ f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
apply tp p
State after:
case right
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
r1 : ℝ
r1p : r1 > 0
rs : ball (↑ch (c, a)) r1 ⊆ s
p : ℂ × S
ps : p ∈ ch.source
pr : ↑ch p ∈ ball (↑ch (c, a)) (min r0 r1)
⊢ p ∈ t

State before:
case right
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
r1 : ℝ
r1p : r1 > 0
rs : ball (↑ch (c, a)) r1 ⊆ s
p : ℂ × S
ps : p ∈ ch.source
pr : ↑ch p ∈ ball (↑ch (c, a)) (min r0 r1)
⊢ p ∈ t
Tactic:
rw [← ch.left_inv ps, ← Set.mem_preimage]
State after:
case right
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
r1 : ℝ
r1p : r1 > 0
rs : ball (↑ch (c, a)) r1 ⊆ s
p : ℂ × S
ps : p ∈ ch.source
pr : ↑ch p ∈ ball (↑ch (c, a)) (min r0 r1)
⊢ ↑ch p ∈ ↑ch.symm ⁻¹' t

State before:
case right
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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
r1 : ℝ
r1p : r1 > 0
rs : ball (↑ch (c, a)) r1 ⊆ s
p : ℂ × S
ps : p ∈ ch.source
pr : ↑ch p ∈ ball (↑ch (c, a)) (min r0 r1)
⊢ ↑ch p ∈ ↑ch.symm ⁻¹' t
Tactic:
exact Set.mem_of_mem_inter_right (rs (Metric.ball_subset_ball (by bound) pr))
State after:
no goals

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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
r1 : ℝ
r1p : r1 > 0
rs : ball (↑ch (c, a)) r1 ⊆ s
⊢ min r0 r1 > 0
Tactic:
bound
State after:
no goals

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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
r1 : ℝ
r1p : r1 > 0
rs : ball (↑ch (c, a)) r1 ⊆ s
⊢ min r0 r1 ≤ r0
Tactic:
bound
State after:
no goals

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
c : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
os : IsOpen s
m : ↑ch (c, a) ∈ s
r1 : ℝ
r1p : r1 > 0
rs : ball (↑ch (c, a)) r1 ⊆ s
p : ℂ × S
ps : p ∈ ch.source
pr : ↑ch p ∈ ball (↑ch (c, a)) (min r0 r1)
⊢ min r0 r1 ≤ r1
Tactic:
bound
State after:
no goals