exact C.mul_mulStab.symm
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
no goals