Theorem: NontrivialAnalyticOn.const (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 ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
p1 : ∃ x ∈ t, p x = a
fp : ∀ x ∈ t, f (p x) = b
⊢ ∀ x ∈ t, p x = a
Tactic:
have disc : DiscreteTopology (↥(s ∩ f ⁻¹' {b})) := n.discreteTopology b
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 ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
p1 : ∃ x ∈ t, p x = a
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
⊢ ∀ x ∈ t, p x = a

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 ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
p1 : ∃ x ∈ t, p x = a
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
⊢ ∀ x ∈ t, p x = a
Tactic:
rcases p1 with ⟨z, zt, z1⟩
State after:
case intro.intro
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 ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
z : X
zt : z ∈ t
z1 : p z = a
⊢ ∀ x ∈ t, p x = a

State before:
case intro.intro
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 ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
z : X
zt : z ∈ t
z1 : p z = a
⊢ ∀ x ∈ t, p x = a
Tactic:
simp only [← z1]
State after:
case intro.intro
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 ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
z : X
zt : z ∈ t
z1 : p z = a
⊢ ∀ x ∈ t, p x = p z

State before:
case intro.intro
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 ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
z : X
zt : z ∈ t
z1 : p z = a
⊢ ∀ x ∈ t, p x = p z
Tactic:
intro x xt
State after:
case intro.intro
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 ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
z : X
zt : z ∈ t
z1 : p z = a
x : X
xt : x ∈ t
⊢ p x = p z

State before:
case intro.intro
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 ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
z : X
zt : z ∈ t
z1 : p z = a
x : X
xt : x ∈ t
⊢ p x = p z
Tactic:
refine @IsPreconnected.constant_of_mapsTo _ _ _ _ _ tc _ disc _ pc ?_ _ _ xt zt
State after:
case intro.intro
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 ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
z : X
zt : z ∈ t
z1 : p z = a
x : X
xt : x ∈ t
⊢ MapsTo p t (s ∩ f ⁻¹' {b})

State before:
case intro.intro
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 ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
z : X
zt : z ∈ t
z1 : p z = a
x : X
xt : x ∈ t
⊢ MapsTo p t (s ∩ f ⁻¹' {b})
Tactic:
intro y yt
State after:
case intro.intro
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 ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
z : X
zt : z ∈ t
z1 : p z = a
x : X
xt : x ∈ t
y : X
yt : y ∈ t
⊢ p y ∈ s ∩ f ⁻¹' {b}

State before:
case intro.intro
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 ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
z : X
zt : z ∈ t
z1 : p z = a
x : X
xt : x ∈ t
y : X
yt : y ∈ t
⊢ p y ∈ s ∩ f ⁻¹' {b}
Tactic:
simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff]
State after:
case intro.intro
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 ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
z : X
zt : z ∈ t
z1 : p z = a
x : X
xt : x ∈ t
y : X
yt : y ∈ t
⊢ p y ∈ s ∧ f (p y) = b

State before:
case intro.intro
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 ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
z : X
zt : z ∈ t
z1 : p z = a
x : X
xt : x ∈ t
y : X
yt : y ∈ t
⊢ p y ∈ s ∧ f (p y) = b
Tactic:
use ps yt, fp _ yt
State after:
no goals