have ht₁ne : t₁.Nonempty := ⟨_, hbt₁⟩
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.inr.inr.intro.intro.intro.intro.intro.intro
α : 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
⊢ False
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.inr.inr.intro.intro.intro.intro.intro.intro
α : 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
⊢ False