α : Type u_1
a : Array α
⊢ size
      (if h : size a ≤ 1 then a
      else reverse.loop a 0 { val := size a - 1, isLt := (_ : Nat.pred (Nat.sub (size a) 0) < Nat.sub (size a) 0) }) =
    size a
α : Type u_1
a : Array α
⊢ size (reverse a) = size a
simp only [reverse]
no goals
α : Type u_1
a : Array α
⊢ size
      (if h : size a ≤ 1 then a
      else reverse.loop a 0 { val := size a - 1, isLt := (_ : Nat.pred (Nat.sub (size a) 0) < Nat.sub (size a) 0) }) =
    size a
split <;> simp [go]
α : Type u_1
a as : Array α
i : Nat
j : Fin (size as)
⊢ size
      (if h : i < j.val then
        let_fun this := (_ : j.val - 1 - (i + 1) < j.val - i);
        let as_1 := swap as { val := i, isLt := (_ : i < size as) } j;
        let_fun this := (_ : j.val - 1 < size as_1);
        reverse.loop as_1 (i + 1) { val := j.val - 1, isLt := this }
      else as) =
    size as
α : Type u_1
a as : Array α
i : Nat
j : Fin (size as)
⊢ size (reverse.loop as i j) = size as
rw [reverse.loop]
α : Type u_1
a as : Array α
i : Nat
j : Fin (size as)
h : i < j.val
this : j.val - 1 - (i + 1) < j.val - i
⊢ size
      (if h : i < j.val then
        let_fun this := (_ : j.val - 1 - (i + 1) < j.val - i);
        let as_1 := swap as { val := i, isLt := (_ : i < size as) } j;
        let_fun this := (_ : j.val - 1 < size as_1);
        reverse.loop as_1 (i + 1) { val := j.val - 1, isLt := this }
      else as) =
    size as
α : Type u_1
a as : Array α
i : Nat
j : Fin (size as)
h : i < j.val
⊢ size
      (if h : i < j.val then
        let_fun this := (_ : j.val - 1 - (i + 1) < j.val - i);
        let as_1 := swap as { val := i, isLt := (_ : i < size as) } j;
        let_fun this := (_ : j.val - 1 < size as_1);
        reverse.loop as_1 (i + 1) { val := j.val - 1, isLt := this }
      else as) =
    size as
have := reverse.termination h
no goals
α : Type u_1
a as : Array α
i : Nat
j : Fin (size as)
h : ¬i < j.val
⊢ size
      (if h : i < j.val then
        let_fun this := (_ : j.val - 1 - (i + 1) < j.val - i);
        let as_1 := swap as { val := i, isLt := (_ : i < size as) } j;
        let_fun this := (_ : j.val - 1 < size as_1);
        reverse.loop as_1 (i + 1) { val := j.val - 1, isLt := this }
      else as) =
    size as
simp [h]