Theorem: Finset.mul_kneser (LeanCamCombi/Kneser/Kneser.lean)

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
⊢ ↑C.mulStab.card - ↑(s₂ * (s₂ * t₂).mulStab).card - ↑(t₂ * (s₂ * t₂).mulStab).card ≤ ↑H.card - (↑s₂.card + ↑t₂.card)
Tactic:
rw [sub_sub]
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
⊢ ↑C.mulStab.card - (↑(s₂ * (s₂ * t₂).mulStab).card + ↑(t₂ * (s₂ * t₂).mulStab).card) ≤ ↑H.card - (↑s₂.card + ↑t₂.card)

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
⊢ ↑C.mulStab.card - (↑(s₂ * (s₂ * t₂).mulStab).card + ↑(t₂ * (s₂ * t₂).mulStab).card) ≤ ↑H.card - (↑s₂.card + ↑t₂.card)
Tactic:
exact sub_le_sub_left (add_le_add (Nat.cast_le.2 $ card_le_card_mul_right _ hH₂ne) $
  Nat.cast_le.2 $ card_le_card_mul_right _ hH₂ne) _
State after:
no goals

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
⊢ ↑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:
have ih₁ :=
  (add_le_add (card_le_card_mul_right _ hH₁ne) $ card_le_card_mul_right _ hH₁ne).trans
    (ih _ _ hst₁)
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
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

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
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:
zify at ih₁
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
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

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
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 [hstconv, ih₁]
State after:
no goals

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
⊢ ↑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]
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
⊢ ↑C.card + ↑(s₁ * t₁).card ≤ ↑(s * t).card

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
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]
State after:
no goals

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
⊢ ↑C.card + ↑(s₁ * t₁).card ≤ ↑(s * t).card
Tactic:
norm_cast
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
⊢ C.card + (s₁ * t₁).card ≤ (s * t).card

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
⊢ C.card + (s₁ * t₁).card ≤ (s * t).card
Tactic:
simp only [← card_union_of_disjoint hCst₁, card_le_card hC₁st]
State after:
no goals

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
⊢ ↑((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]
State after:
no goals

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₂.card + ↑t₂.card - ↑H₂.card <
    ↑S.card + ↑T.card + ↑(s ∪ t).card + ↑(s ∩ t).card - ↑(s * t).card + ↑(s₂ * t₂).card
Tactic:
have ih₂ :=
  (add_le_add (card_le_card_mul_right _ hH₂ne) $ card_le_card_mul_right _ hH₂ne).trans
    (ih _ _ hst₂)
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
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

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:
zify at hstconv ih₂
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
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

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₂]
State after:
no goals

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]
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

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]
State after:
no goals

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:
norm_cast
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

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]
State after:
no goals

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]
State after:
no goals

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
⊢ H.card ≤ S.card + (s₁.card + t₂.card)
Tactic:
rw [← card_smul_finset a H]
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
aux3₂ : ↑S.card + ↑T.card + ↑s₂.card + ↑t₂.card - ↑H₂.card < ↑H.card
⊢ (a • H).card ≤ S.card + (s₁.card + t₂.card)

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 _ _) _)
State after:
no goals

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)
⊢ H.card ≤ T.card + (s₂.card + t₁.card)
Tactic:
rw [← card_smul_finset b H]
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
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)

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 _ _) _)
State after:
no goals