How to use Finset.Nonempty.cons_induction in induction using

Stream: new members

[Kevin Cheung]

I have the following which works:

import Mathlib.Algebra.BigOperators.Basic

open BigOperators
open Finset

def p := fun (T : Finset ℕ) ↦ fun (_ : T.Nonempty) ↦ (∀ s ∈ T, s > 0) → (∑ s in T, s) > 0

example (T : Finset ℕ) (g : T.Nonempty) : p T g := by
  apply Nonempty.cons_induction
  . simp [p]
  . intro a s
    intro a' hs ih
    simp [p]
    intro a'' _
    have : ∑ x in insert a s, x = a + ∑ x in  s, x  := by exact sum_insert a'
    rw [this]
    simp [p] at ih
    exact Nat.add_pos_left a'' (∑ x in s, x)

It seems to me that apply Nonempty.cons_induction can be replaced with induction...using. My attempt is

example (T : Finset ℕ) (g : T.Nonempty) : p T g := by
  induction g using Nonempty.cons_induction with
  | _ a => sorry

But I have a feeling that this is wrong. First, g is not a set so the induction on g doesn't seem to make sense. But putting T there gives the error
target T has type Finset ℕ : Type but is expected to have type ?m.12030.Nonempty : Prop
Second, I cannot replace the underscore in | _ a with any letter as it would complain that it is an invalid alternate name. I don't know what is supposed to be a valid alternate name there.

In any case, I am probably not understanding how to make use of induction...using in this context. Any help is greatly appreciated.

[Yaël Dillies]

What does induction T using g.cons_induction with do?

[Kevin Cheung]

It says unknown constant 'g.cons_induction'

[Yaël Dillies]

That's what I thought as well. I think it's safe to say it's not supported.

[Yaël Dillies]

Try induction T using Nonempty.cons_induction with, just in case

[Kevin Cheung]

That gives the error message I quoted:

target
  T
has type
  Finset ℕ : Type
but is expected to have type
  ?m.12030.Nonempty : Prop

[Yaël Dillies]

I give up :sad:

[Kevin Cheung]

That's ok. I am just puzzled by what induction...using expects from an induction principle. I don't think I get what it actually does.

[Eric Wieser]

Your mwe doesn't work for me, the imports don't exist

[Ruben Van de Velde]

That's probably Yaël's fault :)

[Eric Wieser]

induction g using Nonempty.cons_induction works for me

[Kevin Cheung]

Lean doesn't complain about that as I mentioned in the post. But I couldn't figure out how to proceed.

[Kevin Cheung]

I don't understand what the underscore in | _ a => is doing; I couldn't figure out what that hole could stand for.

[Ruben Van de Velde]

Oh, you need

| singleton a => sorry
| cons a s ha hs ih => sorry

[Kevin Cheung]

Thanks. How did you figure that out? (Or maybe, how should I have figured that out?)

[Kevin Cheung]

Hmm. I wonder why the import of Mathlib.Algebra.BigOperators.Basic worked in my VScode but not on the web lean 4 playground.

[Kevin Cheung]

import Mathlib.Algebra.BigOperators.Fin works in both. How did I even end up with .Basic?

[Ruben Van de Velde]

The file was moved very recently

[Kevin Cheung]

Oh. So it no longer exists?

[Ruben Van de Velde]

I looked at docs#Finset.Nonempty.cons_induction , which has two explicit arguments - singleton and cons

[Ruben Van de Velde]

#13277

[Ruben Van de Velde]

Split into Algebra.BigOperators.Group.Finset and Algebra.BigOperators.GroupWithZero.Finset

[Kevin Cheung]

So that means the Mathlib in my project is outdated. Now I guess I have to dig up how to update it.

[Ruben Van de Velde]

https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4

[Kevin Cheung]

Ruben Van de Velde said:

I looked at docs#Finset.Nonempty.cons_induction , which has two explicit arguments - singleton and cons

induction...using seems a bit magical to me. When it is invoked, does it create as many cases as there are things before the colon in the induction principle?

[Ruben Van de Velde]

That's as far as my understanding goes as well

[Ruben Van de Velde]

I only use it, I don't claim to understand it :)

[Kevin Cheung]

Thank you for your help. Maybe I should not try to understand it too much.