!4#3392

Stream: mathlib4

[Eric Rodriguez]

there's a weird issue that I can't seem to fix, I can't do @this in lean4 it seems or use named arguments, but the TC problem gets stuck - what's the right way to resolve this? otherwise this file is super chill

[Eric Rodriguez]

I just fixed this with the horrific hack:

    rename ∀ _ : Type _, _ => h2 -- horrific hack
    have := @h2 E _ _ F
    exact this u b a hb ha h (le_of_not_le hab)

please tell me there's a better way to do this - why can't I do @this specifically?

[Eric Rodriguez]

(this was given by wlog I think, not sure if there's a way to edit that)

[Thomas Murrills]

wlog h : P with H will use H instead of this—does @H work?

[Eric Rodriguez]

that worked, Thomas, many thanks!

[Eric Rodriguez]

is there still a lean4 issues memorandum or not? I still think it's worth reporting

[Eric Rodriguez]

(sorry, I've taken a backseat lately with Lean stuff)