internlm/Lean-Github huggingface dataset:
Theorem: Finset.card_mul_add_card_lt
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hC : C.Nonempty
hs : s' ⊆ s
ht : t' ⊆ t
hCst : C ⊆ s * t
hCst' : Disjoint C (s' * t')
⊢ ((s * t) \ (s' * t')).Nonempty
Tactic:
exact hC.mono (subset_sdiff.2 ⟨hCst, hCst'⟩)
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
set n : ℕ := (s * t).card + s.card with hn
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
n : ℕ := (s * t).card + s.card
hn : n = (s * t).card + s.card
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
n : ℕ := (s * t).card + s.card
hn : n = (s * t).card + s.card
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
clear_value n
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
n : ℕ
hn : n = (s * t).card + s.card
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
n : ℕ
hn : n = (s * t).card + s.card
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
clear s' t' C a b
Proof state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hn : n = (s * t).card + s.card
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Theorem: Finset.mul_kneser
Proof state before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hn : n = (s * t).card + s.card
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
induction' n using Nat.strong_induction_on with n ih generalizing α
Proof state after:
case h
n : ℕ
ih :
  ∀ m < n,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hn : n = (s * t).card + s.card
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Theorem: Finset.mul_kneser
Proof state before:
case h
n : ℕ
ih :
  ∀ m < n,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hn : n = (s * t).card + s.card
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
subst hn
Proof state after:
case h
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ih :
  ∀ m < (s * t).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Theorem: Finset.mul_kneser
Proof state before:
case h
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ih :
  ∀ m < (s * t).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
Proof state after:
case h.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
t : Finset α
ih :
  ∀ m < (∅ * t).card + ∅.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
⊢ (∅ * (∅ * t).mulStab).card + (t * (∅ * t).mulStab).card ≤ (∅ * t).card + (∅ * t).mulStab.card

case h.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ih :
  ∀ m < (s * t).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
hs : s.Nonempty
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Theorem: Finset.mul_kneser
Proof state before:
case h.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ih :
  ∀ m < (s * t).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
hs : s.Nonempty
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty
Proof state after:
case h.inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
ih :
  ∀ m < (s * ∅).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
⊢ (s * (s * ∅).mulStab).card + (∅ * (s * ∅).mulStab).card ≤ (s * ∅).card + (s * ∅).mulStab.card

case h.inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ih :
  ∀ m < (s * t).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
hs : s.Nonempty
ht : t.Nonempty
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Theorem: Finset.mul_kneser
Proof state before:
case h.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
t : Finset α
ih :
  ∀ m < (∅ * t).card + ∅.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
⊢ (∅ * (∅ * t).mulStab).card + (t * (∅ * t).mulStab).card ≤ (∅ * t).card + (∅ * t).mulStab.card
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
ih :
  ∀ m < (s * ∅).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
⊢ (s * (s * ∅).mulStab).card + (∅ * (s * ∅).mulStab).card ≤ (s * ∅).card + (s * ∅).mulStab.card
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ih :
  ∀ m < (s * t).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
hs : s.Nonempty
ht : t.Nonempty
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
obtain hstab | hstab := ne_or_eq (s * t).mulStab 1
Proof state after:
case h.inr.inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ih :
  ∀ m < (s * t).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
hs : s.Nonempty
ht : t.Nonempty
hstab : (s * t).mulStab ≠ 1
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card

case h.inr.inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ih :
  ∀ m < (s * t).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
hs : s.Nonempty
ht : t.Nonempty
hstab : (s * t).mulStab = 1
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ih :
  ∀ m < (s * t).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
hs : s.Nonempty
ht : t.Nonempty
hstab : (s * t).mulStab = 1
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
simp only [hstab, mul_one, card_one] at ih ⊢
Proof state after:
case h.inr.inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ih :
  ∀ m < (s * t).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
hs : s.Nonempty
ht : t.Nonempty
hstab : (s * t).mulStab = 1
⊢ s.card + t.card ≤ (s * t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ih :
  ∀ m < (s * t).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
hs : s.Nonempty
ht : t.Nonempty
hstab : (s * t).mulStab = 1
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
replace ih := fun s' t' h => @ih _ h α _ _ s' t' rfl
Proof state after:
case h.inr.inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
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
⊢ s.card + t.card ≤ (s * t).card + 1
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
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
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
obtain ⟨a, rfl⟩ | ⟨a, ha, b, hb, hab⟩ := hs.exists_eq_singleton_or_nontrivial
Proof state after:
case h.inr.inr.inr.inl.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
t : Finset α
ht : t.Nonempty
a : α
hs : {a}.Nonempty
hstab : ({a} * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < ({a} * t).card + {a}.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
⊢ {a}.card + t.card ≤ ({a} * t).card + 1

case h.inr.inr.inr.inr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
⊢ 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
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
have : b / a ∉ t.mulStab := by
  refine' fun h => hab (Eq.symm (eq_of_div_eq_one _))
  replace h := subset_mulStab_mul_right hs h
  rw [hstab, mem_one] at h
  exact h
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b / a ∉ t.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
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b / a ∉ t.mulStab
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
simp only [mem_mulStab' ht, smul_eq_mul, Classical.not_forall, exists_prop] at this
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : ∃ x ∈ t, b / a * x ∉ t
⊢ 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
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : ∃ x ∈ t, b / a * x ∉ t
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
obtain ⟨c, hc, hbac⟩ := this
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
hc : c ∈ t
hbac : b / a * c ∉ t
⊢ 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 t : Finset α
hs : s.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
hc : c ∈ t
hbac : b / a * c ∉ t
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
set t' := (a / c) • t with ht'
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
hc : c ∈ t
hbac : b / a * c ∉ t
t' : Finset α := (a / c) • t
ht' : t' = (a / c) • t
⊢ 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 t : Finset α
hs : s.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
hc : c ∈ t
hbac : b / a * c ∉ t
t' : Finset α := (a / c) • t
ht' : t' = (a / c) • t
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
clear_value t'
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
hc : c ∈ t
hbac : b / a * c ∉ t
t' : Finset α
ht' : t' = (a / c) • t
⊢ 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 t : Finset α
hs : s.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
hc : c ∈ t
hbac : b / a * c ∉ t
t' : Finset α
ht' : t' = (a / c) • t
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
rw [← inv_smul_eq_iff] 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 t : Finset α
hs : s.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
hc : c ∈ t
hbac : b / a * c ∉ t
t' : Finset α
ht' : (a / c)⁻¹ • t' = t
⊢ 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 t : Finset α
hs : s.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
hc : c ∈ t
hbac : b / a * c ∉ t
t' : Finset α
ht' : (a / c)⁻¹ • t' = t
⊢ s.card + t.card ≤ (s * t).card + 1
Tactic:
subst 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 : ((a / c)⁻¹ • t').Nonempty
hstab : (s * (a / c)⁻¹ • t').mulStab = 1
ih :
  ∀ (s' t'_1 : Finset α),
    (s' * t'_1).card + s'.card < (s * (a / c)⁻¹ • t').card + s.card →
      (s' * (s' * t'_1).mulStab).card + (t'_1 * (s' * t'_1).mulStab).card ≤ (s' * t'_1).card + (s' * t'_1).mulStab.card
hc : c ∈ (a / c)⁻¹ • t'
hbac : b / a * c ∉ (a / c)⁻¹ • 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'_1 : Finset α),
    (s' * t'_1).card + s'.card < (s * (a / c)⁻¹ • t').card + s.card →
      (s' * (s' * t'_1).mulStab).card + (t'_1 * (s' * t'_1).mulStab).card ≤ (s' * t'_1).card + (s' * t'_1).mulStab.card
hc : c ∈ (a / c)⁻¹ • t'
hbac : b / a * c ∉ (a / c)⁻¹ • t'
⊢ s.card + ((a / c)⁻¹ • t').card ≤ (s * (a / c)⁻¹ • t').card + 1
Tactic:
rename' t' => t
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 : c ∈ (a / c)⁻¹ • t
hbac : b / a * c ∉ (a / c)⁻¹ • 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 : c ∈ (a / c)⁻¹ • t
hbac : b / a * c ∉ (a / c)⁻¹ • t
⊢ s.card + ((a / c)⁻¹ • t).card ≤ (s * (a / c)⁻¹ • t).card + 1
Tactic:
rw [mem_inv_smul_finset_iff, smul_eq_mul, div_mul_cancel] at 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 : ((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