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

State before:
α : Type u_1
m n✝ n : ℕ
xs : List α
⊢ take n (take m xs) = take (min n m) xs
Tactic:
revert m xs
State after:
α : Type u_1
n✝ n : ℕ
⊢ ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs

State before:
α : Type u_1
n✝ n : ℕ
⊢ ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
Tactic:
induction n with
| zero =>
  intro m xs
  rw [nat_min_zero]
  repeat rw [take]
| succ n ihn =>
  intro m xs
  cases m with
  | zero =>
    unfold min
    unfold instMinNat
    unfold minOfLe
    rw [take]
    simp only [take]
  | succ m =>
    unfold min
    unfold instMinNat
    unfold minOfLe
    simp only
    split
    case succ.succ.inl h =>
      rw [nat_succ_le_succ_iff] at h
      cases xs with
      | nil =>
        rw [take]
      | cons x xs =>
        repeat rw [take]
        apply (congrArg (cons x))
        have hmin : min n m = n := by
          unfold min
          unfold instMinNat
          unfold minOfLe
          simp only [ite_eq_left_iff, not_le]
          intro hless
          linarith
        have ihn' : _ := @ihn m xs
        rw [hmin] at ihn'
        exact ihn'
    case succ.succ.inr h =>
      rw [nat_succ_le_succ_iff] at h
      cases xs with
      | nil =>
        rw [take]
        apply list_take_nil
      | cons x xs =>
        repeat rw [take]
        apply (congrArg (cons x))
        have hmin : min n m = m := by
          unfold min
          unfold instMinNat
          unfold minOfLe
          simp only [ite_eq_right_iff]
          intro hless
          linarith
        have ihn' : _ := @ihn m xs
        rw [hmin] at ihn'
        exact ihn'
State after:
no goals

State before:
case zero
α : Type u_1
n : ℕ
⊢ ∀ {m : ℕ} (xs : List α), take zero (take m xs) = take (min zero m) xs
Tactic:
intro m xs
State after:
case zero
α : Type u_1
n m : ℕ
xs : List α
⊢ take zero (take m xs) = take (min zero m) xs

State before:
case zero
α : Type u_1
n m : ℕ
xs : List α
⊢ take zero (take m xs) = take (min zero m) xs
Tactic:
rw [nat_min_zero]
State after:
case zero
α : Type u_1
n m : ℕ
xs : List α
⊢ take zero (take m xs) = take 0 xs

State before:
case zero
α : Type u_1
n m : ℕ
xs : List α
⊢ take zero (take m xs) = take 0 xs
Tactic:
repeat rw [take]
State after:
no goals

State before:
case zero
α : Type u_1
n m : ℕ
xs : List α
⊢ [] = take 0 xs
Tactic:
rw [take]
State after:
no goals

State before:
case succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
⊢ ∀ {m : ℕ} (xs : List α), take (succ n) (take m xs) = take (min (succ n) m) xs
Tactic:
intro m xs
State after:
case succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
xs : List α
⊢ take (succ n) (take m xs) = take (min (succ n) m) xs

State before:
case succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
xs : List α
⊢ take (succ n) (take m xs) = take (min (succ n) m) xs
Tactic:
cases m with
| zero =>
  unfold min
  unfold instMinNat
  unfold minOfLe
  rw [take]
  simp only [take]
| succ m =>
  unfold min
  unfold instMinNat
  unfold minOfLe
  simp only
  split
  case succ.succ.inl h =>
    rw [nat_succ_le_succ_iff] at h
    cases xs with
    | nil =>
      rw [take]
    | cons x xs =>
      repeat rw [take]
      apply (congrArg (cons x))
      have hmin : min n m = n := by
        unfold min
        unfold instMinNat
        unfold minOfLe
        simp only [ite_eq_left_iff, not_le]
        intro hless
        linarith
      have ihn' : _ := @ihn m xs
      rw [hmin] at ihn'
      exact ihn'
  case succ.succ.inr h =>
    rw [nat_succ_le_succ_iff] at h
    cases xs with
    | nil =>
      rw [take]
      apply list_take_nil
    | cons x xs =>
      repeat rw [take]
      apply (congrArg (cons x))
      have hmin : min n m = m := by
        unfold min
        unfold instMinNat
        unfold minOfLe
        simp only [ite_eq_right_iff]
        intro hless
        linarith
      have ihn' : _ := @ihn m xs
      rw [hmin] at ihn'
      exact ihn'
State after:
no goals

State before:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) (take zero xs) = take (min (succ n) zero) xs
Tactic:
unfold min
State after:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) (take zero xs) = take (instMinNat.1 (succ n) zero) xs

State before:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) (take zero xs) = take (instMinNat.1 (succ n) zero) xs
Tactic:
unfold instMinNat
State after:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) (take zero xs) = take (minOfLe.1 (succ n) zero) xs

