case base
F : Type ?u.352257
α : Type u_1
β : Type ?u.352263
γ : Type ?u.352266
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
hs : 1 ∈ s
⊢ s ^ m ⊆ s ^ m

case succ
F : Type ?u.352257
α : Type u_1
β : Type ?u.352263
γ : Type ?u.352266
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
hs : 1 ∈ s
⊢ ∀ (n : ℕ), m ≤ n → s ^ m ⊆ s ^ n → s ^ m ⊆ s ^ (n + 1)
F : Type ?u.352257
α : Type u_1
β : Type ?u.352263
γ : Type ?u.352266
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
hs : 1 ∈ s
⊢ m ≤ n → s ^ m ⊆ s ^ n
apply Nat.le_induction
no goals
case base
F : Type ?u.352257
α : Type u_1
β : Type ?u.352263
γ : Type ?u.352266
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
hs : 1 ∈ s
⊢ s ^ m ⊆ s ^ m
exact fun _ hn => hn
case succ
F : Type ?u.352257
α : Type u_1
β : Type ?u.352263
γ : Type ?u.352266
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
hs : 1 ∈ s
n : ℕ
hn✝ : m ≤ n
hmn : s ^ m ⊆ s ^ n
⊢ s ^ m ⊆ s ^ (n + 1)
case succ
F : Type ?u.352257
α : Type u_1
β : Type ?u.352263
γ : Type ?u.352266
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
hs : 1 ∈ s
⊢ ∀ (n : ℕ), m ≤ n → s ^ m ⊆ s ^ n → s ^ m ⊆ s ^ (n + 1)
intro n _ hmn
case succ
F : Type ?u.352257
α : Type u_1
β : Type ?u.352263
γ : Type ?u.352266
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
hs : 1 ∈ s
n : ℕ
hn✝ : m ≤ n
hmn : s ^ m ⊆ s ^ n
⊢ s ^ m ⊆ s * s ^ n
case succ
F : Type ?u.352257
α : Type u_1
β : Type ?u.352263
γ : Type ?u.352266
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
hs : 1 ∈ s
n : ℕ
hn✝ : m ≤ n
hmn : s ^ m ⊆ s ^ n
⊢ s ^ m ⊆ s ^ (n + 1)
rw [pow_succ]
no goals
case succ
F : Type ?u.352257
α : Type u_1
β : Type ?u.352263
γ : Type ?u.352266
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
hs : 1 ∈ s
n : ℕ
hn✝ : m ≤ n
hmn : s ^ m ⊆ s ^ n
⊢ s ^ m ⊆ s * s ^ n
exact hmn.trans (subset_mul_right (s ^ n) hs)