internlm/Lean-Github huggingface dataset:
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
α : 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
⊢ False
Tactic:
set H₂ := (s₂ * t₂).mulStab with hH₂
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.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}
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
⊢ False
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
α : 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
⊢ False
Tactic:
have hC₁st : C₁ ⊆ s * t := union_subset hCst (mul_subset_mul hs₁s ht₁t)
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.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}
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
⊢ False
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
α : 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
⊢ False
Tactic:
have hC₂st : C₂ ⊆ s * t := union_subset hCst (mul_subset_mul hs₂s ht₂t)
Proof state after:
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.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}
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
⊢ False
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.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
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)
aux4₂ : H.card ≤ T.card + (s₂.card + t₁.card)
⊢ False
Tactic:
linarith [aux2₁, aux2₂, aux3₁, aux3₂, aux4₁, aux4₂]
Proof state after:
no goals
Theorem: Finset.mul_kneser
Proof state before:
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
Tactic:
have image_coe_mul :
  ((s * t).image (↑) : Finset (α ⧸ stabilizer α (s * t))) = s.image (↑) * t.image (↑) :=
  sorry
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
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
⊢ (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.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
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
suffices hineq :
  (s * t).mulStab.card *
      ((s.image (↑) : Finset (α ⧸ stabilizer α (s * t))).card +
          (t.image (↑) : Finset (α ⧸ stabilizer α (s * t))).card -
        1) ≤
    (s * t).card by
rw [mul_tsub, mul_one, mul_add, tsub_le_iff_left, card_mulStab_mul_card_image_coe',
    card_mulStab_mul_card_image_coe'] at hineq
  convert hineq using 1
  exact add_comm _ _
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
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
⊢ (s * t).mulStab.card * ((image QuotientGroup.mk s).card + (image QuotientGroup.mk t).card - 1) ≤ (s * t).card
Theorem: Finset.mul_kneser
Proof state before:
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
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
⊢ (s * t).mulStab.card * ((image QuotientGroup.mk s).card + (image QuotientGroup.mk t).card - 1) ≤ (s * t).card
Tactic:
refine le_of_le_of_eq (mul_le_mul_left' ?_ _) (card_mul_card_eq_mulStab_card_mul_coe s t).symm
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
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
⊢ (image QuotientGroup.mk s).card + (image QuotientGroup.mk t).card - 1 ≤ (image QuotientGroup.mk (s * t)).card
Theorem: Finset.mul_kneser
Proof state before:
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
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
⊢ (image QuotientGroup.mk s).card + (image QuotientGroup.mk t).card - 1 ≤ (image QuotientGroup.mk (s * t)).card
Tactic:
have := ih _ ?_ (s.image (↑) : Finset (α ⧸ stabilizer α (s * t))) (t.image (↑)) rfl
Proof state after:
case h.inr.inr.inl.refine_2
α : 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
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
this :
  (image QuotientGroup.mk s * (image QuotientGroup.mk s * image QuotientGroup.mk t).mulStab).card +
      (image QuotientGroup.mk t * (image QuotientGroup.mk s * image QuotientGroup.mk t).mulStab).card ≤
    (image QuotientGroup.mk s * image QuotientGroup.mk t).card +
      (image QuotientGroup.mk s * image QuotientGroup.mk t).mulStab.card
⊢ (image QuotientGroup.mk s).card + (image QuotientGroup.mk t).card - 1 ≤ (image QuotientGroup.mk (s * t)).card

case h.inr.inr.inl.refine_1
α : 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
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
⊢ (image QuotientGroup.mk s * image QuotientGroup.mk t).card + (image QuotientGroup.mk s).card < (s * t).card + s.card
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inl.refine_2
α : 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
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
this :
  (image QuotientGroup.mk s * (image QuotientGroup.mk s * image QuotientGroup.mk t).mulStab).card +
      (image QuotientGroup.mk t * (image QuotientGroup.mk s * image QuotientGroup.mk t).mulStab).card ≤
    (image QuotientGroup.mk s * image QuotientGroup.mk t).card +
      (image QuotientGroup.mk s * image QuotientGroup.mk t).mulStab.card
⊢ (image QuotientGroup.mk s).card + (image QuotientGroup.mk t).card - 1 ≤ (image QuotientGroup.mk (s * t)).card

case h.inr.inr.inl.refine_1
α : 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
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
⊢ (image QuotientGroup.mk s * image QuotientGroup.mk t).card + (image QuotientGroup.mk s).card < (s * t).card + s.card
Tactic:
simpa only [← image_coe_mul, mulStab_image_coe_quotient (hs.mul ht), mul_one,
  tsub_le_iff_right, card_one] using this
Proof state after:
case h.inr.inr.inl.refine_1
α : 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
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
⊢ (image QuotientGroup.mk s * image QuotientGroup.mk t).card + (image QuotientGroup.mk s).card < (s * t).card + s.card
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inl.refine_1
α : 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
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
⊢ (image QuotientGroup.mk s * image QuotientGroup.mk t).card + (image QuotientGroup.mk s).card < (s * t).card + s.card
Tactic:
rw [← image_coe_mul, card_mul_card_eq_mulStab_card_mul_coe]
Proof state after:
case h.inr.inr.inl.refine_1
α : 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
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
⊢ (image QuotientGroup.mk (s * t)).card + (image QuotientGroup.mk s).card <
    (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card + s.card
Theorem: Finset.mul_kneser
Proof state before:
case h.inr.inr.inl.refine_1
α : 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
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
⊢ (image QuotientGroup.mk (s * t)).card + (image QuotientGroup.mk s).card <
    (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card + s.card
Tactic:
exact
  add_lt_add_of_lt_of_le
    (lt_mul_left ((hs.mul ht).image _).card_pos $
      Finset.one_lt_card.2 ((hs.mul ht).mulStab_nontrivial.2 hstab))
    card_image_le
Proof state after:
no goals