internlm/Lean-Github huggingface dataset:
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
C : Finset α
H : Finset α := C.mulStab
hH : H = C.mulStab
hCst : C ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
hC : C.Nonempty
hCstab : C.mulStab.Nontrivial
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : ¬(a * b) • H ⊆ s * t
s₁ : Finset α := s ∩ a • H
hs₁ : s₁ = s ∩ a • H
s₂ : Finset α := s ∩ b • H
hs₂ : s₂ = s ∩ b • H
t₁ : Finset α := t ∩ b • H
ht₁ : t₁ = t ∩ b • H
t₂ : Finset α := t ∩ a • H
ht₂ : t₂ = t ∩ a • H
hs₁s : s₁ ⊆ s
hs₂s : s₂ ⊆ s
ht₁t : t₁ ⊆ t
ht₂t : t₂ ⊆ t
has₁ : a ∈ s₁
hbt₁ : b ∈ t₁
hs₁ne : s₁.Nonempty
ht₁ne : t₁.Nonempty
C₁ : Finset α := C ∪ s₁ * t₁
hC₁ : C₁ = C ∪ s₁ * t₁
C₂ : Finset α := C ∪ s₂ * t₂
hC₂ : C₂ = C ∪ s₂ * t₂
H₁ : Finset α := (s₁ * t₁).mulStab
hH₁ : H₁ = (s₁ * t₁).mulStab
H₂ : Finset α := (s₂ * t₂).mulStab
hH₂ : H₂ = (s₂ * t₂).mulStab
hC₁st : C₁ ⊆ s * t
hC₂st : C₂ ⊆ s * t
hstabH₁ : s₁ * t₁ ⊆ (a * b) • H
⊢ t₂ * s₂ ⊆ a • C.mulStab * b • C.mulStab
Tactic:
apply mul_subset_mul inter_subset_right inter_subset_right
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.inr.inr.intro.intro.intro.intro.intro.intro.inl
α : 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₂ : t₂ = ∅
aux₁_contr :
  ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card ≤
    ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card
⊢ False
Tactic:
linarith [aux1₁, aux₁_contr, Int.natCast_nonneg (t₁ * (s₁ * t₁).mulStab).card]
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.inr.inr.intro.intro.intro.intro.intro.intro.inr.inl
α : 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₂ : s₂ = ∅
aux1₁_contr :
  ↑C.mulStab.card - ↑(t ∩ b • C.mulStab * (s₁ * t₁).mulStab).card ≤
    ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₁ * t₁).mulStab).card
⊢ False
Tactic:
linarith [aux1₁, aux1₁_contr, Int.natCast_nonneg (s₁ * (s₁ * t₁).mulStab).card]
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
C : Finset α
H : Finset α := C.mulStab
hH : H = C.mulStab
hCst : C ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
hC : C.Nonempty
hCstab : C.mulStab.Nontrivial
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : ¬(a * b) • H ⊆ s * t
s₁ : Finset α := s ∩ a • H
hs₁ : s₁ = s ∩ a • H
s₂ : Finset α := s ∩ b • H
hs₂✝ : s₂ = s ∩ b • H
t₁ : Finset α := t ∩ b • H
ht₁ : t₁ = t ∩ b • H
t₂ : Finset α := t ∩ a • H
ht₂ : t₂ = t ∩ a • H
hs₁s : s₁ ⊆ s
hs₂s : s₂ ⊆ s
ht₁t : t₁ ⊆ t
ht₂t : t₂ ⊆ t
has₁ : a ∈ s₁
hbt₁ : b ∈ t₁
hs₁ne : s₁.Nonempty
ht₁ne : t₁.Nonempty
C₁ : Finset α := C ∪ s₁ * t₁
hC₁ : C₁ = C ∪ s₁ * t₁
C₂ : Finset α := C ∪ s₂ * t₂
hC₂ : C₂ = C ∪ s₂ * t₂
H₁ : Finset α := (s₁ * t₁).mulStab
hH₁ : H₁ = (s₁ * t₁).mulStab
H₂ : Finset α := (s₂ * t₂).mulStab
hH₂ : H₂ = (s₂ * t₂).mulStab
hC₁st : C₁ ⊆ s * t
hC₂st : C₂ ⊆ s * t
hstabH₁ : s₁ * t₁ ⊆ (a * b) • H
hstabH₂ : s₂ * t₂ ⊆ (a * b) • H
hCst₁ : Disjoint C (s₁ * t₁)
hCst₂ : Disjoint C (s₂ * t₂)
hst₁ : (s₁ * t₁).card + s₁.card < (s * t).card + s.card
hst₂ : (s₂ * t₂).card + s₂.card < (s * t).card + s.card
hC₁stab : C₁.mulStab = H₁
hH₁H : H₁ ⊂ H
aux1₁ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₁ * t₁).mulStab).card <
    ↑C.mulStab.card - ↑(s₁ * (s₁ * t₁).mulStab).card - ↑(t₁ * (s₁ * t₁).mulStab).card
