Theorem: Finset.card_mul_add_card_lt (LeanCamCombi/Kneser/Kneser.lean)

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hC : C.Nonempty
hs : s' ⊆ s
ht : t' ⊆ t
hCst : C ⊆ s * t
hCst' : Disjoint C (s' * t')
⊢ (s' * t').card < (s * t).card
Tactic:
rw [← tsub_pos_iff_lt, ← card_sdiff (mul_subset_mul hs ht), card_pos]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hC : C.Nonempty
hs : s' ⊆ s
ht : t' ⊆ t
hCst : C ⊆ s * t
hCst' : Disjoint C (s' * t')
⊢ ((s * t) \ (s' * t')).Nonempty

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hC : C.Nonempty
hs : s' ⊆ s
ht : t' ⊆ t
hCst : C ⊆ s * t
hCst' : Disjoint C (s' * t')
⊢ ((s * t) \ (s' * t')).Nonempty
Tactic:
exact hC.mono (subset_sdiff.2 ⟨hCst, hCst'⟩)
State after:
no goals