Theorem: SizedArray.get_mapIdx (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
f : Fin n → α → β
x : SizedArray α n
i : Nat
hi : i < n
⊢ (mapIdx f x)[i] = f { val := i, isLt := hi } 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 [Nat.zero_eq, get_cons_zero]
  | succ i =>
    simp only [Nat.zero_eq, Nat.succ_eq_add_one]
    rw [get_cons_succ (hi₂:=Nat.lt_of_succ_lt_succ hi)]
    rw [get_cons_succ (hi₂:=Nat.lt_of_succ_lt_succ hi)]
    exact IH ..
State after:
no goals

State before:
case empty
α : Type u
β : Type v
γ : Type w
n : Nat
f : Fin 0 → α → β
i : Nat
hi : i < 0
⊢ (mapIdx f empty)[i] = f { val := i, isLt := hi } empty[i]
Tactic:
cases hi
State after:
no goals

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

State before:
case cons
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : i < n✝ + 1
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ n✝) } a) (mapIdx (f ∘ Fin.succ) x))[i] =
    f { val := i, isLt := hi } (cons a x)[i]
Tactic:
cases i with
| zero => simp only [Nat.zero_eq, get_cons_zero]
| succ i =>
  simp only [Nat.zero_eq, Nat.succ_eq_add_one]
  rw [get_cons_succ (hi₂:=Nat.lt_of_succ_lt_succ hi)]
  rw [get_cons_succ (hi₂:=Nat.lt_of_succ_lt_succ hi)]
  exact IH ..
State after:
no goals

State before:
case cons.zero
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
hi : Nat.zero < n✝ + 1
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ n✝) } a) (mapIdx (f ∘ Fin.succ) x))[Nat.zero] =
    f { val := Nat.zero, isLt := hi } (cons a x)[Nat.zero]
Tactic:
simp only [Nat.zero_eq, get_cons_zero]
State after:
no goals

State before:
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ n✝) } a) (mapIdx (f ∘ Fin.succ) x))[Nat.succ i] =
    f { val := Nat.succ i, isLt := hi } (cons a x)[Nat.succ i]
Tactic:
simp only [Nat.zero_eq, Nat.succ_eq_add_one]
State after:
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ n✝) } a) (mapIdx (f ∘ Fin.succ) x))[i + 1] =
    f { val := i + 1, isLt := hi } (cons a x)[i + 1]

State before:
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ n✝) } a) (mapIdx (f ∘ Fin.succ) x))[i + 1] =
    f { val := i + 1, isLt := hi } (cons a x)[i + 1]
Tactic:
rw [get_cons_succ (hi₂:=Nat.lt_of_succ_lt_succ hi)]
State after:
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (mapIdx (f ∘ Fin.succ) x)[i] = f { val := i + 1, isLt := hi } (cons a x)[i + 1]

State before:
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (mapIdx (f ∘ Fin.succ) x)[i] = f { val := i + 1, isLt := hi } (cons a x)[i + 1]
Tactic:
rw [get_cons_succ (hi₂:=Nat.lt_of_succ_lt_succ hi)]
State after:
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (mapIdx (f ∘ Fin.succ) x)[i] = f { val := i + 1, isLt := hi } x[i]

State before:
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (mapIdx (f ∘ Fin.succ) x)[i] = f { val := i + 1, isLt := hi } x[i]
Tactic:
exact IH ..
State after:
no goals