[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
⊢ length ((a :: as) {0 ↦ a✝}) = max (length (a :: as)) (0 + 1)
[PROOFSTEP]
rw [max_eq_left]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
⊢ length ((a :: as) {0 ↦ a✝}) = length (a :: as)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
⊢ 0 + 1 ≤ length (a :: as)
[PROOFSTEP]
simp [Nat.le_add_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
⊢ 1 ≤ Nat.succ (length as)
[PROOFSTEP]
exact Nat.succ_le_succ (Nat.zero_le _)
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
m : ℕ
⊢ length ([] {m + 1 ↦ a}) = max (length []) (m + 1 + 1)
[PROOFSTEP]
have := @length_set m []
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
m : ℕ
this : length ([] {m ↦ a}) = max (length []) (m + 1)
⊢ length ([] {m + 1 ↦ a}) = max (length []) (m + 1 + 1)
[PROOFSTEP]
simp [set, length, @length_set m, Nat.zero_max]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
m : ℕ
head✝ : α
as : List α
⊢ length ((head✝ :: as) {m + 1 ↦ a}) = max (length (head✝ :: as)) (m + 1 + 1)
[PROOFSTEP]
simp [set, length, @length_set m, Nat.max_succ_succ]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
k : ℕ
⊢ get k [] = default
[PROOFSTEP]
cases k
[GOAL]
case zero
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
⊢ get Nat.zero [] = default
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n✝ : ℕ
⊢ get (Nat.succ n✝) [] = default
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
h1 : length (a :: as) ≤ 0
⊢ get 0 (a :: as) = default
[PROOFSTEP]
cases h1
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
k : ℕ
head✝ : α
as : List α
h1 : length (head✝ :: as) ≤ k + 1
⊢ get (k + 1) (head✝ :: as) = default
[PROOFSTEP]
apply get_eq_default_of_le k
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
k : ℕ
head✝ : α
as : List α
h1 : length (head✝ :: as) ≤ k + 1
⊢ length as ≤ k
[PROOFSTEP]
rw [← Nat.succ_le_succ_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
k : ℕ
head✝ : α
as : List α
h1 : length (head✝ :: as) ≤ k + 1
⊢ Nat.succ (length as) ≤ Nat.succ k
[PROOFSTEP]
apply h1
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
⊢ get 0 (as {0 ↦ a}) = a
[PROOFSTEP]
cases as
[GOAL]
case nil
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
⊢ get 0 ([] {0 ↦ a}) = a
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a head✝ : α
tail✝ : List α
⊢ get 0 ((head✝ :: tail✝) {0 ↦ a}) = a
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
as : List α
⊢ get (k + 1) (as {k + 1 ↦ a}) = a
[PROOFSTEP]
cases as
[GOAL]
case nil
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
⊢ get (k + 1) ([] {k + 1 ↦ a}) = a
[PROOFSTEP]
simp [get_set]
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
head✝ : α
tail✝ : List α
⊢ get (k + 1) ((head✝ :: tail✝) {k + 1 ↦ a}) = a
[PROOFSTEP]
simp [get_set]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
h : a ∈ []
⊢ ∃ n, a = get n []
[PROOFSTEP]
cases h
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a b : α
as : List α
h : a ∈ b :: as
⊢ ∃ n, a = get n (b :: as)
[PROOFSTEP]
rw [mem_cons] at h
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a b : α
as : List α
h : a = b ∨ a ∈ as
⊢ ∃ n, a = get n (b :: as)
[PROOFSTEP]
cases h with
| inl h => exact ⟨0, h⟩
| inr h =>
  rcases eq_get_of_mem h with ⟨n, h⟩
  exact ⟨n + 1, h⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a b : α
as : List α
h : a = b ∨ a ∈ as
⊢ ∃ n, a = get n (b :: as)
[PROOFSTEP]
cases h with
| inl h => exact ⟨0, h⟩
| inr h =>
  rcases eq_get_of_mem h with ⟨n, h⟩
  exact ⟨n + 1, h⟩
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a b : α
as : List α
h : a = b
⊢ ∃ n, a = get n (b :: as)
[PROOFSTEP]

| inl h => exact ⟨0, h⟩
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a b : α
as : List α
h : a = b
⊢ ∃ n, a = get n (b :: as)
[PROOFSTEP]
exact ⟨0, h⟩
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a b : α
as : List α
h : a ∈ as
⊢ ∃ n, a = get n (b :: as)
[PROOFSTEP]

| inr h =>
  rcases eq_get_of_mem h with ⟨n, h⟩
  exact ⟨n + 1, h⟩
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a b : α
as : List α
h : a ∈ as
⊢ ∃ n, a = get n (b :: as)
[PROOFSTEP]
rcases eq_get_of_mem h with ⟨n, h⟩
[GOAL]
case inr.intro
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a b : α
as : List α
h✝ : a ∈ as
n : ℕ
h : a = get n as
⊢ ∃ n, a = get n (b :: as)
[PROOFSTEP]
exact ⟨n + 1, h⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x✝ : ℕ
h1 : x✝ < length []
⊢ get x✝ [] ∈ []
[PROOFSTEP]
cases h1
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
x✝ : 0 < length (a :: as)
⊢ get 0 (a :: as) ∈ a :: as
[PROOFSTEP]
rw [mem_cons]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
x✝ : 0 < length (a :: as)
⊢ get 0 (a :: as) = a ∨ get 0 (a :: as) ∈ as
[PROOFSTEP]
exact Or.inl rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : n + 1 < length (a :: as)
⊢ get (n + 1) (a :: as) ∈ a :: as
[PROOFSTEP]
rw [mem_cons]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : n + 1 < length (a :: as)
⊢ get (n + 1) (a :: as) = a ∨ get (n + 1) (a :: as) ∈ as
[PROOFSTEP]
apply Or.inr
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : n + 1 < length (a :: as)
⊢ get (n + 1) (a :: as) ∈ as
[PROOFSTEP]
unfold get
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : n + 1 < length (a :: as)
⊢ get (Nat.add n 0) as ∈ as
[PROOFSTEP]
apply mem_get_of_le
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : n + 1 < length (a :: as)
⊢ Nat.add n 0 < length as
[PROOFSTEP]
apply Nat.lt_of_succ_lt_succ h1
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x✝ : ℕ
h1 : get x✝ [] ≠ default
⊢ get x✝ [] ∈ []
[PROOFSTEP]
exfalso
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x✝ : ℕ
h1 : get x✝ [] ≠ default
⊢ False
[PROOFSTEP]
apply h1
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x✝ : ℕ
h1 : get x✝ [] ≠ default
⊢ get x✝ [] = default
[PROOFSTEP]
rw [get_nil]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
x✝ : get 0 (a :: as) ≠ default
⊢ get 0 (a :: as) ∈ a :: as
[PROOFSTEP]
rw [mem_cons]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
x✝ : get 0 (a :: as) ≠ default
⊢ get 0 (a :: as) = a ∨ get 0 (a :: as) ∈ as
[PROOFSTEP]
exact Or.inl rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : get (n + 1) (a :: as) ≠ default
⊢ get (n + 1) (a :: as) ∈ a :: as
[PROOFSTEP]
rw [mem_cons]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : get (n + 1) (a :: as) ≠ default
⊢ get (n + 1) (a :: as) = a ∨ get (n + 1) (a :: as) ∈ as
[PROOFSTEP]
unfold get
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : get (n + 1) (a :: as) ≠ default
⊢ get (Nat.add n 0) as = a ∨ get (Nat.add n 0) as ∈ as
[PROOFSTEP]
apply Or.inr (mem_get_of_ne_zero _)
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : get (n + 1) (a :: as) ≠ default
⊢ get (Nat.add n 0) as ≠ default
[PROOFSTEP]
apply h1
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
m : ℕ
h1 : m ≠ 0
⊢ get m (as {0 ↦ a}) = get m as
[PROOFSTEP]
cases m
[GOAL]
case zero
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
h1 : Nat.zero ≠ 0
⊢ get Nat.zero (as {0 ↦ a}) = get Nat.zero as
case succ
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
n✝ : ℕ
h1 : Nat.succ n✝ ≠ 0
⊢ get (Nat.succ n✝) (as {0 ↦ a}) = get (Nat.succ n✝) as
[PROOFSTEP]
contradiction
[GOAL]
case succ
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
n✝ : ℕ
h1 : Nat.succ n✝ ≠ 0
⊢ get (Nat.succ n✝) (as {0 ↦ a}) = get (Nat.succ n✝) as
[PROOFSTEP]
cases as
[GOAL]
case succ.nil
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
n✝ : ℕ
h1 : Nat.succ n✝ ≠ 0
⊢ get (Nat.succ n✝) ([] {0 ↦ a}) = get (Nat.succ n✝) []
[PROOFSTEP]
simp only [set, get, get_nil]
[GOAL]
case succ.cons
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
n✝ : ℕ
h1 : Nat.succ n✝ ≠ 0
head✝ : α
tail✝ : List α
⊢ get (Nat.succ n✝) ((head✝ :: tail✝) {0 ↦ a}) = get (Nat.succ n✝) (head✝ :: tail✝)
[PROOFSTEP]
simp only [set, get, get_nil]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
k m : ℕ
h1 : m ≠ k + 1
⊢ get m (as {k + 1 ↦ a}) = get m as
[PROOFSTEP]
cases as
[GOAL]
case nil
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k m : ℕ
h1 : m ≠ k + 1
⊢ get m ([] {k + 1 ↦ a}) = get m []
[PROOFSTEP]
cases m
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k m : ℕ
h1 : m ≠ k + 1
head✝ : α
tail✝ : List α
⊢ get m ((head✝ :: tail✝) {k + 1 ↦ a}) = get m (head✝ :: tail✝)
[PROOFSTEP]
cases m
[GOAL]
case nil.zero
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
h1 : Nat.zero ≠ k + 1
⊢ get Nat.zero ([] {k + 1 ↦ a}) = get Nat.zero []
case nil.succ
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k n✝ : ℕ
h1 : Nat.succ n✝ ≠ k + 1
⊢ get (Nat.succ n✝) ([] {k + 1 ↦ a}) = get (Nat.succ n✝) []
case cons.zero
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
head✝ : α
tail✝ : List α
h1 : Nat.zero ≠ k + 1
⊢ get Nat.zero ((head✝ :: tail✝) {k + 1 ↦ a}) = get Nat.zero (head✝ :: tail✝)
case cons.succ
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
head✝ : α
tail✝ : List α
n✝ : ℕ
h1 : Nat.succ n✝ ≠ k + 1
⊢ get (Nat.succ n✝) ((head✝ :: tail✝) {k + 1 ↦ a}) = get (Nat.succ n✝) (head✝ :: tail✝)
[PROOFSTEP]
case nil => simp only [set, get]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
h1 : Nat.zero ≠ k + 1
⊢ get Nat.zero ([] {k + 1 ↦ a}) = get Nat.zero []
[PROOFSTEP]
case nil => simp only [set, get]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
h1 : Nat.zero ≠ k + 1
⊢ get Nat.zero ([] {k + 1 ↦ a}) = get Nat.zero []
[PROOFSTEP]
simp only [set, get]
[GOAL]
case nil.succ
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k n✝ : ℕ
h1 : Nat.succ n✝ ≠ k + 1
⊢ get (Nat.succ n✝) ([] {k + 1 ↦ a}) = get (Nat.succ n✝) []
case cons.zero
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
head✝ : α
tail✝ : List α
h1 : Nat.zero ≠ k + 1
⊢ get Nat.zero ((head✝ :: tail✝) {k + 1 ↦ a}) = get Nat.zero (head✝ :: tail✝)
case cons.succ
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
head✝ : α
tail✝ : List α
n✝ : ℕ
h1 : Nat.succ n✝ ≠ k + 1
⊢ get (Nat.succ n✝) ((head✝ :: tail✝) {k + 1 ↦ a}) = get (Nat.succ n✝) (head✝ :: tail✝)
[PROOFSTEP]
case nil
  m =>
  have h3 : get m (nil {k ↦ a}) = default :=
    by
    rw [get_set_eq_of_ne k m, get_nil]
    intro hc
    apply h1
    simp [hc]
  apply h3
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k m : ℕ
h1 : Nat.succ m ≠ k + 1
⊢ get (Nat.succ m) ([] {k + 1 ↦ a}) = get (Nat.succ m) []
[PROOFSTEP]
case nil
  m =>
  have h3 : get m (nil {k ↦ a}) = default :=
    by
    rw [get_set_eq_of_ne k m, get_nil]
    intro hc
    apply h1
    simp [hc]
  apply h3
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k m : ℕ
h1 : Nat.succ m ≠ k + 1
⊢ get (Nat.succ m) ([] {k + 1 ↦ a}) = get (Nat.succ m) []
[PROOFSTEP]
have h3 : get m (nil {k ↦ a}) = default :=
  by
  rw [get_set_eq_of_ne k m, get_nil]
  intro hc
  apply h1
  simp [hc]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k m : ℕ
h1 : Nat.succ m ≠ k + 1
⊢ get m ([] {k ↦ a}) = default
[PROOFSTEP]
rw [get_set_eq_of_ne k m, get_nil]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k m : ℕ
h1 : Nat.succ m ≠ k + 1
⊢ m ≠ k
[PROOFSTEP]
intro hc
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k m : ℕ
h1 : Nat.succ m ≠ k + 1
hc : m = k
⊢ False
[PROOFSTEP]
apply h1
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k m : ℕ
h1 : Nat.succ m ≠ k + 1
hc : m = k
⊢ Nat.succ m = k + 1
[PROOFSTEP]
simp [hc]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k m : ℕ
h1 : Nat.succ m ≠ k + 1
h3 : get m ([] {k ↦ a}) = default
⊢ get (Nat.succ m) ([] {k + 1 ↦ a}) = get (Nat.succ m) []
[PROOFSTEP]
apply h3
[GOAL]
case cons.zero
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
head✝ : α
tail✝ : List α
h1 : Nat.zero ≠ k + 1
⊢ get Nat.zero ((head✝ :: tail✝) {k + 1 ↦ a}) = get Nat.zero (head✝ :: tail✝)
case cons.succ
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
head✝ : α
tail✝ : List α
n✝ : ℕ
h1 : Nat.succ n✝ ≠ k + 1
⊢ get (Nat.succ n✝) ((head✝ :: tail✝) {k + 1 ↦ a}) = get (Nat.succ n✝) (head✝ :: tail✝)
[PROOFSTEP]
case zero => simp only [set, get]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
head✝ : α
tail✝ : List α
h1 : Nat.zero ≠ k + 1
⊢ get Nat.zero ((head✝ :: tail✝) {k + 1 ↦ a}) = get Nat.zero (head✝ :: tail✝)
[PROOFSTEP]
case zero => simp only [set, get]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
head✝ : α
tail✝ : List α
h1 : Nat.zero ≠ k + 1
⊢ get Nat.zero ((head✝ :: tail✝) {k + 1 ↦ a}) = get Nat.zero (head✝ :: tail✝)
[PROOFSTEP]
simp only [set, get]
[GOAL]
case cons.succ
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
head✝ : α
tail✝ : List α
n✝ : ℕ
h1 : Nat.succ n✝ ≠ k + 1
⊢ get (Nat.succ n✝) ((head✝ :: tail✝) {k + 1 ↦ a}) = get (Nat.succ n✝) (head✝ :: tail✝)
[PROOFSTEP]
case _ _ m =>
  apply get_set_eq_of_ne k m
  intro hc
  apply h1
  simp [hc]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
head✝ : α
tail✝ : List α
m : ℕ
h1 : Nat.succ m ≠ k + 1
⊢ get (Nat.succ m) ((head✝ :: tail✝) {k + 1 ↦ a}) = get (Nat.succ m) (head✝ :: tail✝)
[PROOFSTEP]
case _ _ m =>
  apply get_set_eq_of_ne k m
  intro hc
  apply h1
  simp [hc]
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
head✝ : α
tail✝ : List α
m : ℕ
h1 : Nat.succ m ≠ k + 1
⊢ get (Nat.succ m) ((head✝ :: tail✝) {k + 1 ↦ a}) = get (Nat.succ m) (head✝ :: tail✝)
[PROOFSTEP]
apply get_set_eq_of_ne k m
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
head✝ : α
tail✝ : List α
m : ℕ
h1 : Nat.succ m ≠ k + 1
⊢ m ≠ k
[PROOFSTEP]
intro hc
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
head✝ : α
tail✝ : List α
m : ℕ
h1 : Nat.succ m ≠ k + 1
hc : m = k
⊢ False
[PROOFSTEP]
apply h1
[GOAL]
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
head✝ : α
tail✝ : List α
m : ℕ
h1 : Nat.succ m ≠ k + 1
hc : m = k
⊢ Nat.succ m = k + 1
[PROOFSTEP]
simp [hc]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
x✝ : ℕ
h : x✝ < length []
⊢ get x✝ (map f []) = f (get x✝ [])
[PROOFSTEP]
cases h
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
head✝ : α
as : List α
h1 : n + 1 < length (head✝ :: as)
⊢ get (n + 1) (map f (head✝ :: as)) = f (get (n + 1) (head✝ :: as))
[PROOFSTEP]
have h2 : n < length as := by
  rw [← Nat.succ_le_iff, ← Nat.lt_succ_iff]
  apply h1
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
head✝ : α
as : List α
h1 : n + 1 < length (head✝ :: as)
⊢ n < length as
[PROOFSTEP]
rw [← Nat.succ_le_iff, ← Nat.lt_succ_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
head✝ : α
as : List α
h1 : n + 1 < length (head✝ :: as)
⊢ Nat.succ n < Nat.succ (length as)
[PROOFSTEP]
apply h1
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
head✝ : α
as : List α
h1 : n + 1 < length (head✝ :: as)
h2 : n < length as
⊢ get (n + 1) (map f (head✝ :: as)) = f (get (n + 1) (head✝ :: as))
[PROOFSTEP]
apply get_map h2
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
as : List α
⊢ f default = default → get n (map f as) = f (get n as)
[PROOFSTEP]
intro h1
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
as : List α
h1 : f default = default
⊢ get n (map f as) = f (get n as)
[PROOFSTEP]
by_cases h2 : n < as.length
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
as : List α
h1 : f default = default
h2 : n < length as
⊢ get n (map f as) = f (get n as)
[PROOFSTEP]
apply get_map h2
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
as : List α
h1 : f default = default
h2 : ¬n < length as
⊢ get n (map f as) = f (get n as)
[PROOFSTEP]
rw [not_lt] at h2
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
as : List α
h1 : f default = default
h2 : length as ≤ n
⊢ get n (map f as) = f (get n as)
[PROOFSTEP]
rw [get_eq_default_of_le _ h2, get_eq_default_of_le, h1]
[GOAL]
case neg.a
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
as : List α
h1 : f default = default
h2 : length as ≤ n
⊢ length (map f as) ≤ n
[PROOFSTEP]
rw [length_map]
[GOAL]
case neg.a
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
as : List α
h1 : f default = default
h2 : length as ≤ n
⊢ length as ≤ n
[PROOFSTEP]
apply h2
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
as : List α
p : α → Prop
⊢ p default → (∀ (x : α), x ∈ as → p x) → ∀ (n : ℕ), p (get n as)
[PROOFSTEP]
intro h1 h2 n
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
as : List α
p : α → Prop
h1 : p default
h2 : ∀ (x : α), x ∈ as → p x
n : ℕ
⊢ p (get n as)
[PROOFSTEP]
by_cases h3 : n < as.length
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
as : List α
p : α → Prop
h1 : p default
h2 : ∀ (x : α), x ∈ as → p x
n : ℕ
h3 : n < length as
⊢ p (get n as)
[PROOFSTEP]
apply h2 _ (mem_get_of_le h3)
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
as : List α
p : α → Prop
h1 : p default
h2 : ∀ (x : α), x ∈ as → p x
n : ℕ
h3 : ¬n < length as
⊢ p (get n as)
[PROOFSTEP]
rw [not_lt] at h3
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
as : List α
p : α → Prop
h1 : p default
h2 : ∀ (x : α), x ∈ as → p x
n : ℕ
h3 : length as ≤ n
⊢ p (get n as)
[PROOFSTEP]
rw [get_eq_default_of_le _ h3]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
as : List α
p : α → Prop
h1 : p default
h2 : ∀ (x : α), x ∈ as → p x
n : ℕ
h3 : length as ≤ n
⊢ p default
[PROOFSTEP]
apply h1
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
⊢ as1 = as2 → Equiv as1 as2
[PROOFSTEP]
intro h1
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
h1 : as1 = as2
⊢ Equiv as1 as2
[PROOFSTEP]
rw [h1]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
h1 : as1 = as2
⊢ Equiv as2 as2
[PROOFSTEP]
apply equiv_refl
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
head✝ : α
tail✝ : List α
h1 : length (head✝ :: tail✝) = length []
x✝ : Equiv (head✝ :: tail✝) []
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
cases h1
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
head✝ : α
tail✝ : List α
h1 : length [] = length (head✝ :: tail✝)
x✝ : Equiv [] (head✝ :: tail✝)
⊢ [] = head✝ :: tail✝
[PROOFSTEP]
cases h1
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
⊢ a1 :: as1 = a2 :: as2
[PROOFSTEP]
congr
[GOAL]
case e_head
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
⊢ a1 = a2
[PROOFSTEP]
apply h2 0
[GOAL]
case e_tail
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
⊢ as1 = as2
[PROOFSTEP]
have h3 : as1.length = as2.length := by simpa [add_left_inj, add_comm, length] using h1
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
⊢ length as1 = length as2
[PROOFSTEP]
simpa [add_left_inj, add_comm, length] using h1
[GOAL]
case e_tail
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
h3 : length as1 = length as2
⊢ as1 = as2
[PROOFSTEP]
apply eq_of_equiv h3
[GOAL]
case e_tail
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
h3 : length as1 = length as2
⊢ Equiv as1 as2
[PROOFSTEP]
intro m
[GOAL]
case e_tail
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
h3 : length as1 = length as2
m : ℕ
⊢ get m as1 = get m as2
[PROOFSTEP]
apply h2 (m + 1)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : AddGroup α
k : ℕ
as : List α
⊢ get k (neg as) = -get k as
[PROOFSTEP]
unfold neg
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : AddGroup α
k : ℕ
as : List α
⊢ get k (map (fun a => -a) as) = -get k as
[PROOFSTEP]
rw [@get_map' α α ⟨0⟩ ⟨0⟩]
  -- porting note: had to add a `⟨0⟩` b/c of instance troubles
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
inst✝ : AddGroup α
k : ℕ
as : List α
⊢ -default = default
[PROOFSTEP]
apply neg_zero
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Neg α
as : List α
⊢ length (neg as) = length as
[PROOFSTEP]
simp only [neg, length_map]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β → γ
b : β
bs : List β
⊢ pointwise f [] (b :: bs) = map (f default) (b :: bs)
[PROOFSTEP]
simp only [nil_pointwise bs, pointwise, eq_self_iff_true, and_self_iff, map]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β → γ
a : α
as : List α
⊢ pointwise f (a :: as) [] = map (fun a => f a default) (a :: as)
[PROOFSTEP]
simp only [pointwise_nil as, pointwise, eq_self_iff_true, and_self_iff, List.map]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Inhabited α
inst✝¹ : Inhabited β
inst✝ : Inhabited γ
f : α → β → γ
h1 : f default default = default
k : ℕ
⊢ get k (pointwise f [] []) = f (get k []) (get k [])
[PROOFSTEP]
simp only [h1, get_nil, pointwise, get]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Inhabited α
inst✝¹ : Inhabited β
inst✝ : Inhabited γ
f : α → β → γ
h1 : f default default = default
b : β
tail✝ : List β
⊢ get 0 (pointwise f [] (b :: tail✝)) = f (get 0 []) (get 0 (b :: tail✝))
[PROOFSTEP]
simp only [get_pointwise, get_nil, pointwise, get, Nat.zero_eq, map]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Inhabited α
inst✝¹ : Inhabited β
inst✝ : Inhabited γ
f : α → β → γ
h1 : f default default = default
k : ℕ
b : β
bs : List β
⊢ get (k + 1) (pointwise f [] (b :: bs)) = f (get (k + 1) []) (get (k + 1) (b :: bs))
[PROOFSTEP]
have : get k (map (f default) bs) = f default (get k bs) := by
  simpa [nil_pointwise, get_nil] using get_pointwise h1 k [] bs
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Inhabited α
inst✝¹ : Inhabited β
inst✝ : Inhabited γ
f : α → β → γ
h1 : f default default = default
k : ℕ
b : β
bs : List β
⊢ get k (map (f default) bs) = f default (get k bs)
[PROOFSTEP]
simpa [nil_pointwise, get_nil] using get_pointwise h1 k [] bs
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Inhabited α
inst✝¹ : Inhabited β
inst✝ : Inhabited γ
f : α → β → γ
h1 : f default default = default
k : ℕ
b : β
bs : List β
this : get k (map (f default) bs) = f default (get k bs)
⊢ get (k + 1) (pointwise f [] (b :: bs)) = f (get (k + 1) []) (get (k + 1) (b :: bs))
[PROOFSTEP]
simpa [get, get_nil, pointwise, map]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Inhabited α
inst✝¹ : Inhabited β
inst✝ : Inhabited γ
f : α → β → γ
h1 : f default default = default
a : α
tail✝ : List α
⊢ get 0 (pointwise f (a :: tail✝) []) = f (get 0 (a :: tail✝)) (get 0 [])
[PROOFSTEP]
simp only [get_pointwise, get_nil, pointwise, get, Nat.zero_eq, map]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Inhabited α
inst✝¹ : Inhabited β
inst✝ : Inhabited γ
f : α → β → γ
h1 : f default default = default
k : ℕ
a : α
as : List α
⊢ get (k + 1) (pointwise f (a :: as) []) = f (get (k + 1) (a :: as)) (get (k + 1) [])
[PROOFSTEP]
simpa [get, get_nil, pointwise, map, pointwise_nil, get_nil] using get_pointwise h1 k as []
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Inhabited α
inst✝¹ : Inhabited β
inst✝ : Inhabited γ
f : α → β → γ
h1 : f default default = default
a : α
tail✝¹ : List α
b : β
tail✝ : List β
⊢ get 0 (pointwise f (a :: tail✝¹) (b :: tail✝)) = f (get 0 (a :: tail✝¹)) (get 0 (b :: tail✝))
[PROOFSTEP]
simp only [pointwise, get]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Inhabited α
inst✝¹ : Inhabited β
inst✝ : Inhabited γ
f : α → β → γ
h1 : f default default = default
k : ℕ
head✝¹ : α
as : List α
head✝ : β
bs : List β
⊢ get (k + 1) (pointwise f (head✝¹ :: as) (head✝ :: bs)) = f (get (k + 1) (head✝¹ :: as)) (get (k + 1) (head✝ :: bs))
[PROOFSTEP]
simp only [get, Nat.add_eq, add_zero, get_pointwise h1 k as bs]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β → γ
head✝ : β
bs : List β
⊢ length (pointwise f [] (head✝ :: bs)) = max (length []) (length (head✝ :: bs))
[PROOFSTEP]
simp only [pointwise, length, length_map, max_eq_right (Nat.zero_le (length bs + 1))]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β → γ
head✝ : α
as : List α
⊢ length (pointwise f (head✝ :: as) []) = max (length (head✝ :: as)) (length [])
[PROOFSTEP]
simp only [pointwise, length, length_map, max_eq_left (Nat.zero_le (length as + 1))]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β → γ
head✝¹ : α
as : List α
head✝ : β
bs : List β
⊢ length (pointwise f (head✝¹ :: as) (head✝ :: bs)) = max (length (head✝¹ :: as)) (length (head✝ :: bs))
[PROOFSTEP]
simp only [pointwise, length, Nat.max_succ_succ, @length_pointwise _ as bs]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
k : ℕ
xs ys : List α
⊢ get k (add xs ys) = get k xs + get k ys
[PROOFSTEP]
apply @get_pointwise _ _ _ ⟨0⟩ ⟨0⟩ ⟨0⟩
[GOAL]
case h1
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
k : ℕ
xs ys : List α
⊢ default + default = default
[PROOFSTEP]
apply zero_add
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
as : List α
⊢ add [] as = as
[PROOFSTEP]
rw [add, @nil_pointwise α α α ⟨0⟩ ⟨0⟩]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
as : List α
⊢ map (fun x => default + x) as = as
[PROOFSTEP]
apply Eq.trans _ (map_id as)
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
as : List α
⊢ map (fun x => default + x) as = map id as
[PROOFSTEP]
congr with x
[GOAL]
case e_f.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
as : List α
x : α
⊢ default + x = id x
[PROOFSTEP]
exact zero_add x
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
as : List α
⊢ add as [] = as
[PROOFSTEP]
rw [add, @pointwise_nil α α α ⟨0⟩ ⟨0⟩]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
as : List α
⊢ map (fun a => a + default) as = as
[PROOFSTEP]
apply Eq.trans _ (map_id as)
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
as : List α
⊢ map (fun a => a + default) as = map id as
[PROOFSTEP]
congr with x
[GOAL]
case e_f.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
as : List α
x : α
⊢ x + default = id x
[PROOFSTEP]
exact add_zero x
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
⊢ add (map f as) (map g as) = map (fun x => f x + g x) as
[PROOFSTEP]
apply @eq_of_equiv _ (⟨0⟩ : Inhabited α)
[GOAL]
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
⊢ length (add (map f as) (map g as)) = length (map (fun x => f x + g x) as)
[PROOFSTEP]
rw [length_map, length_add, max_eq_left, length_map]
[GOAL]
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
⊢ length (map g as) ≤ length (map f as)
[PROOFSTEP]
apply le_of_eq
[GOAL]
case a.a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
⊢ length (map g as) = length (map f as)
[PROOFSTEP]
rw [length_map, length_map]
[GOAL]
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
⊢ Equiv (add (map f as) (map g as)) (map (fun x => f x + g x) as)
[PROOFSTEP]
intro m
[GOAL]
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
⊢ get m (add (map f as) (map g as)) = get m (map (fun x => f x + g x) as)
[PROOFSTEP]
rw [get_add]
[GOAL]
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
⊢ get m (map f as) + get m (map g as) = get m (map (fun x => f x + g x) as)
[PROOFSTEP]
by_cases h : m < length as
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : m < length as
⊢ get m (map f as) + get m (map g as) = get m (map (fun x => f x + g x) as)
[PROOFSTEP]
repeat' rw [@get_map α α ⟨0⟩ ⟨0⟩ _ _ _ h]
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : m < length as
⊢ get m (map f as) + get m (map g as) = get m (map (fun x => f x + g x) as)
[PROOFSTEP]
rw [@get_map α α ⟨0⟩ ⟨0⟩ _ _ _ h]
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : m < length as
⊢ f (get m as) + get m (map g as) = get m (map (fun x => f x + g x) as)
[PROOFSTEP]
rw [@get_map α α ⟨0⟩ ⟨0⟩ _ _ _ h]
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : m < length as
⊢ f (get m as) + g (get m as) = get m (map (fun x => f x + g x) as)
[PROOFSTEP]
rw [@get_map α α ⟨0⟩ ⟨0⟩ _ _ _ h]
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : ¬m < length as
⊢ get m (map f as) + get m (map g as) = get m (map (fun x => f x + g x) as)
[PROOFSTEP]
rw [not_lt] at h
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ get m (map f as) + get m (map g as) = get m (map (fun x => f x + g x) as)
[PROOFSTEP]
repeat' rw [@get_eq_default_of_le _ ⟨0⟩ m] <;> try rw [length_map]; apply h
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ get m (map f as) + get m (map g as) = get m (map (fun x => f x + g x) as)
[PROOFSTEP]
rw [@get_eq_default_of_le _ ⟨0⟩ m]
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ default + get m (map g as) = get m (map (fun x => f x + g x) as)
[PROOFSTEP]
try rw [length_map]; apply h
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ default + get m (map g as) = get m (map (fun x => f x + g x) as)
[PROOFSTEP]
rw [length_map]
[GOAL]
case neg.a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ length (map f as) ≤ m
[PROOFSTEP]
try rw [length_map]; apply h
[GOAL]
case neg.a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ length (map f as) ≤ m
[PROOFSTEP]
rw [length_map]
[GOAL]
case neg.a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ length as ≤ m
[PROOFSTEP]
apply h
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ default + get m (map g as) = get m (map (fun x => f x + g x) as)
[PROOFSTEP]
rw [@get_eq_default_of_le _ ⟨0⟩ m]
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ default + default = get m (map (fun x => f x + g x) as)
[PROOFSTEP]
try rw [length_map]; apply h
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ default + default = get m (map (fun x => f x + g x) as)
[PROOFSTEP]
rw [length_map]
[GOAL]
case neg.a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ length (map g as) ≤ m
[PROOFSTEP]
try rw [length_map]; apply h
[GOAL]
case neg.a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ length (map g as) ≤ m
[PROOFSTEP]
rw [length_map]
[GOAL]
case neg.a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ length as ≤ m
[PROOFSTEP]
apply h
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ default + default = get m (map (fun x => f x + g x) as)
[PROOFSTEP]
rw [@get_eq_default_of_le _ ⟨0⟩ m]
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ default + default = default
[PROOFSTEP]
try rw [length_map]; apply h
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ default + default = default
[PROOFSTEP]
rw [length_map]
[GOAL]
case neg.a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ length (map (fun x => f x + g x) as) ≤ m
[PROOFSTEP]
try rw [length_map]; apply h
[GOAL]
case neg.a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ length (map (fun x => f x + g x) as) ≤ m
[PROOFSTEP]
rw [length_map]
[GOAL]
case neg.a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ length as ≤ m
[PROOFSTEP]
apply h
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ default + default = default
[PROOFSTEP]
rw [@get_eq_default_of_le _ ⟨0⟩ m]
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ default + default = default
[PROOFSTEP]
exact zero_add _
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddGroup α
k : ℕ
xs ys : List α
⊢ get k (sub xs ys) = get k xs - get k ys
[PROOFSTEP]
apply @get_pointwise _ _ _ ⟨0⟩ ⟨0⟩ ⟨0⟩
[GOAL]
case h1
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddGroup α
k : ℕ
xs ys : List α
⊢ Sub.sub default default = default
[PROOFSTEP]
apply sub_zero
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : AddGroup α
as : List α
⊢ sub [] as = neg as
[PROOFSTEP]
rw [sub, @nil_pointwise _ _ _ ⟨0⟩ ⟨0⟩]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : AddGroup α
as : List α
⊢ map (Sub.sub default) as = neg as
[PROOFSTEP]
congr with x
[GOAL]
case e_f.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : AddGroup α
as : List α
x : α
⊢ Sub.sub default x = -x
[PROOFSTEP]
exact zero_sub x
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : AddGroup α
as : List α
⊢ sub as [] = as
[PROOFSTEP]
rw [sub, @pointwise_nil _ _ _ ⟨0⟩ ⟨0⟩]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : AddGroup α
as : List α
⊢ map (fun a => Sub.sub a default) as = as
[PROOFSTEP]
apply Eq.trans _ (map_id as)
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : AddGroup α
as : List α
⊢ map (fun a => Sub.sub a default) as = map id as
[PROOFSTEP]
congr with x
[GOAL]
case e_f.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : AddGroup α
as : List α
x : α
⊢ Sub.sub x default = id x
[PROOFSTEP]
exact sub_zero x


[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdrop [] n = []
[PROOFSTEP]
simp [rdrop]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdrop l 0 = l
[PROOFSTEP]
simp [rdrop]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdrop l n = reverse (drop n (reverse l))
[PROOFSTEP]
rw [rdrop]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ take (length l - n) l = reverse (drop n (reverse l))
[PROOFSTEP]
induction' l using List.reverseRecOn with xs x IH generalizing n
[GOAL]
case H0
α : Type u_1
p : α → Bool
l : List α
n✝ n : ℕ
⊢ take (length [] - n) [] = reverse (drop n (reverse []))
[PROOFSTEP]
simp
[GOAL]
case H1
α : Type u_1
p : α → Bool
l : List α
n✝ : ℕ
xs : List α
x : α
IH : ∀ (n : ℕ), take (length xs - n) xs = reverse (drop n (reverse xs))
n : ℕ
⊢ take (length (xs ++ [x]) - n) (xs ++ [x]) = reverse (drop n (reverse (xs ++ [x])))
[PROOFSTEP]
cases n
[GOAL]
case H1.zero
α : Type u_1
p : α → Bool
l : List α
n : ℕ
xs : List α
x : α
IH : ∀ (n : ℕ), take (length xs - n) xs = reverse (drop n (reverse xs))
⊢ take (length (xs ++ [x]) - Nat.zero) (xs ++ [x]) = reverse (drop Nat.zero (reverse (xs ++ [x])))
[PROOFSTEP]
simp [take_append]
[GOAL]
case H1.succ
α : Type u_1
p : α → Bool
l : List α
n : ℕ
xs : List α
x : α
IH : ∀ (n : ℕ), take (length xs - n) xs = reverse (drop n (reverse xs))
n✝ : ℕ
⊢ take (length (xs ++ [x]) - Nat.succ n✝) (xs ++ [x]) = reverse (drop (Nat.succ n✝) (reverse (xs ++ [x])))
[PROOFSTEP]
simp [take_append_eq_append_take, IH]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
⊢ rdrop (l ++ [x]) (n + 1) = rdrop l n
[PROOFSTEP]
simp [rdrop_eq_reverse_drop_reverse]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtake [] n = []
[PROOFSTEP]
simp [rtake]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtake l 0 = []
[PROOFSTEP]
simp [rtake]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtake l n = reverse (take n (reverse l))
[PROOFSTEP]
rw [rtake]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ drop (length l - n) l = reverse (take n (reverse l))
[PROOFSTEP]
induction' l using List.reverseRecOn with xs x IH generalizing n
[GOAL]
case H0
α : Type u_1
p : α → Bool
l : List α
n✝ n : ℕ
⊢ drop (length [] - n) [] = reverse (take n (reverse []))
[PROOFSTEP]
simp
[GOAL]
case H1
α : Type u_1
p : α → Bool
l : List α
n✝ : ℕ
xs : List α
x : α
IH : ∀ (n : ℕ), drop (length xs - n) xs = reverse (take n (reverse xs))
n : ℕ
⊢ drop (length (xs ++ [x]) - n) (xs ++ [x]) = reverse (take n (reverse (xs ++ [x])))
[PROOFSTEP]
cases n
[GOAL]
case H1.zero
α : Type u_1
p : α → Bool
l : List α
n : ℕ
xs : List α
x : α
IH : ∀ (n : ℕ), drop (length xs - n) xs = reverse (take n (reverse xs))
⊢ drop (length (xs ++ [x]) - Nat.zero) (xs ++ [x]) = reverse (take Nat.zero (reverse (xs ++ [x])))
[PROOFSTEP]
exact drop_length _
[GOAL]
case H1.succ
α : Type u_1
p : α → Bool
l : List α
n : ℕ
xs : List α
x : α
IH : ∀ (n : ℕ), drop (length xs - n) xs = reverse (take n (reverse xs))
n✝ : ℕ
⊢ drop (length (xs ++ [x]) - Nat.succ n✝) (xs ++ [x]) = reverse (take (Nat.succ n✝) (reverse (xs ++ [x])))
[PROOFSTEP]
simp [drop_append_eq_append_drop, IH]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
⊢ rtake (l ++ [x]) (n + 1) = rtake l n ++ [x]
[PROOFSTEP]
simp [rtake_eq_reverse_take_reverse]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdropWhile p [] = []
[PROOFSTEP]
simp [rdropWhile, dropWhile]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
⊢ rdropWhile p (l ++ [x]) = if p x = true then rdropWhile p l else l ++ [x]
[PROOFSTEP]
simp only [rdropWhile, dropWhile, reverse_append, reverse_singleton, singleton_append]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
⊢ reverse
      (match p x with
      | true => dropWhile p (reverse l)
      | false => x :: reverse l) =
    if p x = true then reverse (dropWhile p (reverse l)) else l ++ [x]
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : p x = true
⊢ reverse
      (match p x with
      | true => dropWhile p (reverse l)
      | false => x :: reverse l) =
    reverse (dropWhile p (reverse l))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : ¬p x = true
⊢ reverse
      (match p x with
      | true => dropWhile p (reverse l)
      | false => x :: reverse l) =
    l ++ [x]
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : p x = true
⊢ rdropWhile p (l ++ [x]) = rdropWhile p l
[PROOFSTEP]
rw [rdropWhile_concat, if_pos h]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : ¬p x = true
⊢ rdropWhile p (l ++ [x]) = l ++ [x]
[PROOFSTEP]
rw [rdropWhile_concat, if_neg h]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
⊢ rdropWhile p [x] = if p x = true then [] else [x]
[PROOFSTEP]
rw [← nil_append [x], rdropWhile_concat, rdropWhile_nil]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
hl : rdropWhile p l ≠ []
⊢ ¬p (getLast (rdropWhile p l) hl) = true
[PROOFSTEP]
simp_rw [rdropWhile]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
hl : rdropWhile p l ≠ []
⊢ ¬p (getLast (reverse (dropWhile p (reverse l))) (_ : reverse (dropWhile p (reverse l)) ≠ [])) = true
[PROOFSTEP]
rw [getLast_reverse]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
hl : rdropWhile p l ≠ []
⊢ ¬p (get (dropWhile p (reverse l)) { val := 0, isLt := (_ : 0 < length (dropWhile p (reverse l))) }) = true
[PROOFSTEP]
exact dropWhile_nthLe_zero_not _ _ _
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdropWhile p l <+: l
[PROOFSTEP]
rw [← reverse_suffix, rdropWhile, reverse_reverse]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ dropWhile p (reverse l) <:+ reverse l
[PROOFSTEP]
exact dropWhile_suffix _
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true
[PROOFSTEP]
simp [rdropWhile]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ dropWhile p l = l ↔ ∀ (hl : 0 < length l), ¬p (nthLe l 0 hl) = true
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case nil
α : Type u_1
p : α → Bool
n : ℕ
⊢ dropWhile p [] = [] ↔ ∀ (hl : 0 < length []), ¬p (nthLe [] 0 hl) = true
[PROOFSTEP]
simp only [dropWhile, true_iff]
[GOAL]
case nil
α : Type u_1
p : α → Bool
n : ℕ
⊢ ∀ (hl : 0 < length []), ¬p (nthLe [] 0 hl) = true
[PROOFSTEP]
intro h
[GOAL]
case nil
α : Type u_1
p : α → Bool
n : ℕ
h : 0 < length []
⊢ ¬p (nthLe [] 0 h) = true
[PROOFSTEP]
by_contra
[GOAL]
case nil
α : Type u_1
p : α → Bool
n : ℕ
h : 0 < length []
a✝ : p (nthLe [] 0 h) = true
⊢ False
[PROOFSTEP]
rwa [length_nil, lt_self_iff_false] at h
[GOAL]
case cons
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
⊢ dropWhile p (hd :: tl) = hd :: tl ↔ ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
[PROOFSTEP]
rw [dropWhile]
[GOAL]
case cons
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
⊢ (match p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
⊢ ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
[PROOFSTEP]
intro _ H
[GOAL]
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p (nthLe (hd :: tl) 0 hl✝) = true
⊢ False
[PROOFSTEP]
rw [nthLe, get] at H
[GOAL]
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ False
[PROOFSTEP]
refine' (cons_ne_self hd tl) (Sublist.antisymm _ (sublist_cons _ _))
[GOAL]
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ hd :: tl <+ tl
[PROOFSTEP]
rw [← h]
[GOAL]
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) <+
    tl
[PROOFSTEP]
simp only [H]
[GOAL]
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ dropWhile p tl <+ tl
[PROOFSTEP]
exact List.isSuffix.sublist (dropWhile_suffix p)
[GOAL]
case cons.refine'_2
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h : ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
[PROOFSTEP]
have := h (by simp only [length, Nat.succ_pos])
[GOAL]
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h : ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
⊢ 0 < length (hd :: tl)
[PROOFSTEP]
simp only [length, Nat.succ_pos]
[GOAL]
case cons.refine'_2
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h : ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
this : ¬p (nthLe (hd :: tl) 0 (_ : 0 < Nat.succ (length tl))) = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
[PROOFSTEP]
rw [nthLe, get] at this
[GOAL]
case cons.refine'_2
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h : ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
this : ¬p hd = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
[PROOFSTEP]
simp_rw [this]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdropWhile p l = l ↔ ∀ (hl : l ≠ []), ¬p (getLast l hl) = true
[PROOFSTEP]
simp only [rdropWhile, reverse_eq_iff, dropWhile_eq_self_iff, getLast_eq_get]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ (∀ (hl : 0 < length (reverse l)), ¬p (nthLe (reverse l) 0 hl) = true) ↔
    ∀ (hl : l ≠ []), ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
[PROOFSTEP]
refine' ⟨fun h hl => _, fun h hl => _⟩
[GOAL]
case refine'_1
α : Type u_1
p : α → Bool
l : List α
n : ℕ
h : ∀ (hl : 0 < length (reverse l)), ¬p (nthLe (reverse l) 0 hl) = true
hl : l ≠ []
⊢ ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
[PROOFSTEP]
rw [← length_pos, ← length_reverse] at hl
[GOAL]
case refine'_1
α : Type u_1
p : α → Bool
l : List α
n : ℕ
h : ∀ (hl : 0 < length (reverse l)), ¬p (nthLe (reverse l) 0 hl) = true
hl✝ : l ≠ []
hl : 0 < length (reverse l)
⊢ ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
[PROOFSTEP]
have := h hl
[GOAL]
case refine'_1
α : Type u_1
p : α → Bool
l : List α
n : ℕ
h : ∀ (hl : 0 < length (reverse l)), ¬p (nthLe (reverse l) 0 hl) = true
hl✝ : l ≠ []
hl : 0 < length (reverse l)
this : ¬p (nthLe (reverse l) 0 hl) = true
⊢ ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
[PROOFSTEP]
rwa [nthLe, get_reverse'] at this
[GOAL]
case refine'_2
α : Type u_1
p : α → Bool
l : List α
n : ℕ
h : ∀ (hl : l ≠ []), ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
hl : 0 < length (reverse l)
⊢ ¬p (nthLe (reverse l) 0 hl) = true
[PROOFSTEP]
rw [length_reverse, length_pos] at hl
[GOAL]
case refine'_2
α : Type u_1
p : α → Bool
l : List α
n : ℕ
h : ∀ (hl : l ≠ []), ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
hl✝ : 0 < length (reverse l)
hl : l ≠ []
⊢ ¬p (nthLe (reverse l) 0 hl✝) = true
[PROOFSTEP]
have := h hl
[GOAL]
case refine'_2
α : Type u_1
p : α → Bool
l : List α
n : ℕ
h : ∀ (hl : l ≠ []), ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
hl✝ : 0 < length (reverse l)
hl : l ≠ []
this : ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
⊢ ¬p (nthLe (reverse l) 0 hl✝) = true
[PROOFSTEP]
rwa [nthLe, get_reverse']
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ dropWhile p (dropWhile p l) = dropWhile p l
[PROOFSTEP]
simp only [dropWhile_eq_self_iff]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ ∀ (hl : 0 < length (dropWhile p l)), ¬p (nthLe (dropWhile p l) 0 hl) = true
[PROOFSTEP]
exact fun h => dropWhile_nthLe_zero_not p l h
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtakeWhile p [] = []
[PROOFSTEP]
simp [rtakeWhile, takeWhile]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
⊢ rtakeWhile p (l ++ [x]) = if p x = true then rtakeWhile p l ++ [x] else []
[PROOFSTEP]
simp only [rtakeWhile, takeWhile, reverse_append, reverse_singleton, singleton_append]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
⊢ reverse
      (match p x with
      | true => x :: takeWhile p (reverse l)
      | false => []) =
    if p x = true then reverse (takeWhile p (reverse l)) ++ [x] else []
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : p x = true
⊢ reverse
      (match p x with
      | true => x :: takeWhile p (reverse l)
      | false => []) =
    reverse (takeWhile p (reverse l)) ++ [x]
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : ¬p x = true
⊢ reverse
      (match p x with
      | true => x :: takeWhile p (reverse l)
      | false => []) =
    []
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : p x = true
⊢ rtakeWhile p (l ++ [x]) = rtakeWhile p l ++ [x]
[PROOFSTEP]
rw [rtakeWhile_concat, if_pos h]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : ¬p x = true
⊢ rtakeWhile p (l ++ [x]) = []
[PROOFSTEP]
rw [rtakeWhile_concat, if_neg h]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtakeWhile p l <:+ l
[PROOFSTEP]
rw [← reverse_prefix, rtakeWhile, reverse_reverse]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ takeWhile p (reverse l) <+: reverse l
[PROOFSTEP]
exact takeWhile_prefix _
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtakeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true
[PROOFSTEP]
simp [rtakeWhile, reverse_eq_iff]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (getLast l hl) = true
[PROOFSTEP]
induction' l using List.reverseRecOn with l a
[GOAL]
case H0
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtakeWhile p [] = [] ↔ ∀ (hl : [] ≠ []), ¬p (getLast [] hl) = true
[PROOFSTEP]
simp only [rtakeWhile, takeWhile, reverse_nil, true_iff]
[GOAL]
case H0
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ ∀ (hl : [] ≠ []), ¬p (getLast [] hl) = true
[PROOFSTEP]
intro f
[GOAL]
case H0
α : Type u_1
p : α → Bool
l : List α
n : ℕ
f : [] ≠ []
⊢ ¬p (getLast [] f) = true
[PROOFSTEP]
contradiction
[GOAL]
case H1
α : Type u_1
p : α → Bool
l✝ : List α
n : ℕ
l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (getLast l hl) = true
⊢ rtakeWhile p (l ++ [a]) = [] ↔ ∀ (hl : l ++ [a] ≠ []), ¬p (getLast (l ++ [a]) hl) = true
[PROOFSTEP]
simp only [rtakeWhile, reverse_append, takeWhile, reverse_eq_nil, getLast_append, ne_eq, append_eq_nil, and_false,
  forall_true_left]
[GOAL]
case H1
α : Type u_1
p : α → Bool
l✝ : List α
n : ℕ
l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (getLast l hl) = true
⊢ (match p a with
      | true => a :: takeWhile p (List.append [] (reverse l))
      | false => []) =
      [] ↔
    ¬p a = true
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case H1.refine'_1
α : Type u_1
p : α → Bool
l✝ : List α
n : ℕ
l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (getLast l hl) = true
h :
  (match p a with
    | true => a :: takeWhile p (List.append [] (reverse l))
    | false => []) =
    []
⊢ ¬p a = true
[PROOFSTEP]
intro pa
[GOAL]
case H1.refine'_1
α : Type u_1
p : α → Bool
l✝ : List α
n : ℕ
l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (getLast l hl) = true
h :
  (match p a with
    | true => a :: takeWhile p (List.append [] (reverse l))
    | false => []) =
    []
pa : p a = true
⊢ False
[PROOFSTEP]
simp only [pa] at h
[GOAL]
case H1.refine'_2
α : Type u_1
p : α → Bool
l✝ : List α
n : ℕ
l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (getLast l hl) = true
h : ¬p a = true
⊢ (match p a with
    | true => a :: takeWhile p (List.append [] (reverse l))
    | false => []) =
    []
[PROOFSTEP]
simp only [h]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
hx : x ∈ rtakeWhile p l
⊢ p x = true
[PROOFSTEP]
rw [rtakeWhile, mem_reverse] at hx
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
hx : x ∈ takeWhile p (reverse l)
⊢ p x = true
[PROOFSTEP]
exact mem_takeWhile_imp hx


[GOAL]
n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.fst + x.snd = n
[PROOFSTEP]
rw [antidiagonal, mem_map]
[GOAL]
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, a ∈ range (n + 1) ∧ (a, n - a) = x) ↔ x.fst + x.snd = n
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, a ∈ range (n + 1) ∧ (a, n - a) = x) → x.fst + x.snd = n
[PROOFSTEP]
rintro ⟨i, hi, rfl⟩
[GOAL]
case mp.intro.intro
n i : ℕ
hi : i ∈ range (n + 1)
⊢ (i, n - i).fst + (i, n - i).snd = n
[PROOFSTEP]
rw [mem_range, lt_succ_iff] at hi
[GOAL]
case mp.intro.intro
n i : ℕ
hi : i ≤ n
⊢ (i, n - i).fst + (i, n - i).snd = n
[PROOFSTEP]
exact add_tsub_cancel_of_le hi
[GOAL]
case mpr
n : ℕ
x : ℕ × ℕ
⊢ x.fst + x.snd = n → ∃ a, a ∈ range (n + 1) ∧ (a, n - a) = x
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
x : ℕ × ℕ
⊢ ∃ a, a ∈ range (x.fst + x.snd + 1) ∧ (a, x.fst + x.snd - a) = x
[PROOFSTEP]
refine' ⟨x.fst, _, _⟩
[GOAL]
case mpr.refine'_1
x : ℕ × ℕ
⊢ x.fst ∈ range (x.fst + x.snd + 1)
[PROOFSTEP]
rw [mem_range, add_assoc, lt_add_iff_pos_right]
[GOAL]
case mpr.refine'_1
x : ℕ × ℕ
⊢ 0 < x.snd + 1
[PROOFSTEP]
exact zero_lt_succ _
[GOAL]
case mpr.refine'_2
x : ℕ × ℕ
⊢ (x.fst, x.fst + x.snd - x.fst) = x
[PROOFSTEP]
exact Prod.ext rfl (by simp only [add_tsub_cancel_left])
[GOAL]
x : ℕ × ℕ
⊢ (x.fst, x.fst + x.snd - x.fst).snd = x.snd
[PROOFSTEP]
simp only [add_tsub_cancel_left]
[GOAL]
n : ℕ
⊢ length (antidiagonal n) = n + 1
[PROOFSTEP]
rw [antidiagonal, length_map, length_range]
[GOAL]
n : ℕ
⊢ antidiagonal (n + 1) = (0, n + 1) :: map (Prod.map succ id) (antidiagonal n)
[PROOFSTEP]
simp only [antidiagonal, range_succ_eq_map, map_cons, true_and_iff, Nat.add_succ_sub_one, add_zero, id.def,
  eq_self_iff_true, tsub_zero, map_map, Prod.map_mk]
[GOAL]
n : ℕ
⊢ (0, n + 1) :: (succ 0, n) :: map ((fun i => (i, n + 1 - i)) ∘ succ ∘ succ) (range n) =
    (0, n + 1) :: (succ 0, n) :: map (Prod.map succ id ∘ (fun i => (i, n - i)) ∘ succ) (range n)
[PROOFSTEP]
apply congr rfl (congr rfl _)
[GOAL]
n : ℕ
⊢ map ((fun i => (i, n + 1 - i)) ∘ succ ∘ succ) (range n) =
    map (Prod.map succ id ∘ (fun i => (i, n - i)) ∘ succ) (range n)
[PROOFSTEP]
ext
[GOAL]
case a.a
n n✝ : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ get? (map ((fun i => (i, n + 1 - i)) ∘ succ ∘ succ) (range n)) n✝ ↔
    a✝ ∈ get? (map (Prod.map succ id ∘ (fun i => (i, n - i)) ∘ succ) (range n)) n✝
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ antidiagonal (n + 1) = map (Prod.map id succ) (antidiagonal n) ++ [(n + 1, 0)]
[PROOFSTEP]
simp only [antidiagonal, range_succ, add_tsub_cancel_left, map_append, append_assoc, tsub_self, singleton_append,
  map_map, map]
[GOAL]
n : ℕ
⊢ map (fun i => (i, n + 1 - i)) (range n) ++ [(n, 1), (n + 1, 0)] =
    map (Prod.map id succ ∘ fun i => (i, n - i)) (range n) ++ [Prod.map id succ (n, 0), (n + 1, 0)]
[PROOFSTEP]
congr 1
[GOAL]
case e_a
n : ℕ
⊢ map (fun i => (i, n + 1 - i)) (range n) = map (Prod.map id succ ∘ fun i => (i, n - i)) (range n)
[PROOFSTEP]
apply map_congr
[GOAL]
case e_a.a
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range n → (x, n + 1 - x) = (Prod.map id succ ∘ fun i => (i, n - i)) x
[PROOFSTEP]
simp (config := { contextual := true }) [le_of_lt, Nat.succ_eq_add_one, Nat.sub_add_comm]
[GOAL]
n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) :: map (Prod.map succ succ) (antidiagonal n) ++ [(n + 2, 0)]
[PROOFSTEP]
rw [antidiagonal_succ']
[GOAL]
n : ℕ
⊢ map (Prod.map id succ) (antidiagonal (n + 1)) ++ [(n + 1 + 1, 0)] =
    (0, n + 2) :: map (Prod.map succ succ) (antidiagonal n) ++ [(n + 2, 0)]
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ map (Prod.map id succ ∘ Prod.map succ id) (antidiagonal n) = map (Prod.map succ succ) (antidiagonal n)
[PROOFSTEP]
ext
[GOAL]
case a.a
n n✝ : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ get? (map (Prod.map id succ ∘ Prod.map succ id) (antidiagonal n)) n✝ ↔
    a✝ ∈ get? (map (Prod.map succ succ) (antidiagonal n)) n✝
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ map Prod.swap (antidiagonal n) = reverse (antidiagonal n)
[PROOFSTEP]
rw [antidiagonal, map_map, ← List.map_reverse, range_eq_range', reverse_range', ← range_eq_range', map_map]
[GOAL]
n : ℕ
⊢ map (Prod.swap ∘ fun i => (i, n - i)) (range (n + 1)) =
    map ((fun i => (i, n - i)) ∘ fun x => 0 + (n + 1) - 1 - x) (range (n + 1))
[PROOFSTEP]
apply map_congr
[GOAL]
case a
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ range (n + 1) → (Prod.swap ∘ fun i => (i, n - i)) x = ((fun i => (i, n - i)) ∘ fun x => 0 + (n + 1) - 1 - x) x
[PROOFSTEP]
simp (config := { contextual := true }) [Nat.sub_sub_self, lt_succ_iff]


[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
l : List α
⊢ l <+: concat l a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m✝ n✝ n m : ℕ
l : List α
⊢ dropSlice n m l = take n l ++ drop m (drop n l)
[PROOFSTEP]
rw [dropSlice_eq, drop_drop, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ dropLast [] ++ [] = []
[PROOFSTEP]
rw [dropLast, List.append_nil]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ tail l <:+ l
[PROOFSTEP]
rw [← drop_one]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ drop 1 l <:+ l
[PROOFSTEP]
apply drop_suffix
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ l₁ <+: l₂ → l₁ ++ drop (length l₁) l₂ = l₂
[PROOFSTEP]
rintro ⟨r, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
l l₁ l₃ : List α
a b : α
m n : ℕ
r : List α
⊢ l₁ ++ drop (length l₁) (l₁ ++ r) = l₁ ++ r
[PROOFSTEP]
rw [drop_left]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ l₁ <:+ l₂ → take (length l₂ - length l₁) l₂ ++ l₁ = l₂
[PROOFSTEP]
rintro ⟨r, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
l l₁ l₃ : List α
a b : α
m n : ℕ
r : List α
⊢ take (length (r ++ l₁) - length l₁) (r ++ l₁) ++ l₁ = r ++ l₁
[PROOFSTEP]
simp only [length_append, add_tsub_cancel_right, take_left]
[GOAL]
α : Type u_1
β : Type u_2
l l₁✝ l₂✝ l₃ : List α
a✝ b✝ : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
h : a = b
⊢ l₁ <+: l₂ ↔ a :: l₁ <+: b :: l₂
[PROOFSTEP]
rw [← h, prefix_cons_inj]
[GOAL]
α : Type u_1
β : Type u_2
l l₁✝ l₂✝ l₃ : List α
a✝ b✝ : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
h : ¬a = b
x✝ : a :: l₁ <+: b :: l₂
t : List α
te : a :: l₁ ++ t = b :: l₂
⊢ a = b
[PROOFSTEP]
injection te
[GOAL]
α : Type u_1
β : Type u_2
l l₁✝ l₂ l₃ : List α
a✝ b : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l₁ : List α
⊢ ¬length (a :: l₁) ≤ length []
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l l₁✝ l₂ l₃ : List α
a✝ b : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l₁ : List α
x✝ : a :: l₁ <:+: []
s t : List α
te : s ++ a :: l₁ ++ t = []
⊢ False
[PROOFSTEP]
simp at te
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List (List (Option α))
hm : m < length L
⊢ take m L <+: take n L ↔ m ≤ n
[PROOFSTEP]
simp only [prefix_iff_eq_take, length_take]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List (List (Option α))
hm : m < length L
⊢ take m L = take (min m (length L)) (take n L) ↔ m ≤ n
[PROOFSTEP]
induction m generalizing L n with
| zero => simp [min_eq_left, eq_self_iff_true, Nat.zero_le, take]
| succ m IH =>
  cases L with
  | nil => exact (not_lt_bot hm).elim
  | cons l ls =>
    cases n with
    | zero =>
      refine' iff_of_false _ (zero_lt_succ _).not_le
      rw [take_zero, take_nil]
      simp only [take]
    | succ n =>
      simp only [length] at hm
      have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
      simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH
      simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
      exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List (List (Option α))
hm : m < length L
⊢ take m L = take (min m (length L)) (take n L) ↔ m ≤ n
[PROOFSTEP]
induction m generalizing L n with
| zero => simp [min_eq_left, eq_self_iff_true, Nat.zero_le, take]
| succ m IH =>
  cases L with
  | nil => exact (not_lt_bot hm).elim
  | cons l ls =>
    cases n with
    | zero =>
      refine' iff_of_false _ (zero_lt_succ _).not_le
      rw [take_zero, take_nil]
      simp only [take]
    | succ n =>
      simp only [length] at hm
      have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
      simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH
      simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
      exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case zero
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
n : ℕ
L : List (List (Option α))
hm : zero < length L
⊢ take zero L = take (min zero (length L)) (take n L) ↔ zero ≤ n
[PROOFSTEP]

| zero => simp [min_eq_left, eq_self_iff_true, Nat.zero_le, take]
[GOAL]
case zero
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
n : ℕ
L : List (List (Option α))
hm : zero < length L
⊢ take zero L = take (min zero (length L)) (take n L) ↔ zero ≤ n
[PROOFSTEP]
simp [min_eq_left, eq_self_iff_true, Nat.zero_le, take]
[GOAL]
case succ
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
L : List (List (Option α))
hm : succ m < length L
⊢ take (succ m) L = take (min (succ m) (length L)) (take n L) ↔ succ m ≤ n
[PROOFSTEP]

| succ m IH =>
  cases L with
  | nil => exact (not_lt_bot hm).elim
  | cons l ls =>
    cases n with
    | zero =>
      refine' iff_of_false _ (zero_lt_succ _).not_le
      rw [take_zero, take_nil]
      simp only [take]
    | succ n =>
      simp only [length] at hm
      have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
      simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH
      simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
      exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case succ
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
L : List (List (Option α))
hm : succ m < length L
⊢ take (succ m) L = take (min (succ m) (length L)) (take n L) ↔ succ m ≤ n
[PROOFSTEP]
cases L with
| nil => exact (not_lt_bot hm).elim
| cons l ls =>
  cases n with
  | zero =>
    refine' iff_of_false _ (zero_lt_succ _).not_le
    rw [take_zero, take_nil]
    simp only [take]
  | succ n =>
    simp only [length] at hm
    have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
    simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH
    simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
    exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case succ
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
L : List (List (Option α))
hm : succ m < length L
⊢ take (succ m) L = take (min (succ m) (length L)) (take n L) ↔ succ m ≤ n
[PROOFSTEP]
cases L with
| nil => exact (not_lt_bot hm).elim
| cons l ls =>
  cases n with
  | zero =>
    refine' iff_of_false _ (zero_lt_succ _).not_le
    rw [take_zero, take_nil]
    simp only [take]
  | succ n =>
    simp only [length] at hm
    have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
    simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH
    simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
    exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case succ.nil
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
hm : succ m < length []
⊢ take (succ m) [] = take (min (succ m) (length [])) (take n []) ↔ succ m ≤ n
[PROOFSTEP]

| nil => exact (not_lt_bot hm).elim
[GOAL]
case succ.nil
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
hm : succ m < length []
⊢ take (succ m) [] = take (min (succ m) (length [])) (take n []) ↔ succ m ≤ n
[PROOFSTEP]
exact (not_lt_bot hm).elim
[GOAL]
case succ.cons
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take n (l :: ls)) ↔ succ m ≤ n
[PROOFSTEP]

| cons l ls =>
  cases n with
  | zero =>
    refine' iff_of_false _ (zero_lt_succ _).not_le
    rw [take_zero, take_nil]
    simp only [take]
  | succ n =>
    simp only [length] at hm
    have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
    simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH
    simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
    exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case succ.cons
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take n (l :: ls)) ↔ succ m ≤ n
[PROOFSTEP]
cases n with
| zero =>
  refine' iff_of_false _ (zero_lt_succ _).not_le
  rw [take_zero, take_nil]
  simp only [take]
| succ n =>
  simp only [length] at hm
  have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
  simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH
  simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
  exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case succ.cons
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take n (l :: ls)) ↔ succ m ≤ n
[PROOFSTEP]
cases n with
| zero =>
  refine' iff_of_false _ (zero_lt_succ _).not_le
  rw [take_zero, take_nil]
  simp only [take]
| succ n =>
  simp only [length] at hm
  have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
  simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH
  simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
  exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case succ.cons.zero
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take zero (l :: ls)) ↔ succ m ≤ zero
[PROOFSTEP]

| zero =>
  refine' iff_of_false _ (zero_lt_succ _).not_le
  rw [take_zero, take_nil]
  simp only [take]
[GOAL]
case succ.cons.zero
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take zero (l :: ls)) ↔ succ m ≤ zero
[PROOFSTEP]
refine' iff_of_false _ (zero_lt_succ _).not_le
[GOAL]
case succ.cons.zero
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ ¬take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take zero (l :: ls))
[PROOFSTEP]
rw [take_zero, take_nil]
[GOAL]
case succ.cons.zero
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ ¬take (succ m) (l :: ls) = []
[PROOFSTEP]
simp only [take]
[GOAL]
case succ.cons.succ
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
n : ℕ
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
[PROOFSTEP]

| succ n =>
  simp only [length] at hm
  have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
  simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH
  simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
  exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case succ.cons.succ
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
n : ℕ
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
[PROOFSTEP]
simp only [length] at hm
[GOAL]
case succ.cons.succ
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
[PROOFSTEP]
have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
[GOAL]
case succ.cons.succ
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
specializedIH : take m ls = take (min m (length ls)) (take n ls) ↔ m ≤ n
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
[PROOFSTEP]
simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH
[GOAL]
case succ.cons.succ
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
specializedIH : take m ls = take m (take n ls) ↔ m ≤ n
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
[PROOFSTEP]
simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
[GOAL]
case succ.cons.succ
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
specializedIH : take m ls = take m (take n ls) ↔ m ≤ n
⊢ m ≤ n ↔ succ m ≤ succ n
[PROOFSTEP]
exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+: b :: l₂ → a = b ∧ l₁ <+: l₂
[PROOFSTEP]
rintro ⟨L, hL⟩
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List α
hL : a :: l₁ ++ L = b :: l₂
⊢ a = b ∧ l₁ <+: l₂
[PROOFSTEP]
simp only [cons_append] at hL
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List α
hL : a :: (l₁ ++ L) = b :: l₂
⊢ a = b ∧ l₁ <+: l₂
[PROOFSTEP]
injection hL with hLLeft hLRight
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List α
hLLeft : a = b
hLRight : l₁ ++ L = l₂
⊢ a = b ∧ l₁ <+: l₂
[PROOFSTEP]
exact ⟨hLLeft, ⟨L, hLRight⟩⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ a = b ∧ l₁ <+: l₂ → a :: l₁ <+: b :: l₂
[PROOFSTEP]
rintro ⟨rfl, h⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a : α
m n : ℕ
h : l₁ <+: l₂
⊢ a :: l₁ <+: a :: l₂
[PROOFSTEP]
rwa [prefix_cons_inj]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h : l₁ <+: l₂
f : α → β
⊢ List.map f l₁ <+: List.map f l₂
[PROOFSTEP]
induction' l₁ with hd tl hl generalizing l₂
[GOAL]
case nil
α : Type u_1
β : Type u_2
l l₁ l₂✝ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂✝
f : α → β
l₂ : List α
h : [] <+: l₂
⊢ List.map f [] <+: List.map f l₂
[PROOFSTEP]
simp only [nil_prefix, map_nil]
[GOAL]
case cons
α : Type u_1
β : Type u_2
l l₁ l₂✝ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂✝
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
l₂ : List α
h : hd :: tl <+: l₂
⊢ List.map f (hd :: tl) <+: List.map f l₂
[PROOFSTEP]
cases' l₂ with hd₂ tl₂
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
h : hd :: tl <+: []
⊢ List.map f (hd :: tl) <+: List.map f []
[PROOFSTEP]
simpa only using eq_nil_of_prefix_nil h
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
hd₂ : α
tl₂ : List α
h : hd :: tl <+: hd₂ :: tl₂
⊢ List.map f (hd :: tl) <+: List.map f (hd₂ :: tl₂)
[PROOFSTEP]
rw [cons_prefix_iff] at h
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
hd₂ : α
tl₂ : List α
h : hd = hd₂ ∧ tl <+: tl₂
⊢ List.map f (hd :: tl) <+: List.map f (hd₂ :: tl₂)
[PROOFSTEP]
simp only [List.map_cons, h, prefix_cons_inj, hl, map]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h : l₁ <+: l₂
f : α → Option β
⊢ filterMap f l₁ <+: filterMap f l₂
[PROOFSTEP]
induction' l₁ with hd₁ tl₁ hl generalizing l₂
[GOAL]
case nil
α : Type u_1
β : Type u_2
l l₁ l₂✝ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂✝
f : α → Option β
l₂ : List α
h : [] <+: l₂
⊢ filterMap f [] <+: filterMap f l₂
[PROOFSTEP]
simp only [nil_prefix, filterMap_nil]
[GOAL]
case cons
α : Type u_1
β : Type u_2
l l₁ l₂✝ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂✝
f : α → Option β
hd₁ : α
tl₁ : List α
hl : ∀ {l₂ : List α}, tl₁ <+: l₂ → filterMap f tl₁ <+: filterMap f l₂
l₂ : List α
h : hd₁ :: tl₁ <+: l₂
⊢ filterMap f (hd₁ :: tl₁) <+: filterMap f l₂
[PROOFSTEP]
cases' l₂ with hd₂ tl₂
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → Option β
hd₁ : α
tl₁ : List α
hl : ∀ {l₂ : List α}, tl₁ <+: l₂ → filterMap f tl₁ <+: filterMap f l₂
h : hd₁ :: tl₁ <+: []
⊢ filterMap f (hd₁ :: tl₁) <+: filterMap f []
[PROOFSTEP]
simpa only using eq_nil_of_prefix_nil h
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → Option β
hd₁ : α
tl₁ : List α
hl : ∀ {l₂ : List α}, tl₁ <+: l₂ → filterMap f tl₁ <+: filterMap f l₂
hd₂ : α
tl₂ : List α
h : hd₁ :: tl₁ <+: hd₂ :: tl₂
⊢ filterMap f (hd₁ :: tl₁) <+: filterMap f (hd₂ :: tl₂)
[PROOFSTEP]
rw [cons_prefix_iff] at h
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → Option β
hd₁ : α
tl₁ : List α
hl : ∀ {l₂ : List α}, tl₁ <+: l₂ → filterMap f tl₁ <+: filterMap f l₂
hd₂ : α
tl₂ : List α
h : hd₁ = hd₂ ∧ tl₁ <+: tl₂
⊢ filterMap f (hd₁ :: tl₁) <+: filterMap f (hd₂ :: tl₂)
[PROOFSTEP]
rw [← @singleton_append _ hd₁ _, ← @singleton_append _ hd₂ _, filterMap_append, filterMap_append, h.left,
  prefix_append_right_inj]
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → Option β
hd₁ : α
tl₁ : List α
hl : ∀ {l₂ : List α}, tl₁ <+: l₂ → filterMap f tl₁ <+: filterMap f l₂
hd₂ : α
tl₂ : List α
h : hd₁ = hd₂ ∧ tl₁ <+: tl₂
⊢ filterMap f tl₁ <+: filterMap f tl₂
[PROOFSTEP]
exact hl h.right
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
s : List α
this : s = [] ↔ s <+: []
⊢ s ∈ inits [] ↔ s <+: []
[PROOFSTEP]
simpa only [inits, mem_singleton]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s✝ : List α
a : α
t : List α
o : s✝ = [] ∨ ∃ l, l ∈ inits t ∧ a :: l = s✝
s r : List α
hr : r ∈ inits t
hs : a :: r = s
⊢ s <+: a :: t
[PROOFSTEP]
let ⟨s, ht⟩ := (mem_inits _ _).1 hr
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ inits t ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ inits t
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ s✝ <+: a :: t
[PROOFSTEP]
rw [← hs, ← ht]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ inits t ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ inits t
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ a :: r <+: a :: (r ++ s)
[PROOFSTEP]
exact ⟨s, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b✝ : α
m n : ℕ
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b = a
st : s ++ r = t
⊢ ∃ l, l ∈ inits t ∧ a :: l = b :: s
[PROOFSTEP]
rw [ba]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b✝ : α
m n : ℕ
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b = a
st : s ++ r = t
⊢ ∃ l, l ∈ inits t ∧ a :: l = a :: s
[PROOFSTEP]
exact ⟨_, (mem_inits _ _).2 ⟨_, st⟩, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s : List α
a : α
t : List α
this : (s = [] ∨ ∃ l, l ∈ inits t ∧ a :: l = s) ↔ s <+: a :: t
⊢ s ∈ inits (a :: t) ↔ s <+: a :: t
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
s : List α
⊢ s ∈ tails [] ↔ s <:+ []
[PROOFSTEP]
simp only [tails, mem_singleton, suffix_nil]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s : List α
a : α
t : List α
⊢ s ∈ tails (a :: t) ↔ s <:+ a :: t
[PROOFSTEP]
simp only [tails, mem_cons, mem_tails s t]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s : List α
a : α
t : List α
⊢ s = a :: t ∨ s <:+ t ↔ s <:+ a :: t
[PROOFSTEP]
exact
  show s = a :: t ∨ s <:+ t ↔ s <:+ a :: t from
    ⟨fun o =>
      match s, t, o with
      | _, t, Or.inl rfl => suffix_rfl
      | s, _, Or.inr ⟨l, rfl⟩ => ⟨a :: l, rfl⟩,
      fun e =>
      match s, t, e with
      | _, t, ⟨[], rfl⟩ => Or.inl rfl
      | s, t, ⟨b :: l, he⟩ => List.noConfusion he fun _ lt => Or.inr ⟨l, lt⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
l : List α
⊢ inits (a :: l) = [] :: map (fun t => a :: t) (inits l)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
l : List α
⊢ tails (a :: l) = (a :: l) :: tails l
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ inits ([] ++ []) = inits [] ++ map (fun l => [] ++ l) (tail (inits []))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
t : List α
⊢ inits ([] ++ a :: t) = inits [] ++ map (fun l => [] ++ l) (tail (inits (a :: t)))
[PROOFSTEP]
simp [· ∘ ·]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
s t : List α
⊢ inits (a :: s ++ t) = inits (a :: s) ++ map (fun l => a :: s ++ l) (tail (inits t))
[PROOFSTEP]
simp [inits_append s t, · ∘ ·]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ tails ([] ++ []) = map (fun l => l ++ []) (tails []) ++ tail (tails [])
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
t : List α
⊢ tails ([] ++ a :: t) = map (fun l => l ++ a :: t) (tails []) ++ tail (tails (a :: t))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
s t : List α
⊢ tails (a :: s ++ t) = map (fun l => l ++ t) (tails (a :: s)) ++ tail (tails t)
[PROOFSTEP]
simp [tails_append s t]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ inits [] = reverse (map reverse (tails (reverse [])))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
l : List α
⊢ inits (a :: l) = reverse (map reverse (tails (reverse (a :: l))))
[PROOFSTEP]
simp [inits_eq_tails l, map_eq_map_iff, reverse_map]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ tails [] = reverse (map reverse (inits (reverse [])))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
l : List α
⊢ tails (a :: l) = reverse (map reverse (inits (reverse (a :: l))))
[PROOFSTEP]
simp [tails_eq_inits l, append_left_inj]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ inits (reverse l) = reverse (map reverse (tails l))
[PROOFSTEP]
rw [tails_eq_inits l]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ inits (reverse l) = reverse (map reverse (reverse (map reverse (inits (reverse l)))))
[PROOFSTEP]
simp [reverse_involutive.comp_self, reverse_map]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ tails (reverse l) = reverse (map reverse (inits l))
[PROOFSTEP]
rw [inits_eq_tails l]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ tails (reverse l) = reverse (map reverse (reverse (map reverse (tails (reverse l)))))
[PROOFSTEP]
simp [reverse_involutive.comp_self, reverse_map]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ map reverse (inits l) = reverse (tails (reverse l))
[PROOFSTEP]
rw [inits_eq_tails l]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ map reverse (reverse (map reverse (tails (reverse l)))) = reverse (tails (reverse l))
[PROOFSTEP]
simp [reverse_involutive.comp_self, reverse_map]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ map reverse (tails l) = reverse (inits (reverse l))
[PROOFSTEP]
rw [tails_eq_inits l]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ map reverse (reverse (map reverse (inits (reverse l)))) = reverse (inits (reverse l))
[PROOFSTEP]
simp [reverse_involutive.comp_self, reverse_map]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ length (tails l) = length l + 1
[PROOFSTEP]
induction' l with x l IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ length (tails []) = length [] + 1
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
x : α
l : List α
IH : length (tails l) = length l + 1
⊢ length (tails (x :: l)) = length (x :: l) + 1
[PROOFSTEP]
simpa using IH
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ length (inits l) = length l + 1
[PROOFSTEP]
simp [inits_eq_tails]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n✝ : ℕ
l : List α
n : ℕ
hn : n < length (tails l)
⊢ nthLe (tails l) n hn = drop n l
[PROOFSTEP]
induction' l with x l IH generalizing n
[GOAL]
case nil
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l : List α
n✝ : ℕ
hn✝ : n✝ < length (tails l)
n : ℕ
hn : n < length (tails [])
⊢ nthLe (tails []) n hn = drop n []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l✝ : List α
n✝ : ℕ
hn✝ : n✝ < length (tails l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (tails l)), nthLe (tails l) n hn = drop n l
n : ℕ
hn : n < length (tails (x :: l))
⊢ nthLe (tails (x :: l)) n hn = drop n (x :: l)
[PROOFSTEP]
cases n
[GOAL]
case cons.zero
α : Type u_1
β : Type u_2
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝ : ℕ
l✝ : List α
n : ℕ
hn✝ : n < length (tails l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (tails l)), nthLe (tails l) n hn = drop n l
hn : zero < length (tails (x :: l))
⊢ nthLe (tails (x :: l)) zero hn = drop zero (x :: l)
[PROOFSTEP]
simp [nthLe_cons]
[GOAL]
case cons.succ
α : Type u_1
β : Type u_2
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l✝ : List α
n : ℕ
hn✝ : n < length (tails l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (tails l)), nthLe (tails l) n hn = drop n l
n✝ : ℕ
hn : succ n✝ < length (tails (x :: l))
⊢ nthLe (tails (x :: l)) (succ n✝) hn = drop (succ n✝) (x :: l)
[PROOFSTEP]
simpa [nthLe_cons] using IH _ _
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n✝ : ℕ
l : List α
n : ℕ
hn : n < length (inits l)
⊢ nthLe (inits l) n hn = take n l
[PROOFSTEP]
induction' l with x l IH generalizing n
[GOAL]
case nil
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l : List α
n✝ : ℕ
hn✝ : n✝ < length (inits l)
n : ℕ
hn : n < length (inits [])
⊢ nthLe (inits []) n hn = take n []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l✝ : List α
n✝ : ℕ
hn✝ : n✝ < length (inits l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (inits l)), nthLe (inits l) n hn = take n l
n : ℕ
hn : n < length (inits (x :: l))
⊢ nthLe (inits (x :: l)) n hn = take n (x :: l)
[PROOFSTEP]
cases n
[GOAL]
case cons.zero
α : Type u_1
β : Type u_2
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝ : ℕ
l✝ : List α
n : ℕ
hn✝ : n < length (inits l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (inits l)), nthLe (inits l) n hn = take n l
hn : zero < length (inits (x :: l))
⊢ nthLe (inits (x :: l)) zero hn = take zero (x :: l)
[PROOFSTEP]
simp [nthLe_cons]
[GOAL]
case cons.succ
α : Type u_1
β : Type u_2
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l✝ : List α
n : ℕ
hn✝ : n < length (inits l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (inits l)), nthLe (inits l) n hn = take n l
n✝ : ℕ
hn : succ n✝ < length (inits (x :: l))
⊢ nthLe (inits (x :: l)) (succ n✝) hn = take (succ n✝) (x :: l)
[PROOFSTEP]
simpa [nthLe_cons] using IH _ _
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l : List α
⊢ l <:+ List.insert a l
[PROOFSTEP]
by_cases h : a ∈ l
[GOAL]
case pos
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ l <:+ List.insert a l
[PROOFSTEP]
simp only [insert_of_mem h, insert, suffix_refl]
[GOAL]
case neg
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <:+ List.insert a l
[PROOFSTEP]
simp only [insert_of_not_mem h, suffix_cons, insert]