giving witness in theorem type

Stream: new members

[tzlil]

def LastExponentMustBeThree {n : ℕ} : IsStrongAchilles n → n.factorization (n.primeFactors.max') ≥ 3 := by sorry

i can provide n.primeFactors.Nonempty since i can prove n != 0 from IsStrongAchilles but how can i provide it in the type here for this definition to work?

[tzlil]

do i need to define e.g nonempty_of_strong_achilles outside and use that in there?

[tzlil]

looks like that works but really i dont need that anywhere else feels pretty silly to do it this way

[Kenny Lau]

@tzlil firstly it's a theorem not a def (very important); secondly there is Finset.sup which is a version that outputs a junk value (the bottom element) for empty input

[tzlil]

is that different from Finset.max that gives WithBot?

[Kenny Lau]

yes, because if you use Finset.max then the result would be in (WithBot Nat), which is not Nat

[tzlil]

that feels slightly unsafe but i will use Finset.sup

[tzlil]

maybe if i rewrite it to .max with the nonempty witness inside the theorem

[Kenny Lau]

tzlil said:

that feels slightly unsafe

well, is 1 strong achilles? :melt:

[tzlil]

@Kenny Lau Finset.sup_mem_of_nonempty is not finding OrderBot for Nat..

[tzlil]

i just wanna get sup \in set

[Kenny Lau]

https://loogle.lean-lang.org/?q=OrderBot+%E2%84%95

[Kenny Lau]

it’s very useful to learn loogle

[Kenny Lau]

you likely dont have the import?