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

State before:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size (shrink as n) = n
Tactic:
refine Eq.trans (size_shrink_loop as ?_) ?_
State after:
case refine_1
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - n ≤ size as

case refine_2
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - (size as - n) = n

State before:
case refine_1
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - n ≤ size as

case refine_2
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - (size as - n) = n
Tactic:
. exact as.size.sub_le_self n
State after:
case refine_2
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - (size as - n) = n

State before:
case refine_2
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - (size as - n) = n
Tactic:
. exact Nat.sub_sub_self h
State after:
no goals

State before:
case refine_1
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - n ≤ size as
Tactic:
exact as.size.sub_le_self n
State after:
no goals

State before:
case refine_2
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - (size as - n) = n
Tactic:
exact Nat.sub_sub_self h
State after:
no goals