awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
rw : P.coxeterWeight i j ≠ 4 ↔ P.coxeterWeightIn S i j ≠ 4
rw₁ :
  Ne.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.coxeterWeightIn S i j) : R) (4 : R) ↔
    P.coxeterWeightIn S i j ≠ 4
rw₂ :
  Ne.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.coxeterWeightIn S i j) : R)
      ((algebraMap S R : (a : S) → R) 4 : R) ↔
    P.coxeterWeightIn S i j ≠ 4
rw₃ rw₄ : P.coxeterWeightIn S i j ≠ 4 ↔ P.coxeterWeightIn S i j ≠ 4
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M) ↔
    P.coxeterWeightIn S i j ≠ 4

Tactic:
rw [linearIndependent_iff_coxeterWeight_ne_four, ← P.algebraMap_coxeterWeightIn S,
    ← map_ofNat (algebraMap S R), (algebraMap_injective S R).ne_iff]

Premises used: Algebra.algebraMap, map_ofNat, RootPairing.algebraMap_coxeterWeightIn, Function.Injective.ne_iff, RootPairing.linearIndependent_iff_coxeterWeight_ne_four, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
rw : P.coxeterWeightIn S i j = 4 ↔ ¬P.coxeterWeightIn S i j ≠ 4
rw₁ rw₂ : P.coxeterWeightIn S i j = 4 ↔ P.coxeterWeightIn S i j = 4
⊢ P.coxeterWeightIn S i j = 4 ↔
    ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)

Tactic:
rw [P.linearIndependent_iff_coxeterWeightIn_ne_four S, not_not]

Premises used: Classical.not_not, RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : P.IsReduced
h : i ≠ j
h' : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
rw :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ P.coxeterWeightIn S i j ≠ 4

Tactic:
rw [ne_eq, coxeterWeightIn_eq_four_iff_not_linearIndependent, not_not]

Premises used: RootPairing.coxeterWeightIn_eq_four_iff_not_linearIndependent, Classical.not_not, ne_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : P.IsReduced
h : i ≠ j
h' : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)

Tactic:
IsReduced.linearIndependent P h h'

Premises used: RootPairing.IsReduced.linearIndependent
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : P.IsReduced
h : i ≠ j
h' : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)

Tactic:
exact IsReduced.linearIndependent P h h'

Premises used: RootPairing.IsReduced.linearIndependent
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
⊢ P.pairingIn S i j = 2 ∧ P.pairingIn S j i = 2 ↔ i = j

Tactic:
simp only [← P.pairing_two_two_iff, ← P.algebraMap_pairingIn S, ← map_ofNat (algebraMap S R),
    (algebraMap_injective S R).eq_iff]

Premises used: RootPairing.pairing_two_two_iff, Algebra.algebraMap, Function.Injective.eq_iff, map_ofNat, RootPairing.algebraMap_pairingIn, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
⊢ P.pairingIn S i j = -2 ∧ P.pairingIn S j i = -2 ↔
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
simp only [← P.pairing_neg_two_neg_two_iff, ← P.algebraMap_pairingIn S,
    ← map_ofNat (algebraMap S R), (algebraMap_injective S R).eq_iff, ← map_neg]

Premises used: Algebra.algebraMap, Function.Injective.eq_iff, map_ofNat, RootPairing.algebraMap_pairingIn, map_neg, FaithfulSMul.algebraMap_injective, RootPairing.pairing_neg_two_neg_two_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : IsTorsionFree R N
rw : P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔ P.pairing i j = 1 ∧ P.pairing j i = 4
rw₁ :
  P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R) (1 : R) ∧ P.pairing j i = 4
rw₂ :
  P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R) (1 : R) ∧
      Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R) (4 : R)
rw₃ :
  P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)
        ((algebraMap S R : (a : S) → R) 1 : R) ∧
      Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R) (4 : R)
rw₄ :
  P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)
        ((algebraMap S R : (a : S) → R) 1 : R) ∧
      Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R)
        ((algebraMap S R : (a : S) → R) 4 : R)
rw₅ :
  P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
    P.pairingIn S i j = 1 ∧
      Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R)
        ((algebraMap S R : (a : S) → R) 4 : R)
rw₆ rw₇ : P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔ P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4
⊢ P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
    (P.root : (a : ι) → M) j = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)

Tactic:
rw [← P.pairing_one_four_iff, ← P.algebraMap_pairingIn S, ← P.algebraMap_pairingIn S,
    ← map_one (algebraMap S R), ← map_ofNat (algebraMap S R), (algebraMap_injective S R).eq_iff,
    (algebraMap_injective S R).eq_iff]

Premises used: Algebra.algebraMap, Function.Injective.eq_iff, map_ofNat, RootPairing.algebraMap_pairingIn, map_one, FaithfulSMul.algebraMap_injective, RootPairing.pairing_one_four_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
B : P.InvariantForm
i : ι
contra : Eq (α := M →ₗ[R] R) ((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) (0 : M →ₗ[R] R)
⊢ Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    (0 : R)

Tactic:
simp [contra]
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
B : P.InvariantForm
i j : ι
rw :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) j : M) =
    HSub.hSub (β := R)
      (HMul.hMul (β := R) (P.pairing i j)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
⊢ HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HMul.hMul (β := R) (P.pairing i j)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)

