internlm/Lean-Github huggingface dataset:
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
have i0 : i 0 = 0 := by nth_rw 1 [← bottcherNear_zero]; rw [ib.self_of_nhds]
Proof state after:
case intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
have inj : ∀ᶠ p : ℂ × ℂ in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2 := by
  refine ia.local_inj ?_
  have d0 : mfderiv I I (fun z : ℂ ↦ z) 0 ≠ 0 := id_mderiv_ne_zero
  rw [(Filter.EventuallyEq.symm ib).mfderiv_eq] at d0
  rw [←Function.comp_def, mfderiv_comp 0 _ ba.differentiableAt.mdifferentiableAt] at d0
  simp only [Ne, mderiv_comp_eq_zero_iff, nc, or_false_iff] at d0
  rw [bottcherNear_zero] at d0; exact d0
  rw [bottcherNear_zero]; exact ia.mdifferentiableAt
Proof state after:
case intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
rcases exist_root_of_unity s.d2 with ⟨a, a1, ad⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
a1 : a ≠ 1
ad : a ^ d = 1
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
a1 : a ≠ 1
ad : a ^ d = 1
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
refine ⟨fun z ↦ i (a * bottcherNear f d z), ?_, ?_, ?_⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
a1 : a ≠ 1
ad : a ^ d = 1
⊢ AnalyticAt ℂ (fun z => i (a * bottcherNear f d z)) 0

case intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
a1 : a ≠ 1
ad : a ^ d = 1
⊢ (fun z => i (a * bottcherNear f d z)) 0 = 0

case intro.intro.intro.intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
a1 : a ≠ 1
ad : a ^ d = 1
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, (fun z => i (a * bottcherNear f d z)) z ≠ z ∧ f ((fun z => i (a * bottcherNear f d z)) z) = f z
Theorem: SuperAt.not_local_inj
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
⊢ mfderiv I I (bottcherNear f d) 0 ≠ 0
Tactic:
rw [mfderiv_eq_fderiv, ← deriv_fderiv, (bottcherNear_monic s).deriv]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
⊢ ContinuousLinearMap.smulRight 1 1 ≠ 0
Theorem: SuperAt.not_local_inj
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
⊢ ContinuousLinearMap.smulRight 1 1 ≠ 0
Tactic:
exact ContinuousLinearMap.smulRight_ne_zero ContinuousLinearMap.one_ne_zero (by norm_num)
Proof state after:
no goals
Theorem: SuperAt.not_local_inj
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
⊢ 1 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: SuperAt.not_local_inj
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
⊢ i 0 = 0
Tactic:
nth_rw 1 [← bottcherNear_zero]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
⊢ i (bottcherNear ?m.13266 ?m.13267 0) = 0

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
⊢ ℂ → ℂ

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
⊢ ℕ
Theorem: SuperAt.not_local_inj
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
⊢ i (bottcherNear ?m.13266 ?m.13267 0) = 0

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
⊢ ℂ → ℂ

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
⊢ ℕ
Tactic:
rw [ib.self_of_nhds]
Proof state after:
no goals
Theorem: SuperAt.not_local_inj
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
⊢ ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
Tactic:
refine ia.local_inj ?_
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
⊢ mfderiv I I i 0 ≠ 0
Theorem: SuperAt.not_local_inj
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
⊢ mfderiv I I i 0 ≠ 0
Tactic:
have d0 : mfderiv I I (fun z : ℂ ↦ z) 0 ≠ 0 := id_mderiv_ne_zero
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
d0 : mfderiv I I (fun z => z) 0 ≠ 0
⊢ mfderiv I I i 0 ≠ 0
Theorem: SuperAt.not_local_inj
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
d0 : mfderiv I I (fun z => z) 0 ≠ 0
⊢ mfderiv I I i 0 ≠ 0
Tactic:
rw [(Filter.EventuallyEq.symm ib).mfderiv_eq] at d0
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
d0 : mfderiv I I (fun x => i (bottcherNear f d x)) 0 ≠ 0
⊢ mfderiv I I i 0 ≠ 0
Theorem: SuperAt.not_local_inj
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
d0 : mfderiv I I (fun x => i (bottcherNear f d x)) 0 ≠ 0
⊢ mfderiv I I i 0 ≠ 0
Tactic:
rw [←Function.comp_def, mfderiv_comp 0 _ ba.differentiableAt.mdifferentiableAt] at d0
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
d0 : (mfderiv I I i (bottcherNear f d 0)).comp (mfderiv I I (bottcherNear f d) 0) ≠ 0
⊢ mfderiv I I i 0 ≠ 0

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
d0 : mfderiv I I (i ∘ fun x => bottcherNear f d x) 0 ≠ 0
⊢ MDifferentiableAt I I i (bottcherNear f d 0)
Theorem: SuperAt.not_local_inj
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
d0 : (mfderiv I I i (bottcherNear f d 0)).comp (mfderiv I I (bottcherNear f d) 0) ≠ 0
⊢ mfderiv I I i 0 ≠ 0

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
d0 : mfderiv I I (i ∘ fun x => bottcherNear f d x) 0 ≠ 0
⊢ MDifferentiableAt I I i (bottcherNear f d 0)
Tactic:
simp only [Ne, mderiv_comp_eq_zero_iff, nc, or_false_iff] at d0
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
d0 : ¬mfderiv I I i (bottcherNear f d 0) = 0
⊢ mfderiv I I i 0 ≠ 0

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
d0 : mfderiv I I (i ∘ fun x => bottcherNear f d x) 0 ≠ 0
⊢ MDifferentiableAt I I i (bottcherNear f d 0)
Theorem: SuperAt.not_local_inj
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
d0 : ¬mfderiv I I i (bottcherNear f d 0) = 0
⊢ mfderiv I I i 0 ≠ 0

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
d0 : mfderiv I I (i ∘ fun x => bottcherNear f d x) 0 ≠ 0
⊢ MDifferentiableAt I I i (bottcherNear f d 0)
Tactic:
rw [bottcherNear_zero] at d0
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
d0 : ¬mfderiv I I i 0 = 0
⊢ mfderiv I I i 0 ≠ 0

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
d0 : mfderiv I I (i ∘ fun x => bottcherNear f d x) 0 ≠ 0
⊢ MDifferentiableAt I I i (bottcherNear f d 0)