internlm/Lean-Github huggingface dataset:
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
C : Finset α
H : Finset α := C.mulStab
hH : H = C.mulStab
hCst : C ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
hC : C.Nonempty
hCstab : C.mulStab.Nontrivial
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : ¬(a * b) • H ⊆ s * t
s₁ : Finset α := s ∩ a • H
hs₁ : s₁ = s ∩ a • H
s₂ : Finset α := s ∩ b • H
hs₂ : s₂ = s ∩ b • H
t₁ : Finset α := t ∩ b • H
ht₁ : t₁ = t ∩ b • H
t₂ : Finset α := t ∩ a • H
ht₂ : t₂ = t ∩ a • H
hs₁s : s₁ ⊆ s
hs₂s : s₂ ⊆ s
ht₁t : t₁ ⊆ t
ht₂t : t₂ ⊆ t
has₁ : a ∈ s₁
hbt₁ : b ∈ t₁
hs₁ne : s₁.Nonempty
ht₁ne : t₁.Nonempty
C₁ : Finset α := C ∪ s₁ * t₁
hC₁ : C₁ = C ∪ s₁ * t₁
C₂ : Finset α := C ∪ s₂ * t₂
hC₂ : C₂ = C ∪ s₂ * t₂
H₁ : Finset α := (s₁ * t₁).mulStab
hH₁ : H₁ = (s₁ * t₁).mulStab
H₂ : Finset α := (s₂ * t₂).mulStab
hH₂ : H₂ = (s₂ * t₂).mulStab
hC₁st : C₁ ⊆ s * t
hC₂st : C₂ ⊆ s * t
hstabH₁ : s₁ * t₁ ⊆ (a * b) • H
hstabH₂ : s₂ * t₂ ⊆ (a * b) • H
hCst₁ : Disjoint C (s₁ * t₁)
hCst₂ : Disjoint C (s₂ * t₂)
hst₁ : (s₁ * t₁).card + s₁.card < (s * t).card + s.card
hst₂ : (s₂ * t₂).card + s₂.card < (s * t).card + s.card
hC₁stab : C₁.mulStab = H₁
hH₁H : H₁ ⊂ H
aux1₁ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₁ * t₁).mulStab).card <
    ↑C.mulStab.card - ↑(s₁ * (s₁ * t₁).mulStab).card - ↑(t₁ * (s₁ * t₁).mulStab).card
ht₂ne : t₂.Nonempty
hs₂ne : s₂.Nonempty
hC₂stab : C₂.mulStab = H₂
hH₂H : H₂ ⊂ H
aux1₂ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₂ * t₂).mulStab).card <
    ↑C.mulStab.card - ↑(s₂ * (s₂ * t₂).mulStab).card - ↑(t₂ * (s₂ * t₂).mulStab).card
habH : a • H ≠ b • H
S : Finset α := a • H \ (s₁ ∪ t₂)
hS : S = a • H \ (s₁ ∪ t₂)
T : Finset α := b • H \ (s₂ ∪ t₁)
hT : T = b • H \ (s₂ ∪ t₁)
hST : Disjoint S T
hSst : S ⊆ a • H \ (s ∪ t)
hTst : T ⊆ b • H \ (s ∪ t)
hSTst : Disjoint (S ∪ T) (s ∪ t)
hstconv : ↑(s * t).card + 1 < ↑(s ∩ t).card + ↑(s ∪ t).card
hSTcard : ↑S.card + ↑T.card + ↑(s ∪ t).card ≤ ↑((s ∪ t) * H).card
hH₁ne : H₁.Nonempty
hH₂ne : H₂.Nonempty
aux2₁ : ↑s₁.card + ↑t₁.card + ↑H₁.card ≤ ↑H.card
aux2₂ : ↑s₂.card + ↑t₂.card + ↑H₂.card ≤ ↑H.card
aux3₁ : ↑S.card + ↑T.card + ↑s₁.card + ↑t₁.card - ↑H₁.card < ↑H.card
ih₂ : ↑s₂.card + ↑t₂.card ≤ ↑(s₂ * t₂).card + ↑(s₂ * t₂).mulStab.card
⊢ ↑S.card + ↑T.card + ↑s₂.card + ↑t₂.card - ↑H₂.card <
    ↑S.card + ↑T.card + ↑(s ∪ t).card + ↑(s ∩ t).card - ↑(s * t).card + ↑(s₂ * t₂).card
