aesop can prove FLT

Stream: general

[Eric Wieser]

import Mathlib

-- we don't mention this in the proof, so we can ignore it
variable {not_used : False}

omit not_used in
def ohno : PLift FermatLastTheorem :=
  ⟨by aesop⟩

[Eric Wieser]

Should by have the "don't capture any more variables" semantics that theorem has?

[Alex Meiburg]

No need for Mathlib here:

-- we don't mention this in the proof, so we can ignore it
variable {not_used : False}

omit not_used

def ohno : PLift FermatLastTheorem := by
  exact? --suggests `exact not_used.elim`, which also works

This seems like omit doesn't do what it says on the box, it doesn't remove variables for defs.

[Eric Wieser]

You need mathlib for docs#FermatLastTheorem

[Aaron Liu]

I've not been able to get omit to do what I want it to do yet. Every time I use it to omit something, the something doesn't get omitted

[Alex Meiburg]

Eric Wieser said:

You need mathlib for docs#FermatLastTheorem

Yeah, I know it's autoimplicit, but that's kind of not the point right? The point is that we pull in this variable that 'should' be omitted

[Sebastian Ullrich]

That's a variant of lean#5595: omit currently only undoes include