internlm/Lean-Github huggingface dataset:
Theorem: NontrivialAnalyticOn.const
Proof 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
Proof 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
Theorem: NontrivialAnalyticOn.const
Proof 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
Proof 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})
Theorem: NontrivialAnalyticOn.const
Proof 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
Proof 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}
Theorem: NontrivialAnalyticOn.const
Proof 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]
Proof 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
Theorem: NontrivialAnalyticOn.const
Proof 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
Proof state after:
no goals
Theorem: eq_of_pow_eq
Proof 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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
⊢ ∀ x ∈ t, p x = q x
Tactic:
generalize hr : (fun x ↦ q x / p x) = r
Proof 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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
⊢ ∀ x ∈ t, p x = q x
Theorem: eq_of_pow_eq
Proof 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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
⊢ ∀ x ∈ t, p x = q x
Tactic:
have rc : ContinuousOn r t := by rw [← hr]; exact qc.div pc p0
Proof 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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
⊢ ∀ x ∈ t, p x = q x
Theorem: eq_of_pow_eq
Proof 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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
⊢ ∀ x ∈ t, p x = q x
Tactic:
have h := eq_one_of_pow_eq_one rc tc dp ?_ ?_
Proof state after:
case refine_3
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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
h : ∀ x ∈ t, r x = 1
⊢ ∀ x ∈ t, p x = q x

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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
⊢ ∃ x ∈ t, r x = 1

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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
⊢ ∀ x ∈ t, r x ^ d = 1
Theorem: eq_of_pow_eq
Proof 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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
⊢ ContinuousOn r t
Tactic:
rw [← hr]
Proof 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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
⊢ ContinuousOn (fun x => q x / p x) t
Theorem: eq_of_pow_eq
Proof 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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
⊢ ContinuousOn (fun x => q x / p x) t
Tactic:
exact qc.div pc p0
Proof state after:
no goals
Theorem: eq_of_pow_eq
Proof state before:
case refine_3
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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
h : ∀ x ∈ t, r x = 1
⊢ ∀ x ∈ t, p x = q x
Tactic:
intro x m
Proof state after:
case refine_3
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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
h : ∀ x ∈ t, r x = 1
x : X
m : x ∈ t
⊢ p x = q x
Theorem: eq_of_pow_eq
Proof state before:
case refine_3
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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
h : ∀ x ∈ t, r x = 1
x : X
m : x ∈ t
⊢ p x = q x
Tactic:
rw [← hr] at h
Proof state after:
case refine_3
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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
h : ∀ x ∈ t, (fun x => q x / p x) x = 1
x : X
m : x ∈ t
⊢ p x = q x
Theorem: eq_of_pow_eq
Proof state before:
case refine_3
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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
h : ∀ x ∈ t, (fun x => q x / p x) x = 1
x : X
m : x ∈ t
⊢ p x = q x
Tactic:
exact ((div_eq_one_iff_eq (p0 _ m)).mp (h _ m)).symm
Proof state after:
no goals
Theorem: eq_of_pow_eq
Proof 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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
⊢ ∃ x ∈ t, r x = 1
Tactic:
rcases pq with ⟨x, m, e⟩
Proof state after:
case refine_1.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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
x : X
m : x ∈ t
e : p x = q x
⊢ ∃ x ∈ t, r x = 1
Theorem: eq_of_pow_eq
Proof state before:
case refine_1.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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
x : X
m : x ∈ t
e : p x = q x
⊢ ∃ x ∈ t, r x = 1
Tactic:
use x, m
Proof state after:
case right
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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
x : X
m : x ∈ t
e : p x = q x
⊢ r x = 1
Theorem: eq_of_pow_eq
Proof state before:
case right
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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
x : X
m : x ∈ t
e : p x = q x
⊢ r x = 1
Tactic:
rw [← hr]
Proof state after:
case right
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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
x : X
m : x ∈ t
e : p x = q x
⊢ (fun x => q x / p x) x = 1
Theorem: eq_of_pow_eq
Proof state before:
case right
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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
x : X
m : x ∈ t
e : p x = q x
⊢ (fun x => q x / p x) x = 1
Tactic:
exact (div_eq_one_iff_eq (p0 _ m)).mpr e.symm
Proof state after:
no goals
Theorem: eq_of_pow_eq
Proof 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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
⊢ ∀ x ∈ t, r x ^ d = 1
Tactic:
intro x m
Proof 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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
x : X
m : x ∈ t
⊢ r x ^ d = 1
Theorem: eq_of_pow_eq
Proof 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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
x : X
m : x ∈ t
⊢ r x ^ d = 1
Tactic:
simp only [div_pow, ← hr]
Proof 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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
x : X
m : x ∈ t
⊢ q x ^ d / p x ^ d = 1