[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
