Theorem: not_local_inj_of_deriv_zero (Ray/Dynamics/Multiple.lean)

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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
set f' := fun z ↦ f (z + c) - f c
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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z

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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
have fa' : AnalyticAt ℂ f' 0 :=
  AnalyticAt.sub
    (AnalyticAt.comp (by simp only [zero_add, fa]) ((analyticAt_id _ _).add analyticAt_const))
    analyticAt_const
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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z

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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
have df' : HasDerivAt f' (0 * 1) 0 := by
  refine HasDerivAt.sub_const ?_ _
  have e : (fun z ↦ f (z + c)) = f ∘ fun z ↦ z + c := rfl
  rw [e]; apply HasDerivAt.comp; simp only [zero_add, df]
  exact HasDerivAt.add_const (hasDerivAt_id _) _
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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' (0 * 1) 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z

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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' (0 * 1) 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
simp only [MulZeroClass.zero_mul] at df'
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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' 0 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z

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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' 0 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
have f0' : (fun z ↦ f (z + c) - f c) 0 = 0 := by simp only [zero_add, sub_self]
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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' 0 0
f0' : (fun z => f (z + c) - f c) 0 = 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z

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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' 0 0
f0' : (fun z => f (z + c) - f c) 0 = 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
rcases not_local_inj_of_deriv_zero' fa' df' f0' with ⟨g, ga, e, h⟩
State after:
case 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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' 0 0
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z

State before:
case 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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' 0 0
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
clear fa df fa' df'
State after:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z

State before:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
refine ⟨fun z ↦ g (z - c) + c, ?_, ?_, ?_⟩
State after:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ AnalyticAt ℂ (fun z => g (z - c) + c) c

case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ (fun z => g (z - c) + c) c = c

case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] c, (fun z => g (z - c) + c) z ≠ z ∧ f ((fun z => g (z - c) + c) z) = f z

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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
⊢ AnalyticAt ℂ f (0 + c)
Tactic:
simp only [zero_add, fa]
State after:
no goals

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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
⊢ HasDerivAt f' (0 * 1) 0
Tactic:
refine HasDerivAt.sub_const ?_ _
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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
⊢ HasDerivAt (fun z => f (z + c)) (0 * 1) 0

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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
⊢ HasDerivAt (fun z => f (z + c)) (0 * 1) 0
Tactic:
have e : (fun z ↦ f (z + c)) = f ∘ fun z ↦ z + c := rfl
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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (fun z => f (z + c)) (0 * 1) 0

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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (fun z => f (z + c)) (0 * 1) 0
Tactic:
rw [e]
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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (f ∘ fun z => z + c) (0 * 1) 0

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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (f ∘ fun z => z + c) (0 * 1) 0
Tactic:
apply HasDerivAt.comp
State after:
case hh₂
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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt f 0 (0 + c)

case hh
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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (fun z => z + c) 1 0

State before:
case hh₂
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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt f 0 (0 + c)

case hh
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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (fun z => z + c) 1 0
Tactic:
simp only [zero_add, df]
State after:
case hh
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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (fun z => z + c) 1 0

State before:
case hh
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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (fun z => z + c) 1 0
Tactic:
exact HasDerivAt.add_const (hasDerivAt_id _) _
State after:
no goals

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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' 0 0
⊢ (fun z => f (z + c) - f c) 0 = 0
Tactic:
simp only [zero_add, sub_self]
State after:
no goals

State before:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ AnalyticAt ℂ (fun z => g (z - c) + c) c
Tactic:
exact AnalyticAt.add (AnalyticAt.comp (by simp only [sub_self, ga])
  ((analyticAt_id _ _).sub analyticAt_const)) analyticAt_const
State after:
no goals

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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ AnalyticAt ℂ g (c - c)
Tactic:
simp only [sub_self, ga]
State after:
no goals

State before:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ (fun z => g (z - c) + c) c = c
Tactic:
simp only [sub_self, e, zero_add]
State after:
no goals

State before:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] c, (fun z => g (z - c) + c) z ≠ z ∧ f ((fun z => g (z - c) + c) z) = f z
Tactic:
simp only [eventually_nhdsWithin_iff] at h ⊢
State after:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
⊢ ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x

State before:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
⊢ ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x
Tactic:
have sc : Tendsto (fun z ↦ z - c) (𝓝 c) (𝓝 0) := by
  rw [← sub_self c]; exact continuousAt_id.sub continuousAt_const
