Theorem: Subarray.castIndex_lt_stop (Algdata/Data/Array/Subarray.lean)

State before:
α : Type u
x : Subarray α
i : Fin (size x)
⊢ ↑(castIndex x i) < x.stop
Tactic:
show x.start + i.1 < x.stop
State after:
α : Type u
x : Subarray α
i : Fin (size x)
⊢ x.start + ↑i < x.stop

State before:
α : Type u
x : Subarray α
i : Fin (size x)
⊢ x.start + ↑i < x.stop
Tactic:
suffices x.stop = x.start + x.size by
  rewrite [this]; exact Nat.add_lt_add_left i.2 x.start
State after:
α : Type u
x : Subarray α
i : Fin (size x)
⊢ x.stop = x.start + size x

State before:
α : Type u
x : Subarray α
i : Fin (size x)
⊢ x.stop = x.start + size x
Tactic:
exact (Nat.add_sub_cancel' x.h₁).symm
State after:
no goals

State before:
α : Type u
x : Subarray α
i : Fin (size x)
this : x.stop = x.start + size x
⊢ x.start + ↑i < x.stop
Tactic:
rewrite [this]
State after:
α : Type u
x : Subarray α
i : Fin (size x)
this : x.stop = x.start + size x
⊢ x.start + ↑i < x.start + size x

State before:
α : Type u
x : Subarray α
i : Fin (size x)
this : x.stop = x.start + size x
⊢ x.start + ↑i < x.start + size x
Tactic:
exact Nat.add_lt_add_left i.2 x.start
State after:
no goals