Using modus ponens inside a definition

Stream: new members

[Hyunsang Hwang]

I am not sure if this is a duplicate of https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/modus.20ponens.20in.20context

I am currently trying to make the following definition:

import Mathlib
variable (R: Type)[commsemiring: CommSemiring R]

lemma temp (r : (α →₀ ℕ) → (α →₀ ℕ) → Prop) (pol: MvPolynomial α R)[DecidableRel r]
[IsTrans (α →₀ ℕ) r] [IsAntisymm (α →₀ ℕ) r] [IsTotal (α →₀ ℕ) r] [nonzero : NeZero pol]
[DecidableEq (α →₀ ℕ)] : Finset.sort r (MvPolynomial.support pol) ≠ []:= by
  simp
  rw [←List.toFinset_eq_empty_iff, Finset.sort_toFinset]
  simp
  apply nonzero.out

def MvPolynomial.leading_mon (r : (α →₀ ℕ) → (α →₀ ℕ) → Prop) [DecidableRel r]
[IsTrans (α →₀ ℕ) r] [IsAntisymm (α →₀ ℕ) r] [IsTotal (α →₀ ℕ) r] (pol: MvPolynomial α R)
[nonzero : NeZero pol]: (α →₀ ℕ) :=
  List.getLast (Finset.sort r (MvPolynomial.support pol))
/-type mismatch
  List.getLast (Finset.sort r (support pol))
has type
  Finset.sort r (support pol) ≠ [] → α →₀ ℕ : Type ?u.6465
but is expected to have type
  α →₀ ℕ : Type ?u.6465-/

Is there a way I can use temp to modify the shape of List.getLast (Finset.sort r (support pol))?

[Eric Wieser]

The error message is telling you that you forgot to pass the last argument to getLast

[Eric Wieser]

Put a _ at the end of the last line, and lean will stop giving you an error and start telling you what to do

[Notification Bot]

This topic was moved here from #Is there code for X? > Using modus ponens inside a definition by Eric Wieser.

[Eric Wieser]

If you ever see an error message that says "has type A → B but expected to have type B", that means you wrote foo x y instead of foo x y a. If you don't yet know the a, write foo x y _.

[Hyunsang Hwang]

Thank you

[Notification Bot]

Hyunsang Hwang has marked this topic as resolved.

[Notification Bot]

Brendan Seamas Murphy has marked this topic as unresolved.