Theorem: NontrivialHolomorphicAt.anti (Ray/AnalyticManifold/Nontrivial.lean)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
h : NontrivialHolomorphicAt (fun z => f (g z)) z
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
⊢ NontrivialHolomorphicAt f (g z) ∧ NontrivialHolomorphicAt g z
Tactic:
replace h := h.nonconst
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
⊢ NontrivialHolomorphicAt f (g z) ∧ NontrivialHolomorphicAt g z

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
⊢ NontrivialHolomorphicAt f (g z) ∧ NontrivialHolomorphicAt g z
Tactic:
refine ⟨⟨fa, ?_⟩, ⟨ga, ?_⟩⟩
State after:
case refine_1
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
⊢ ∃ᶠ (w : T) in 𝓝 (g z), f w ≠ f (g z)

case refine_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
⊢ ∃ᶠ (w : S) in 𝓝 z, g w ≠ g z

State before:
case refine_1
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
⊢ ∃ᶠ (w : T) in 𝓝 (g z), f w ≠ f (g z)
Tactic:
contrapose h
State after:
case refine_1
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ¬∃ᶠ (w : T) in 𝓝 (g z), f w ≠ f (g z)
⊢ ¬∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)

State before:
case refine_1
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ¬∃ᶠ (w : T) in 𝓝 (g z), f w ≠ f (g z)
⊢ ¬∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
Tactic:
simp only [Filter.not_frequently, not_not] at h ⊢
State after:
case refine_1
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ∀ᶠ (x : T) in 𝓝 (g z), f x = f (g z)
⊢ ∀ᶠ (x : S) in 𝓝 z, f (g x) = f (g z)

State before:
case refine_1
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ∀ᶠ (x : T) in 𝓝 (g z), f x = f (g z)
⊢ ∀ᶠ (x : S) in 𝓝 z, f (g x) = f (g z)
Tactic:
exact (ga.continuousAt.eventually h).mp (eventually_of_forall fun _ h ↦ h)
State after:
no goals

State before:
case refine_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
⊢ ∃ᶠ (w : S) in 𝓝 z, g w ≠ g z
Tactic:
contrapose h
State after:
case refine_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ¬∃ᶠ (w : S) in 𝓝 z, g w ≠ g z
⊢ ¬∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)

State before:
case refine_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ¬∃ᶠ (w : S) in 𝓝 z, g w ≠ g z
⊢ ¬∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
Tactic:
simp only [Filter.not_frequently, not_not] at h ⊢
State after:
case refine_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ∀ᶠ (x : S) in 𝓝 z, g x = g z
⊢ ∀ᶠ (x : S) in 𝓝 z, f (g x) = f (g z)

State before:
case refine_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ∀ᶠ (x : S) in 𝓝 z, g x = g z
⊢ ∀ᶠ (x : S) in 𝓝 z, f (g x) = f (g z)
Tactic:
exact h.mp (eventually_of_forall fun x h ↦ by rw [h])
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h✝ : ∀ᶠ (x : S) in 𝓝 z, g x = g z
x : S
h : g x = g z
⊢ f (g x) = f (g z)
Tactic:
rw [h]
State after:
no goals