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

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
⊢ ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card ≤
    ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card
Tactic:
obtain rfl | hC := C.eq_empty_or_nonempty
State after:
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C : Finset α
a✝ b✝ a b : α
s t : Finset α
has : a ∈ s
hsC : Disjoint t (a • ∅.mulStab)
hst : (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab ⊆ ∅.mulStab
⊢ ↑∅.mulStab.card - ↑(s ∩ a • ∅.mulStab * (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab).card ≤
    ↑((s ∪ t) * ∅.mulStab).card - ↑((s ∪ t) * (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab).card

case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card ≤
    ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card

State before:
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C : Finset α
a✝ b✝ a b : α
s t : Finset α
has : a ∈ s
hsC : Disjoint t (a • ∅.mulStab)
hst : (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab ⊆ ∅.mulStab
⊢ ↑∅.mulStab.card - ↑(s ∩ a • ∅.mulStab * (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab).card ≤
    ↑((s ∪ t) * ∅.mulStab).card - ↑((s ∪ t) * (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab).card
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card =
    ↑(a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)).card
Tactic:
rw [card_sdiff
    (subset_trans (mul_subset_mul_left hst)
      (subset_trans (mul_subset_mul_right inter_subset_right) _)),
  card_smul_finset, Int.ofNat_sub]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card ≤ C.mulStab.card

α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ a • C.mulStab * C.mulStab ⊆ a • C.mulStab

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card ≤ C.mulStab.card
Tactic:
apply le_trans (card_le_card (mul_subset_mul_left hst))
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (s ∩ a • C.mulStab * C.mulStab).card ≤ C.mulStab.card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (s ∩ a • C.mulStab * C.mulStab).card ≤ C.mulStab.card
Tactic:
apply
  le_trans (card_le_card inter_mul_subset)
    (le_of_le_of_eq (card_le_card inter_subset_right) _)
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (a • C.mulStab * C.mulStab).card = C.mulStab.card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (a • C.mulStab * C.mulStab).card = C.mulStab.card
Tactic:
rw [smul_mul_assoc, mulStab_mul_mulStab, card_smul_finset]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ a • C.mulStab * C.mulStab ⊆ a • C.mulStab
Tactic:
simp only [smul_mul_assoc, mulStab_mul_mulStab, Subset.rfl]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑(a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)).card ≤
    ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card
Tactic:
rw [← Int.ofNat_sub (card_le_card (mul_subset_mul_left hst)), ←
  card_sdiff (mul_subset_mul_left hst)]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑(a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)).card ≤
    ↑(((s ∪ t) * C.mulStab) \ ((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)).card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑(a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)).card ≤
    ↑(((s ∪ t) * C.mulStab) \ ((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)).card
Tactic:
norm_cast
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)).card ≤
    (((s ∪ t) * C.mulStab) \ ((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)).card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)).card ≤
    (((s ∪ t) * C.mulStab) \ ((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)).card
Tactic:
apply card_le_card
State after:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab) ⊆
    ((s ∪ t) * C.mulStab) \ ((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)

State before:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab) ⊆
    ((s ∪ t) * C.mulStab) \ ((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
Tactic:
refine' fun x hx => mem_sdiff.mpr ⟨_, _⟩
State after:
case a.refine'_1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
⊢ x ∈ (s ∪ t) * C.mulStab

case a.refine'_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
⊢ x ∉ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

State before:
case a.refine'_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
⊢ x ∉ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
have hx' := (mem_sdiff.mp hx).2
State after:
case a.refine'_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∉ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
⊢ x ∉ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

State before:
case a.refine'_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∉ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
⊢ x ∉ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
contrapose! hx'
State after:
case a.refine'_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

State before:
case a.refine'_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
obtain ⟨y, hyst, d, hd, hxyd⟩ := mem_mul.mp hx'
State after:
case a.refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
hxyd : y * d = x
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

State before:
case a.refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
hxyd : y * d = x
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
obtain ⟨c, hc, hcx⟩ := mem_smul_finset.mp (mem_sdiff.mp hx).1
State after:
case a.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
hxyd : y * d = x
c : α
hc : c ∈ C.mulStab
hcx : a • c = x
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

State before:
case a.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
hxyd : y * d = x
c : α
hc : c ∈ C.mulStab
hcx : a • c = x
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
rw [← hcx, ← eq_mul_inv_iff_mul_eq] at hxyd
State after:
case a.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

State before:
case a.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
have hyC : y ∈ a • C.mulStab := by
  rw [hxyd, smul_mul_assoc, smul_mem_smul_finset_iff, ← mulStab_mul_mulStab]
  apply mul_mem_mul hc ((mem_mulStab hC).mpr (inv_smul_eq_iff.mpr _))
  exact Eq.symm ((mem_mulStab hC).mp (hst hd))
State after:
case a.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

State before:
case a.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
replace hyst : y ∈ s := by
  apply or_iff_not_imp_right.mp (mem_union.mp hyst)
  contrapose! hsC
  exact not_disjoint_iff.mpr ⟨y, hsC, hyC⟩
State after:
case a.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
hyst : y ∈ s
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

State before:
case a.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
hyst : y ∈ s
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
rw [eq_mul_inv_iff_mul_eq, hcx] at hxyd
State after:
case a.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y * d = x
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
hyst : y ∈ s
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

State before:
case a.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y * d = x
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
hyst : y ∈ s
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
rw [← hxyd]
State after:
case a.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y * d = x
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
hyst : y ∈ s
⊢ y * d ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

State before:
case a.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y * d = x
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
hyst : y ∈ s
⊢ y * d ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
exact mul_mem_mul (mem_inter.mpr ⟨hyst, hyC⟩) hd
State after:
no goals

State before:
case a.refine'_1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
⊢ x ∈ (s ∪ t) * C.mulStab
Tactic:
apply smul_finset_subset_smul (mem_union_left t has) (mem_sdiff.mp hx).1
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
⊢ y ∈ a • C.mulStab
Tactic:
rw [hxyd, smul_mul_assoc, smul_mem_smul_finset_iff, ← mulStab_mul_mulStab]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
⊢ c * d⁻¹ ∈ C.mulStab * C.mulStab

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
⊢ c * d⁻¹ ∈ C.mulStab * C.mulStab
Tactic:
apply mul_mem_mul hc ((mem_mulStab hC).mpr (inv_smul_eq_iff.mpr _))
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
⊢ C = d • C

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
⊢ C = d • C
Tactic:
exact Eq.symm ((mem_mulStab hC).mp (hst hd))
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
⊢ y ∈ s
Tactic:
apply or_iff_not_imp_right.mp (mem_union.mp hyst)
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
⊢ y ∉ t

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
⊢ y ∉ t
Tactic:
contrapose! hsC
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
hsC : y ∈ t
⊢ ¬Disjoint t (a • C.mulStab)

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
hsC : y ∈ t
⊢ ¬Disjoint t (a • C.mulStab)
Tactic:
exact not_disjoint_iff.mpr ⟨y, hsC, hyC⟩
State after:
no goals