X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (X.a ≫ f.f) xs = str Y (Ultrafilter.map f.f xs)
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ Monad.Algebra.Hom.f f (str X xs) = str Y (Ultrafilter.map f.f xs)
change (X.a ≫ f.f) _ = _
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (β.toFunctor.map f.f ≫ Y.a) xs = str Y (Ultrafilter.map f.f xs)
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (X.a ≫ f.f) xs = str Y (Ultrafilter.map f.f xs)
rw [← f.h]
no goals
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (β.toFunctor.map f.f ≫ Y.a) xs = str Y (Ultrafilter.map f.f xs)
rfl