Theorem: Finset.mul_kneser' (LeanCamCombi/Kneser/KneserRuzsa.lean)

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ s t : Finset α
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
State after:
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t✝ t : Finset α
⊢ (∅ * (∅ * t).mulStab).card + (t * (∅ * t).mulStab).card ≤ (∅ * t).card + (∅ * t).mulStab.card

case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ s t : Finset α
hs : s.Nonempty
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card

State before:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ s t : Finset α
hs : s.Nonempty
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty
State after:
case inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t s : Finset α
hs : s.Nonempty
⊢ (s * (s * ∅).mulStab).card + (∅ * (s * ∅).mulStab).card ≤ (s * ∅).card + (s * ∅).mulStab.card

case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card

State before:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
refine'
  (le_card_mul_add_card_mulStab_mul (hs.mul (hs.mul ht).mulStab) $
        ht.mul (hs.mul ht).mulStab).trans_eq
    _
State after:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ (s * (s * t).mulStab * (t * (s * t).mulStab)).card + (s * (s * t).mulStab * (t * (s * t).mulStab)).mulStab.card =
    (s * t).card + (s * t).mulStab.card

State before:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ (s * (s * t).mulStab * (t * (s * t).mulStab)).card + (s * (s * t).mulStab * (t * (s * t).mulStab)).mulStab.card =
    (s * t).card + (s * t).mulStab.card
Tactic:
rw [mul_mulStab_mul_mul_mul_mulStab_mul]
State after:
no goals

State before:
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t✝ t : Finset α
⊢ (∅ * (∅ * t).mulStab).card + (t * (∅ * t).mulStab).card ≤ (∅ * t).card + (∅ * t).mulStab.card
Tactic:
simp
State after:
no goals

State before:
case inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t s : Finset α
hs : s.Nonempty
⊢ (s * (s * ∅).mulStab).card + (∅ * (s * ∅).mulStab).card ≤ (s * ∅).card + (s * ∅).mulStab.card
Tactic:
simp
State after:
no goals