no goals
α : Type u
β : Type v
γ : Type w
as : List α
i : Nat
a : α
⊢ length (set as i a) = length as
induction as generalizing i with
| nil => rfl
| cons x xs ih =>
  cases i with
  | zero => rfl
  | succ i => simp [set, ih]
no goals
case nil
α : Type u
β : Type v
γ : Type w
a : α
i : Nat
⊢ length (set nil i a) = length nil
rfl
no goals
case cons
α : Type u
β : Type v
γ : Type w
a x : α
xs : List α
ih : ∀ (i : Nat), length (set xs i a) = length xs
i : Nat
⊢ length (set (x :: xs) i a) = length (x :: xs)
cases i with
| zero => rfl
| succ i => simp [set, ih]
no goals
case cons.zero
α : Type u
β : Type v
γ : Type w
a x : α
xs : List α
ih : ∀ (i : Nat), length (set xs i a) = length xs
⊢ length (set (x :: xs) Nat.zero a) = length (x :: xs)
rfl
no goals
case cons.succ
α : Type u
β : Type v
γ : Type w
a x : α
xs : List α
ih : ∀ (i : Nat), length (set xs i a) = length xs
i : Nat
⊢ length (set (x :: xs) (Nat.succ i) a) = length (x :: xs)
simp [set, ih]