ht₂ne : t₂.Nonempty
hs₂ : s₂ = ∅
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
Tactic:
exact hH₁H.subset
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
C : Finset α
H : Finset α := C.mulStab
hH : H = C.mulStab
hCst : C ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
hC : C.Nonempty
hCstab : C.mulStab.Nontrivial
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : ¬(a * b) • H ⊆ s * t
s₁ : Finset α := s ∩ a • H
hs₁ : s₁ = s ∩ a • H
s₂ : Finset α := s ∩ b • H
hs₂ : s₂ = s ∩ b • H
t₁ : Finset α := t ∩ b • H
ht₁ : t₁ = t ∩ b • H
t₂ : Finset α := t ∩ a • H
ht₂ : t₂ = t ∩ a • H
hs₁s : s₁ ⊆ s
hs₂s : s₂ ⊆ s
ht₁t : t₁ ⊆ t
ht₂t : t₂ ⊆ t
has₁ : a ∈ s₁
hbt₁ : b ∈ t₁
hs₁ne : s₁.Nonempty
ht₁ne : t₁.Nonempty
C₁ : Finset α := C ∪ s₁ * t₁
hC₁ : C₁ = C ∪ s₁ * t₁
C₂ : Finset α := C ∪ s₂ * t₂
hC₂ : C₂ = C ∪ s₂ * t₂
H₁ : Finset α := (s₁ * t₁).mulStab
hH₁ : H₁ = (s₁ * t₁).mulStab
H₂ : Finset α := (s₂ * t₂).mulStab
hH₂ : H₂ = (s₂ * t₂).mulStab
hC₁st : C₁ ⊆ s * t
hC₂st : C₂ ⊆ s * t
hstabH₁ : s₁ * t₁ ⊆ (a * b) • H
hstabH₂ : s₂ * t₂ ⊆ (a * b) • H
hCst₁ : Disjoint C (s₁ * t₁)
hCst₂ : Disjoint C (s₂ * t₂)
hst₁ : (s₁ * t₁).card + s₁.card < (s * t).card + s.card
hst₂ : (s₂ * t₂).card + s₂.card < (s * t).card + s.card
hC₁stab : C₁.mulStab = H₁
hH₁H : H₁ ⊂ H
aux1₁ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₁ * t₁).mulStab).card <
    ↑C.mulStab.card - ↑(s₁ * (s₁ * t₁).mulStab).card - ↑(t₁ * (s₁ * t₁).mulStab).card