State after:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
⊢ ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x

State before:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
⊢ ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x
Tactic:
refine (sc.eventually h).mp (eventually_of_forall ?_)
State after:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
⊢ ∀ (x : ℂ),
    (x - c ∈ {0}ᶜ → g (x - c) ≠ x - c ∧ f' (g (x - c)) = f' (x - c)) →
      x ∈ {c}ᶜ → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x

State before:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
⊢ ∀ (x : ℂ),
    (x - c ∈ {0}ᶜ → g (x - c) ≠ x - c ∧ f' (g (x - c)) = f' (x - c)) →
      x ∈ {c}ᶜ → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x
Tactic:
simp only [mem_compl_singleton_iff, sub_ne_zero]
State after:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
⊢ ∀ (x : ℂ),
    (x ≠ c → g (x - c) ≠ x - c ∧ f' (g (x - c)) = f' (x - c)) → x ≠ c → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x

State before:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
⊢ ∀ (x : ℂ),
    (x ≠ c → g (x - c) ≠ x - c ∧ f' (g (x - c)) = f' (x - c)) → x ≠ c → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x
Tactic:
intro z h zc
State after:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
⊢ g (z - c) + c ≠ z ∧ f (g (z - c) + c) = f z

State before:
case 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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
⊢ g (z - c) + c ≠ z ∧ f (g (z - c) + c) = f z
Tactic:
rcases h zc with ⟨gz, ff⟩
State after:
case intro.intro.intro.refine_3.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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ g (z - c) + c ≠ z ∧ f (g (z - c) + c) = f z

State before:
case intro.intro.intro.refine_3.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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ g (z - c) + c ≠ z ∧ f (g (z - c) + c) = f z
Tactic:
constructor
State after:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ g (z - c) + c ≠ z

case intro.intro.intro.refine_3.intro.right
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z

State before:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ g (z - c) + c ≠ z

case intro.intro.intro.refine_3.intro.right
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z
Tactic:
contrapose gz
State after:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
ff : f' (g (z - c)) = f' (z - c)
gz : ¬g (z - c) + c ≠ z
⊢ ¬g (z - c) ≠ z - c

case intro.intro.intro.refine_3.intro.right
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z

State before:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
ff : f' (g (z - c)) = f' (z - c)
gz : ¬g (z - c) + c ≠ z
⊢ ¬g (z - c) ≠ z - c

case intro.intro.intro.refine_3.intro.right
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z
Tactic:
simp only [not_not] at gz ⊢
State after:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
ff : f' (g (z - c)) = f' (z - c)
gz : g (z - c) + c = z
⊢ g (z - c) = z - c

case intro.intro.intro.refine_3.intro.right
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z

State before:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
ff : f' (g (z - c)) = f' (z - c)
gz : g (z - c) + c = z
⊢ g (z - c) = z - c

case intro.intro.intro.refine_3.intro.right
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z
Tactic:
nth_rw 2 [← gz]
State after:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
ff : f' (g (z - c)) = f' (z - c)
gz : g (z - c) + c = z
⊢ g (z - c) = g (z - c) + c - c

case intro.intro.intro.refine_3.intro.right
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z

State before:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
ff : f' (g (z - c)) = f' (z - c)
gz : g (z - c) + c = z
⊢ g (z - c) = g (z - c) + c - c

case intro.intro.intro.refine_3.intro.right
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z
Tactic:
ring
State after:
case intro.intro.intro.refine_3.intro.right
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z

State before:
case intro.intro.intro.refine_3.intro.right
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z
Tactic:
simp only [sub_left_inj, sub_add_cancel, f'] at ff
State after:
case intro.intro.intro.refine_3.intro.right
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f (g (z - c) + c) = f z
⊢ f (g (z - c) + c) = f z

State before:
case intro.intro.intro.refine_3.intro.right
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f (g (z - c) + c) = f z
⊢ f (g (z - c) + c) = f z
Tactic:
exact ff
State after:
no goals

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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
⊢ Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
Tactic:
rw [← sub_self c]
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
⊢ Tendsto (fun z => z - c) (𝓝 c) (𝓝 (c - c))

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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
⊢ Tendsto (fun z => z - c) (𝓝 c) (𝓝 (c - c))
Tactic:
exact continuousAt_id.sub continuousAt_const
State after:
no goals