Equality subgoal

Stream: lean4

[Robin Green]

For some reason I am unable to state an equality subgoal using the have tactic - I keep getting syntax errors. Other kinds of subgoals work fine with have. I even rewrote it as Eq a b instead of a = b but that didn't help! This is with hierarchical bullets.

[Kyle Miller]

Could you make some working example that illustrates the error? (#mwe has some pointers)

[Robin Green]

import Mathlib.Logic.Equiv.Defs

theorem foo : String.Pos.Valid { data := c :: cs } (e - i) -> String.Pos.Valid { data := cs } (e - (i + c)) := by
  simp [String.Pos.Valid]
  intros s s1 seq h1
  cases s
  . case nil =>
      admit

  . case cons h t =>
      exists t
      constructor
      . case left =>
          admit

      . case right =>
          have h2 : h = c
          . case h2 =>
              injection seq
          . case blah =>
              admit

I am getting unexpected token '.'; expected '|' from Lean 4.5.0 after the have line.

[Kyle Miller]

Without mathlib tactics, the only have available is the have h2 : h = c := ... form (that ... could be by ... for example).

If you add import Mathlib.Tactic you'll get the one you want. You can do import Mathlib.Tactic.Have if you just want this tactic.