ht₂ne : t₂.Nonempty
hs₂ne : s₂.Nonempty
⊢ ¬(b * a) • C.mulStab ⊆ s * t
Tactic:
rwa [mul_comm]
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
C : Finset α
H : Finset α := C.mulStab
hH : H = C.mulStab
hCst : C ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
hC : C.Nonempty
hCstab : C.mulStab.Nontrivial
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : ¬(a * b) • H ⊆ s * t
s₁ : Finset α := s ∩ a • H
hs₁ : s₁ = s ∩ a • H
s₂ : Finset α := s ∩ b • H
hs₂ : s₂ = s ∩ b • H
t₁ : Finset α := t ∩ b • H
ht₁ : t₁ = t ∩ b • H
t₂ : Finset α := t ∩ a • H
ht₂ : t₂ = t ∩ a • H
hs₁s : s₁ ⊆ s
hs₂s : s₂ ⊆ s
ht₁t : t₁ ⊆ t
ht₂t : t₂ ⊆ t
has₁ : a ∈ s₁
hbt₁ : b ∈ t₁
hs₁ne : s₁.Nonempty
ht₁ne : t₁.Nonempty
C₁ : Finset α := C ∪ s₁ * t₁
hC₁ : C₁ = C ∪ s₁ * t₁
C₂ : Finset α := C ∪ s₂ * t₂
hC₂ : C₂ = C ∪ s₂ * t₂
H₁ : Finset α := (s₁ * t₁).mulStab
hH₁ : H₁ = (s₁ * t₁).mulStab
H₂ : Finset α := (s₂ * t₂).mulStab
hH₂ : H₂ = (s₂ * t₂).mulStab
hC₁st : C₁ ⊆ s * t
hC₂st : C₂ ⊆ s * t
hstabH₁ : s₁ * t₁ ⊆ (a * b) • H
hstabH₂ : s₂ * t₂ ⊆ (a * b) • H
hCst₁ : Disjoint C (s₁ * t₁)
hCst₂ : Disjoint C (s₂ * t₂)
hst₁ : (s₁ * t₁).card + s₁.card < (s * t).card + s.card
hst₂ : (s₂ * t₂).card + s₂.card < (s * t).card + s.card
hC₁stab : C₁.mulStab = H₁
hH₁H : H₁ ⊂ H
aux1₁ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₁ * t₁).mulStab).card <
    ↑C.mulStab.card - ↑(s₁ * (s₁ * t₁).mulStab).card - ↑(t₁ * (s₁ * t₁).mulStab).card
ht₂ne : t₂.Nonempty
hs₂ne : s₂.Nonempty
hC₂stab : C₂.mulStab = H₂
⊢ ¬(b * a) • C.mulStab ⊆ s * t
Tactic:
rwa [mul_comm]
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.inr.inr.intro.intro.intro.intro.intro.intro.inr.inr.inl
α : 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 : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊂ C.mulStab
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
⊢ ↑C.mulStab.card - ↑(s₁ * (s₁ * t₁).mulStab).card - ↑(t₁ * (s₁ * t₁).mulStab).card ≤
    ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₁ * t₁).mulStab).card
Tactic:
simp only [hs₁, ht₁, ← habH, inter_mul_sub_card_le (hs₁s has₁) hH₁H.subset]
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
C : Finset α
H : Finset α := C.mulStab
hH : H = C.mulStab
hCst : C ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
hC : C.Nonempty
hCstab : C.mulStab.Nontrivial
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : ¬(a * b) • H ⊆ s * t
s₁ : Finset α := s ∩ a • H
hs₁ : s₁ = s ∩ a • H
s₂ : Finset α := s ∩ b • H
hs₂ : s₂ = s ∩ b • H
t₁ : Finset α := t ∩ b • H
ht₁ : t₁ = t ∩ b • H
t₂ : Finset α := t ∩ a • H
ht₂ : t₂ = t ∩ a • H
hs₁s : s₁ ⊆ s
hs₂s : s₂ ⊆ s
ht₁t : t₁ ⊆ t
ht₂t : t₂ ⊆ t
has₁ : a ∈ s₁
hbt₁ : b ∈ t₁
hs₁ne : s₁.Nonempty
ht₁ne : t₁.Nonempty
C₁ : Finset α := C ∪ s₁ * t₁
hC₁ : C₁ = C ∪ s₁ * t₁
C₂ : Finset α := C ∪ s₂ * t₂
hC₂ : C₂ = C ∪ s₂ * t₂
H₁ : Finset α := (s₁ * t₁).mulStab
hH₁ : H₁ = (s₁ * t₁).mulStab
H₂ : Finset α := (s₂ * t₂).mulStab
hH₂ : H₂ = (s₂ * t₂).mulStab
hC₁st : C₁ ⊆ s * t
hC₂st : C₂ ⊆ s * t
hstabH₁ : s₁ * t₁ ⊆ (a * b) • H
hstabH₂ : s₂ * t₂ ⊆ (a * b) • H
hCst₁ : Disjoint C (s₁ * t₁)
hCst₂ : Disjoint C (s₂ * t₂)
hst₁ : (s₁ * t₁).card + s₁.card < (s * t).card + s.card
hst₂ : (s₂ * t₂).card + s₂.card < (s * t).card + s.card
hC₁stab : C₁.mulStab = H₁
hH₁H : H₁ ⊂ H
aux1₁ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₁ * t₁).mulStab).card <
    ↑C.mulStab.card - ↑(s₁ * (s₁ * t₁).mulStab).card - ↑(t₁ * (s₁ * t₁).mulStab).card
