Theorem: Imo1965P2.lemma2 (Compfiles/Imo1965P2.lean)

State before:
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)
Tactic:
intro i
State after:
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)

State before:
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)
Tactic:
rw [Function.Bijective.sum_comp hp]
State after:
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 < ∑ i_1 : Fin 3, a (p i) i_1

State before:
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 < ∑ i_1 : Fin 3, a (p i) i_1
Tactic:
exact hc (p i)
State after:
no goals