Theorem: Finset.le_card_sup_add_card_mulStab_sup (LeanCamCombi/Kneser/KneserRuzsa.lean)

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
s : Finset ι
f : ι → Finset α
hs : s.Nonempty
⊢ (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
Tactic:
induction' s using Finset.cons_induction with i s hi ih
State after:
case empty
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ι : Type u_2
f : ι → Finset α
hs : ∅.Nonempty
⊢ (∅.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (∅.sup f).card + (∅.sup f).mulStab.card

case cons
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hs : s.Nonempty), (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
hs : (cons i s hi).Nonempty
⊢ ((cons i s hi).inf' hs fun i => (f i).card + (f i).mulStab.card) ≤
    ((cons i s hi).sup f).card + ((cons i s hi).sup f).mulStab.card

State before:
case cons
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hs : s.Nonempty), (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
hs : (cons i s hi).Nonempty
⊢ ((cons i s hi).inf' hs fun i => (f i).card + (f i).mulStab.card) ≤
    ((cons i s hi).sup f).card + ((cons i s hi).sup f).mulStab.card
Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
State after:
case cons.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
hi : i ∉ ∅
ih : ∀ (hs : ∅.Nonempty), (∅.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (∅.sup f).card + (∅.sup f).mulStab.card
hs : (cons i ∅ hi).Nonempty
⊢ ((cons i ∅ hi).inf' hs fun i => (f i).card + (f i).mulStab.card) ≤
    ((cons i ∅ hi).sup f).card + ((cons i ∅ hi).sup f).mulStab.card

case cons.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hs : s.Nonempty), (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
hs✝ : (cons i s hi).Nonempty
hs : s.Nonempty
⊢ ((cons i s hi).inf' hs✝ fun i => (f i).card + (f i).mulStab.card) ≤
    ((cons i s hi).sup f).card + ((cons i s hi).sup f).mulStab.card

State before:
case cons.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hs : s.Nonempty), (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
hs✝ : (cons i s hi).Nonempty
hs : s.Nonempty
⊢ ((cons i s hi).inf' hs✝ fun i => (f i).card + (f i).mulStab.card) ≤
    ((cons i s hi).sup f).card + ((cons i s hi).sup f).mulStab.card
Tactic:
simp only [hs, inf'_cons, sup_cons, sup_eq_union]
State after:
case cons.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hs : s.Nonempty), (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
hs✝ : (cons i s hi).Nonempty
hs : s.Nonempty
⊢ (((f i).card + (f i).mulStab.card) ⊓ s.inf' ⋯ fun i => (f i).card + (f i).mulStab.card) ≤
    (f i ∪ s.sup f).card + (f i ∪ s.sup f).mulStab.card

State before:
case cons.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hs : s.Nonempty), (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
hs✝ : (cons i s hi).Nonempty
hs : s.Nonempty
⊢ (((f i).card + (f i).mulStab.card) ⊓ s.inf' ⋯ fun i => (f i).card + (f i).mulStab.card) ≤
    (f i ∪ s.sup f).card + (f i ∪ s.sup f).mulStab.card
Tactic:
exact (inf_le_inf_left _ $ ih hs).trans le_card_union_add_card_mulStab_union
State after:
no goals

State before:
case empty
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ι : Type u_2
f : ι → Finset α
hs : ∅.Nonempty
⊢ (∅.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (∅.sup f).card + (∅.sup f).mulStab.card
Tactic:
cases not_nonempty_empty hs
State after:
no goals

State before:
case cons.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
hi : i ∉ ∅
ih : ∀ (hs : ∅.Nonempty), (∅.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (∅.sup f).card + (∅.sup f).mulStab.card
hs : (cons i ∅ hi).Nonempty
⊢ ((cons i ∅ hi).inf' hs fun i => (f i).card + (f i).mulStab.card) ≤
    ((cons i ∅ hi).sup f).card + ((cons i ∅ hi).sup f).mulStab.card
Tactic:
simp
State after:
no goals