Theorem: Array.getElem_mapIdx_safe (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
x : Array α
f : Fin (size x) → α → β
i : Nat
hi : i < size (mapIdx x f)
⊢ (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
Tactic:
induction x using cons_induction generalizing i with
| empty => cases hi
| cons a x IH =>
  simp only [mapIdx_cons]
  cases i with
  | zero => simp only [getElem_cons_zero]
  | succ i =>
    simp only [getElem_cons_succ]
    have : i < x.size :=
      Nat.lt_of_succ_lt_succ <| trans (s:=Eq) hi (size_mapIdx' ..)
    rw [IH (f ∘ Fin.succ) i ((x.size_mapIdx' (f ∘ Fin.succ)).symm ▸ this)]
    rfl
State after:
no goals

State before:
case empty
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : Fin (size #[]) → α → β
i : Nat
hi : i < size (mapIdx #[] f)
⊢ (mapIdx #[] f)[i] = f { val := i, isLt := (_ : i < size #[]) } #[][i]
Tactic:
cases hi
State after:
no goals

State before:
case cons
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : i < size (mapIdx (cons a x) f)
⊢ (mapIdx (cons a x) f)[i] = f { val := i, isLt := (_ : i < size (cons a x)) } (cons a x)[i]
Tactic:
simp only [mapIdx_cons]
State after:
case cons
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : i < size (mapIdx (cons a x) f)
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a) (mapIdx x (f ∘ Fin.succ)))[i] =
    f { val := i, isLt := (_ : i < size (cons a x)) } (cons a x)[i]

State before:
case cons
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : i < size (mapIdx (cons a x) f)
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a) (mapIdx x (f ∘ Fin.succ)))[i] =
    f { val := i, isLt := (_ : i < size (cons a x)) } (cons a x)[i]
Tactic:
cases i with
| zero => simp only [getElem_cons_zero]
| succ i =>
  simp only [getElem_cons_succ]
  have : i < x.size :=
    Nat.lt_of_succ_lt_succ <| trans (s:=Eq) hi (size_mapIdx' ..)
  rw [IH (f ∘ Fin.succ) i ((x.size_mapIdx' (f ∘ Fin.succ)).symm ▸ this)]
  rfl
State after:
no goals

State before:
case cons.zero
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
hi : Nat.zero < size (mapIdx (cons a x) f)
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a) (mapIdx x (f ∘ Fin.succ)))[Nat.zero] =
    f { val := Nat.zero, isLt := (_ : Nat.zero < size (cons a x)) } (cons a x)[Nat.zero]
Tactic:
simp only [getElem_cons_zero]
State after:
no goals

State before:
case cons.succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : Nat.succ i < size (mapIdx (cons a x) f)
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a) (mapIdx x (f ∘ Fin.succ)))[Nat.succ i] =
    f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } (cons a x)[Nat.succ i]
Tactic:
simp only [getElem_cons_succ]
State after:
case cons.succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : Nat.succ i < size (mapIdx (cons a x) f)
⊢ (mapIdx x (f ∘ Fin.succ))[i] = f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } x[i]

State before:
case cons.succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : Nat.succ i < size (mapIdx (cons a x) f)
⊢ (mapIdx x (f ∘ Fin.succ))[i] = f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } x[i]
Tactic:
have : i < x.size :=
  Nat.lt_of_succ_lt_succ <| trans (s:=Eq) hi (size_mapIdx' ..)
State after:
case cons.succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : Nat.succ i < size (mapIdx (cons a x) f)
this : i < size x
⊢ (mapIdx x (f ∘ Fin.succ))[i] = f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } x[i]

State before:
case cons.succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : Nat.succ i < size (mapIdx (cons a x) f)
this : i < size x
⊢ (mapIdx x (f ∘ Fin.succ))[i] = f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } x[i]
Tactic:
rw [IH (f ∘ Fin.succ) i ((x.size_mapIdx' (f ∘ Fin.succ)).symm ▸ this)]
State after:
case cons.succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : Nat.succ i < size (mapIdx (cons a x) f)
this : i < size x
⊢ (f ∘ Fin.succ) { val := i, isLt := (_ : i < size x) } x[i] =
    f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } x[i]

State before:
case cons.succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : Nat.succ i < size (mapIdx (cons a x) f)
this : i < size x
⊢ (f ∘ Fin.succ) { val := i, isLt := (_ : i < size x) } x[i] =
    f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } x[i]
Tactic:
rfl
State after:
no goals