intro i
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hc : ∀ (i : Fin 3), 0 < ∑ j : Fin 3, a i j
⊢ ∀ (i : Fin 3), 0 < ∑ j : Fin 3, a (p i) (p j)
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hc : ∀ (i : Fin 3), 0 < ∑ j : Fin 3, a i j
i : Fin 3
⊢ 0 < ∑ j : Fin 3, a (p i) (p j)