α : Type u_1
b : α
l : List α
H₂ : ∀ (x : α), x ∈ l → x = b
H : ∀ (b_1 : α), b_1 ∈ b :: l → b_1 = b
⊢ b :: l = replicate (length (b :: l)) b
α : Type u_1
a b : α
l : List α
H : ∀ (b_1 : α), b_1 ∈ b :: l → b_1 = a
⊢ b :: l = replicate (length (b :: l)) a
let ⟨rfl, H₂⟩ := forall_mem_cons.1 H
no goals
α : Type u_1
b : α
l : List α
H₂ : ∀ (x : α), x ∈ l → x = b
H : ∀ (b_1 : α), b_1 ∈ b :: l → b_1 = b
⊢ b :: l = replicate (length (b :: l)) b
rw [length_cons, replicate, ← eq_replicate_of_mem H₂]