case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x✝ y x : FreeGroup α
L : List (α × Bool)
⊢ ↑(map _root_.id) (Quot.mk Red.Step L) = Quot.mk Red.Step L
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x✝ y x : FreeGroup α
⊢ ↑(map _root_.id) x = x
rcases x with ⟨L⟩
no goals
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x✝ y x : FreeGroup α
L : List (α × Bool)
⊢ ↑(map _root_.id) (Quot.mk Red.Step L) = Quot.mk Red.Step L
simp [List.map_id']