Induction starting not at the bottom

Stream: general

[Chase Meadors]

Is there an easy way to perform induction with a "different starting element"? (easy = without writing a lemma :wink: ). Perhaps some way to leverage the existing induction theorem?
In my case, I want to prove something about nonempty finsets. Namely, that finite sup in a directed set stays in the directed set:

lemma test {α : Type} [decidable_eq α] [complete_lattice α] (S : set α) (hdir : directed_on (≤) S)
  (F : finset α) (hemp : F.nonempty) (hF : ↑F ⊆ S) : F.sup id ∈ S :=

I'd love to start with

apply finset.induction F,

but alas, this is only necessarily true for nonempty finsets.
I've had the same case before when wanting to prove something about positive naturals, so I thought I'd ask for some tips.

[Kevin Buzzard]

You can probably just use the usual induction principle in any given case. Or you can just write your own and apply it. Why do you think the usual induction principle won't work for you? I think that all other induction principles are derived from it, in some sense. What happens after applying finset.induction? The base case should be provable by contradiction, no?

[Chase Meadors]

Well, the base case here needs ⊥ ∈ S, which I have no reason to assume for an arbitrary directed set S. But, I think I see what you're saying - namely a "custom" induction principle will not be hard to write since it can simply use the regular one?

[Mario Carneiro]

You just prove by induction that ⊥ ∈ S -> P S

[Mario Carneiro]

the implication ensures that the case S = ⊥ is vacuously true

[Chase Meadors]

Ah, that's perfect! I had tried something like that in proving the implication F.nonempty -> F.sup id in S by induction, but rather your proposition is what I need. Thanks!
Well, wait, this would still ensure I need bottom in S anywhere to apply it...