Theorem: List.dropLast_take' (One.lean)

State before:
n : ℕ
α✝ : Type u_1
l : List α✝
⊢ dropLast (take n l) = take (min n (length l) - 1) l
Tactic:
cases h: decide (n < length l) with
| true => 
  simp only [decide_eq_true_eq] at h
  simp only [List.dropLast_take h, Nat.pred_eq_sub_one, tsub_le_iff_right, ge_iff_le, min_eq_left (le_of_lt h)]
| false =>
  simp only [decide_eq_false_iff_not, not_lt] at h
  rw [List.take_length_le h]
  simp only [dropLast_eq_take, Nat.pred_eq_sub_one, tsub_le_iff_right, ge_iff_le, min_le_iff, h, min_eq_right]
State after:
no goals

State before:
case true
n : ℕ
α✝ : Type u_1
l : List α✝
h : decide (n < length l) = true
⊢ dropLast (take n l) = take (min n (length l) - 1) l
Tactic:
simp only [decide_eq_true_eq] at h
State after:
case true
n : ℕ
α✝ : Type u_1
l : List α✝
h : n < length l
⊢ dropLast (take n l) = take (min n (length l) - 1) l

State before:
case true
n : ℕ
α✝ : Type u_1
l : List α✝
h : n < length l
⊢ dropLast (take n l) = take (min n (length l) - 1) l
Tactic:
simp only [List.dropLast_take h, Nat.pred_eq_sub_one, tsub_le_iff_right, ge_iff_le, min_eq_left (le_of_lt h)]
State after:
no goals

State before:
case false
n : ℕ
α✝ : Type u_1
l : List α✝
h : decide (n < length l) = false
⊢ dropLast (take n l) = take (min n (length l) - 1) l
Tactic:
simp only [decide_eq_false_iff_not, not_lt] at h
State after:
case false
n : ℕ
α✝ : Type u_1
l : List α✝
h : length l ≤ n
⊢ dropLast (take n l) = take (min n (length l) - 1) l

State before:
case false
n : ℕ
α✝ : Type u_1
l : List α✝
h : length l ≤ n
⊢ dropLast (take n l) = take (min n (length l) - 1) l
Tactic:
rw [List.take_length_le h]
State after:
case false
n : ℕ
α✝ : Type u_1
l : List α✝
h : length l ≤ n
⊢ dropLast l = take (min n (length l) - 1) l

State before:
case false
n : ℕ
α✝ : Type u_1
l : List α✝
h : length l ≤ n
⊢ dropLast l = take (min n (length l) - 1) l
Tactic:
simp only [dropLast_eq_take, Nat.pred_eq_sub_one, tsub_le_iff_right, ge_iff_le, min_le_iff, h, min_eq_right]
State after:
no goals