Tactic:
linarith [ih₂]
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
C : Finset α
H : Finset α := C.mulStab
hH : H = C.mulStab
hCst : C ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
hC : C.Nonempty
hCstab : C.mulStab.Nontrivial
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : ¬(a * b) • H ⊆ s * t
s₁ : Finset α := s ∩ a • H
hs₁ : s₁ = s ∩ a • H
s₂ : Finset α := s ∩ b • H
hs₂ : s₂ = s ∩ b • H
t₁ : Finset α := t ∩ b • H
ht₁ : t₁ = t ∩ b • H
t₂ : Finset α := t ∩ a • H
ht₂ : t₂ = t ∩ a • H
hs₁s : s₁ ⊆ s
hs₂s : s₂ ⊆ s
ht₁t : t₁ ⊆ t
ht₂t : t₂ ⊆ t
has₁ : a ∈ s₁
hbt₁ : b ∈ t₁
hs₁ne : s₁.Nonempty
ht₁ne : t₁.Nonempty
C₁ : Finset α := C ∪ s₁ * t₁
hC₁ : C₁ = C ∪ s₁ * t₁
C₂ : Finset α := C ∪ s₂ * t₂
hC₂ : C₂ = C ∪ s₂ * t₂
H₁ : Finset α := (s₁ * t₁).mulStab
hH₁ : H₁ = (s₁ * t₁).mulStab
H₂ : Finset α := (s₂ * t₂).mulStab
hH₂ : H₂ = (s₂ * t₂).mulStab
hC₁st : C₁ ⊆ s * t
hC₂st : C₂ ⊆ s * t
hstabH₁ : s₁ * t₁ ⊆ (a * b) • H
hstabH₂ : s₂ * t₂ ⊆ (a * b) • H
hCst₁ : Disjoint C (s₁ * t₁)
hCst₂ : Disjoint C (s₂ * t₂)
hst₁ : (s₁ * t₁).card + s₁.card < (s * t).card + s.card
hst₂ : (s₂ * t₂).card + s₂.card < (s * t).card + s.card
hC₁stab : C₁.mulStab = H₁
hH₁H : H₁ ⊂ H
aux1₁ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₁ * t₁).mulStab).card <
    ↑C.mulStab.card - ↑(s₁ * (s₁ * t₁).mulStab).card - ↑(t₁ * (s₁ * t₁).mulStab).card
ht₂ne : t₂.Nonempty
hs₂ne : s₂.Nonempty
hC₂stab : C₂.mulStab = H₂
hH₂H : H₂ ⊂ H
aux1₂ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₂ * t₂).mulStab).card <
    ↑C.mulStab.card - ↑(s₂ * (s₂ * t₂).mulStab).card - ↑(t₂ * (s₂ * t₂).mulStab).card
habH : a • H ≠ b • H
S : Finset α := a • H \ (s₁ ∪ t₂)
hS : S = a • H \ (s₁ ∪ t₂)
T : Finset α := b • H \ (s₂ ∪ t₁)
hT : T = b • H \ (s₂ ∪ t₁)
hST : Disjoint S T
hSst : S ⊆ a • H \ (s ∪ t)
hTst : T ⊆ b • H \ (s ∪ t)
hSTst : Disjoint (S ∪ T) (s ∪ t)
hstconv : ↑(s * t).card + 1 < ↑(s ∩ t).card + ↑(s ∪ t).card
hSTcard : ↑S.card + ↑T.card + ↑(s ∪ t).card ≤ ↑((s ∪ t) * H).card
hH₁ne : H₁.Nonempty
hH₂ne : H₂.Nonempty
aux2₁ : ↑s₁.card + ↑t₁.card + ↑H₁.card ≤ ↑H.card
aux2₂ : ↑s₂.card + ↑t₂.card + ↑H₂.card ≤ ↑H.card
aux3₁ : ↑S.card + ↑T.card + ↑s₁.card + ↑t₁.card - ↑H₁.card < ↑H.card
this : ↑C.card + ↑(s₂ * t₂).card ≤ ↑(s * t).card
⊢ ↑S.card + ↑T.card + ↑(s ∪ t).card + ↑(s ∩ t).card - ↑(s * t).card + ↑(s₂ * t₂).card ≤
    ↑((s ∪ t) * H).card + ↑(s ∩ t).card - ↑C.card
