ι : Type ?u.374432
α : Type ?u.374435
X : Type ?u.374438
M : Type u_1
N : Type ?u.374444
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto ((fun b_1 => b_1 * b) ∘ fun x => x * a) (cocompact M) (cocompact M)
ι : Type ?u.374432
α : Type ?u.374435
X : Type ?u.374438
M : Type u_1
N : Type ?u.374444
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto (fun x => x * a) (cocompact M) (cocompact M)
refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_mul_right b))
ι : Type ?u.374432
α : Type ?u.374435
X : Type ?u.374438
M : Type u_1
N : Type ?u.374444
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto (fun x => x) (cocompact M) (cocompact M)
ι : Type ?u.374432
α : Type ?u.374435
X : Type ?u.374438
M : Type u_1
N : Type ?u.374444
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto ((fun b_1 => b_1 * b) ∘ fun x => x * a) (cocompact M) (cocompact M)
simp only [comp_mul_right, ha, mul_one]
no goals
ι : Type ?u.374432
α : Type ?u.374435
X : Type ?u.374438
M : Type u_1
N : Type ?u.374444
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto (fun x => x) (cocompact M) (cocompact M)
exact Filter.tendsto_id