Stuck on fun in hypothesis

Stream: new members

[Anders Larsson]

import Mathlib.Data.Complex.Basic

example (a b a' b' : ℂ) (h : (fun z => a * z + b) = fun z => a' * z + b') : a = a' := by

admit

I somewhat would like to do funext backwards and work with special cases where z=0 and z=1.

[Yaël Dillies]

That's called docs#congr_fun. Do have := congr_fun h 0; have := congr_fun h 1.

[Yaël Dillies]

You can also use the congr() elaborator by doing have := congr($h 0); have := congr($h 1)

[Anders Larsson]

Thank you, that was helpful.

import Mathlib.Data.Complex.Basic

example (a b a' b' : ℂ) (h : (fun z => a * z + b) = fun z => a' * z + b') : a = a' := by
apply congr_fun at h
have hb: b = b' := by
  specialize h 0
  simp at h; exact h
rw [hb] at h
specialize h 1
simp at h
exact h

[Yaël Dillies]

Note you can replace

have hb: b = b' := by
  ...
rw [hb] at h

by

obtain rfl : b = b' := by
  ...

[Anders Larsson]

That works like a charm, but I had a hard time finding documentation about 'obtain'.

I guess this is it:
https://leanprover-community.github.io/mathlib4_docs/Init/RCases.html#Lean.Parser.Tactic.obtain

But being part of the parser could maybe explain why there are no hovering help over 'obtain' like it it is for other tactics.

[Yaël Dillies]

No, that's a bug. Can you please open an issue?

[Anders Larsson]

Sure, like this?
https://github.com/leanprover-community/lean4web/issues/26

[Yaël Dillies]

Oh I believe this is more of a Lean 4 issue, not lean4web

[Anders Larsson]

I can indeed reproduce the issue in Visuas Studio.

[Anders Larsson]

I updated the issue with a smaller example. It seems to be the := that kills the hover help . I think that is as much as I have skills to contribute with at the moment.

example  : True := by
obtain h: True := by  -- Hovering over obtain unexpectedly displays "True"
admit

example (a: Prop) : a -> a := by
obtain h: 3 = 3 -- Hovering over obtain displays useful help "The obtain tactic is a combination..."
admit