Obtain/rcases can only eliminate into prop

Stream: new members

[VayusElytra]

Hi, I have this snippet of code:

  have h : ∃ n, (IsCompl (LinearMap.ker (f ^ n)) (range (f ^ n))) := by
    sorry
  obtain ⟨n, h_n⟩ := h

Lean is mad at the 2nd line and says "tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop". What is the proper way to extract n from the hypothesis h then?

[Yaël Dillies]

You should use docs#Exists.choose

[Yaël Dillies]

... along with docs#Exists.choose_spec

[Eric Wieser]

It's unusual to be using obtain to construct data in the first place; what's the context of this "proof"?

[VayusElytra]

I am attempting to write the Fitting lemma in a different form.

theorem ExistsFittingfit (R : Type) [DivisionRing R] (M : ModuleCat R)
  [Module.Finite R M] (f : M →ₗ[R] M)
  : ∃ n, IsIsomorphic ((LinearMap.ker (f ^ n) × range (f ^ n))) M := by
  have h : ∃ n, (IsCompl (LinearMap.ker (f ^ n)) (range (f ^ n))) := by sorry

I have proper code to prove h, but for the purpose of an MWE sorry is sufficient.
After this, I should just need to extract an n that satisfies this condition from h to use it to prove the result.

[Eric Wieser]

obtain will work fine for that example

[Eric Wieser]

Can you provide a #mwe where it fails?

[VayusElytra]

I just tried on my end again, and it does indeed work. Here's the code where it did not, uncensored:

noncomputable def FittingLemma (R : Type) [DivisionRing R] (M : ModuleCat R)
  [Module.Finite R M] (f : M →ₗ[R] M)
  : ((LinearMap.ker (f ^ n) × range (f ^ n)) ≃ₗ[R] M) := by
  have h : ∃ n, (IsCompl (LinearMap.ker (f ^ n)) (range (f ^ n))) := by
    sorry
  obtain ⟨n, h_n⟩ := h
  apply Submodule.prodEquivOfIsCompl (ker (f ^ n)) (range (f ^ n)) (h_n)

I believe the issue is that the statement of the theorem is faulty here. There is an n in it that is completely undefined.

[Eric Wieser]

I recommend using set_option autoImplicit false to avoid that type of mistake

[Eric Wieser]

Ignoring the fact that this is indeed likely mis-stated, the reason for the error here is that this is a def and not a theorem, because ≃ₗ[R] is a Type not a Prop; in that scenario Yael's advice about choose applies.

[VayusElytra]

I think I've run into this issue before. What is the reason to implement isomorphisms as a type and not a prop? (I assume there is probably a Prop version elsewhere...)
I would also be curious to understand the distinction between def/lemma/theorem better. As it stands i am using them mostly like I would in normal maths, but id like to know a little bit more.

[Yury G. Kudryashov]

def produces data. lemma and theorem are the same, they prove statements.

[Yury G. Kudryashov]

We use equivalences in Type*, because sometimes the actual formula matters. E.g., for docs#Equiv.prodAssoc you want to know that the equivalence sends ((a, b), c) to (a, (b, c)), not something else.

[Yury G. Kudryashov]

If you want existence of an isomorphism, then you can use something like Nonempty (α ≃ β).

[Kevin Buzzard]

VayusElytra said:

I think I've run into this issue before. What is the reason to implement isomorphisms as a type and not a prop? (I assume there is probably a Prop version elsewhere...)
I would also be curious to understand the distinction between def/lemma/theorem better. As it stands i am using them mostly like I would in normal maths, but id like to know a little bit more.

"Here is a map which is an isomorphism" is different to "these things happen to be isomorphic". The first is data so it's a def. The second is a true-false statement so it's a theorem. Equivs are concrete isomorphisms so they're defs. Your lemma isn't a lemma, it's not the statement that something is isomorphic to M, it's the data of the isomorphism itself. The phenomenon is like mis-stating the first isomorphism theorem in group theory as "G / kernel is isomorphic to image". That's not what you want, you want "this explicit map from G / kernel to the image is an isomorphism" rather than "an unspecified isomorphism exists".

[VayusElytra]

Thank you, that makes perfect sense.

[Riccardo Brasca]

The Prop-valued version is Nonempty ..., but usually the other one is better.

[VayusElytra]

I stumbled upon another situation where rcases failed, so I'm providing it as an MWE. Choose does work in this instance. (The goal and proofs are dummies).

theorem MWE (R : Type) [DivisionRing R] (M : ModuleCat R) (N : ModuleCat R)
  (θ : M →ₗ[R] N) (x : N) : ℕ = ℕ := by
  have hmem : (∃ z, θ z = x):= by
    sorry
  rcases hmem with z
  --rcases does not give a z that satisfies hmem
  let z := Exists.choose hmem
  have hz : θ z = x := by
    apply Exists.choose_spec hmem
  sorry

[Riccardo Brasca]

Not tested, but does rcases hmem with ⟨z, hz⟩ work?

[VayusElytra]

It does, thank you!