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.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:
suffices (C.card : ℤ) + (s₂ * t₂).card ≤ (s * t).card by linarith [this, hSTcard]
Proof state after:
α : 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