X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ ((Monad.μ β).app X.A ≫ X.a) uux = str X (Ultrafilter.map (str X) uux)
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ str X (join X uux) = str X (Ultrafilter.map (str X) uux)
change ((β ).μ.app _ ≫ X.a) _ = _
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ (β.toFunctor.map X.a ≫ X.a) uux = str X (Ultrafilter.map (str X) uux)
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ ((Monad.μ β).app X.A ≫ X.a) uux = str X (Ultrafilter.map (str X) uux)
rw [Monad.Algebra.assoc]
no goals
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ (β.toFunctor.map X.a ≫ X.a) uux = str X (Ultrafilter.map (str X) uux)
rfl