Theorem: list_take_length (Katydid/Std/Lists.lean)

State before:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) = min n (length xs)
Tactic:
unfold min
State after:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) = instMinNat.1 n (length xs)

State before:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) = instMinNat.1 n (length xs)
Tactic:
unfold instMinNat
State after:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) = minOfLe.1 n (length xs)

State before:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) = minOfLe.1 n (length xs)
Tactic:
unfold minOfLe
State after:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) = { min := fun x y => if x ≤ y then x else y }.1 n (length xs)

State before:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) = { min := fun x y => if x ≤ y then x else y }.1 n (length xs)
Tactic:
simp only [length_take, ge_iff_le]
State after:
α : Type u_1
n : ℕ
xs : List α
⊢ min n (length xs) = if n ≤ length xs then n else length xs

State before:
α : Type u_1
n : ℕ
xs : List α
⊢ min n (length xs) = if n ≤ length xs then n else length xs
Tactic:
split
State after:
case inl
α : Type u_1
n : ℕ
xs : List α
h✝ : n ≤ length xs
⊢ min n (length xs) = n

case inr
α : Type u_1
n : ℕ
xs : List α
h✝ : ¬n ≤ length xs
⊢ min n (length xs) = length xs

State before:
α : Type u_1
n : ℕ
xs : List α
h✝ : n ≤ length xs
⊢ min n (length xs) = n
Tactic:
case inl =>
  rename_i c
  unfold min; unfold instMinNat; unfold minOfLe; simp only [ite_eq_left_iff, not_le]
  intro c'
  linarith
State after:
no goals

State before:
α : Type u_1
n : ℕ
xs : List α
h✝ : ¬n ≤ length xs
⊢ min n (length xs) = length xs
Tactic:
case inr =>
  rename_i c
  have c' := gt_of_not_le c
  unfold min; unfold instMinNat; unfold minOfLe; simp only [ite_eq_right_iff]
  intro c''
  linarith
State after:
no goals

State before:
α : Type u_1
n : ℕ
xs : List α
h✝ : n ≤ length xs
⊢ min n (length xs) = n
Tactic:
rename_i c
State after:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ min n (length xs) = n

State before:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ min n (length xs) = n
Tactic:
unfold min
State after:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ instMinNat.1 n (length xs) = n

State before:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ instMinNat.1 n (length xs) = n
Tactic:
unfold instMinNat
State after:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ minOfLe.1 n (length xs) = n

State before:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ minOfLe.1 n (length xs) = n
Tactic:
unfold minOfLe
State after:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ { min := fun x y => if x ≤ y then x else y }.1 n (length xs) = n

State before:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ { min := fun x y => if x ≤ y then x else y }.1 n (length xs) = n
Tactic:
simp only [ite_eq_left_iff, not_le]
State after:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ length xs < n → length xs = n

State before:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ length xs < n → length xs = n
Tactic:
intro c'
State after:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
c' : length xs < n
⊢ length xs = n

State before:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
c' : length xs < n
⊢ length xs = n
Tactic:
linarith
State after:
no goals

State before:
α : Type u_1
n : ℕ
xs : List α
h✝ : ¬n ≤ length xs
⊢ min n (length xs) = length xs
Tactic:
rename_i c
State after:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
⊢ min n (length xs) = length xs

State before:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
⊢ min n (length xs) = length xs
Tactic:
have c' := gt_of_not_le c
State after:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ min n (length xs) = length xs

State before:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ min n (length xs) = length xs
Tactic:
unfold min
State after:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ instMinNat.1 n (length xs) = length xs

State before:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ instMinNat.1 n (length xs) = length xs
Tactic:
unfold instMinNat
State after:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ minOfLe.1 n (length xs) = length xs

State before:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ minOfLe.1 n (length xs) = length xs
Tactic:
unfold minOfLe
State after:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ { min := fun x y => if x ≤ y then x else y }.1 n (length xs) = length xs

State before:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ { min := fun x y => if x ≤ y then x else y }.1 n (length xs) = length xs
Tactic:
simp only [ite_eq_right_iff]
State after:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ n ≤ length xs → n = length xs

State before:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ n ≤ length xs → n = length xs
Tactic:
intro c''
State after:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
c'' : n ≤ length xs
⊢ n = length xs

State before:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
c'' : n ≤ length xs
⊢ n = length xs
Tactic:
linarith
State after:
no goals