case zero
α : Type u_2
β : Type ?u.21041
A : Type ?u.21044
B : Type ?u.21047
M : Type u_1
N : Type ?u.21053
P : Type ?u.21056
R : Type ?u.21059
S : Type ?u.21062
G : Type ?u.21065
M₀ : Type ?u.21068
G₀ : Type ?u.21071
ι : Sort ?u.21074
inst✝ : Monoid M
f : α → M
⊢ (mulSupport fun x => f x ^ Nat.zero) ⊆ mulSupport f

case succ
α : Type u_2
β : Type ?u.21041
A : Type ?u.21044
B : Type ?u.21047
M : Type u_1
N : Type ?u.21053
P : Type ?u.21056
R : Type ?u.21059
S : Type ?u.21062
G : Type ?u.21065
M₀ : Type ?u.21068
G₀ : Type ?u.21071
ι : Sort ?u.21074
inst✝ : Monoid M
f : α → M
n : ℕ
hfn : (mulSupport fun x => f x ^ n) ⊆ mulSupport f
⊢ (mulSupport fun x => f x ^ Nat.succ n) ⊆ mulSupport f
α : Type u_2
β : Type ?u.21041
A : Type ?u.21044
B : Type ?u.21047
M : Type u_1
N : Type ?u.21053
P : Type ?u.21056
R : Type ?u.21059
S : Type ?u.21062
G : Type ?u.21065
M₀ : Type ?u.21068
G₀ : Type ?u.21071
ι : Sort ?u.21074
inst✝ : Monoid M
f : α → M
n : ℕ
⊢ (mulSupport fun x => f x ^ n) ⊆ mulSupport f
induction' n with n hfn
no goals
case zero
α : Type u_2
β : Type ?u.21041
A : Type ?u.21044
B : Type ?u.21047
M : Type u_1
N : Type ?u.21053
P : Type ?u.21056
R : Type ?u.21059
S : Type ?u.21062
G : Type ?u.21065
M₀ : Type ?u.21068
G₀ : Type ?u.21071
ι : Sort ?u.21074
inst✝ : Monoid M
f : α → M
⊢ (mulSupport fun x => f x ^ Nat.zero) ⊆ mulSupport f
simp [pow_zero, mulSupport_one]
no goals
case succ
α : Type u_2
β : Type ?u.21041
A : Type ?u.21044
B : Type ?u.21047
M : Type u_1
N : Type ?u.21053
P : Type ?u.21056
R : Type ?u.21059
S : Type ?u.21062
G : Type ?u.21065
M₀ : Type ?u.21068
G₀ : Type ?u.21071
ι : Sort ?u.21074
inst✝ : Monoid M
f : α → M
n : ℕ
hfn : (mulSupport fun x => f x ^ n) ⊆ mulSupport f
⊢ (mulSupport fun x => f x ^ Nat.succ n) ⊆ mulSupport f
simpa only [pow_succ] using (mulSupport_mul f _).trans (union_subset Subset.rfl hfn)