Theorem: Smt.Reconstruct.Prop.length_take (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
n : Nat
α✝ : Type u_1
l : List α✝
h : n ≤ l.length
⊢ (take n l).length = n
Tactic:
revert n
State after:
α✝ : Type u_1
l : List α✝
⊢ ∀ {n : Nat}, n ≤ l.length → (take n l).length = n

State before:
α✝ : Type u_1
l : List α✝
⊢ ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
Tactic:
induction l with
| nil => intro n h; simp at h; simp [h]
| cons t l ih =>
  intro n h
  cases n with
  | zero => simp
  | succ n => simp [ih (by rw [length_cons, succ_le_succ_iff] at h; exact h)]
State after:
no goals

State before:
case nil
α✝ : Type u_1
⊢ ∀ {n : Nat}, n ≤ [].length → (take n []).length = n
Tactic:
intro n h
State after:
case nil
α✝ : Type u_1
n : Nat
h : n ≤ [].length
⊢ (take n []).length = n

State before:
case nil
α✝ : Type u_1
n : Nat
h : n ≤ [].length
⊢ (take n []).length = n
Tactic:
simp at h
State after:
case nil
α✝ : Type u_1
n : Nat
h : n = 0
⊢ (take n []).length = n

State before:
case nil
α✝ : Type u_1
n : Nat
h : n = 0
⊢ (take n []).length = n
Tactic:
simp [h]
State after:
no goals

State before:
case cons
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
⊢ ∀ {n : Nat}, n ≤ (t :: l).length → (take n (t :: l)).length = n
Tactic:
intro n h
State after:
case cons
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
n : Nat
h : n ≤ (t :: l).length
⊢ (take n (t :: l)).length = n

State before:
case cons
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
n : Nat
h : n ≤ (t :: l).length
⊢ (take n (t :: l)).length = n
Tactic:
cases n with
| zero => simp
| succ n => simp [ih (by rw [length_cons, succ_le_succ_iff] at h; exact h)]
State after:
no goals

State before:
case cons.zero
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
h : 0 ≤ (t :: l).length
⊢ (take 0 (t :: l)).length = 0
Tactic:
simp
State after:
no goals

State before:
case cons.succ
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
n : Nat
h : n + 1 ≤ (t :: l).length
⊢ (take (n + 1) (t :: l)).length = n + 1
Tactic:
simp [ih (by rw [length_cons, succ_le_succ_iff] at h; exact h)]
State after:
no goals

State before:
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
n : Nat
h : n + 1 ≤ (t :: l).length
⊢ ?m.37095 ≤ l.length
Tactic:
rw [length_cons, succ_le_succ_iff] at h
State after:
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
n : Nat
h✝ : n + 1 ≤ (t :: l).length
h : n ≤ l.length
⊢ ?m.37095 ≤ l.length

State before:
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
n : Nat
h✝ : n + 1 ≤ (t :: l).length
h : n ≤ l.length
⊢ ?m.37095 ≤ l.length
Tactic:
exact h
State after:
no goals