α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
⊢ Subgroup.closure (Set.range f) ≤ MonoidHom.range (↑lift f)
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
⊢ MonoidHom.range (↑lift f) = Subgroup.closure (Set.range f)
apply le_antisymm (lift.range_le Subgroup.subset_closure)
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
⊢ Set.range f ⊆ ↑(MonoidHom.range (↑lift f))
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
⊢ Subgroup.closure (Set.range f) ≤ MonoidHom.range (↑lift f)
rw [Subgroup.closure_le]
case intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
a : α
⊢ f a ∈ ↑(MonoidHom.range (↑lift f))
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
⊢ Set.range f ⊆ ↑(MonoidHom.range (↑lift f))
rintro _ ⟨a, rfl⟩
no goals
case intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
a : α
⊢ f a ∈ ↑(MonoidHom.range (↑lift f))
exact ⟨FreeGroup.of a, by simp only [lift.of]⟩
no goals
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
a : α
⊢ ↑(↑lift f) (FreeGroup.of a) = f a
simp only [lift.of]