case inl
ι : Type ?u.503527
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
x : α
xs : List α
d✝ : α
n✝ : ℕ
l l' : List α
d : α
n : ℕ
h : length l ≤ n
h' : n < length (l ++ l')
⊢ getD (l ++ l') n d = getD l' (n - length l) d

case inr
ι : Type ?u.503527
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
x : α
xs : List α
d✝ : α
n✝ : ℕ
l l' : List α
d : α
n : ℕ
h : length l ≤ n
h' : length (l ++ l') ≤ n
⊢ getD (l ++ l') n d = getD l' (n - length l) d
ι : Type ?u.503527
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
x : α
xs : List α
d✝ : α
n✝ : ℕ
l l' : List α
d : α
n : ℕ
h : length l ≤ n
⊢ getD (l ++ l') n d = getD l' (n - length l) d
cases' lt_or_le n (l ++l').length with h' h'
case inl.hn
ι : Type ?u.503527
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
x : α
xs : List α
d✝ : α
n✝ : ℕ
l l' : List α
d : α
n : ℕ
h : length l ≤ n
h' : n < length (l ++ l')
⊢ n - length l < length l'

case inl.h
ι : Type ?u.503527
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
x : α
xs : List α
d✝ : α
n✝ : ℕ
l l' : List α
d : α
n : ℕ
h : length l ≤ n
h' : n < length (l ++ l')
⊢ ¬n < length l
case inl
ι : Type ?u.503527
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
x : α
xs : List α
d✝ : α
n✝ : ℕ
l l' : List α
d : α
n : ℕ
h : length l ≤ n
h' : n < length (l ++ l')
⊢ getD (l ++ l') n d = getD l' (n - length l) d
rw [getD_eq_get (l ++ l') d h', get_append_right, getD_eq_get]
case inl.hn
ι : Type ?u.503527
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
x : α
xs : List α
d✝ : α
n✝ : ℕ
l l' : List α
d : α
n : ℕ
h : length l ≤ n
h' : n < length l + length l'
⊢ n - length l < length l'
case inl.hn
ι : Type ?u.503527
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
x : α
xs : List α
d✝ : α
n✝ : ℕ
l l' : List α
d : α
n : ℕ
h : length l ≤ n
h' : n < length (l ++ l')
⊢ n - length l < length l'
rw [length_append] at h'
no goals
case inl.hn
ι : Type ?u.503527
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
x : α
xs : List α
d✝ : α
n✝ : ℕ
l l' : List α
d : α
n : ℕ
h : length l ≤ n
h' : n < length l + length l'
⊢ n - length l < length l'
exact Nat.sub_lt_left_of_lt_add h h'
no goals
case inl.h
ι : Type ?u.503527
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
x : α
xs : List α
d✝ : α
n✝ : ℕ
l l' : List α
d : α
n : ℕ
h : length l ≤ n
h' : n < length (l ++ l')
⊢ ¬n < length l
exact not_lt_of_le h
case inr.hn
ι : Type ?u.503527
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
x : α
xs : List α
d✝ : α
n✝ : ℕ
l l' : List α
d : α
n : ℕ
h : length l ≤ n
h' : length (l ++ l') ≤ n
⊢ length l' ≤ n - length l
case inr
ι : Type ?u.503527
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
x : α
xs : List α
d✝ : α
n✝ : ℕ
l l' : List α
d : α
n : ℕ
h : length l ≤ n
h' : length (l ++ l') ≤ n
⊢ getD (l ++ l') n d = getD l' (n - length l) d
rw [getD_eq_default _ _ h', getD_eq_default]
no goals
case inr.hn
ι : Type ?u.503527
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
x : α
xs : List α
d✝ : α
n✝ : ℕ
l l' : List α
d : α
n : ℕ
h : length l ≤ n
h' : length (l ++ l') ≤ n
⊢ length l' ≤ n - length l
rwa [le_tsub_iff_left h, ← length_append]