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

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ Disjoint s (a • s.mulStab)
Tactic:
suffices Disjoint (a • s.mulStab) (s * s.mulStab) by
  simpa [mul_comm, disjoint_comm, mulStab_mul]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ Disjoint (a • s.mulStab) (s * s.mulStab)

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ Disjoint (a • s.mulStab) (s * s.mulStab)
Tactic:
apply disjoint_smul_finset_mulStab_mul_mulStab
State after:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ ¬a • s.mulStab ⊆ s * s.mulStab

State before:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ ¬a • s.mulStab ⊆ s * s.mulStab
Tactic:
rw [mul_comm, mulStab_mul]
State after:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ ¬a • s.mulStab ⊆ s

State before:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ ¬a • s.mulStab ⊆ s
Tactic:
contrapose! has
State after:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : a • s.mulStab ⊆ s
⊢ a • s.mulStab ⊆ t

State before:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : a • s.mulStab ⊆ s
⊢ a • s.mulStab ⊆ t
Tactic:
exact subset_trans has hst
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
this : Disjoint (a • s.mulStab) (s * s.mulStab)
⊢ Disjoint s (a • s.mulStab)
Tactic:
simpa [mul_comm, disjoint_comm, mulStab_mul]
State after:
no goals