Theorem: Finset.disjoint_smul_finset_mulStab_mul_mulStab (LeanCamCombi/Kneser/MulStab.lean)

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ¬a • s.mulStab ⊆ t * s.mulStab → Disjoint (a • s.mulStab) (t * s.mulStab)
Tactic:
simp_rw [@not_imp_comm (_ ⊆ _), ← smul_eq_mul, ← biUnion_smul_finset, disjoint_biUnion_right,
  Classical.not_forall]
State after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ (∃ x, ∃ (_ : x ∈ t), ¬Disjoint (a • s.mulStab) (x • s.mulStab)) → a • s.mulStab ⊆ t.biUnion fun x => x • s.mulStab

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ (∃ x, ∃ (_ : x ∈ t), ¬Disjoint (a • s.mulStab) (x • s.mulStab)) → a • s.mulStab ⊆ t.biUnion fun x => x • s.mulStab
Tactic:
rintro ⟨b, hb, h⟩
State after:
case intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a b : α
hb : b ∈ t
h : ¬Disjoint (a • s.mulStab) (b • s.mulStab)
⊢ a • s.mulStab ⊆ t.biUnion fun x => x • s.mulStab

State before:
case intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a b : α
hb : b ∈ t
h : ¬Disjoint (a • s.mulStab) (b • s.mulStab)
⊢ a • s.mulStab ⊆ t.biUnion fun x => x • s.mulStab
Tactic:
rw [s.pairwiseDisjoint_smul_finset_mulStab.eq (Set.mem_range_self _) (Set.mem_range_self _) h]
State after:
case intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a b : α
hb : b ∈ t
h : ¬Disjoint (a • s.mulStab) (b • s.mulStab)
⊢ b • s.mulStab ⊆ t.biUnion fun x => x • s.mulStab