Tactic:
linarith [this, hSTcard]
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
C : Finset α
H : Finset α := C.mulStab
hH : H = C.mulStab
hCst : C ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
hC : C.Nonempty
hCstab : C.mulStab.Nontrivial
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : ¬(a * b) • H ⊆ s * t
s₁ : Finset α := s ∩ a • H
hs₁ : s₁ = s ∩ a • H
s₂ : Finset α := s ∩ b • H
hs₂ : s₂ = s ∩ b • H
t₁ : Finset α := t ∩ b • H
ht₁ : t₁ = t ∩ b • H
t₂ : Finset α := t ∩ a • H
ht₂ : t₂ = t ∩ a • H
hs₁s : s₁ ⊆ s
hs₂s : s₂ ⊆ s
ht₁t : t₁ ⊆ t
ht₂t : t₂ ⊆ t
has₁ : a ∈ s₁
hbt₁ : b ∈ t₁
hs₁ne : s₁.Nonempty
ht₁ne : t₁.Nonempty
C₁ : Finset α := C ∪ s₁ * t₁
hC₁ : C₁ = C ∪ s₁ * t₁
C₂ : Finset α := C ∪ s₂ * t₂
hC₂ : C₂ = C ∪ s₂ * t₂
H₁ : Finset α := (s₁ * t₁).mulStab
hH₁ : H₁ = (s₁ * t₁).mulStab
H₂ : Finset α := (s₂ * t₂).mulStab
hH₂ : H₂ = (s₂ * t₂).mulStab
hC₁st : C₁ ⊆ s * t
hC₂st : C₂ ⊆ s * t
hstabH₁ : s₁ * t₁ ⊆ (a * b) • H
hstabH₂ : s₂ * t₂ ⊆ (a * b) • H
hCst₁ : Disjoint C (s₁ * t₁)
hCst₂ : Disjoint C (s₂ * t₂)
hst₁ : (s₁ * t₁).card + s₁.card < (s * t).card + s.card
hst₂ : (s₂ * t₂).card + s₂.card < (s * t).card + s.card
hC₁stab : C₁.mulStab = H₁
hH₁H : H₁ ⊂ H
aux1₁ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₁ * t₁).mulStab).card <
    ↑C.mulStab.card - ↑(s₁ * (s₁ * t₁).mulStab).card - ↑(t₁ * (s₁ * t₁).mulStab).card
ht₂ne : t₂.Nonempty
hs₂ne : s₂.Nonempty
hC₂stab : C₂.mulStab = H₂
hH₂H : H₂ ⊂ H
aux1₂ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₂ * t₂).mulStab).card <
    ↑C.mulStab.card - ↑(s₂ * (s₂ * t₂).mulStab).card - ↑(t₂ * (s₂ * t₂).mulStab).card
