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
α : 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
cases m
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
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
contradiction
no goals
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
cases as <;> simp only [set, get, get_nil]
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✝)
α : 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
cases as <;> cases m
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✝)
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✝)
case nil =>
  simp only [set, get]
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✝)
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✝)
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
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✝)
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✝)
case zero =>
  simp only [set, get]
no goals
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✝)
case _ _ m =>
  apply get_set_eq_of_ne k m
  intro hc
  apply h1
  simp [hc]
no goals
α : 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 []
simp only [set, get]
α : 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) []
α : 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) []
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]
no goals
α : 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) []
apply h3
α : 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
α : 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
rw [get_set_eq_of_ne k m, get_nil]
α : 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
α : 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
intro hc
α : 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
α : 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
apply h1
no goals
α : 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
simp [hc]
no goals
α : 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✝)
simp only [set, get]
α : 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
α : 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✝)
apply get_set_eq_of_ne k m
α : 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
α : 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
intro hc
α : 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
α : 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
apply h1
no goals
α : 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
simp [hc]