internlm/Lean-Github huggingface dataset:
Theorem: Super.fr_prop
Proof 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
Proof 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
Theorem: Super.fr_prop
Proof 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
Proof 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
Theorem: Super.fr_prop
Proof 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⟩
Proof 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
Theorem: Super.fr_prop
Proof 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 _ _)
Proof 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
Theorem: Super.fr_prop
Proof 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 _ _)]
Proof 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
Theorem: Super.fr_prop
Proof 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
Proof state after:
no goals
Theorem: Super.fr_prop
Proof 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
Proof 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
Theorem: Super.fr_prop
Proof 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))
Proof 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
Theorem: Super.fr_prop
Proof 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
Proof 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
Theorem: Super.fr_prop
Proof 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
Proof 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
Theorem: Super.fr_prop
Proof 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]
Proof 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
Theorem: Super.fr_prop
Proof 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))
Proof state after:
no goals
Theorem: Super.fr_prop
Proof 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
Proof state after:
no goals
Theorem: Super.fr_prop
Proof 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
Proof state after:
no goals
Theorem: Super.fr_prop
Proof 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
Proof state after:
no goals
Theorem: prod_zero_mem_ball
Proof 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 : ℕ
c b : ℂ
r : ℝ
m : b ∈ ball c r
⊢ (b, 0) ∈ ball (c, 0) r
Tactic:
simp only [Metric.mem_ball] at m
Proof 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 : ℕ
c b : ℂ
r : ℝ
m : dist b c < r
⊢ (b, 0) ∈ ball (c, 0) r
Theorem: prod_zero_mem_ball
Proof 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 : ℕ
c b : ℂ
r : ℝ
m : dist b c < r
⊢ (b, 0) ∈ ball (c, 0) r
Tactic:
simpa only [Metric.mem_ball, dist_prod_same_right]
Proof state after:
no goals
Theorem: Super.exists_superNearC
Proof 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
⊢ ∃ t ⊆ s.fls, SuperNearC s.fl d univ t
Tactic:
refine s.superAtC.superNearC' s.fls_open fun c _ ↦ ?_
Proof 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 : ℂ
x✝ : c ∈ univ
⊢ (c, 0) ∈ s.fls
Theorem: Super.exists_superNearC
Proof 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 : ℂ
x✝ : c ∈ univ
⊢ (c, 0) ∈ s.fls
Tactic:
rw [Super.fls, Set.mem_iUnion]
Proof 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 : ℂ
x✝ : c ∈ univ
⊢ ∃ i, (c, 0) ∈ ball (i, 0) (s.fr i)
Theorem: Super.exists_superNearC
Proof 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 : ℂ
x✝ : c ∈ univ
⊢ ∃ i, (c, 0) ∈ ball (i, 0) (s.fr i)
Tactic:
use c
Proof state after:
case h
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 : ℂ
x✝ : c ∈ univ
⊢ (c, 0) ∈ ball (c, 0) (s.fr c)
Theorem: Super.exists_superNearC
Proof state before:
case h
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 : ℂ
x✝ : c ∈ univ
⊢ (c, 0) ∈ ball (c, 0) (s.fr c)
Tactic:
exact mem_ball_self (s.frp c)
Proof state after:
no goals
Theorem: Super.isOpen_near
Proof 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
⊢ IsOpen s.near
Tactic:
apply (continuousOn_extChartAt _ _).isOpen_inter_preimage (isOpen_extChartAt_source _ _)
Proof 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
⊢ IsOpen {p | (p.1, p.2 - ↑(extChartAt I a) a) ∈ s.near'}
Theorem: Super.isOpen_near
Proof 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
⊢ IsOpen {p | (p.1, p.2 - ↑(extChartAt I a) a) ∈ s.near'}
Tactic:
exact IsOpen.preimage (continuous_fst.prod_mk (continuous_snd.sub continuous_const))
  s.superNearC.o
Proof state after:
no goals
Theorem: Super.mem_near
Proof 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 : ℂ
⊢ (c, a) ∈ s.near
Tactic:
simp only [Super.near, extChartAt_prod, PartialEquiv.prod_source, Set.mem_prod, Set.mem_inter_iff,
  mem_extChartAt_source, extChartAt_eq_refl, PartialEquiv.refl_source, Set.mem_univ, true_and_iff,
  Set.mem_preimage, PartialEquiv.prod_coe, PartialEquiv.refl_coe, id, Set.mem_setOf_eq, sub_self]
Proof 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 : ℂ
⊢ (c, 0) ∈ s.near'
Theorem: Super.mem_near
Proof 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 : ℂ
⊢ (c, 0) ∈ s.near'
Tactic:
exact (s.superNearC.s (Set.mem_univ _)).t0
Proof state after:
no goals
Theorem: Super.near_subset_chart
Proof 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 : ℂ
z : S
m : (c, z) ∈ s.near
⊢ z ∈ (extChartAt I a).source
Tactic:
have h := Set.mem_of_mem_inter_left m
Proof 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 : ℂ
z : S
m : (c, z) ∈ s.near
h : (c, z) ∈ (extChartAt (I.prod I) (0, a)).source
⊢ z ∈ (extChartAt I a).source