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

State before:
x : Fin 3 → ℝ
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
he : propEqs x a
⊢ propEqs (x ∘ p) fun i j => a (p i) (p j)
Tactic:
intro i
State after:
x : Fin 3 → ℝ
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
he : propEqs x a
i : Fin 3
⊢ ∑ j : Fin 3, (fun i j => a (p i) (p j)) i j * (x ∘ p) j = 0

State before:
x : Fin 3 → ℝ
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
he : propEqs x a
i : Fin 3
⊢ ∑ j : Fin 3, (fun i j => a (p i) (p j)) i j * (x ∘ p) j = 0
Tactic:
dsimp
State after:
x : Fin 3 → ℝ
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
he : propEqs x a
i : Fin 3
⊢ ∑ j : Fin 3, a (p i) (p j) * x (p j) = 0

State before:
x : Fin 3 → ℝ
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
he : propEqs x a
i : Fin 3
⊢ ∑ j : Fin 3, a (p i) (p j) * x (p j) = 0
Tactic:
have hi := he (p i)
State after:
x : Fin 3 → ℝ
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
he : propEqs x a
i : Fin 3
hi : ∑ j : Fin 3, a (p i) j * x j = 0
⊢ ∑ j : Fin 3, a (p i) (p j) * x (p j) = 0

State before:
x : Fin 3 → ℝ
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
he : propEqs x a
i : Fin 3
hi : ∑ j : Fin 3, a (p i) j * x j = 0
⊢ ∑ j : Fin 3, a (p i) (p j) * x (p j) = 0
Tactic:
rwa [Function.Bijective.sum_comp hp (fun j ↦ a (p i) j * x j)]
State after:
no goals