Theorem: Array.getElem_shrink (Fifteen/Data/Array/Basic.lean)

State before:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
i : Nat
hi : i < size (shrink as n)
⊢ (shrink as n)[i] = as[i]
Tactic:
dsimp [shrink] at hi ⊢
State after:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
i : Nat
hi : i < size (shrink.loop (size as - n) as)
⊢ (shrink.loop (size as - n) as)[i] = as[i]

State before:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
i : Nat
hi : i < size (shrink.loop (size as - n) as)
⊢ (shrink.loop (size as - n) as)[i] = as[i]
Tactic:
revert i
State after:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ ∀ (i : Nat) (hi : i < size (shrink.loop (size as - n) as)), (shrink.loop (size as - n) as)[i] = as[i]

State before:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ ∀ (i : Nat) (hi : i < size (shrink.loop (size as - n) as)), (shrink.loop (size as - n) as)[i] = as[i]
Tactic:
suffices ∀ (i k : Nat) (hk : k ≤ as.size) (hi : i < as.size - k), (shrink.loop k as)[i]'(as.size_shrink_loop hk ▸ hi) = as[i]'(trans (r:=LT.lt (α:=Nat)) hi (as.size.sub_le_self k))
from fun i hi =>
  this i (as.size - n) (as.size.sub_le_self n) (by rw [Nat.sub_sub_self h]; exact trans (r:=LT.lt (α:=Nat)) (s:=Eq) hi (as.size_shrink h))
State after:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ ∀ (i k : Nat) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]

State before:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ ∀ (i k : Nat) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
Tactic:
clear h n
State after:
α : Type u
as : Array α
⊢ ∀ (i k : Nat) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]

State before:
α : Type u
as : Array α
⊢ ∀ (i k : Nat) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
Tactic:
intro i k hk hi
State after:
α : Type u
as : Array α
i k : Nat
hk : k ≤ size as
hi : i < size as - k
⊢ (shrink.loop k as)[i] = as[i]

State before:
α : Type u
as : Array α
i k : Nat
hk : k ≤ size as
hi : i < size as - k
⊢ (shrink.loop k as)[i] = as[i]
Tactic:
induction k generalizing as with
| zero => rfl
| succ k IH =>
  dsimp [shrink.loop]
  specialize IH as.pop (as.size_pop ▸ Nat.le_sub_of_add_le hk) (by rewrite [as.size_pop, Nat.sub_sub, Nat.add_comm]; exact hi)
  rewrite [IH]
  exact as.getElem_pop i _
State after:
no goals

State before:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
this : ∀ (i k : Nat) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
i : Nat
hi : i < size (shrink.loop (size as - n) as)
⊢ i < size as - (size as - n)
Tactic:
rw [Nat.sub_sub_self h]
State after:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
this : ∀ (i k : Nat) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
i : Nat
hi : i < size (shrink.loop (size as - n) as)
⊢ i < n

State before:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
this : ∀ (i k : Nat) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
i : Nat
hi : i < size (shrink.loop (size as - n) as)
⊢ i < n
Tactic:
exact trans (r:=LT.lt (α:=Nat)) (s:=Eq) hi (as.size_shrink h)
State after:
no goals

State before:
case zero
α : Type u
i : Nat
as : Array α
hk : Nat.zero ≤ size as
hi : i < size as - Nat.zero
⊢ (shrink.loop Nat.zero as)[i] = as[i]
Tactic:
rfl
State after:
no goals

State before:
case succ
α : Type u
i k : Nat
IH : ∀ (as : Array α) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
⊢ (shrink.loop (Nat.succ k) as)[i] = as[i]
Tactic:
dsimp [shrink.loop]
State after:
case succ
α : Type u
i k : Nat
IH : ∀ (as : Array α) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
⊢ (shrink.loop k (pop as))[i] = as[i]

State before:
case succ
α : Type u
i k : Nat
IH : ∀ (as : Array α) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
⊢ (shrink.loop k (pop as))[i] = as[i]
Tactic:
specialize IH as.pop (as.size_pop ▸ Nat.le_sub_of_add_le hk) (by rewrite [as.size_pop, Nat.sub_sub, Nat.add_comm]; exact hi)
State after:
case succ
α : Type u
i k : Nat
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
IH : (shrink.loop k (pop as))[i] = (pop as)[i]
⊢ (shrink.loop k (pop as))[i] = as[i]

State before:
case succ
α : Type u
i k : Nat
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
IH : (shrink.loop k (pop as))[i] = (pop as)[i]
⊢ (shrink.loop k (pop as))[i] = as[i]
Tactic:
rewrite [IH]
State after:
case succ
α : Type u
i k : Nat
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
IH : (shrink.loop k (pop as))[i] = (pop as)[i]
⊢ (pop as)[i] = as[i]

State before:
case succ
α : Type u
i k : Nat
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
IH : (shrink.loop k (pop as))[i] = (pop as)[i]
⊢ (pop as)[i] = as[i]
Tactic:
exact as.getElem_pop i _
State after:
no goals

State before:
α : Type u
i k : Nat
IH : ∀ (as : Array α) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
⊢ i < size (pop as) - k
Tactic:
rewrite [as.size_pop, Nat.sub_sub, Nat.add_comm]
State after:
α : Type u
i k : Nat
IH : ∀ (as : Array α) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
⊢ i < size as - (k + 1)

State before:
α : Type u
i k : Nat
IH : ∀ (as : Array α) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
⊢ i < size as - (k + 1)
Tactic:
exact hi
State after:
no goals