error with obtain

Stream: mathlib4

[Madison Crim]

I'm trying to prove the second noncomputable def, however I keep getting the following error with obtain: tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop. However, I'm not getting this error with the first noncomputable def. I am only using the first one to try to get the obtain to work. I'm not sure why one would work, but not the other.

universe u
variable {R : Type u} [CommRing R]
variable {ι : Type u}
variable {N : ι → Type u} [∀ i, AddCommMonoid (N i)] [∀ i, Module R (N i)]
variable {M : Type u} [AddCommGroup M] [Module R M]

noncomputable def test  [Module.FinitePresentation R M] : Module.FinitePresentation R M := by
  have hfpB : Module.FinitePresentation R M := inferInstance
  obtain ⟨L, hL, fL, K, hK, hFree, hFinite, hFG⟩ := Module.FinitePresentation.equiv_quotient R M
  sorry

noncomputable def tensorProdEquiv [Module.FinitePresentation R M] :
  M ⊗[R] (∀ i, N i) ≃ₗ[R] ∀ i, (M ⊗[R] N i) := by
    have hfpB : Module.FinitePresentation R M := inferInstance
    obtain ⟨L, hL, fL, K, hK, hFree, hFinite, hFG⟩ := Module.FinitePresentation.equiv_quotient R M
    sorry

[Junyan Xu]

The first is a Prop and you should use lemma rather than def for it.
For the second you need to use the choose tactic.

[Madison Crim]

Yes, I originally had it as a theorem, but I thought maybe it being a noncomputable def was the issue. Using choose worked thank you. Do you know why obtain wouldn't work here?

[Junyan Xu]

You might want to read this starting from Large elimination. What's happening in the first example is small elimination.

[Madison Crim]

Thank you!

[Kevin Buzzard]

As you can probably imagine, when you're writing Lean tactics, Lean is secretly making some function piece by piece -- the goals that you see in tactic mode are the holes where the definition is incomplete. The cases, obtain, induction etc etc tactics are secretly applying functions called recursors, which are made automatically whenever the user creates an inductive type. For example this code

inductive MyNat : Type
| zero : MyNat
| succ : MyNat -> MyNat

creates a new type MyNat, a new term MyNat.zero of this type, a new function MyNat.succ from MyNat to MyNat, and a secret fourth thing MyNat.rec which is the principle of recursion and induction (it works for types and props, because it has Sort u as its conclusion, and Sort u means "either Prop or Type u").

import Mathlib

inductive MyNat : Type
| zero : MyNat
| succ : MyNat -> MyNat

#check @MyNat.rec
/-
@MyNat.rec : {motive : MyNat → Sort u_1} →
  motive MyNat.zero → ((a : MyNat) → motive a → motive a.succ) → (t : MyNat) → motive t

i.e.

"for any function `motive` from the naturals to propositions or types, if you can make
`motive 0`, and also `motive (n+1)` given a term of type `motive n`, then
you can make terms of type `motive t` for any natural t"
-/

If you have some goal which is a proposition involving n : MyNat, then induction n basically does apply MyNat.rec,
lets t be n, fills in the last goal and opens two new goals corresponding to the inputs of MyNat.rec which are the zero case and the succ case.

If you look at Exists.rec though, it says something a bit different:

#check Exists.rec
/-
Exists.rec.{u} {α : Sort u} {p : α → Prop} {motive : Exists p → Prop} (intro : ∀ (w : α) (h : p w), motive ⋯)
  (t : Exists p) : motive t
-/

The motive only takes values in Prop. This means in practice that if your goal isn't a theorem statement, then cases h/obtain ... := h/induction h won't work if h : \exists x, p x because Lean can't make the relevant function which tactic mode makes because things don't match up. The reason the recursor only takes values in Prop is basically because Exists itself is a Prop,
and moving from the Prop universe to the Type universe is fraught with danger in type theory; you allow it to happen and your theory can become inconsistent. Moving from Prop to Type is exactly what the type theory axiom of choice does, but this is an extra axiom in Lean's theory.