Theorem: Finset.inter_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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
⊢ ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card -
      ↑(t ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card ≤
    ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t : Finset α
has : a ∈ s
hst : (s ∩ a • ∅.mulStab * (t ∩ a • ∅.mulStab)).mulStab ⊆ ∅.mulStab
⊢ ↑∅.mulStab.card - ↑(s ∩ a • ∅.mulStab * (s ∩ a • ∅.mulStab * (t ∩ a • ∅.mulStab)).mulStab).card -
      ↑(t ∩ a • ∅.mulStab * (s ∩ a • ∅.mulStab * (t ∩ a • ∅.mulStab)).mulStab).card ≤
    ↑((s ∪ t) * ∅.mulStab).card - ↑((s ∪ t) * (s ∩ a • ∅.mulStab * (t ∩ a • ∅.mulStab)).mulStab).card

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

State before:
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C : Finset α
a✝ b a : α
s t : Finset α
has : a ∈ s
hst : (s ∩ a • ∅.mulStab * (t ∩ a • ∅.mulStab)).mulStab ⊆ ∅.mulStab
⊢ ↑∅.mulStab.card - ↑(s ∩ a • ∅.mulStab * (s ∩ a • ∅.mulStab * (t ∩ a • ∅.mulStab)).mulStab).card -
      ↑(t ∩ a • ∅.mulStab * (s ∩ a • ∅.mulStab * (t ∩ a • ∅.mulStab)).mulStab).card ≤
    ↑((s ∪ t) * ∅.mulStab).card - ↑((s ∪ t) * (s ∩ a • ∅.mulStab * (t ∩ a • ∅.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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card -
      ↑(t ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card ≤
    ↑(a • C.mulStab \
          ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)).card
Tactic:
rw [card_sdiff, Int.ofNat_sub (card_le_card _), card_smul_finset]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card -
      ↑(t ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card ≤
    ↑C.mulStab.card -
      ↑((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card

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

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

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

α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ a • C.mulStab
Tactic:
all_goals
  apply subset_trans (mul_subset_mul_left hst)
  rw [← union_inter_distrib_right]
  refine' subset_trans (mul_subset_mul_right inter_subset_right) _
  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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card -
      ↑(t ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card ≤
    ↑C.mulStab.card -
      ↑((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card
Tactic:
rw [union_mul, le_sub_iff_add_le]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card -
        ↑(t ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card +
      ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ∪
            t ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card ≤
    ↑C.mulStab.card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card -
        ↑(t ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card +
      ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ∪
            t ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card ≤
    ↑C.mulStab.card
Tactic:
apply le_trans (add_le_add_left (Int.ofNat_le.mpr $ card_union_le _ _) _)
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card -
        ↑(t ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card +
      ↑((s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card +
          (t ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card) ≤
    ↑C.mulStab.card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card -
        ↑(t ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card +
      ↑((s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card +
          (t ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card) ≤
    ↑C.mulStab.card
Tactic:
norm_num
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ a • C.mulStab
Tactic:
apply subset_trans (mul_subset_mul_left hst)
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (s ∩ a • C.mulStab ∪ t ∩ 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * C.mulStab ⊆ a • C.mulStab
Tactic:
rw [← union_inter_distrib_right]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (s ∪ t) ∩ 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (s ∪ t) ∩ a • C.mulStab * C.mulStab ⊆ a • C.mulStab
Tactic:
refine' subset_trans (mul_subset_mul_right inter_subset_right) _
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑(a • C.mulStab \
          ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)).card ≤
    ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑(a • C.mulStab \
          ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)).card ≤
    ↑(((s ∪ t) * C.mulStab) \ ((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)).card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑(a • C.mulStab \
          ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)).card ≤
    ↑(((s ∪ t) * C.mulStab) \ ((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)).card ≤
    (((s ∪ t) * C.mulStab) \ ((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)).card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)).card ≤
    (((s ∪ t) * C.mulStab) \ ((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab) ⊆
    ((s ∪ t) * C.mulStab) \ ((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)

State before:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab) ⊆
    ((s ∪ t) * C.mulStab) \ ((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
⊢ x ∉ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
⊢ x ∉ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∉ (s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
⊢ x ∉ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∉ (s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
⊢ x ∉ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
⊢ x ∈ (s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
⊢ x ∈ (s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
Tactic:
rw [← union_inter_distrib_right]
State after:
case a.refine'_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
⊢ x ∈ (s ∪ t) ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
⊢ x ∈ (s ∪ t) ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
hxyd : y * d = x
⊢ x ∈ (s ∪ t) ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
hxyd : y * d = x
⊢ x ∈ (s ∪ t) ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
hxyd : y * d = x
c : α
hc : c ∈ C.mulStab
hcx : a • c = x
⊢ x ∈ (s ∪ t) ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
hxyd : y * d = x
c : α
hc : c ∈ C.mulStab
hcx : a • c = x
⊢ x ∈ (s ∪ t) ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
⊢ x ∈ (s ∪ t) ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
⊢ x ∈ (s ∪ t) ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
⊢ x ∈ (s ∪ t) ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
c : α
hxyd : y = a • c * d⁻¹
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
⊢ x ∈ (s ∪ t) ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
c : α
hxyd : y * d = x
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
⊢ x ∈ (s ∪ t) ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
c : α
hxyd : y * d = x
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
⊢ x ∈ (s ∪ t) ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
c : α
hxyd : y * d = x
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
⊢ y * d ∈ (s ∪ t) ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
c : α
hxyd : y * d = x
hc : c ∈ C.mulStab
hcx : a • c = x
hyC : y ∈ a • C.mulStab
⊢ y * d ∈ (s ∪ t) ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • 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 : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ a • 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