Theorem: Vec.toList_length_eq_n (Qpf/Util/Vec.lean)

State before:
α : Type u_1
n : ℕ
v : Vec α n
⊢ List.length (toList v) = n
Tactic:
induction n
State after:
case zero
α : Type u_1
v : Vec α Nat.zero
⊢ List.length (toList v) = Nat.zero

case succ
α : Type u_1
n✝ : ℕ
n_ih✝ : ∀ {v : Vec α n✝}, List.length (toList v) = n✝
v : Vec α (Nat.succ n✝)
⊢ List.length (toList v) = Nat.succ n✝

State before:
α : Type u_1
v : Vec α Nat.zero
⊢ List.length (toList v) = Nat.zero
Tactic:
case zero => rfl
State after:
no goals

State before:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ List.length (toList v) = Nat.succ n
Tactic:
case succ n ih =>
  dsimp only [toList, List.length]
  dsimp only [HAdd.hAdd, Add.add, Nat.add]
  apply congrArg
  apply ih
State after:
no goals

State before:
α : Type u_1
v : Vec α Nat.zero
⊢ List.length (toList v) = Nat.zero
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ List.length (toList v) = Nat.succ n
Tactic:
dsimp only [toList, List.length]
State after:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ List.length (toList (drop v)) + 1 = Nat.succ n

State before:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ List.length (toList (drop v)) + 1 = Nat.succ n
Tactic:
dsimp only [HAdd.hAdd, Add.add, Nat.add]
State after:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ Nat.succ (List.length (toList (drop v))) = Nat.succ n

State before:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ Nat.succ (List.length (toList (drop v))) = Nat.succ n
Tactic:
apply congrArg
State after:
case h
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ List.length (toList (drop v)) = n

State before:
case h
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ List.length (toList (drop v)) = n
Tactic:
apply ih
State after:
no goals