Theorem: List.lastN_length (One.lean)

State before:
α : Type u_1
l : List α
i : ℕ
⊢ length (lastN i l) = min i (length l)
Tactic:
unfold lastN
State after:
α : Type u_1
l : List α
i : ℕ
⊢ length (drop (length l - i) l) = min i (length l)

State before:
α : Type u_1
l : List α
i : ℕ
⊢ length (drop (length l - i) l) = min i (length l)
Tactic:
simp only [ge_iff_le, length_drop]
State after:
α : Type u_1
l : List α
i : ℕ
⊢ length l - (length l - i) = min i (length l)

State before:
α : Type u_1
l : List α
i : ℕ
⊢ length l - (length l - i) = min i (length l)
Tactic:
cases h: decide (i ≤  length l) with
| true => 
  simp at h
  rw [Nat.sub_sub_self h, Nat.min_eq_left h]
| false =>
  simp at h
  have h₂: length l ≤ i := Nat.le_of_lt h
  simp [h₂]
State after:
no goals

State before:
case true
α : Type u_1
l : List α
i : ℕ
h : decide (i ≤ length l) = true
⊢ length l - (length l - i) = min i (length l)
Tactic:
simp at h
State after:
case true
α : Type u_1
l : List α
i : ℕ
h : i ≤ length l
⊢ length l - (length l - i) = min i (length l)

State before:
case true
α : Type u_1
l : List α
i : ℕ
h : i ≤ length l
⊢ length l - (length l - i) = min i (length l)
Tactic:
rw [Nat.sub_sub_self h, Nat.min_eq_left h]
State after:
no goals

State before:
case false
α : Type u_1
l : List α
i : ℕ
h : decide (i ≤ length l) = false
⊢ length l - (length l - i) = min i (length l)
Tactic:
simp at h
State after:
case false
α : Type u_1
l : List α
i : ℕ
h : length l < i
⊢ length l - (length l - i) = min i (length l)

State before:
case false
α : Type u_1
l : List α
i : ℕ
h : length l < i
⊢ length l - (length l - i) = min i (length l)
Tactic:
have h₂: length l ≤ i := Nat.le_of_lt h
State after:
case false
α : Type u_1
l : List α
i : ℕ
h : length l < i
h₂ : length l ≤ i
⊢ length l - (length l - i) = min i (length l)

State before:
case false
α : Type u_1
l : List α
i : ℕ
h : length l < i
h₂ : length l ≤ i
⊢ length l - (length l - i) = min i (length l)
Tactic:
simp [h₂]
State after:
no goals