ι : Type ?u.425891
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
a : α
l : List α
this : Eq a = Eq (f a) ∘ f
⊢ map f (List.erase l a) = List.erase (map f l) (f a)
ι : Type ?u.425891
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
a : α
l : List α
⊢ map f (List.erase l a) = List.erase (map f l) (f a)
have this : Eq a = Eq (f a) ∘ f := by ext b; simp [finj.eq_iff]
ι : Type ?u.425891
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
a : α
l : List α
this : Eq a = Eq (f a) ∘ f
⊢ map f (eraseP (fun b => decide (f a = f b)) l) = map f (eraseP ((fun b => decide (f a = b)) ∘ f) l)
ι : Type ?u.425891
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
a : α
l : List α
this : Eq a = Eq (f a) ∘ f
⊢ map f (List.erase l a) = List.erase (map f l) (f a)
simp [erase_eq_eraseP, erase_eq_eraseP, eraseP_map, this]
no goals
ι : Type ?u.425891
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
a : α
l : List α
this : Eq a = Eq (f a) ∘ f
⊢ map f (eraseP (fun b => decide (f a = f b)) l) = map f (eraseP ((fun b => decide (f a = b)) ∘ f) l)
rfl
case h.a
ι : Type ?u.425891
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
a : α
l : List α
b : α
⊢ a = b ↔ (Eq (f a) ∘ f) b
ι : Type ?u.425891
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
a : α
l : List α
⊢ Eq a = Eq (f a) ∘ f
ext b
no goals
case h.a
ι : Type ?u.425891
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
a : α
l : List α
b : α
⊢ a = b ↔ (Eq (f a) ∘ f) b
simp [finj.eq_iff]