-- Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
@[simp]
lemma apply_root_root_zero_iff :
    B.form (P.root i) (P.root j) = 0 ↔ P.pairing i j = 0

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
_i : CharZero R
⊢ P.pairing i j * (B.form (P.root j)) (P.root j) = 0 ↔ P.pairing i j = 0

Tactic:
simp [B.form_apply_root_ne_zero j]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
⊢ (B.form (P.root i)) (P.root j) = 0 ↔ P.pairing i j = 0

Tactic:
have _i := Algebra.charZero_of_charZero S R

Result:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
_i : CharZero R
⊢ (B.form (P.root i)) (P.root j) = 0 ↔ P.pairing i j = 0

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
_i : CharZero R
⊢ (B.form (P.root i)) (P.root j) = 0 ↔ P.pairing i j = 0

Tactic:
calc B.form (P.root i) (P.root j) = 0
    ↔ 2 * B.form (P.root i) (P.root j) = 0 := by simp
  _ ↔ P.pairing i j * B.form (P.root j) (P.root j) = 0 := by rw [B.two_mul_apply_root_root i j]
  _ ↔ P.pairing i j = 0 := by simp [B.form_apply_root_ne_zero j]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
_i : CharZero R
⊢ (B.form (P.root i)) (P.root j) = 0 ↔ 2 * (B.form (P.root i)) (P.root j) = 0

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
_i : CharZero R
⊢ 2 * (B.form (P.root i)) (P.root j) = 0 ↔ P.pairing i j * (B.form (P.root j)) (P.root j) = 0

Tactic:
rw [B.two_mul_apply_root_root i j]

Result:
no goals