Error with rcases

Stream: maths

[Esteban Martínez Vañó]

Hi everyone.

I have the following code:

class DirectedSet (D: Type*) extends Preorder D, Inhabited D, IsDirected D (fun d d' ↦ d ≤ d')

def DirectedSetFA {X: Type*} (F: Filter X) (A: Set X) (_: A ∈ F) := {P : X × Set X | P.1 ∈ P.2 ∧ P.2 ∈ F ∧ P.2 ⊆ A}

instance DirectedSetFA.isntDirectedSet {X: Type*} (F: Filter X) [Filter.NeBot F] (A: Set X) (h: A ∈ F) : DirectedSet (DirectedSetFA F A h) where
  le := fun P Q ↦ Q.1.2 ⊆ P.1.2
  le_refl := by
    intro P x xin
    exact xin
  le_trans := by
    intro P Q R PleQ QleR
    apply subset_trans QleR PleQ
  default := by
    have : A ≠ ∅ := by
      intro Aempty
      have := empty_not_mem F
      rw [← Aempty] at this
      contradiction
    rw [← nonempty_iff_ne_empty, nonempty_def] at this
    sorry
  directed := by
    intro P Q
    have : P.1.2 ∩ Q.1.2 ∈ F := by
      exact inter_mem (P.2.2.1) (Q.2.2.1)
    have : ∃ (x: X), x ∈ P.1.2 ∩ Q.1.2 := by
      exact Eventually.exists this
    rcases this with ⟨x, xininter⟩
    have : (x, P.1.2 ∩ Q.1.2) ∈ DirectedSetFA F A h := by
      simp only [DirectedSetFA, Set.mem_setOf_eq]
      constructor
      · assumption
      · constructor
        · assumption
        · intro x xininter
          apply P.2.2.2
          exact xininter.1
    use ⟨(x, P.1.2 ∩ Q.1.2), this⟩
    constructor
    · exact Set.inter_subset_left
    · exact Set.inter_subset_right

In palce of the sorry I'd like to put an rcases this with ... that will conclude my proof but when I do it I get the following error:

tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop

What is going on? It is the first time that has happened to me. Can it be fixed in any way? If not, how can I conclude my proof?

Thanks in advance

[Etienne Marion]

You know that some object exists, but to actually build such an object you need the axiom of choice, because otherwise you can't build some data out of nothing. That's why it says the recursor can only eliminate into Prop, it's because if you want to use the object without axiom of choice you can only do it to prove something, but not to build something.
Anyway to get around this you can use docs#Exists.choose and docs#Exists.choose_spec.

[Etienne Marion]

This is well explained in Theorem Proving in Lean 4, in chapter 12 (though you may also need chapter 7 to understand it).

[Esteban Martínez Vañó]

Okay, now everything makes sense. I've used Classical.choose and Classical.choose_spec before, but not in this context and that was confusing.

[Esteban Martínez Vañó]

And, I get the difference. I know why we need to use some choice in this context. Thanks!