simp only [reduceIte] at h0
case pos
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i : Fin 3
h0 : if p i = p i then 0 < a (p i) (p i) else a (p i) (p i) < 0
⊢ 0 < (fun i j => a (p i) (p j)) i i
case pos
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i : Fin 3
h0 : 0 < a (p i) (p i)
⊢ 0 < (fun i j => a (p i) (p j)) i i