internlm/Lean-Github huggingface dataset:
Theorem: Finset.inter_mul_sub_card_le
Proof 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)
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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]
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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) _
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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]
Proof state after:
no goals
Theorem: Finset.inter_mul_sub_card_le
Proof 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)]
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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
Proof 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)
Theorem: Finset.inter_mul_sub_card_le
Proof 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 ⟨_, _⟩
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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'
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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]
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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'
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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))
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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]
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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
Proof state after:
no goals
Theorem: Finset.inter_mul_sub_card_le
Proof 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
Proof state after:
no goals
Theorem: Finset.inter_mul_sub_card_le
Proof 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]
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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 _))
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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))
Proof state after:
no goals
Theorem: Finset.card_mul_add_card_lt
Proof 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]
Proof 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