no goals
ι : Type ?u.120563
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a✝ a b : α
as : List α
x✝ : 0 ≤ length as
⊢ a ∈ insertNth 0 b as ↔ a = b ∨ a ∈ as
simp
no goals
ι : Type ?u.120563
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a✝ a b : α
n : ℕ
a' : α
as : List α
h : n + 1 ≤ length (a' :: as)
⊢ a ∈ insertNth (n + 1) b (a' :: as) ↔ a = b ∨ a ∈ a' :: as
rw [List.insertNth_succ_cons, mem_cons, mem_insertNth (Nat.le_of_succ_le_succ h),
  ← or_assoc, @or_comm (a = a'), or_assoc, mem_cons]