F : Type ?u.52486
α : Type u_1
β : Type ?u.52492
γ : Type ?u.52495
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hst : s ⊆ t
⊢ 1 ⊆ t ^ 0
F : Type ?u.52486
α : Type u_1
β : Type ?u.52492
γ : Type ?u.52495
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hst : s ⊆ t
⊢ s ^ 0 ⊆ t ^ 0
rw [pow_zero]
no goals
F : Type ?u.52486
α : Type u_1
β : Type ?u.52492
γ : Type ?u.52495
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hst : s ⊆ t
⊢ 1 ⊆ t ^ 0
exact Subset.rfl
F : Type ?u.52486
α : Type u_1
β : Type ?u.52492
γ : Type ?u.52495
inst✝ : Monoid α
s t : Set α
a : α
m n✝ : ℕ
hst : s ⊆ t
n : ℕ
⊢ s * s ^ n ⊆ t ^ (n + 1)
F : Type ?u.52486
α : Type u_1
β : Type ?u.52492
γ : Type ?u.52495
inst✝ : Monoid α
s t : Set α
a : α
m n✝ : ℕ
hst : s ⊆ t
n : ℕ
⊢ s ^ (n + 1) ⊆ t ^ (n + 1)
rw [pow_succ]
no goals
F : Type ?u.52486
α : Type u_1
β : Type ?u.52492
γ : Type ?u.52495
inst✝ : Monoid α
s t : Set α
a : α
m n✝ : ℕ
hst : s ⊆ t
n : ℕ
⊢ s * s ^ n ⊆ t ^ (n + 1)
exact mul_subset_mul hst (pow_subset_pow hst _)