internlm/Lean-Github huggingface dataset:
Theorem: Finset.mul_aux1
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
hconv : (s ∩ t).card + ((s ∪ t) * H).card ≤ C.card + H.card
H' : Finset α := (s' * t').mulStab
ih : (s' * H').card + (t' * H').card ≤ (s' * t').card + H'.card
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hnotconv : C'.card + C'.mulStab.card < (s ∩ t).card + ((s ∪ t) * C'.mulStab).card
hCun : C'.mulStab = H'
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * H').card < ↑H.card - ↑(s' * H').card - ↑(t' * H').card
Tactic:
zify at hconv hnotconv ih
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * H').card < ↑H.card - ↑(s' * H').card - ↑(t' * H').card
Theorem: Finset.mul_aux1
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * H').card < ↑H.card - ↑(s' * H').card - ↑(t' * H').card
Tactic:
calc
  (((s ∪ t) * H).card - ((s ∪ t) * H').card : ℤ) <
      C.card + H.card - (s ∩ t).card - (C'.card + H'.card - (s ∩ t).card) := by
    rw [← hCun]
    linarith [hconv, hnotconv]
  _ = H.card - (s' * t').card - H'.card := by
    rw [card_union_of_disjoint hdisj, Int.ofNat_add]
    abel
  _ ≤ H.card - (s' * H').card - (t' * H').card := by linarith [ih]
Proof state after:
no goals
Theorem: Finset.mul_aux1
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * H').card < ↑C.card + ↑H.card - ↑(s ∩ t).card - (↑C'.card + ↑H'.card - ↑(s ∩ t).card)
Tactic:
rw [← hCun]
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * C'.mulStab).card <
    ↑C.card + ↑H.card - ↑(s ∩ t).card - (↑C'.card + ↑C'.mulStab.card - ↑(s ∩ t).card)
Theorem: Finset.mul_aux1
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * C'.mulStab).card <
    ↑C.card + ↑H.card - ↑(s ∩ t).card - (↑C'.card + ↑C'.mulStab.card - ↑(s ∩ t).card)
Tactic:
linarith [hconv, hnotconv]
Proof state after:
no goals
Theorem: Finset.mul_aux1
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑C.card + ↑H.card - ↑(s ∩ t).card - (↑C'.card + ↑H'.card - ↑(s ∩ t).card) = ↑H.card - ↑(s' * t').card - ↑H'.card
Tactic:
rw [card_union_of_disjoint hdisj, Int.ofNat_add]
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑C.card + ↑H.card - ↑(s ∩ t).card - (↑C.card + ↑(s' * t').card + ↑H'.card - ↑(s ∩ t).card) =
    ↑H.card - ↑(s' * t').card - ↑H'.card
Theorem: Finset.mul_aux1
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑C.card + ↑H.card - ↑(s ∩ t).card - (↑C.card + ↑(s' * t').card + ↑H'.card - ↑(s ∩ t).card) =
    ↑H.card - ↑(s' * t').card - ↑H'.card
Tactic:
abel
Proof state after:
no goals
Theorem: Finset.mul_aux1
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑H.card - ↑(s' * t').card - ↑H'.card ≤ ↑H.card - ↑(s' * H').card - ↑(t' * H').card
Tactic:
linarith [ih]
Proof state after:
no goals
Theorem: Finset.disjoint_smul_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ Disjoint s (a • s.mulStab)
Tactic:
suffices Disjoint (a • s.mulStab) (s * s.mulStab) by
  simpa [mul_comm, disjoint_comm, mulStab_mul]
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ Disjoint (a • s.mulStab) (s * s.mulStab)
Theorem: Finset.disjoint_smul_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ Disjoint (a • s.mulStab) (s * s.mulStab)
Tactic:
apply disjoint_smul_finset_mulStab_mul_mulStab
Proof state after:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ ¬a • s.mulStab ⊆ s * s.mulStab
Theorem: Finset.disjoint_smul_mulStab
Proof state before:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ ¬a • s.mulStab ⊆ s * s.mulStab
Tactic:
rw [mul_comm, mulStab_mul]
Proof state after:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ ¬a • s.mulStab ⊆ s
Theorem: Finset.disjoint_smul_mulStab
Proof state before:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ ¬a • s.mulStab ⊆ s
Tactic:
contrapose! has
Proof state after:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : a • s.mulStab ⊆ s
⊢ a • s.mulStab ⊆ t
Theorem: Finset.disjoint_smul_mulStab
Proof state before:
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : a • s.mulStab ⊆ s
⊢ a • s.mulStab ⊆ t
Tactic:
exact subset_trans has hst
Proof state after:
no goals
Theorem: Finset.disjoint_smul_mulStab
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
this : Disjoint (a • s.mulStab) (s * s.mulStab)
⊢ Disjoint s (a • s.mulStab)
Tactic:
simpa [mul_comm, disjoint_comm, mulStab_mul]
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
⊢ ↑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
Proof 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
Theorem: Finset.disjoint_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 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
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
⊢ ↑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]
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
⊢ (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
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
⊢ (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))
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
⊢ (s ∩ a • C.mulStab * C.mulStab).card ≤ C.mulStab.card
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
⊢ (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) _)
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
⊢ (a • C.mulStab * C.mulStab).card = C.mulStab.card
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
⊢ (a • C.mulStab * C.mulStab).card = C.mulStab.card
Tactic:
rw [smul_mul_assoc, mulStab_mul_mulStab, card_smul_finset]
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
⊢ 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.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
⊢ ↑(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)]
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
⊢ ↑(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
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
⊢ ↑(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
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
⊢ (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
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
⊢ (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
Proof 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)
Theorem: Finset.disjoint_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 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 ⟨_, _⟩
Proof 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
Theorem: Finset.disjoint_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 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
Proof 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
Theorem: Finset.disjoint_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 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'
Proof 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
Theorem: Finset.disjoint_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 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'
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 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
Theorem: Finset.disjoint_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 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
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
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