α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ ↑(MonoidHom.comp prod (map f)) x = ↑prod (↑(map f) x)

case hg
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ ∀ (x : α), ↑(MonoidHom.comp prod (map f)) (of x) = f x
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ ↑(↑lift f) x = ↑prod (↑(map f) x)
rw [← lift.unique (prod.comp (map f))]
no goals
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ ↑(MonoidHom.comp prod (map f)) x = ↑prod (↑(map f) x)
rfl
no goals
case hg
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ ∀ (x : α), ↑(MonoidHom.comp prod (map f)) (of x) = f x
simp