State before:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) (take zero xs) = take (minOfLe.1 (succ n) zero) xs
Tactic:
unfold minOfLe
State after:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) (take zero xs) = take ({ min := fun x y => if x ≤ y then x else y }.1 (succ n) zero) xs

State before:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) (take zero xs) = take ({ min := fun x y => if x ≤ y then x else y }.1 (succ n) zero) xs
Tactic:
rw [take]
State after:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) [] = take ({ min := fun x y => if x ≤ y then x else y }.1 (succ n) zero) xs

State before:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) [] = take ({ min := fun x y => if x ≤ y then x else y }.1 (succ n) zero) xs
Tactic:
simp only [take]
State after:
no goals

State before:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take (min (succ n) (succ m)) xs
Tactic:
unfold min
State after:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take (instMinNat.1 (succ n) (succ m)) xs

State before:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take (instMinNat.1 (succ n) (succ m)) xs
Tactic:
unfold instMinNat
State after:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take (minOfLe.1 (succ n) (succ m)) xs

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

State before:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take ({ min := fun x y => if x ≤ y then x else y }.1 (succ n) (succ m)) xs
Tactic:
simp only
State after:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take (if succ n ≤ succ m then succ n else succ m) xs

State before:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take (if succ n ≤ succ m then succ n else succ m) xs
Tactic:
split
State after:
case succ.succ.inl
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
h✝ : succ n ≤ succ m
⊢ take (succ n) (take (succ m) xs) = take (succ n) xs

case succ.succ.inr
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
h✝ : ¬succ n ≤ succ m
⊢ take (succ n) (take (succ m) xs) = take (succ m) xs

State before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
h : succ n ≤ succ m
⊢ take (succ n) (take (succ m) xs) = take (succ n) xs
Tactic:
case succ.succ.inl h =>
  rw [nat_succ_le_succ_iff] at h
  cases xs with
  | nil =>
    rw [take]
  | cons x xs =>
    repeat rw [take]
    apply (congrArg (cons x))
    have hmin : min n m = n := by
      unfold min
      unfold instMinNat
      unfold minOfLe
      simp only [ite_eq_left_iff, not_le]
      intro hless
      linarith
    have ihn' : _ := @ihn m xs
    rw [hmin] at ihn'
    exact ihn'
State after:
no goals

State before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
h : ¬succ n ≤ succ m
⊢ take (succ n) (take (succ m) xs) = take (succ m) xs
Tactic:
case succ.succ.inr h =>
  rw [nat_succ_le_succ_iff] at h
  cases xs with
  | nil =>
    rw [take]
    apply list_take_nil
  | cons x xs =>
    repeat rw [take]
    apply (congrArg (cons x))
    have hmin : min n m = m := by
      unfold min
      unfold instMinNat
      unfold minOfLe
      simp only [ite_eq_right_iff]
      intro hless
      linarith
    have ihn' : _ := @ihn m xs
    rw [hmin] at ihn'
    exact ihn'
State after:
no goals

State before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
h : succ n ≤ succ m
⊢ take (succ n) (take (succ m) xs) = take (succ n) xs
Tactic:
rw [nat_succ_le_succ_iff] at h
State after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
h : n ≤ m
⊢ take (succ n) (take (succ m) xs) = take (succ n) xs

State before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
h : n ≤ m
⊢ take (succ n) (take (succ m) xs) = take (succ n) xs
Tactic:
cases xs with
| nil =>
  rw [take]
| cons x xs =>
  repeat rw [take]
  apply (congrArg (cons x))
  have hmin : min n m = n := by
    unfold min
    unfold instMinNat
    unfold minOfLe
    simp only [ite_eq_left_iff, not_le]
    intro hless
    linarith
  have ihn' : _ := @ihn m xs
  rw [hmin] at ihn'
  exact ihn'
State after:
no goals

State before:
case nil
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
⊢ take (succ n) (take (succ m) []) = take (succ n) []
Tactic:
rw [take]
State after:
no goals

State before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
⊢ take (succ n) (take (succ m) (x :: xs)) = take (succ n) (x :: xs)
Tactic:
repeat rw [take]
State after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
⊢ x :: take n (take m xs) = x :: take n xs

State before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
⊢ x :: take n (take m xs) = x :: take n xs
Tactic:
apply (congrArg (cons x))
State after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
⊢ take n (take m xs) = take n xs

State before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
⊢ take n (take m xs) = take n xs
Tactic:
have hmin : min n m = n := by
  unfold min
  unfold instMinNat
  unfold minOfLe
  simp only [ite_eq_left_iff, not_le]
  intro hless
  linarith
State after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
hmin : min n m = n
⊢ take n (take m xs) = take n xs

