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

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
⊢ (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab = (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
obtain rfl | hCne := C.eq_empty_or_nonempty
State after:
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' : Finset α
a b : α
hs₁ : (s ∩ a • ∅.mulStab).Nonempty
ht₁ : (t ∩ b • ∅.mulStab).Nonempty
hab : ¬(a * b) • ∅.mulStab ⊆ s * t
hC : Disjoint ∅ (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab))
⊢ (∅ ∪ s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab = (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab

case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
⊢ (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab = (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

State before:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
⊢ (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab = (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
refine'
  ((subset_inter (mulStab_mul_ssubset_mulStab hs₁ ht₁ hab).subset Subset.rfl).trans
        inter_mulStab_subset_mulStab_union).antisymm'
    fun x hx => _
State after:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x ∈ (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

State before:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x ∈ (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
replace hx := (mem_mulStab $ (hs₁.mul ht₁).mono subset_union_right).mp hx
State after:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

State before:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
rw [smul_finset_union] at hx
State after:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

State before:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
suffices hxC : x ∈ C.mulStab by
  rw [(mem_mulStab hCne).mp hxC] at hx
  rw [mem_mulStab_iff_subset_smul_finset (hs₁.mul ht₁)]
  exact hC.symm.left_le_of_le_sup_left (le_sup_right.trans hx.ge)
State after:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x ∈ C.mulStab

State before:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x ∈ C.mulStab
Tactic:
rw [mem_mulStab_iff_smul_finset_subset hCne]
State after:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x • C ⊆ C

State before:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x • C ⊆ C
Tactic:
obtain h | h := disjoint_or_nonempty_inter (x • C) (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
State after:
case inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : Disjoint (x • C) (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
⊢ x • C ⊆ C

case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C

State before:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C
Tactic:
have hUn :
  ((C.biUnion fun y => x • y • C.mulStab) ∩
      (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty := by
  have : (x • C.biUnion fun y => y • C.mulStab) = C.biUnion fun y => x • y • C.mulStab :=
    biUnion_image
  simpa [← this]
State after:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hUn : ((C.biUnion fun y => x • y • C.mulStab) ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C

State before:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hUn : ((C.biUnion fun y => x • y • C.mulStab) ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C
Tactic:
simp_rw [biUnion_inter, biUnion_nonempty, ← smul_assoc, smul_eq_mul] at hUn
State after:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hUn : ∃ x_1 ∈ C, ((x * x_1) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C

State before:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hUn : ∃ x_1 ∈ C, ((x * x_1) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C
Tactic:
obtain ⟨y, hy, hyne⟩ := hUn
State after:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C

State before:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ x • C ⊆ C
Tactic:
have hxyCsubC : (x * y) • C.mulStab ⊆ x • C := by
  rw [← smul_eq_mul, smul_assoc, smul_finset_subset_smul_finset_iff]
  exact smul_finset_mulStab_subset hy
State after:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
⊢ x • C ⊆ C

State before:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
⊢ x • C ⊆ C
Tactic:
have hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) :=
  hxyC.left_le_of_le_sup_left (hxyCsubC.trans $ subset_union_left.trans hx.subset')
State after:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x • C ⊆ C

State before:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ x • C ⊆ C
Tactic:
suffices s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab by
  have := (card_le_card hxysub).not_lt ((card_lt_card this).trans_eq ?_)
  cases this
  simp_rw [card_smul_finset]
State after:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab

State before:
case inr.inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
Tactic:
apply ssubset_of_subset_not_subset
State after:
case inr.inr.intro.intro.h₁
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * b) • C.mulStab

case inr.inr.intro.intro.h₂
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ ¬(a * b) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)

State before:
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' : Finset α
a b : α
hs₁ : (s ∩ a • ∅.mulStab).Nonempty
ht₁ : (t ∩ b • ∅.mulStab).Nonempty
hab : ¬(a * b) • ∅.mulStab ⊆ s * t
hC : Disjoint ∅ (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab))
⊢ (∅ ∪ s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab = (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab
Tactic:
simp [hs₁]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
hxC : x ∈ C.mulStab
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
rw [(mem_mulStab hCne).mp hxC] at hx
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
hxC : x ∈ C.mulStab
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
hxC : x ∈ C.mulStab
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
Tactic:
rw [mem_mulStab_iff_subset_smul_finset (hs₁.mul ht₁)]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
hxC : x ∈ C.mulStab
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
hxC : x ∈ C.mulStab
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
Tactic:
exact hC.symm.left_le_of_le_sup_left (le_sup_right.trans hx.ge)
State after:
no goals

State before:
case inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : Disjoint (x • C) (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
⊢ x • C ⊆ C
Tactic:
exact h.left_le_of_le_sup_right (le_sup_left.trans_eq hx)
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ ((C.biUnion fun y => x • y • C.mulStab) ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
Tactic:
have : (x • C.biUnion fun y => y • C.mulStab) = C.biUnion fun y => x • y • C.mulStab :=
  biUnion_image
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
this : (x • C.biUnion fun y => y • C.mulStab) = C.biUnion fun y => x • y • C.mulStab
⊢ ((C.biUnion fun y => x • y • C.mulStab) ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
this : (x • C.biUnion fun y => y • C.mulStab) = C.biUnion fun y => x • y • C.mulStab
⊢ ((C.biUnion fun y => x • y • C.mulStab) ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
Tactic:
simpa [← this]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ (x * y) • C.mulStab ⊆ x • C
Tactic:
rw [← smul_eq_mul, smul_assoc, smul_finset_subset_smul_finset_iff]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ y • C.mulStab ⊆ C

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
⊢ y • C.mulStab ⊆ C
Tactic:
exact smul_finset_mulStab_subset hy
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
⊢ Disjoint ((x * y) • C.mulStab) C
Tactic:
convert disjoint_smul_finset_mulStab_mul_mulStab fun hxyC => _
State after:
case h.e'_5
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
⊢ C = ?convert_5 * C.mulStab

case convert_5
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
⊢ Finset α

case convert_7
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : (x * y) • C.mulStab ⊆ ?convert_5 * C.mulStab
⊢ False

State before:
case convert_7
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : (x * y) • C.mulStab ⊆ C * C.mulStab
⊢ False
Tactic:
rw [mul_mulStab] at hxyC
State after:
case convert_7
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : (x * y) • C.mulStab ⊆ C
⊢ False

State before:
case convert_7
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : (x * y) • C.mulStab ⊆ C
⊢ False
Tactic:
exact hyne.not_disjoint (hC.mono_left $ le_iff_subset.2 hxyC)
State after:
no goals

State before:
case h.e'_5
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
⊢ C = ?convert_5 * C.mulStab
Tactic:
exact C.mul_mulStab.symm
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
⊢ x • C ⊆ C
Tactic:
have := (card_le_card hxysub).not_lt ((card_lt_card this).trans_eq ?_)
State after:
case refine_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this✝ : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
this : False
⊢ x • C ⊆ C

case refine_1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
⊢ ((a * b) • C.mulStab).card = ((x * y) • C.mulStab).card

State before:
case refine_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this✝ : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
this : False
⊢ x • C ⊆ C

case refine_1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
⊢ ((a * b) • C.mulStab).card = ((x * y) • C.mulStab).card
Tactic:
cases this
State after:
case refine_1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
⊢ ((a * b) • C.mulStab).card = ((x * y) • C.mulStab).card

State before:
case refine_1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab
⊢ ((a * b) • C.mulStab).card = ((x * y) • C.mulStab).card
Tactic:
simp_rw [card_smul_finset]
State after:
no goals

State before:
case inr.inr.intro.intro.h₁
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * b) • C.mulStab
Tactic:
refine' (mul_subset_mul inter_subset_right inter_subset_right).trans _
State after:
case inr.inr.intro.intro.h₁
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ a • C.mulStab * b • C.mulStab ⊆ (a * b) • C.mulStab

State before:
case inr.inr.intro.intro.h₁
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ a • C.mulStab * b • C.mulStab ⊆ (a * b) • C.mulStab
Tactic:
simp only [smul_mul_smul, mulStab_mul_mulStab, subset_refl]
State after:
no goals

State before:
case inr.inr.intro.intro.h₂
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ ¬(a * b) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
Tactic:
contrapose! hab
State after:
case inr.inr.intro.intro.h₂
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
hab : (a * b) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ (a * b) • C.mulStab ⊆ s * t

State before:
case inr.inr.intro.intro.h₂
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x • C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
h : (x • C ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
y : α
hy : y ∈ C
hyne : ((x * y) • C.mulStab ∩ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))).Nonempty
hxyCsubC : (x * y) • C.mulStab ⊆ x • C
hxyC : Disjoint ((x * y) • C.mulStab) C
hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
hab : (a * b) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ (a * b) • C.mulStab ⊆ s * t
Tactic:
exact hab.trans (mul_subset_mul inter_subset_left inter_subset_left)
State after:
no goals