obtain with holes

Stream: mathlib4

[Yury G. Kudryashov]

In Lean 3, one can write

  obtain ⟨x, hx⟩ := my_lemma f _

and get to goals: one for the main state after obtain and one for filling in the hole _. In Lean 4, there is only 1 goal and the proof is broken.

[Yakov Pechersky]

does my_lemma f ?_ work for you here?

[Heather Macbeth]

I've encountered this too.

[Yury G. Kudryashov]

No

[Yury G. Kudryashov]

For now, I do the following:

1. replace obtain with have to see the types of the holes.
2. Prove the holes before have.
3. Bring back obtain.

[Yury G. Kudryashov]

It would be nice to have ?_. @Mario Carneiro Is this another withMainContext? From what you say, I have an impression that it usually is.

[Mario Carneiro]

Can you make a MWE?

[Yury G. Kudryashov]

Can't make it "loose" the goal yet. Here is an #mwe that forces me to supply _ right away without a syntax to postpone it:

import Std.Tactic.RCases

namespace mwe_obtain

theorem aux (b : Bool) (hb : b ≠ true) : ∃ b', b' = b ∧ b' ≠ true :=
  ⟨b, rfl, hb⟩

example (b : Bool) (hb : b ≠ true) : ∃ b', b' ≠ true := by
  rcases aux b _ with ⟨b', -, hb'⟩
  exact ⟨b', hb'⟩

[Heather Macbeth]

Here's an example of this I hit quite early in the port, if it helps:
https://github.com/leanprover-community/mathlib4/blob/526ab32ac62f3b2a9004d911c7ead5f3468d13ed/Mathlib/Order/Zorn.lean#L216

[Mario Carneiro]

Note: the general pattern here is that any tactic which elaborates a term (and there are a lot of them) has to explicitly collect subgoals from the result and append them after the main tactic results, or else it will have the same no-defer behavior as exact

[Mario Carneiro]

I looked into this, and it looks like this cannot easily be implemented in RCases because the required function elabTermWithHoles is in TacticM while the main elaboration of rcases is in TermElabM. I think this would need a change to lean4 core

[Yury G. Kudryashov]

I'll try to find an example when it makes the goals disappear.

[Mario Carneiro]

note that cases also does not support this, or interval_cases or a long list of other tactics

[Mario Carneiro]

you should not get dropped goals though

[Mario Carneiro]

refine (or things that macro expand to it) is basically the only tactic that supports ?_ -> subgoals

[Yury G. Kudryashov]

A non-minimal example: in !4#2157, if you change the proof of exists_of_compact to

theorem exists_of_compat [CompactSpace X] (Qs : (Q : DiscreteQuotient X) → Q)
    (compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLe h (Qs _) = Qs _) :
    ∃ x : X, ∀ Q : DiscreteQuotient X, Q.proj x = Qs _ := by
  obtain ⟨x, hx⟩ : (⋂ Q, proj Q ⁻¹' {Qs Q}).Nonempty :=
    IsCompact.nonempty_interᵢ_of_directed_nonempty_compact_closed
      (fun Q : DiscreteQuotient X => Q.proj ⁻¹' {Qs _}) (directed_of_inf fun A B h => _)
      (fun Q => (singleton_nonempty _).preimage Q.proj_surjective)
      (fun i => (isClosed_preimage _ _).isCompact) fun i => isClosed_preimage _ _
  · refine' ⟨x, fun Q => _⟩
    exact hx _ ⟨Q, rfl⟩
  · rw [← compat _ _ h]
    exact fiber_subset_of_le _ _

then the first obtain looses a goal.

[Yury G. Kudryashov]

The non-filled in _ is in directed_of_inf fun A B h => _

[Jireh Loreaux]

I ran into this also. It would be great if we could come up with a fix (aside from Yury's have then obtain workaround).

[Jireh Loreaux]

Oh actually, I misread Yury's workaround and found another. This works and requires minimal changes to the proof.

have := expression_with_holes ?_ -- this gives us the goal we need.
obtain ⟨pattern⟩ := this