Theorem: bottcherNear_eqn (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ bottcherNear f d (f z) = bottcherNear f d z ^ d
Tactic:
simp_rw [bottcherNear]
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ f z * ∏' (n : ℕ), term f d n (f z) = (z * ∏' (n : ℕ), term f d n z) ^ d

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ f z * ∏' (n : ℕ), term f d n (f z) = (z * ∏' (n : ℕ), term f d n z) ^ d
Tactic:
have pe := (term_prod_exists s) z zt
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
pe : ProdExists fun n => term f d n z
⊢ f z * ∏' (n : ℕ), term f d n (f z) = (z * ∏' (n : ℕ), term f d n z) ^ d

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
pe : ProdExists fun n => term f d n z
⊢ f z * ∏' (n : ℕ), term f d n (f z) = (z * ∏' (n : ℕ), term f d n z) ^ d
Tactic:
simp only [mul_pow, product_pow' pe]
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
pe : ProdExists fun n => term f d n z
⊢ f z * ∏' (n : ℕ), term f d n (f z) = z ^ d * ∏' (n : ℕ), term f d n z ^ d

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
pe : ProdExists fun n => term f d n z
⊢ f z * ∏' (n : ℕ), term f d n (f z) = z ^ d * ∏' (n : ℕ), term f d n z ^ d
Tactic:
have pe : ProdExists fun n ↦ term f d n z ^ d := by
  rcases pe with ⟨g, hg⟩; exact ⟨_, product_pow d hg⟩
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
pe✝ : ProdExists fun n => term f d n z
pe : ProdExists fun n => term f d n z ^ d
⊢ f z * ∏' (n : ℕ), term f d n (f z) = z ^ d * ∏' (n : ℕ), term f d n z ^ d

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
pe✝ : ProdExists fun n => term f d n z
pe : ProdExists fun n => term f d n z ^ d
⊢ f z * ∏' (n : ℕ), term f d n (f z) = z ^ d * ∏' (n : ℕ), term f d n z ^ d
Tactic:
simp only [product_split pe, ← term_eqn s, ← mul_assoc, ← mul_pow, ← term_base s]
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
pe : ProdExists fun n => term f d n z
⊢ ProdExists fun n => term f d n z ^ d
Tactic:
rcases pe with ⟨g, hg⟩
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
g : ℂ
hg : HasProd (fun n => term f d n z) g
⊢ ProdExists fun n => term f d n z ^ d

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
g : ℂ
hg : HasProd (fun n => term f d n z) g
⊢ ProdExists fun n => term f d n z ^ d
Tactic:
exact ⟨_, product_pow d hg⟩
State after:
no goals