ht₂ne : t₂.Nonempty
hs₂ne : s₂.Nonempty
hC₂stab : C₂.mulStab = H₂
hH₂H : H₂ ⊂ H
aux1₂ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₂ * t₂).mulStab).card <
    ↑C.mulStab.card - ↑(s₂ * (s₂ * t₂).mulStab).card - ↑(t₂ * (s₂ * t₂).mulStab).card
habH : a • H ≠ b • H
S : Finset α := a • H \ (s₁ ∪ t₂)
hS : S = a • H \ (s₁ ∪ t₂)
T : Finset α := b • H \ (s₂ ∪ t₁)
hT : T = b • H \ (s₂ ∪ t₁)
hST : Disjoint S T
⊢ S ⊆ a • H \ (s ∪ t)
Tactic:
simp only [hS, hs₁, ht₂, ← union_inter_distrib_right, sdiff_inter_self_right, Subset.rfl]
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
C : Finset α
H : Finset α := C.mulStab
hH : H = C.mulStab
hCst : C ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
hC : C.Nonempty
hCstab : C.mulStab.Nontrivial
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : ¬(a * b) • H ⊆ s * t
s₁ : Finset α := s ∩ a • H
hs₁ : s₁ = s ∩ a • H
s₂ : Finset α := s ∩ b • H
hs₂ : s₂ = s ∩ b • H
t₁ : Finset α := t ∩ b • H
ht₁ : t₁ = t ∩ b • H
t₂ : Finset α := t ∩ a • H
ht₂ : t₂ = t ∩ a • H
hs₁s : s₁ ⊆ s
hs₂s : s₂ ⊆ s
ht₁t : t₁ ⊆ t
ht₂t : t₂ ⊆ t
has₁ : a ∈ s₁
hbt₁ : b ∈ t₁
hs₁ne : s₁.Nonempty
ht₁ne : t₁.Nonempty
C₁ : Finset α := C ∪ s₁ * t₁
hC₁ : C₁ = C ∪ s₁ * t₁
C₂ : Finset α := C ∪ s₂ * t₂
hC₂ : C₂ = C ∪ s₂ * t₂
H₁ : Finset α := (s₁ * t₁).mulStab
hH₁ : H₁ = (s₁ * t₁).mulStab
H₂ : Finset α := (s₂ * t₂).mulStab
hH₂ : H₂ = (s₂ * t₂).mulStab
hC₁st : C₁ ⊆ s * t
hC₂st : C₂ ⊆ s * t
hstabH₁ : s₁ * t₁ ⊆ (a * b) • H
hstabH₂ : s₂ * t₂ ⊆ (a * b) • H
hCst₁ : Disjoint C (s₁ * t₁)
hCst₂ : Disjoint C (s₂ * t₂)
hst₁ : (s₁ * t₁).card + s₁.card < (s * t).card + s.card
hst₂ : (s₂ * t₂).card + s₂.card < (s * t).card + s.card
hC₁stab : C₁.mulStab = H₁
hH₁H : H₁ ⊂ H
aux1₁ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₁ * t₁).mulStab).card <
    ↑C.mulStab.card - ↑(s₁ * (s₁ * t₁).mulStab).card - ↑(t₁ * (s₁ * t₁).mulStab).card
ht₂ne : t₂.Nonempty
hs₂ne : s₂.Nonempty
hC₂stab : C₂.mulStab = H₂
hH₂H : H₂ ⊂ H
aux1₂ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₂ * t₂).mulStab).card <
    ↑C.mulStab.card - ↑(s₂ * (s₂ * t₂).mulStab).card - ↑(t₂ * (s₂ * t₂).mulStab).card