habH : a • H ≠ b • H
S : Finset α := a • H \ (s₁ ∪ t₂)
hS : S = a • H \ (s₁ ∪ t₂)
T : Finset α := b • H \ (s₂ ∪ t₁)
hT : T = b • H \ (s₂ ∪ t₁)
hST : Disjoint S T
hSst : S ⊆ a • H \ (s ∪ t)
hTst : T ⊆ b • H \ (s ∪ t)
hSTst : Disjoint (S ∪ T) (s ∪ t)
hstconv : ↑(s * t).card + 1 < ↑(s ∩ t).card + ↑(s ∪ t).card
hSTcard : ↑S.card + ↑T.card + ↑(s ∪ t).card ≤ ↑((s ∪ t) * H).card
hH₁ne : H₁.Nonempty
hH₂ne : H₂.Nonempty
aux2₁ : ↑s₁.card + ↑t₁.card + ↑H₁.card ≤ ↑H.card
aux2₂ : ↑s₂.card + ↑t₂.card + ↑H₂.card ≤ ↑H.card
aux3₁ : ↑S.card + ↑T.card + ↑s₁.card + ↑t₁.card - ↑H₁.card < ↑H.card
⊢ C.card + (s₂ * t₂).card ≤ (s * t).card
Tactic:
simp only [← card_union_of_disjoint hCst₂, card_le_card hC₂st]
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
C : Finset α
H : Finset α := C.mulStab
hH : H = C.mulStab
hCst : C ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
hC : C.Nonempty
hCstab : C.mulStab.Nontrivial
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : ¬(a * b) • H ⊆ s * t
s₁ : Finset α := s ∩ a • H
hs₁ : s₁ = s ∩ a • H
s₂ : Finset α := s ∩ b • H
hs₂ : s₂ = s ∩ b • H
t₁ : Finset α := t ∩ b • H
ht₁ : t₁ = t ∩ b • H
t₂ : Finset α := t ∩ a • H
ht₂ : t₂ = t ∩ a • H
hs₁s : s₁ ⊆ s
hs₂s : s₂ ⊆ s
ht₁t : t₁ ⊆ t
ht₂t : t₂ ⊆ t
has₁ : a ∈ s₁
hbt₁ : b ∈ t₁
hs₁ne : s₁.Nonempty
ht₁ne : t₁.Nonempty
C₁ : Finset α := C ∪ s₁ * t₁
hC₁ : C₁ = C ∪ s₁ * t₁
C₂ : Finset α := C ∪ s₂ * t₂
hC₂ : C₂ = C ∪ s₂ * t₂
H₁ : Finset α := (s₁ * t₁).mulStab
hH₁ : H₁ = (s₁ * t₁).mulStab
H₂ : Finset α := (s₂ * t₂).mulStab
hH₂ : H₂ = (s₂ * t₂).mulStab
hC₁st : C₁ ⊆ s * t
hC₂st : C₂ ⊆ s * t
hstabH₁ : s₁ * t₁ ⊆ (a * b) • H
hstabH₂ : s₂ * t₂ ⊆ (a * b) • H
hCst₁ : Disjoint C (s₁ * t₁)
hCst₂ : Disjoint C (s₂ * t₂)
hst₁ : (s₁ * t₁).card + s₁.card < (s * t).card + s.card
hst₂ : (s₂ * t₂).card + s₂.card < (s * t).card + s.card
hC₁stab : C₁.mulStab = H₁
hH₁H : H₁ ⊂ H
aux1₁ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₁ * t₁).mulStab).card <
    ↑C.mulStab.card - ↑(s₁ * (s₁ * t₁).mulStab).card - ↑(t₁ * (s₁ * t₁).mulStab).card
ht₂ne : t₂.Nonempty
hs₂ne : s₂.Nonempty
hC₂stab : C₂.mulStab = H₂
hH₂H : H₂ ⊂ H
aux1₂ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₂ * t₂).mulStab).card <
    ↑C.mulStab.card - ↑(s₂ * (s₂ * t₂).mulStab).card - ↑(t₂ * (s₂ * t₂).mulStab).card
