α : Type u_1
inst✝ : DecidableEq α
a : Array α
i : Nat
⊢ (if h : i < size a then
      let_fun this := (_ : i < size a);
      decide (a[i] = a[i]) && isEqvAux a a (_ : size a = size a) (fun x y => decide (x = y)) (i + 1)
    else true) =
    true
α : Type u_1
inst✝ : DecidableEq α
a : Array α
i : Nat
⊢ isEqvAux a a (_ : size a = size a) (fun x y => decide (x = y)) i = true
unfold Array.isEqvAux
case inl
α : Type u_1
inst✝ : DecidableEq α
a : Array α
i : Nat
h✝ : i < size a
⊢ (let_fun this := (_ : i < size a);
    decide (a[i] = a[i]) && isEqvAux a a (_ : size a = size a) (fun x y => decide (x = y)) (i + 1)) =
    true

case inr
α : Type u_1
inst✝ : DecidableEq α
a : Array α
i : Nat
h✝ : ¬i < size a
⊢ true = true
α : Type u_1
inst✝ : DecidableEq α
a : Array α
i : Nat
⊢ (if h : i < size a then
      let_fun this := (_ : i < size a);
      decide (a[i] = a[i]) && isEqvAux a a (_ : size a = size a) (fun x y => decide (x = y)) (i + 1)
    else true) =
    true
split
case inr
α : Type u_1
inst✝ : DecidableEq α
a : Array α
i : Nat
h✝ : ¬i < size a
⊢ true = true
case inl
α : Type u_1
inst✝ : DecidableEq α
a : Array α
i : Nat
h✝ : i < size a
⊢ (let_fun this := (_ : i < size a);
    decide (a[i] = a[i]) && isEqvAux a a (_ : size a = size a) (fun x y => decide (x = y)) (i + 1)) =
    true

case inr
α : Type u_1
inst✝ : DecidableEq α
a : Array α
i : Nat
h✝ : ¬i < size a
⊢ true = true
case inl h => simp [h, isEqvAux_self a (i+1)]
no goals
case inr
α : Type u_1
inst✝ : DecidableEq α
a : Array α
i : Nat
h✝ : ¬i < size a
⊢ true = true
case inr h => simp [h]
no goals
α : Type u_1
inst✝ : DecidableEq α
a : Array α
i : Nat
h : i < size a
⊢ (let_fun this := (_ : i < size a);
    decide (a[i] = a[i]) && isEqvAux a a (_ : size a = size a) (fun x y => decide (x = y)) (i + 1)) =
    true
simp [h, isEqvAux_self a (i+1)]
no goals
α : Type u_1
inst✝ : DecidableEq α
a : Array α
i : Nat
h : ¬i < size a
⊢ true = true
simp [h]