case base
F : Type ?u.59752
α : Type u_1
β : Type ?u.59758
γ : Type ?u.59761
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hs : 1 ∈ s
⊢ s ^ m ⊆ s ^ m

case succ
F : Type ?u.59752
α : Type u_1
β : Type ?u.59758
γ : Type ?u.59761
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hs : 1 ∈ s
n✝ : ℕ
hn✝ : m ≤ n✝
ih : s ^ m ⊆ s ^ n✝
⊢ s ^ m ⊆ s ^ (n✝ + 1)
F : Type ?u.59752
α : Type u_1
β : Type ?u.59758
γ : Type ?u.59761
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hs : 1 ∈ s
hn : m ≤ n
⊢ s ^ m ⊆ s ^ n
induction' n, hn using Nat.le_induction with _ _ ih
no goals
case base
F : Type ?u.59752
α : Type u_1
β : Type ?u.59758
γ : Type ?u.59761
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hs : 1 ∈ s
⊢ s ^ m ⊆ s ^ m
exact Subset.rfl
case succ
F : Type ?u.59752
α : Type u_1
β : Type ?u.59758
γ : Type ?u.59761
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hs : 1 ∈ s
n✝ : ℕ
hn✝ : m ≤ n✝
ih : s ^ m ⊆ s ^ n✝
⊢ s ^ m ⊆ s ^ (n✝ + 1)
case succ
F : Type ?u.59752
α : Type u_1
β : Type ?u.59758
γ : Type ?u.59761
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hs : 1 ∈ s
n✝ : ℕ
hn✝ : m ≤ n✝
ih : s ^ m ⊆ s ^ n✝
⊢ s ^ m ⊆ s ^ (n✝ + 1)
dsimp only
case succ
F : Type ?u.59752
α : Type u_1
β : Type ?u.59758
γ : Type ?u.59761
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hs : 1 ∈ s
n✝ : ℕ
hn✝ : m ≤ n✝
ih : s ^ m ⊆ s ^ n✝
⊢ s ^ m ⊆ s * s ^ n✝
case succ
F : Type ?u.59752
α : Type u_1
β : Type ?u.59758
γ : Type ?u.59761
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hs : 1 ∈ s
n✝ : ℕ
hn✝ : m ≤ n✝
ih : s ^ m ⊆ s ^ n✝
⊢ s ^ m ⊆ s ^ (n✝ + 1)
rw [pow_succ]
no goals
case succ
F : Type ?u.59752
α : Type u_1
β : Type ?u.59758
γ : Type ?u.59761
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hs : 1 ∈ s
n✝ : ℕ
hn✝ : m ≤ n✝
ih : s ^ m ⊆ s ^ n✝
⊢ s ^ m ⊆ s * s ^ n✝
exact ih.trans (subset_mul_right _ hs)