Losing definition when using Finset.induction_on'

Stream: mathlib4

[Sese Mueller]

Sorry if this is weird, I'm a bit new with Lean.

I want to perform a Finset.induction on (f S) for some function that maps a Set to another set. (Doing this directly on the original set is much harder because the main property I am working on comes from a Set passing through f.
(I do have the a lemma that this property p holds \forall e \in (f S)).

I want to use this property about elements of (f S) inside the induction. This could either be done using the definition of the set the induction is being done on, or by somehow passing information about the base of the induction.

Consider the example case below:

theorem test_finset_induction_on' {α : Type*} [DecidableEq α] (S : Finset α)  (f g: (Finset α) → (Finset α)) : Disjoint (f S) (g S) := by {
  induction (f S) using Finset.induction_on' with
    | empty =>
       exact fun ⦃x⦄ a a_1 ↦ a
    | insert new Old new_in_total Old_subset_total new_not_in_Old h_ind => {
       -- Definition of total is lost, property of Old or Total cannot be expressed
    }
}

My guess is that inductions shouldn't be done like this and that somehow, lean discards information about the Finset the induction is on. (It could also be a classic X Y Problem, I'm still quite new with lean)

Is there some way to proceed here? I do know that if I can use the property inside that I can continue my proof (I introduced it with sorry and used it to complete it)

[Aaron Liu]

induction h : f S using Finset.induction_on' with

[Kyle Miller]

Two options, either what Aaron said, or use generalize h : f S = x first and then do induction x. Aaron's suggestion is the more convenient one.

[Sese Mueller]

Thanks for the quick help, that looks good. I'll see whether I can use it

[Sese Mueller]

It doesn't do what I expected it to; I thought it would have x: Finset \alpha := f S in the assumptions, but I can only get f S = insert new Old by declaring the hypothesis outside the induction twice. Specifically, there doesn't seem to be a way to show x = f S inside, only x \subseteq f S. Might be enough for me, but I'm still not that well with Lean

[Aaron Liu]

Sese Mueller said:

It doesn't do what I expected it to; I thought it would have x: Finset \alpha := f S in the assumptions, but I can only get f S = insert new Old by declaring the hypothesis outside the induction twice. Specifically, there doesn't seem to be a way to show x = f S inside, only x \subseteq f S. Might be enough for me, but I'm still not that well with Lean

You can always do let x := f S

[Sese Mueller]

I'm not sure how that could help or where I can do that, if I do it inside the induction, the old x, which the hypothesis new_in_total and Old_subset_total depend on just gets shadowed

[Aaron Liu]

Sese Mueller said:

I'm not sure how that could help or where I can do that, if I do it inside the induction, the old x, which the hypothesis new_in_total and Old_subset_total depend on just gets shadowed

can you write out the goal state you have in the induction step and the goal state you want to have?

[Sese Mueller]

Not really, it's quite long but also not the point. I want to use the property of f on the assumptions to, after some work, show that applying f to new and taking the union of mapping f on Old is disjoint.

I would like to have the state that contains h2: x = f S where new_in_total and Old_subset_total refer to x.

[Aaron Liu]

I'm asking this because the thing I think you want to do is unsound

[Aaron Liu]

the great thing about Lean is that it's really really hard to accidentally do unsound things

[Sese Mueller]

Hm, yeah, that might be a possibility. But introducing have h_unsound : f S = x := by sorry into the example doesn't produce any false statements as far as I (or exact? or aesop) can see.
I think the gap between x and f S in the induction is that the induction, there is no limit/filter on what could be in x. So Lean plays it safe and doesn't allow any hypothesis about what couldn't be in x and instead only gives the two hypothesis for new and Old being in x. (But I might be wrong)

[Sese Mueller]

Also, there seems to be a weird difference between using induction (f S) using … and induction h: (f S) using ...; when omitting the h, hind := Disjoint Old (g S) but when h is used, hind:= f S \to Disjoint Old (g S).

[Sese Mueller]

This leads to it being elimated by a simp_all via simp_all only [Finset.insert_eq_self, IsEmpty.forall_iff, Finset.disjoint_insert_left]. This doesn't happen without the h. Weird.

[Kyle Miller]

Yes, including h changes the induction hypothesis, since you need to prove that the variable being inducted on is equal to f S, to justify why you could get such an equality.