Theorem: List.getD_take (One.lean)

State before:
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
⊢ getD (take n l) i d = getD l i d
Tactic:
conv => right; rw [← List.take_append_drop n l]
State after:
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d

State before:
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d
Tactic:
cases h: decide (i < List.length l) with
| true =>
  simp only [decide_eq_true_eq] at h
  rw [List.getD_append]
  simp only [length_take, min_le_iff, ge_iff_le, lt_min_iff]
  exact ⟨P,h⟩
| false =>
  simp only [decide_eq_false_iff_not, not_lt] at h
  rw [List.getD_eq_default, List.getD_eq_default]
  . simp only [take_append_drop, ge_iff_le, h]
  . simp only [length_take, min_le_iff, ge_iff_le, h, or_true]
State after:
no goals

State before:
case true
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : decide (i < length l) = true
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d
Tactic:
simp only [decide_eq_true_eq] at h
State after:
case true
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : i < length l
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d

State before:
case true
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : i < length l
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d
Tactic:
rw [List.getD_append]
State after:
case true.h
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : i < length l
⊢ i < length (take n l)

State before:
case true.h
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : i < length l
⊢ i < length (take n l)
Tactic:
simp only [length_take, min_le_iff, ge_iff_le, lt_min_iff]
State after:
case true.h
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : i < length l
⊢ i < n ∧ i < length l

State before:
case true.h
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : i < length l
⊢ i < n ∧ i < length l
Tactic:
exact ⟨P,h⟩
State after:
no goals

State before:
case false
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : decide (i < length l) = false
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d
Tactic:
simp only [decide_eq_false_iff_not, not_lt] at h
State after:
case false
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d

State before:
case false
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d
Tactic:
rw [List.getD_eq_default, List.getD_eq_default]
State after:
case false.hn
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ length (take n l ++ drop n l) ≤ i

case false.hn
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ length (take n l) ≤ i

State before:
case false.hn
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ length (take n l ++ drop n l) ≤ i

case false.hn
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ length (take n l) ≤ i
Tactic:
. simp only [take_append_drop, ge_iff_le, h]
State after:
case false.hn
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ length (take n l) ≤ i

State before:
case false.hn
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ length (take n l) ≤ i
Tactic:
. simp only [length_take, min_le_iff, ge_iff_le, h, or_true]
State after:
no goals