State before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
hmin : min n m = n
⊢ take n (take m xs) = take n xs
Tactic:
have ihn' : _ := @ihn m xs
State after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
hmin : min n m = n
ihn' : take n (take m xs) = take (min n m) xs
⊢ take n (take m xs) = take n xs

State before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
hmin : min n m = n
ihn' : take n (take m xs) = take (min n m) xs
⊢ take n (take m xs) = take n xs
Tactic:
rw [hmin] at ihn'
State after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
hmin : min n m = n
ihn' : take n (take m xs) = take n xs
⊢ take n (take m xs) = take n xs

State before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
hmin : min n m = n
ihn' : take n (take m xs) = take n xs
⊢ take n (take m xs) = take n xs
Tactic:
exact ihn'
State after:
no goals

State before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
⊢ x :: take n (take m xs) = take (succ n) (x :: xs)
Tactic:
rw [take]
State after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
⊢ x :: take n (take m xs) = x :: take n xs

State before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
⊢ min n m = n
Tactic:
unfold min
State after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
⊢ instMinNat.1 n m = n

State before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
⊢ instMinNat.1 n m = n
Tactic:
unfold instMinNat
State after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
⊢ minOfLe.1 n m = n

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

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

State before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
⊢ m < n → m = n
Tactic:
intro hless
State after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
hless : m < n
⊢ m = n

State before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
hless : m < n
⊢ m = n
Tactic:
linarith
State after:
no goals

State before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
h : ¬succ n ≤ succ m
⊢ take (succ n) (take (succ m) xs) = take (succ m) xs
Tactic:
rw [nat_succ_le_succ_iff] at h
State after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
h : ¬n ≤ m
⊢ take (succ n) (take (succ m) xs) = take (succ m) xs

State before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
h : ¬n ≤ m
⊢ take (succ n) (take (succ m) xs) = take (succ m) xs
Tactic:
cases xs with
| nil =>
  rw [take]
  apply list_take_nil
| cons x xs =>
  repeat rw [take]
  apply (congrArg (cons x))
  have hmin : min n m = m := by
    unfold min
    unfold instMinNat
    unfold minOfLe
    simp only [ite_eq_right_iff]
    intro hless
    linarith
  have ihn' : _ := @ihn m xs
  rw [hmin] at ihn'
  exact ihn'
State after:
no goals

State before:
case nil
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
⊢ take (succ n) (take (succ m) []) = take (succ m) []
Tactic:
rw [take]
State after:
case nil
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
⊢ take (succ n) [] = []

State before:
case nil
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
⊢ take (succ n) [] = []
Tactic:
apply list_take_nil
State after:
no goals

State before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ take (succ n) (take (succ m) (x :: xs)) = take (succ m) (x :: xs)
Tactic:
repeat rw [take]
State after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ x :: take n (take m xs) = x :: take m xs

State before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ x :: take n (take m xs) = x :: take m xs
Tactic:
apply (congrArg (cons x))
State after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ take n (take m xs) = take m xs

State before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ take n (take m xs) = take m xs
Tactic:
have hmin : min n m = m := by
  unfold min
  unfold instMinNat
  unfold minOfLe
  simp only [ite_eq_right_iff]
  intro hless
  linarith
State after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hmin : min n m = m
⊢ take n (take m xs) = take m xs

State before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hmin : min n m = m
⊢ take n (take m xs) = take m xs
Tactic:
have ihn' : _ := @ihn m xs
State after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hmin : min n m = m
ihn' : take n (take m xs) = take (min n m) xs
⊢ take n (take m xs) = take m xs

State before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hmin : min n m = m
ihn' : take n (take m xs) = take (min n m) xs
⊢ take n (take m xs) = take m xs
Tactic:
rw [hmin] at ihn'
State after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hmin : min n m = m
ihn' : take n (take m xs) = take m xs
⊢ take n (take m xs) = take m xs

State before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hmin : min n m = m
ihn' : take n (take m xs) = take m xs
⊢ take n (take m xs) = take m xs
Tactic:
exact ihn'
State after:
no goals

State before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ take (succ n) (x :: take m xs) = x :: take m xs
Tactic:
rw [take]
State after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ x :: take n (take m xs) = x :: take m xs

State before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ min n m = m
Tactic:
unfold min
State after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ instMinNat.1 n m = m

State before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ instMinNat.1 n m = m
Tactic:
unfold instMinNat
State after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ minOfLe.1 n m = m

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

State before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ { min := fun x y => if x ≤ y then x else y }.1 n m = m
Tactic:
simp only [ite_eq_right_iff]
State after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ n ≤ m → n = m

State before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ n ≤ m → n = m
Tactic:
intro hless
State after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hless : n ≤ m
⊢ n = m

State before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hless : n ≤ m
⊢ n = m
Tactic:
linarith
State after:
no goals