Theorem: List.length_uniform (MLIR/Util/List.lean)

State before:
α : Type u_1
v : α
n : ℕ
⊢ length (uniform v n) = n
Tactic:
induction n <;> simp [uniform]
State after:
case succ
α : Type u_1
v : α
n✝ : ℕ
n_ih✝ : length (uniform v n✝) = n✝
⊢ length (uniform v n✝) = n✝

State before:
case succ
α : Type u_1
v : α
n✝ : ℕ
n_ih✝ : length (uniform v n✝) = n✝
⊢ length (uniform v n✝) = n✝
Tactic:
assumption
State after:
no goals