Theorem: eq_of_pow_eq (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 ℂ
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
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

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
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

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 ?_ ?_
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

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]
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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⟩
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

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
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

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]
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

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
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 ℂ
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
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

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]
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

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
⊢ q x ^ d / p x ^ d = 1
Tactic:
rw [div_eq_one_iff_eq]
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

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
⊢ p x ^ d ≠ 0

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
⊢ q x ^ d = p x ^ d
Tactic:
exact (pqd _ m).symm
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 ℂ
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
⊢ p x ^ d ≠ 0
Tactic:
exact pow_ne_zero _ (p0 _ m)
State after:
no goals