no goals
β : Type u_1
A : Type ?u.79462
G : Type ?u.79465
M : Type u_2
R : Type ?u.79471
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
f : β → M
hf : Monotone f
⊢ Monotone fun a => f a ^ 0
simpa using monotone_const
β : Type u_1
A : Type ?u.79462
G : Type ?u.79465
M : Type u_2
R : Type ?u.79471
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone fun a => f a * f a ^ n
β : Type u_1
A : Type ?u.79462
G : Type ?u.79465
M : Type u_2
R : Type ?u.79471
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone fun a => f a ^ (n + 1)
simp_rw [pow_succ]
no goals
β : Type u_1
A : Type ?u.79462
G : Type ?u.79465
M : Type u_2
R : Type ?u.79471
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone fun a => f a * f a ^ n
exact hf.mul' (Monotone.pow_right hf _)