Timeout in `set .. with`

Stream: mathlib4

[Yury G. Kudryashov]

In !4#4912, if you add with hg to set in line https://github.com/leanprover-community/mathlib4/pull/4912/files#diff-6f2f772b41622ce6d9a4dc922f7e26f8aeb129f555c3aa567f4a386979db4acdR156, then Lean timeouts.

[Yury G. Kudryashov]

The same happens if you uncomment, e.g., line 160

[Yury G. Kudryashov]

Minimizing.

[Alex J. Best]

I already started doing the same
got to

theorem horizontal_strip
    (hB : ∃ c < π / (b - a), ∃ B,
       c = B)
     : ‖f z‖ ≤ C := by
  -- If `im z = a` or `im z = b`, then we apply `hle_a` or `hle_b`, otherwise `im z ∈ Ioo a b`.
  -- After a change of variables, we deal with the strip `a - b < im z < a + b` instead
  -- of `a < im z < b`
  -- Choose some `c B : ℝ` satisfying `hB`, then choose `max c 0 < d < π / 2 / b`.
  rcases hB with ⟨c, hc, B, hO⟩
  obtain ⟨d, hd⟩ : ∃ d, c < d := by
    sorry
  set aff : ℂ → ℂ := fun w => 1
  set g : ℝ → ℂ → ℂ := fun ε w => exp (ε * (exp (aff w) + exp (-aff w))) with h

so far

[Yury G. Kudryashov]

I've got

import Mathlib.Data.Complex.Basic

open Complex

variable {a b d B C : ℝ} {z : ℂ} {exp : ℂ → ℂ}

example : 1 = 2 := by
  set aff : ℂ → ℂ := fun w => d * (w - a * I)
  set g : ℝ → ℂ → ℂ := fun ε w => exp (ε * (exp (aff w) + exp (-aff w))) with hg

[Alex J. Best]

edited:

example : 1 = 2 := by
  set g : ℝ →  ℂ  := (fun ε => ε) with h

[Yury G. Kudryashov]

Your example fails with type mismatch

[Yury G. Kudryashov]

Adding fun (ε : ℝ) (w : ℂ) helps with your example. Trying in the original source.

[Yury G. Kudryashov]

Works!

[Yury G. Kudryashov]

Probably, set parses RHS without expected type

[Yury G. Kudryashov]

(and in Lean 3 it used the expected type)

[Alex J. Best]

!4#4917, lets see if anything breaks with this change

[Yury G. Kudryashov]

Note that sometimes set fails too (with "type mismatch" error)

[Yury G. Kudryashov]

I had to move type information from left to right here and there.

[Alex J. Best]

I finally finished the above PR, please say if you find more distinct issues. Do you have an example of this type mismatch error I can look at?

[Yury G. Kudryashov]

A very non-minimal example: if you remove type annotations on the right in sets in src4#PhragmenLindelof.horizontal_strip, then the proof timeouts.

[Yury G. Kudryashov]

Even if you move them to the LHS

[Yury G. Kudryashov]

If you replace line 154 with

set g : ℝ → ℂ → ℂ := fun ε w => exp (ε * (exp (aff w) + exp (-aff w)))

then it timeouts, even if you comment out everything after line 157

[Alex J. Best]

#5386 should fix this :fingers_crossed:

[Yury G. Kudryashov]

Thanks a lot!