habH : a • H ≠ b • H
S : Finset α := a • H \ (s₁ ∪ t₂)
hS : S = a • H \ (s₁ ∪ t₂)
T : Finset α := b • H \ (s₂ ∪ t₁)
hT : T = b • H \ (s₂ ∪ t₁)
hST : Disjoint S T
hSst : S ⊆ a • H \ (s ∪ t)
hTst : T ⊆ b • H \ (s ∪ t)
hSTst : Disjoint (S ∪ T) (s ∪ t)
hstconv : ↑(s * t).card + 1 < ↑(s ∩ t).card + ↑(s ∪ t).card
hSTcard : ↑S.card + ↑T.card + ↑(s ∪ t).card ≤ ↑((s ∪ t) * H).card
hH₁ne : H₁.Nonempty
hH₂ne : H₂.Nonempty
aux2₁ : ↑s₁.card + ↑t₁.card + ↑H₁.card ≤ ↑H.card
aux2₂ : ↑s₂.card + ↑t₂.card + ↑H₂.card ≤ ↑H.card
aux3₁ : ↑S.card + ↑T.card + ↑s₁.card + ↑t₁.card - ↑H₁.card < ↑H.card
⊢ ↑((s ∪ t) * H).card + ↑(s ∩ t).card - ↑C.card ≤ ↑H.card
Tactic:
simp only [sub_le_iff_le_add, ← Int.ofNat_add, Int.ofNat_le, add_comm _ C.card,
  add_comm _ (s ∩ t).card, hCcard]
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
C : Finset α
H : Finset α := C.mulStab
hH : H = C.mulStab
hCst : C ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
hC : C.Nonempty
hCstab : C.mulStab.Nontrivial
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : ¬(a * b) • H ⊆ s * t
s₁ : Finset α := s ∩ a • H
hs₁ : s₁ = s ∩ a • H
s₂ : Finset α := s ∩ b • H
hs₂ : s₂ = s ∩ b • H
t₁ : Finset α := t ∩ b • H
ht₁ : t₁ = t ∩ b • H
t₂ : Finset α := t ∩ a • H
ht₂ : t₂ = t ∩ a • H
hs₁s : s₁ ⊆ s
hs₂s : s₂ ⊆ s
ht₁t : t₁ ⊆ t
ht₂t : t₂ ⊆ t
has₁ : a ∈ s₁
hbt₁ : b ∈ t₁
hs₁ne : s₁.Nonempty
ht₁ne : t₁.Nonempty
C₁ : Finset α := C ∪ s₁ * t₁
hC₁ : C₁ = C ∪ s₁ * t₁
C₂ : Finset α := C ∪ s₂ * t₂
hC₂ : C₂ = C ∪ s₂ * t₂
H₁ : Finset α := (s₁ * t₁).mulStab
hH₁ : H₁ = (s₁ * t₁).mulStab
H₂ : Finset α := (s₂ * t₂).mulStab
hH₂ : H₂ = (s₂ * t₂).mulStab
hC₁st : C₁ ⊆ s * t
hC₂st : C₂ ⊆ s * t
hstabH₁ : s₁ * t₁ ⊆ (a * b) • H
hstabH₂ : s₂ * t₂ ⊆ (a * b) • H
hCst₁ : Disjoint C (s₁ * t₁)
hCst₂ : Disjoint C (s₂ * t₂)
hst₁ : (s₁ * t₁).card + s₁.card < (s * t).card + s.card
hst₂ : (s₂ * t₂).card + s₂.card < (s * t).card + s.card
hC₁stab : C₁.mulStab = H₁
hH₁H : H₁ ⊂ H
aux1₁ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₁ * t₁).mulStab).card <
    ↑C.mulStab.card - ↑(s₁ * (s₁ * t₁).mulStab).card - ↑(t₁ * (s₁ * t₁).mulStab).card
ht₂ne : t₂.Nonempty
hs₂ne : s₂.Nonempty
hC₂stab : C₂.mulStab = H₂
hH₂H : H₂ ⊂ H
aux1₂ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₂ * t₂).mulStab).card <
    ↑C.mulStab.card - ↑(s₂ * (s₂ * t₂).mulStab).card - ↑(t₂ * (s₂ * t₂).mulStab).card
