ι : Type ?u.371356
α : Type ?u.371359
X : Type ?u.371362
M : Type u_1
N : Type ?u.371368
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto ((fun b_1 => b * b_1) ∘ fun x => a * x) (cocompact M) (cocompact M)
ι : Type ?u.371356
α : Type ?u.371359
X : Type ?u.371362
M : Type u_1
N : Type ?u.371368
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto (fun x => a * x) (cocompact M) (cocompact M)
refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_mul_left b))
ι : Type ?u.371356
α : Type ?u.371359
X : Type ?u.371362
M : Type u_1
N : Type ?u.371368
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto (fun x => x) (cocompact M) (cocompact M)
ι : Type ?u.371356
α : Type ?u.371359
X : Type ?u.371362
M : Type u_1
N : Type ?u.371368
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto ((fun b_1 => b * b_1) ∘ fun x => a * x) (cocompact M) (cocompact M)
simp only [comp_mul_left, ha, one_mul]
no goals
ι : Type ?u.371356
α : Type ?u.371359
X : Type ?u.371362
M : Type u_1
N : Type ?u.371368
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto (fun x => x) (cocompact M) (cocompact M)
exact Filter.tendsto_id