-- Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
lemma root_add_root_mem_of_pairingIn_neg (h : P.pairingIn ℤ i j < 0) (h' : α i ≠ - α j) :
    α i + α j ∈ Φ

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h' : P.root i ≠ -P.root j
_i : InvolutiveNeg ι := P.indexNeg
h : 0 < P.pairingIn ℤ i (-j)
⊢ i ≠ -j

Tactic:
contrapose! h'

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
_i : InvolutiveNeg ι := P.indexNeg
h : 0 < P.pairingIn ℤ i (-j)
h' : i = -j
⊢ P.root i = -P.root j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h : P.pairingIn ℤ i j < 0
h' : P.root i ≠ -P.root j
_i : InvolutiveNeg ι := P.indexNeg
⊢ 0 < P.pairingIn ℤ i (-j)

Tactic:
simpa

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h' : P.root i ≠ -P.root j
_i : InvolutiveNeg ι := P.indexNeg
h : 0 < P.pairingIn ℤ i (-j)
⊢ P.root i + P.root j ∈ range ⇑P.root

Tactic:
replace h' : i ≠ -j := by contrapose! h'; simp [h']

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
_i : InvolutiveNeg ι := P.indexNeg
h : 0 < P.pairingIn ℤ i (-j)
h' : i ≠ -j
⊢ P.root i + P.root j ∈ range ⇑P.root

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h : P.pairingIn ℤ i j < 0
h' : P.root i ≠ -P.root j
⊢ P.root i + P.root j ∈ range ⇑P.root

Tactic:
let _i := P.indexNeg

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h : P.pairingIn ℤ i j < 0
h' : P.root i ≠ -P.root j
_i : InvolutiveNeg ι := P.indexNeg
⊢ P.root i + P.root j ∈ range ⇑P.root

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h : P.pairingIn ℤ i j < 0
h' : P.root i ≠ -P.root j
_i : InvolutiveNeg ι := P.indexNeg
⊢ P.root i + P.root j ∈ range ⇑P.root

Tactic:
replace h : 0 < P.pairingIn ℤ i (-j) := by simpa

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h' : P.root i ≠ -P.root j
_i : InvolutiveNeg ι := P.indexNeg
h : 0 < P.pairingIn ℤ i (-j)
⊢ P.root i + P.root j ∈ range ⇑P.root

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
_i : InvolutiveNeg ι := P.indexNeg
h : 0 < P.pairingIn ℤ i (-j)
h' : i = -j
⊢ P.root i = -P.root j

Tactic:
simp [h']

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
_i : InvolutiveNeg ι := P.indexNeg
h : 0 < P.pairingIn ℤ i (-j)
h' : i ≠ -j
⊢ P.root i + P.root j ∈ range ⇑P.root

Tactic:
simpa using P.root_sub_root_mem_of_pairingIn_pos h h'

Result:
no goals