Phantom sorry

Stream: lean4

[Chris Birkbeck]

I've just come across what seems to be a bug. I have a lemma saying it uses sorry, but there are no sorries in sight. Here is my MWE

import Mathlib.Analysis.Complex.UpperHalfPlane.Basic
import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

open Complex UpperHalfPlane

noncomputable abbrev csqrt : ℂ → ℂ := fun a => cexp ((1 / 2) * log a)

lemma upperHalfPlane_mem_slitPlane (z : ℍ) : (z : ℂ) ∈ slitPlane := by
  simp only [slitPlane, Set.mem_setOf_eq]
  right
  exact im_ne_zero z

lemma csqrt_differentiableAt (z : ℂ) (hz : z ∈ slitPlane) : DifferentiableAt ℂ csqrt z := by
  exact DifferentiableAt.cexp (DifferentiableAt.const_mul (differentiableAt_log hz) (1 / 2))

lemma test (z : ℍ) :  DifferentiableAt ℂ csqrt z  := by
   apply csqrt_differentiableAt upperHalfPlane_mem_slitPlane


#print axioms upperHalfPlane_mem_slitPlane  -- clean
#print axioms csqrt_differentiableAt        -- clean
#print axioms test                          -- sorryAx!

[Eric Wieser]

This might be #lean4 > optConfig causes tactics to be ignored

[Chris Birkbeck]

Ah yes that looks like it, thanks!

[Snir Broshi]

btw splitting the apply in 2 works:

lemma test (z : ℍ) :  DifferentiableAt ℂ csqrt z  := by
  apply csqrt_differentiableAt
  apply upperHalfPlane_mem_slitPlane

[Chris Birkbeck]

yeah and also exact csqrt_differentiableAt z (upperHalfPlane_mem_slitPlane z) but I was mainly curious about the bug, but I'm glad a fix seems to be on the way.