habH : a • H ≠ b • H
S : Finset α := a • H \ (s₁ ∪ t₂)
hS : S = a • H \ (s₁ ∪ t₂)
T : Finset α := b • H \ (s₂ ∪ t₁)
hT : T = b • H \ (s₂ ∪ t₁)
hST : Disjoint S T
hSst : S ⊆ a • H \ (s ∪ t)
hTst : T ⊆ b • H \ (s ∪ t)
hSTst : Disjoint (S ∪ T) (s ∪ t)
hstconv : ↑(s * t).card + 1 < ↑(s ∩ t).card + ↑(s ∪ t).card
hSTcard : ↑S.card + ↑T.card + ↑(s ∪ t).card ≤ ↑((s ∪ t) * H).card
hH₁ne : H₁.Nonempty
hH₂ne : H₂.Nonempty
aux2₁ : ↑s₁.card + ↑t₁.card + ↑H₁.card ≤ ↑H.card
aux2₂ : ↑s₂.card + ↑t₂.card + ↑H₂.card ≤ ↑H.card
aux3₁ : ↑S.card + ↑T.card + ↑s₁.card + ↑t₁.card - ↑H₁.card < ↑H.card
aux3₂ : ↑S.card + ↑T.card + ↑s₂.card + ↑t₂.card - ↑H₂.card < ↑H.card
⊢ (a • H).card ≤ S.card + (s₁.card + t₂.card)
Tactic:
exact card_le_card_sdiff_add_card.trans (add_le_add_left (card_union_le _ _) _)
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
C : Finset α
H : Finset α := C.mulStab
hH : H = C.mulStab
hCst : C ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
hC : C.Nonempty
hCstab : C.mulStab.Nontrivial
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : ¬(a * b) • H ⊆ s * t
s₁ : Finset α := s ∩ a • H
hs₁ : s₁ = s ∩ a • H
s₂ : Finset α := s ∩ b • H
hs₂ : s₂ = s ∩ b • H
t₁ : Finset α := t ∩ b • H
ht₁ : t₁ = t ∩ b • H
t₂ : Finset α := t ∩ a • H
ht₂ : t₂ = t ∩ a • H
hs₁s : s₁ ⊆ s
hs₂s : s₂ ⊆ s
ht₁t : t₁ ⊆ t
ht₂t : t₂ ⊆ t
has₁ : a ∈ s₁
hbt₁ : b ∈ t₁
hs₁ne : s₁.Nonempty
ht₁ne : t₁.Nonempty
C₁ : Finset α := C ∪ s₁ * t₁
hC₁ : C₁ = C ∪ s₁ * t₁
C₂ : Finset α := C ∪ s₂ * t₂
hC₂ : C₂ = C ∪ s₂ * t₂
H₁ : Finset α := (s₁ * t₁).mulStab
hH₁ : H₁ = (s₁ * t₁).mulStab
H₂ : Finset α := (s₂ * t₂).mulStab
hH₂ : H₂ = (s₂ * t₂).mulStab
hC₁st : C₁ ⊆ s * t
hC₂st : C₂ ⊆ s * t
hstabH₁ : s₁ * t₁ ⊆ (a * b) • H
hstabH₂ : s₂ * t₂ ⊆ (a * b) • H
hCst₁ : Disjoint C (s₁ * t₁)
hCst₂ : Disjoint C (s₂ * t₂)
hst₁ : (s₁ * t₁).card + s₁.card < (s * t).card + s.card
hst₂ : (s₂ * t₂).card + s₂.card < (s * t).card + s.card
hC₁stab : C₁.mulStab = H₁
hH₁H : H₁ ⊂ H
aux1₁ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₁ * t₁).mulStab).card <
    ↑C.mulStab.card - ↑(s₁ * (s₁ * t₁).mulStab).card - ↑(t₁ * (s₁ * t₁).mulStab).card
ht₂ne : t₂.Nonempty
hs₂ne : s₂.Nonempty
hC₂stab : C₂.mulStab = H₂
hH₂H : H₂ ⊂ H
aux1₂ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₂ * t₂).mulStab).card <
    ↑C.mulStab.card - ↑(s₂ * (s₂ * t₂).mulStab).card - ↑(t₂ * (s₂ * t₂).mulStab).card
habH : a • H ≠ b • H
S : Finset α := a • H \ (s₁ ∪ t₂)
hS : S = a • H \ (s₁ ∪ t₂)
T : Finset α := b • H \ (s₂ ∪ t₁)
hT : T = b • H \ (s₂ ∪ t₁)
hST : Disjoint S T
hSst : S ⊆ a • H \ (s ∪ t)
hTst : T ⊆ b • H \ (s ∪ t)
hSTst : Disjoint (S ∪ T) (s ∪ t)
hstconv : ↑(s * t).card + 1 < ↑(s ∩ t).card + ↑(s ∪ t).card
hSTcard : ↑S.card + ↑T.card + ↑(s ∪ t).card ≤ ↑((s ∪ t) * H).card
hH₁ne : H₁.Nonempty
hH₂ne : H₂.Nonempty
aux2₁ : ↑s₁.card + ↑t₁.card + ↑H₁.card ≤ ↑H.card
aux2₂ : ↑s₂.card + ↑t₂.card + ↑H₂.card ≤ ↑H.card
aux3₁ : ↑S.card + ↑T.card + ↑s₁.card + ↑t₁.card - ↑H₁.card < ↑H.card
aux3₂ : ↑S.card + ↑T.card + ↑s₂.card + ↑t₂.card - ↑H₂.card < ↑H.card
aux4₁ : H.card ≤ S.card + (s₁.card + t₂.card)
⊢ (b • H).card ≤ T.card + (s₂.card + t₁.card)
Tactic:
exact card_le_card_sdiff_add_card.trans (add_le_add_left (card_union_le _ _) _)
Proof state after:
no goals
Theorem: ZMod.totalDegree_f₁_add_totalDegree_f₂
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ (ZMod.f₁ s).totalDegree + (ZMod.f₂ s).totalDegree < 2 * p - 1
Tactic:
refine (add_le_add (totalDegree_finset_sum _ _) $ (totalDegree_finset_sum _ _).trans $
  Finset.sup_mono_fun fun a _ ↦ totalDegree_smul_le _ _).trans_lt ?_