habH : a • H ≠ b • H
S : Finset α := a • H \ (s₁ ∪ t₂)
hS : S = a • H \ (s₁ ∪ t₂)
T : Finset α := b • H \ (s₂ ∪ t₁)
hT : T = b • H \ (s₂ ∪ t₁)
hST : Disjoint S T
hSst : S ⊆ a • H \ (s ∪ t)
⊢ T ⊆ b • H \ (s ∪ t)
Tactic:
simp only [hT, hs₂, ht₁, ← union_inter_distrib_right, sdiff_inter_self_right, Subset.rfl]
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
C : Finset α
H : Finset α := C.mulStab
hH : H = C.mulStab
hCst : C ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
hC : C.Nonempty
hCstab : C.mulStab.Nontrivial
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : ¬(a * b) • H ⊆ s * t
s₁ : Finset α := s ∩ a • H
hs₁ : s₁ = s ∩ a • H
s₂ : Finset α := s ∩ b • H
hs₂ : s₂ = s ∩ b • H
t₁ : Finset α := t ∩ b • H
ht₁ : t₁ = t ∩ b • H
t₂ : Finset α := t ∩ a • H
ht₂ : t₂ = t ∩ a • H
hs₁s : s₁ ⊆ s
hs₂s : s₂ ⊆ s
ht₁t : t₁ ⊆ t
ht₂t : t₂ ⊆ t
has₁ : a ∈ s₁
hbt₁ : b ∈ t₁
hs₁ne : s₁.Nonempty
ht₁ne : t₁.Nonempty
C₁ : Finset α := C ∪ s₁ * t₁
hC₁ : C₁ = C ∪ s₁ * t₁
C₂ : Finset α := C ∪ s₂ * t₂
hC₂ : C₂ = C ∪ s₂ * t₂
H₁ : Finset α := (s₁ * t₁).mulStab
hH₁ : H₁ = (s₁ * t₁).mulStab
H₂ : Finset α := (s₂ * t₂).mulStab
hH₂ : H₂ = (s₂ * t₂).mulStab
hC₁st : C₁ ⊆ s * t
hC₂st : C₂ ⊆ s * t
hstabH₁ : s₁ * t₁ ⊆ (a * b) • H
hstabH₂ : s₂ * t₂ ⊆ (a * b) • H
hCst₁ : Disjoint C (s₁ * t₁)
hCst₂ : Disjoint C (s₂ * t₂)
hst₁ : (s₁ * t₁).card + s₁.card < (s * t).card + s.card
hst₂ : (s₂ * t₂).card + s₂.card < (s * t).card + s.card
hC₁stab : C₁.mulStab = H₁
hH₁H : H₁ ⊂ H
aux1₁ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₁ * t₁).mulStab).card <
    ↑C.mulStab.card - ↑(s₁ * (s₁ * t₁).mulStab).card - ↑(t₁ * (s₁ * t₁).mulStab).card
ht₂ne : t₂.Nonempty
hs₂ne : s₂.Nonempty
hC₂stab : C₂.mulStab = H₂
hH₂H : H₂ ⊂ H
aux1₂ :
  ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s₂ * t₂).mulStab).card <
    ↑C.mulStab.card - ↑(s₂ * (s₂ * t₂).mulStab).card - ↑(t₂ * (s₂ * t₂).mulStab).card
habH : a • H ≠ b • H
S : Finset α := a • H \ (s₁ ∪ t₂)
hS : S = a • H \ (s₁ ∪ t₂)
T : Finset α := b • H \ (s₂ ∪ t₁)
hT : T = b • H \ (s₂ ∪ t₁)
hST : Disjoint S T
hSst : S ⊆ a • H \ (s ∪ t)
hTst : T ⊆ b • H \ (s ∪ t)
hSTst : Disjoint (S ∪ T) (s ∪ t)
⊢ 1 ⊆ C.mulStab
Tactic:
simp only [one_subset, one_mem_mulStab, hC]
Proof state after:
no goals