Golfing a have in !4#4738

Stream: mathlib4

[Jeremy Tan]

!4#4738 This works, but is there a way to prove h₁ (with a real 3 exponent) in one line? I can't see the theorems that norm_cast used

theorem deriv2_sqrt_mul_log (x : ℝ) :
    (deriv^[2]) (fun x => sqrt x * log x) x = -log x / (4 * sqrt x ^ 3) := by
  simp only [Nat.iterate, deriv_sqrt_mul_log']
  cases' le_or_lt x 0 with hx hx
  · rw [sqrt_eq_zero_of_nonpos hx]
    norm_num
    refine' HasDerivWithinAt.deriv_eq_zero _ (uniqueDiffOn_Iic 0 x hx)
    refine' (hasDerivWithinAt_const _ _ 0).congr_of_mem (fun x hx => _) hx
    rw [sqrt_eq_zero_of_nonpos hx, MulZeroClass.mul_zero, div_zero]
  · have h₀ : sqrt x ≠ 0 := sqrt_ne_zero'.2 hx
    convert (((hasDerivAt_log hx.ne').const_add 2).div ((hasDerivAt_sqrt hx.ne').const_mul 2) <|
      mul_ne_zero two_ne_zero h₀).deriv using 1
    nth_rw 3 [← mul_self_sqrt hx.le]
    have := pow_ne_zero 3 h₀
    have h₁ : sqrt x ^ 3 ≠ 0 := by norm_cast
    field_simp; norm_cast; ring

[Jeremy Tan]

Note that in pow_ne_zero 3 h₀ the 3 is natural

[Damiano Testa]

have h₁ : sqrt x ^ 3 ≠ 0 := ne_of_eq_of_ne (rpow_nat_cast (sqrt x) 3) (pow_ne_zero 3 h₀)

seems to work. I am not sure that this is really better, though.

[Jireh Loreaux]

@Jeremy Tan that 3 should have type ℕ, see docs#deriv2_sqrt_mul_log. You need the HPow local macro hack.

[Jireh Loreaux]

In general, if you see things that are naturals in powers that are being coerced to ℝ, there's a good chance lean4#2220 is to blame.

[Jeremy Tan]

Then why are you not fixing this now?

[Ruben Van de Velde]

Probably for much of the same reasons you aren't

[Jireh Loreaux]

Because you're working on the file? I'm in the middle of my own projects; it would be inconvenient for me to switch branches, pull, cache, change and push, not to mention the fact that the PR is not marked as help-wanted. There's a separation of responsibilities.

[Jeremy Tan]

I meant lean4#2220

[Jeremy Tan]

I've read the comments and there are a few nice proposals there

[Jireh Loreaux]

Again, separation of responsibilities (and authority). This is a Lean 4 core issue, and I have essentially no experience there. I trust others who are more comfortable in that space to handle it at some point. Maybe I will eventually get comfortable making PRs to Lean 4 core, but I don't feel a strong impetus to do so right now.

[Jeremy Tan]

I admit I did put the hack in one of my other PRs

[Jireh Loreaux]

That's the right approach for the moment. It preserves the intended declaration from mathlib3, and as long as you leave a porting note referencing lean4#2220, it can easily be removed when that issue is fixed.

[Jeremy Tan]

...though I had not included the hack when I started working on !4#4738, so I've re-ported the file properly at !4#4746

[Jeremy Tan]

With the hack the haves indeed disappear