Set.Finite.induction_on

Stream: Is there code for X?

[Antoine Chambert-Loir]

I was trying to use the induction tactic for docs#Set.Finite.induction_on but couldn't make it work. On the other hand, making the Set argument implicit in that function makes it functional.

import Mathlib.Data.Set.Finite.Basic

@[elab_as_elim]
theorem Set.Finite.my_induction_on {motive : ∀ {s : Set α}, s.Finite → Prop} {s : Set α} (hs : s.Finite)
    (empty : motive (s := ∅) finite_empty)
    (insert : ∀ {a s}, a ∉ s →
      ∀ hs : Set.Finite s, motive hs → motive (s := insert a s) (hs.insert a)) :
    motive hs := by
  lift s to Finset α using id hs
  induction' s using Finset.cons_induction_on with a s ha ih
  · simpa
  · simpa using @insert a s ha (Set.toFinite _) (ih _)

example (s : Set ℕ) (hs : s.Finite) :
    ∃ n, ∀ x ∈ s, x ≤ n := by
  induction hs using Set.Finite.my_induction_on with
  | empty => sorry
  | insert => sorry

[Robin Arnez]

Use induction s, hs using Set.Finite.induction_on with | empty | insert

[Antoine Chambert-Loir]

great! the general syntax is to put all arguments separated by commas?

[Robin Arnez]

Yes, all explicit arguments separated by commas