ι : Type ?u.144145
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
b₁ b₂ : β
l : List α
h : b₁ ∈ replicate (length l) b₂
⊢ b₁ = b₂
ι : Type ?u.144145
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) l
⊢ b₁ = b₂
rw [map_const] at h
no goals
ι : Type ?u.144145
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
b₁ b₂ : β
l : List α
h : b₁ ∈ replicate (length l) b₂
⊢ b₁ = b₂
exact eq_of_mem_replicate h