Theorem: dene_eq (Ray/Dynamics/Multibrot/Potential.lean)

State before:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
⊢ dene (z.log.log - k) = (-k).exp * z.log * z ^ (-(-k).exp)
Tactic:
have l0 : 0 < log z := Real.log_pos z1
State after:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
l0 : 0 < z.log
⊢ dene (z.log.log - k) = (-k).exp * z.log * z ^ (-(-k).exp)

State before:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
l0 : 0 < z.log
⊢ dene (z.log.log - k) = (-k).exp * z.log * z ^ (-(-k).exp)
Tactic:
simp only [dene, sub_eq_add_neg, Real.exp_add, Real.exp_log l0, mul_comm _ (exp (-k)), ←neg_mul]
State after:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
l0 : 0 < z.log
⊢ (-k).exp * z.log * (-(-k).exp * z.log).exp = (-k).exp * z.log * z ^ (-(-k).exp)

State before:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
l0 : 0 < z.log
⊢ (-k).exp * z.log * (-(-k).exp * z.log).exp = (-k).exp * z.log * z ^ (-(-k).exp)
Tactic:
apply congr_arg₂ _ rfl
State after:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
l0 : 0 < z.log
⊢ (-(-k).exp * z.log).exp = z ^ (-(-k).exp)

State before:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
l0 : 0 < z.log
⊢ (-(-k).exp * z.log).exp = z ^ (-(-k).exp)
Tactic:
rw [mul_comm, Real.exp_mul, Real.exp_log (by positivity)]
State after:
no goals

State before:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
l0 : 0 < z.log
⊢ 0 < z
Tactic:
positivity
State after:
no goals