M : Type u_1
A : Type ?u.78612
B : Type ?u.78615
inst✝ : Monoid M
s : Set M
⊢ Set.range ↑(↑FreeMonoid.lift Subtype.val) = Set.range (List.prod ∘ List.map Subtype.val)
M : Type u_1
A : Type ?u.78612
B : Type ?u.78615
inst✝ : Monoid M
s : Set M
⊢ ↑(closure s) = List.prod '' {l | ∀ (x : M), x ∈ l → x ∈ s}
rw [closure_eq_mrange, coe_mrange, ← Set.range_list_map_coe, ← Set.range_comp]
no goals
M : Type u_1
A : Type ?u.78612
B : Type ?u.78615
inst✝ : Monoid M
s : Set M
⊢ Set.range ↑(↑FreeMonoid.lift Subtype.val) = Set.range (List.prod ∘ List.map Subtype.val)
exact congrArg _ (funext <| FreeMonoid.lift_apply _)