internlm/Lean-Github huggingface dataset:
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
t : Finset α
ht : ((a / c)⁻¹ • t).Nonempty
hstab : (s * (a / c)⁻¹ • t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * (a / c)⁻¹ • t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hc : a ∈ t
hbac : b / a * c ∉ (a / c)⁻¹ • t
⊢ s.card + ((a / c)⁻¹ • t).card ≤ (s * (a / c)⁻¹ • t).card + 1
Tactic:
rw [div_mul_comm, mem_inv_smul_finset_iff, smul_eq_mul, ← mul_assoc, div_mul_div_cancel',
  div_self', one_mul] at hbac
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
t : Finset α
ht : ((a / c)⁻¹ • t).Nonempty
hstab : (s * (a / c)⁻¹ • t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * (a / c)⁻¹ • t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hc : a ∈ t
hbac : b ∉ t
⊢ s.card + ((a / c)⁻¹ • t).card ≤ (s * (a / c)⁻¹ • t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
t : Finset α
ht : ((a / c)⁻¹ • t).Nonempty
hstab : (s * (a / c)⁻¹ • t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * (a / c)⁻¹ • t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hc : a ∈ t
hbac : b ∉ t
⊢ s.card + ((a / c)⁻¹ • t).card ≤ (s * (a / c)⁻¹ • t).card + 1
Tactic:
rw [smul_finset_nonempty] at ht
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * (a / c)⁻¹ • t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * (a / c)⁻¹ • t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hc : a ∈ t
hbac : b ∉ t
⊢ s.card + ((a / c)⁻¹ • t).card ≤ (s * (a / c)⁻¹ • t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * (a / c)⁻¹ • t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * (a / c)⁻¹ • t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hc : a ∈ t
hbac : b ∉ t
⊢ s.card + ((a / c)⁻¹ • t).card ≤ (s * (a / c)⁻¹ • t).card + 1
Tactic:
simp only [mul_smul_comm, smul_mul_assoc, mulStab_smul, card_smul_finset] at *
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
t : Finset α
ht : t.Nonempty
hc : a ∈ t
hbac : b ∉ t
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
⊢ s.card + t.card ≤ (s * t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
t : Finset α
ht : t.Nonempty
hc : a ∈ t
hbac : b ∉ t
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
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
have hst : (s ∩ t).Nonempty := ⟨_, mem_inter.2 ⟨ha, hc⟩⟩
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
t : Finset α
ht : t.Nonempty
hc : a ∈ t
hbac : b ∉ t
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
⊢ s.card + t.card ≤ (s * t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
t : Finset α
ht : t.Nonempty
hc : a ∈ t
hbac : b ∉ t
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
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
have hsts : s ∩ t ⊂ s :=
  ⟨inter_subset_left, not_subset.2 ⟨_, hb, fun h => hbac $ inter_subset_right h⟩⟩
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
t : Finset α
ht : t.Nonempty
hc : a ∈ t
hbac : b ∉ t
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
⊢ s.card + t.card ≤ (s * t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
t : Finset α
ht : t.Nonempty
hc : a ∈ t
hbac : b ∉ t
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
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
clear! a b
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
⊢ s.card + t.card ≤ (s * t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
set convergent : Set (Finset α) :=
  {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
⊢ s.card + t.card ≤ (s * t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
have convergent_nonempty : convergent.Nonempty := by
  refine' ⟨s ∩ t * (s ∪ t), inter_mul_union_subset, (add_le_add_right (card_le_card $
    subset_mul_left _ $ one_mem_mulStab.2 $ hst.mul $ hs.mono subset_union_left) _).trans $
      ih (s ∩ t) (s ∪ t) _⟩
  exact add_lt_add_of_le_of_lt (card_le_card inter_mul_union_subset) (card_lt_card hsts)
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
convergent_nonempty : convergent.Nonempty
⊢ s.card + t.card ≤ (s * t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
convergent_nonempty : convergent.Nonempty
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
let C := argminOn (fun C : Finset α => C.mulStab.card) IsWellFounded.wf _ convergent_nonempty
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
convergent_nonempty : convergent.Nonempty
C : Finset α := argminOn (fun C => C.mulStab.card) ⋯ convergent convergent_nonempty
⊢ s.card + t.card ≤ (s * t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
convergent_nonempty : convergent.Nonempty
C : Finset α := argminOn (fun C => C.mulStab.card) ⋯ convergent convergent_nonempty
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
set H := C.mulStab with hH
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
convergent_nonempty : convergent.Nonempty
C : Finset α := argminOn (fun C => C.mulStab.card) ⋯ convergent convergent_nonempty
H : Finset α := C.mulStab
hH : H = C.mulStab
⊢ s.card + t.card ≤ (s * t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
convergent_nonempty : convergent.Nonempty
C : Finset α := argminOn (fun C => C.mulStab.card) ⋯ convergent convergent_nonempty
H : Finset α := C.mulStab
hH : H = C.mulStab
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
obtain ⟨hCst, hCcard⟩ : C ∈ convergent := argminOn_mem _ _ _ _
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
convergent_nonempty : convergent.Nonempty
C : Finset α := argminOn (fun C => C.mulStab.card) ⋯ convergent convergent_nonempty
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
⊢ s.card + t.card ≤ (s * t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
convergent_nonempty : convergent.Nonempty
C : Finset α := argminOn (fun C => C.mulStab.card) ⋯ convergent convergent_nonempty
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
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
have hCmin : ∀ D : Finset α, D.mulStab ⊂ H → ¬D ∈ convergent := fun D hDH hD =>
  (card_lt_card hDH).not_le $ argminOn_le (fun D : Finset α => D.mulStab.card) _ _ hD
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
convergent_nonempty : convergent.Nonempty
C : Finset α := argminOn (fun C => C.mulStab.card) ⋯ convergent convergent_nonempty
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
⊢ s.card + t.card ≤ (s * t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
convergent_nonempty : convergent.Nonempty
C : Finset α := argminOn (fun C => C.mulStab.card) ⋯ convergent convergent_nonempty
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
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
clear_value C
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
convergent_nonempty : convergent.Nonempty
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
⊢ s.card + t.card ≤ (s * t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
convergent_nonempty : convergent.Nonempty
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
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
clear convergent_nonempty
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
C : Finset α
H : Finset α := C.mulStab
hH : H = C.mulStab
hCst : C ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
⊢ s.card + t.card ≤ (s * t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hst : (s ∩ t).Nonempty
hsts : s ∩ t ⊂ s
convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
C : Finset α
H : Finset α := C.mulStab
hH : H = C.mulStab
hCst : C ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
obtain rfl | hC := C.eq_empty_or_nonempty
Proof state after:
case h.inr.inr.inr.inr.intro.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}
H : Finset α := ∅.mulStab
hH : H = ∅.mulStab
hCst : ∅ ⊆ s * t
hCcard : (s ∩ t).card + ((s ∪ t) * ∅.mulStab).card ≤ ∅.card + ∅.mulStab.card
hCmin : ∀ (D : Finset α), D.mulStab ⊂ H → D ∉ convergent
⊢ s.card + t.card ≤ (s * t).card + 1

case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.inr
α : 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
⊢ s.card + t.card ≤ (s * t).card + 1