Tactic:
rw [two_mul, ← eq_sub_iff_add_eq]

Premises used: eq_sub_iff_add_eq, two_mul
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
B : P.InvariantForm
i j : ι
nth_rw :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M)) : M →ₗ[R] R) :
        (a : M) → R)
      ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) j : M) : M) =
    HSub.hSub (β := R)
      (HMul.hMul (β := R) (P.pairing i j)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
⊢ (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) j : M) =
    HSub.hSub (β := R)
      (HMul.hMul (β := R) (P.pairing i j)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)

Tactic:
nth_rw 1 [← B.isOrthogonal_reflection j]

Premises used: RootPairing.InvariantForm.isOrthogonal_reflection
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
B : P.InvariantForm
i j : ι
rw :
  HMul.hMul (β := R) (P.pairing j i)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R) =
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
rw₁ :
  HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R) =
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
rw₂ :
  HMul.hMul (α := R) (β := R) (2 : R)
      ((RingHom.id R : (a : R) → R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) :
            R) :
        R) =
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
rw₃ rw₄ :
  HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
⊢ HMul.hMul (β := R) (P.pairing j i)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R) =
    HMul.hMul (β := R) (P.pairing i j)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)

Tactic:
rw [← B.two_mul_apply_root_root i j, ← B.two_mul_apply_root_root j i, ← B.symm.eq,
    RingHom.id_apply]

Premises used: RingHom.id_apply, RootPairing.InvariantForm.symm, LinearMap.IsSymm.eq, RootPairing.InvariantForm.two_mul_apply_root_root
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
B : P.InvariantForm
i : ι
x y : M
⊢ Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.reflection i : (a : M) → M) x) : M →ₗ[R] R) : (a : M) → R)
        ((P.reflection i : (a : M) → M) y : M) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
B.isOrthogonal_reflection i x y

Premises used: RootPairing.InvariantForm.isOrthogonal_reflection
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
B : P.InvariantForm
i j : ι
inst_5 : IsDomain R
inst_6 : NeZero.{u_2} (R := R) 2
⊢ Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
      (0 : R) ↔
    HMul.hMul (α := R) (β := R) (2 : R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R) =
      0

Tactic:
simp [two_ne_zero]

Premises used: two_ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
B : P.InvariantForm
i j : ι
inst_5 : IsDomain R
inst_6 : NeZero.{u_2} (R := R) 2
rw rw₁ :
  HMul.hMul (β := R) (P.pairing i j)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R) =
      0 ↔
    HMul.hMul (β := R) (P.pairing i j)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R) =
      0
⊢ HMul.hMul (α := R) (β := R) (2 : R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R) =
      0 ↔
    HMul.hMul (β := R) (P.pairing i j)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R) =
      0

Tactic:
rw [B.two_mul_apply_root_root i j]

Premises used: RootPairing.InvariantForm.two_mul_apply_root_root
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
B : P.InvariantForm
i j : ι
inst_5 : IsDomain R
inst_6 : NeZero.{u_2} (R := R) 2
⊢ HMul.hMul (β := R) (P.pairing i j)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R) =
      0 ↔
    P.pairing i j = 0

Tactic:
simp [B.ne_zero j]

Premises used: RootPairing.InvariantForm.ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
B : P.InvariantForm
i j : ι
inst_5 : IsDomain R
inst_6 : NeZero.{u_2} (R := R) 2
calc :
  Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
      (0 : R) ↔
    HMul.hMul (α := R) (β := R) (2 : R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R) =
      0
calc₁ :
  HMul.hMul (α := R) (β := R) (2 : R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R) =
      0 ↔
    HMul.hMul (β := R) (P.pairing i j)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R) =
      0
calc₂ :
  HMul.hMul (β := R) (P.pairing i j)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R) =
      0 ↔
    P.pairing i j = 0
⊢ Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
      (0 : R) ↔
    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 [two_ne_zero]
    _ ↔ 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.ne_zero j]

Premises used: RootPairing.pairing, RootPairing.root, RootPairing.InvariantForm.form, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing S
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : Algebra S R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsValuedIn S
B : RootPositiveForm S P
inst_9 : FaithfulSMul S R
i : ι
obtain :
  ∀ (s : S) (hs : s > 0)
    (hs' :
      Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)),
    Ne.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      (0 : R)
⊢ Ne.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    (0 : R)

Tactic:
obtain ⟨s, hs, hs'⟩ := B.exists_pos_eq i

Premises used: RootPairing.RootPositiveForm.exists_pos_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing S
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : Algebra S R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsValuedIn S
B : RootPositiveForm S P
inst_9 : FaithfulSMul S R
i : ι
s : S
hs : s > 0
hs' :
  Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
⊢ Ne.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    (0 : R)

Tactic:
simpa [← hs'] using hs.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing S
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : Algebra S R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst_9 : FaithfulSMul S R
⊢ HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HMul.hMul (β := R) (P.pairing i j)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)

Tactic:
B.toInvariantForm.two_mul_apply_root_root i j

Premises used: RootPairing.InvariantForm.two_mul_apply_root_root, RootPairing.RootPositiveForm.toInvariantForm