Proof state after:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ ((s.toEnumFinset.attach.sup fun i => (X i ^ (p - 1)).totalDegree) +
      s.toEnumFinset.attach.sup fun a => (X a ^ (p - 1)).totalDegree) <
    2 * p - 1
Theorem: ZMod.totalDegree_f₁_add_totalDegree_f₂
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ ((s.toEnumFinset.attach.sup fun i => (X i ^ (p - 1)).totalDegree) +
      s.toEnumFinset.attach.sup fun a => (X a ^ (p - 1)).totalDegree) <
    2 * p - 1
Tactic:
simp only [totalDegree_X_pow, ← two_mul]
Proof state after:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ (2 * s.toEnumFinset.attach.sup fun i => p - 1) < 2 * p - 1
Theorem: ZMod.totalDegree_f₁_add_totalDegree_f₂
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ (2 * s.toEnumFinset.attach.sup fun i => p - 1) < 2 * p - 1
Tactic:
refine (mul_le_mul_left' Finset.sup_const_le _).trans_lt ?_
Proof state after:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ 2 * (p - 1) < 2 * p - 1
Theorem: ZMod.totalDegree_f₁_add_totalDegree_f₂
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ 2 * (p - 1) < 2 * p - 1
Tactic:
rw [mul_tsub, mul_one]
Proof state after:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ 2 * p - 2 < 2 * p - 1
Theorem: ZMod.totalDegree_f₁_add_totalDegree_f₂
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ 2 * p - 2 < 2 * p - 1
Tactic:
exact tsub_lt_tsub_left_of_le ((Fact.out : p.Prime).two_le.trans $
  le_mul_of_one_le_left' one_le_two) one_lt_two
Proof state after:
no goals
Theorem: ZMod.aux
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
haveI : NeZero p := inferInstance
Proof state after:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
this : NeZero p
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Theorem: ZMod.aux
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
this : NeZero p
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
set N := Fintype.card {x // eval x (f₁ s) = 0 ∧ eval x (f₂ s) = 0}
Proof state after:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 }
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Theorem: ZMod.aux
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 }
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
let zero_sol : {x // eval x (f₁ s) = 0 ∧ eval x (f₂ s) = 0} :=
  ⟨0, by simp [f₁, f₂, map_sum, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]⟩
Proof state after:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 }
zero_sol : { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 } := ⟨0, ⋯⟩
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Theorem: ZMod.aux
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 }
zero_sol : { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 } := ⟨0, ⋯⟩
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
have hN₀ : 0 < N := @Fintype.card_pos _ _ ⟨zero_sol⟩
Proof state after:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 }
zero_sol : { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Theorem: ZMod.aux
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 }
zero_sol : { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
have hs' : 2 * p - 1 = Fintype.card s.toEnumFinset := by simp [hs]
Proof state after:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 }
zero_sol : { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card { x // x ∈ s.toEnumFinset }
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Theorem: ZMod.aux
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 }
zero_sol : { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card { x // x ∈ s.toEnumFinset }
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
have hpN : p ∣ N := char_dvd_card_solutions_of_add_lt p
  (totalDegree_f₁_add_totalDegree_f₂.trans_eq hs')
Proof state after:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 }
zero_sol : { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card { x // x ∈ s.toEnumFinset }
hpN : p ∣ N
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0