no goals
F : Type ?u.302112
α : Type u_1
β : Type ?u.302118
γ : Type ?u.302121
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
hst : s ⊆ t
⊢ s ^ 0 ⊆ t ^ 0
simp [pow_zero]
F : Type ?u.302112
α : Type u_1
β : Type ?u.302118
γ : Type ?u.302121
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
hst : s ⊆ t
n : ℕ
⊢ s * s ^ n ⊆ t ^ (n + 1)
F : Type ?u.302112
α : Type u_1
β : Type ?u.302118
γ : Type ?u.302121
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
hst : s ⊆ t
n : ℕ
⊢ s ^ (n + 1) ⊆ t ^ (n + 1)
rw [pow_succ]
no goals
F : Type ?u.302112
α : Type u_1
β : Type ?u.302118
γ : Type ?u.302121
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
hst : s ⊆ t
n : ℕ
⊢ s * s ^ n ⊆ t ^ (n + 1)
exact mul_subset_mul hst (pow_subset_pow hst n)