internlm/Lean-Github huggingface dataset:
Theorem: Finset.disjoint_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 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
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 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
Theorem: Finset.disjoint_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 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))
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 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
Theorem: Finset.disjoint_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 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⟩
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 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
Theorem: Finset.disjoint_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 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
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 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
Theorem: Finset.disjoint_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 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]
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 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
Theorem: Finset.disjoint_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 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
Proof state after:
no goals
Theorem: Finset.disjoint_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 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
Proof state after:
no goals
Theorem: Finset.disjoint_mul_sub_card_le
Proof 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]
Proof 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
Theorem: Finset.disjoint_mul_sub_card_le
Proof 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 _))
Proof 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
Theorem: Finset.disjoint_mul_sub_card_le
Proof 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))
Proof state after:
no goals
Theorem: Finset.disjoint_mul_sub_card_le
Proof 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)
Proof 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
Theorem: Finset.disjoint_mul_sub_card_le
Proof 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
Proof 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)
Theorem: Finset.disjoint_mul_sub_card_le
Proof 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⟩
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
⊢ ↑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
Proof 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
Theorem: Finset.inter_mul_sub_card_le
Proof 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
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
⊢ ↑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]
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
⊢ ↑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
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

α : 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]
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
⊢ ↑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]
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
⊢ ↑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
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
⊢ ↑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 _ _) _)
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
⊢ ↑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
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
⊢ ↑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
Proof state after:
no goals