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

State before:
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
⊢ propsAB fun i j => a (p i) (p j)
Tactic:
intro i j
State after:
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
⊢ if i = j then 0 < (fun i j => a (p i) (p j)) i j else (fun i j => a (p i) (p j)) i j < 0

State before:
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
⊢ if i = j then 0 < (fun i j => a (p i) (p j)) i j else (fun i j => a (p i) (p j)) i j < 0
Tactic:
have h0 := hab (p i) (p j)
State after:
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
⊢ if i = j then 0 < (fun i j => a (p i) (p j)) i j else (fun i j => a (p i) (p j)) i j < 0

State before:
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
⊢ if i = j then 0 < (fun i j => a (p i) (p j)) i j else (fun i j => a (p i) (p j)) i j < 0
Tactic:
split_ifs with h1
State after:
case pos
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
h1 : i = j
⊢ 0 < (fun i j => a (p i) (p j)) i j

case neg
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
h1 : ¬i = j
⊢ (fun i j => a (p i) (p j)) i j < 0

State before:
case pos
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
h1 : i = j
⊢ 0 < (fun i j => a (p i) (p j)) i j
Tactic:
subst h1
State after:
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

State before:
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
Tactic:
simp only [reduceIte] at h0
State after:
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

State before:
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
Tactic:
exact h0
State after:
no goals

State before:
case neg
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
h1 : ¬i = j
⊢ (fun i j => a (p i) (p j)) i j < 0
Tactic:
have h2 : p i ≠ p j := fun a ↦ h1 (hp.1 a)
State after:
case neg
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
h1 : ¬i = j
h2 : p i ≠ p j
⊢ (fun i j => a (p i) (p j)) i j < 0

State before:
case neg
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
h1 : ¬i = j
h2 : p i ≠ p j
⊢ (fun i j => a (p i) (p j)) i j < 0
Tactic:
simp only [h2] at h0
State after:
case neg
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h1 : ¬i = j
h2 : p i ≠ p j
h0 : if False then 0 < a (p i) (p j) else a (p i) (p j) < 0
⊢ (fun i j => a (p i) (p j)) i j < 0

State before:
case neg
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h1 : ¬i = j
h2 : p i ≠ p j
h0 : if False then 0 < a (p i) (p j) else a (p i) (p j) < 0
⊢ (fun i j => a (p i) (p j)) i j < 0
Tactic:
exact h0
State after:
no goals