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

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
ih : (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hconv : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hnotconv : (C ∪ s' * t').card + (C ∪ s' * t').mulStab.card < (s ∩ t).card + ((s ∪ t) * (C ∪ s' * t').mulStab).card
hCun : (C ∪ s' * t').mulStab = (s' * t').mulStab
hsub : (s' * t').mulStab ⊆ C.mulStab
hdisj : Disjoint C (s' * t')
⊢ ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s' * t').mulStab).card <
    ↑C.mulStab.card - ↑(s' * (s' * t').mulStab).card - ↑(t' * (s' * t').mulStab).card
Tactic:
set H := C.mulStab
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
ih : (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hnotconv : (C ∪ s' * t').card + (C ∪ s' * t').mulStab.card < (s ∩ t).card + ((s ∪ t) * (C ∪ s' * t').mulStab).card
hCun : (C ∪ s' * t').mulStab = (s' * t').mulStab
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
hconv : (s ∩ t).card + ((s ∪ t) * H).card ≤ C.card + H.card
hsub : (s' * t').mulStab ⊆ H
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * (s' * t').mulStab).card <
    ↑H.card - ↑(s' * (s' * t').mulStab).card - ↑(t' * (s' * t').mulStab).card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
ih : (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hnotconv : (C ∪ s' * t').card + (C ∪ s' * t').mulStab.card < (s ∩ t).card + ((s ∪ t) * (C ∪ s' * t').mulStab).card
hCun : (C ∪ s' * t').mulStab = (s' * t').mulStab
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
hconv : (s ∩ t).card + ((s ∪ t) * H).card ≤ C.card + H.card
hsub : (s' * t').mulStab ⊆ H
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * (s' * t').mulStab).card <
    ↑H.card - ↑(s' * (s' * t').mulStab).card - ↑(t' * (s' * t').mulStab).card
Tactic:
set H' := (s' * t').mulStab
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hnotconv : (C ∪ s' * t').card + (C ∪ s' * t').mulStab.card < (s ∩ t).card + ((s ∪ t) * (C ∪ s' * t').mulStab).card
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
hconv : (s ∩ t).card + ((s ∪ t) * H).card ≤ C.card + H.card
H' : Finset α := (s' * t').mulStab
ih : (s' * H').card + (t' * H').card ≤ (s' * t').card + H'.card
hCun : (C ∪ s' * t').mulStab = H'
hsub : H' ⊆ H
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * H').card < ↑H.card - ↑(s' * H').card - ↑(t' * H').card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hnotconv : (C ∪ s' * t').card + (C ∪ s' * t').mulStab.card < (s ∩ t).card + ((s ∪ t) * (C ∪ s' * t').mulStab).card
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
hconv : (s ∩ t).card + ((s ∪ t) * H).card ≤ C.card + H.card
H' : Finset α := (s' * t').mulStab
ih : (s' * H').card + (t' * H').card ≤ (s' * t').card + H'.card
hCun : (C ∪ s' * t').mulStab = H'
hsub : H' ⊆ H
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * H').card < ↑H.card - ↑(s' * H').card - ↑(t' * H').card
Tactic:
set C' := C ∪ s' * t'
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
hconv : (s ∩ t).card + ((s ∪ t) * H).card ≤ C.card + H.card
H' : Finset α := (s' * t').mulStab
ih : (s' * H').card + (t' * H').card ≤ (s' * t').card + H'.card
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hnotconv : C'.card + C'.mulStab.card < (s ∩ t).card + ((s ∪ t) * C'.mulStab).card
hCun : C'.mulStab = H'
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * H').card < ↑H.card - ↑(s' * H').card - ↑(t' * H').card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
hconv : (s ∩ t).card + ((s ∪ t) * H).card ≤ C.card + H.card
H' : Finset α := (s' * t').mulStab
ih : (s' * H').card + (t' * H').card ≤ (s' * t').card + H'.card
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hnotconv : C'.card + C'.mulStab.card < (s ∩ t).card + ((s ∪ t) * C'.mulStab).card
hCun : C'.mulStab = H'
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * H').card < ↑H.card - ↑(s' * H').card - ↑(t' * H').card
Tactic:
zify at hconv hnotconv ih
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * H').card < ↑H.card - ↑(s' * H').card - ↑(t' * H').card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * H').card < ↑H.card - ↑(s' * H').card - ↑(t' * H').card
Tactic:
calc
  (((s ∪ t) * H).card - ((s ∪ t) * H').card : ℤ) <
      C.card + H.card - (s ∩ t).card - (C'.card + H'.card - (s ∩ t).card) := by
    rw [← hCun]
    linarith [hconv, hnotconv]
  _ = H.card - (s' * t').card - H'.card := by
    rw [card_union_of_disjoint hdisj, Int.ofNat_add]
    abel
  _ ≤ H.card - (s' * H').card - (t' * H').card := by linarith [ih]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * H').card < ↑C.card + ↑H.card - ↑(s ∩ t).card - (↑C'.card + ↑H'.card - ↑(s ∩ t).card)
Tactic:
rw [← hCun]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * C'.mulStab).card <
    ↑C.card + ↑H.card - ↑(s ∩ t).card - (↑C'.card + ↑C'.mulStab.card - ↑(s ∩ t).card)

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * C'.mulStab).card <
    ↑C.card + ↑H.card - ↑(s ∩ t).card - (↑C'.card + ↑C'.mulStab.card - ↑(s ∩ t).card)
Tactic:
linarith [hconv, hnotconv]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑C.card + ↑H.card - ↑(s ∩ t).card - (↑C'.card + ↑H'.card - ↑(s ∩ t).card) = ↑H.card - ↑(s' * t').card - ↑H'.card
Tactic:
rw [card_union_of_disjoint hdisj, Int.ofNat_add]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑C.card + ↑H.card - ↑(s ∩ t).card - (↑C.card + ↑(s' * t').card + ↑H'.card - ↑(s ∩ t).card) =
    ↑H.card - ↑(s' * t').card - ↑H'.card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑C.card + ↑H.card - ↑(s ∩ t).card - (↑C.card + ↑(s' * t').card + ↑H'.card - ↑(s ∩ t).card) =
    ↑H.card - ↑(s' * t').card - ↑H'.card
Tactic:
abel
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑H.card - ↑(s' * t').card - ↑H'.card ≤ ↑H.card - ↑(s' * H').card - ↑(t' * H').card
Tactic:
linarith [ih]
State after:
no goals