awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
s : (i : ι) → S
hs : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (s i) : R) ((P.coroot' i : (a : M) → R) x : R)
suffices :
  Eq.{u_5 + 1} (α := S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
                x hx) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x
          hx) :
      S)
    (∑ i : ι, s i * s i : S)
⊢ IsSumSq.{u_5} (R := S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
                x hx) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x
          hx) :
      S)

Tactic:
suffices (P.posRootForm S).posForm ⟨x, hx⟩ ⟨x, hx⟩ = ∑ i, s i * s i from
    this ▸ IsSumSq.sum_mul_self Finset.univ s
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
s : (i : ι) → S
hs : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (s i) : R) ((P.coroot' i : (a : M) → R) x : R)
a :
  Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((((RootPositiveForm.posForm (P.posRootForm S) :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  (Subtype.mk (p := fun (x : M) ↦
                    Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
                      x)
                    x hx) :
                LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
                  (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x
              hx) :
          S) :
      R)
    ((algebraMap S R : (a : S) → R) (∑ i : ι, s i * s i) : R)
⊢ Eq.{u_5 + 1} (α := S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
                x hx) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x
          hx) :
      S)
    (∑ i : ι, s i * s i : S)

Tactic:
apply FaithfulSMul.algebraMap_injective S R

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
s : (i : ι) → S
hs : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (s i) : R) ((P.coroot' i : (a : M) → R) x : R)
a :
  Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
    (∑ x : ι,
        HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) (s x) : R)
          ((algebraMap S R : (a : S) → R) (s x) : R) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((((RootPositiveForm.posForm (P.posRootForm S) :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  (Subtype.mk (p := fun (x : M) ↦
                    Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
                      x)
                    x hx) :
                LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
                  (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x
              hx) :
          S) :
      R)
    ((algebraMap S R : (a : S) → R) (∑ i : ι, s i * s i) : R)

Tactic:
simp only [posRootForm, RootPositiveForm.algebraMap_posForm, map_sum, map_mul]

Premises used: map_sum, RootPairing.posRootForm, map_mul, RootPairing.RootPositiveForm.algebraMap_posForm
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
s : (i : ι) → S
hs : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (s i) : R) ((P.coroot' i : (a : M) → R) x : R)
⊢ Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
    (∑ x : ι,
        HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) (s x) : R)
          ((algebraMap S R : (a : S) → R) (s x) : R) :
      R)

Tactic:
simp [hs, rootForm_apply_apply]

Premises used: RootPairing.rootForm_apply_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x y : ↥(P.rootSpan S)
⊢ Eq.{u_5 + 1} (α := S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        y :
      S)
    (∑ i : ι,
        HMul.hMul (α := S) (β := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S)
          ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) y : S) :
      S)

Tactic:
(FaithfulSMul.algebraMap_injective S R) ?_

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x y : ↥(P.rootSpan S)
refine :
  Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((((RootPositiveForm.posForm (P.posRootForm S) :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  x :
                LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
                  (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            y :
          S) :
      R)
    ((algebraMap S R : (a : S) → R)
        (∑ i : ι,
          HMul.hMul (α := S) (β := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S)
            ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) y : S)) :
      R)
⊢ Eq.{u_5 + 1} (α := S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        y :
      S)
    (∑ i : ι,
        HMul.hMul (α := S) (β := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S)
          ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) y : S) :
      S)

Tactic:
refine (FaithfulSMul.algebraMap_injective S R) ?_

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x y : ↥(P.rootSpan S)
⊢ Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((((RootPositiveForm.posForm (P.posRootForm S) :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  x :
                LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
                  (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            y :
          S) :
      R)
    ((algebraMap S R : (a : S) → R)
        (∑ i : ι,
          HMul.hMul (α := S) (β := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S)
            ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) y : S)) :
      R)

Tactic:
simp [posRootForm, rootForm_apply_apply]

Premises used: RootPairing.rootForm_apply_apply, RootPairing.posRootForm
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
obtain :
  ∀ s ≥ 0,
    ∀
      (hs :
        Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
          ((((P.RootForm : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)),
      LE.le.{u_5} (α := S) (0 : S)
        ((((RootPositiveForm.posForm (P.posRootForm S) :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  x :
                LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
                  (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            x :
          S)
⊢ LE.le.{u_5} (α := S) (0 : S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        x :
      S)

Tactic:
obtain ⟨s, _, hs⟩ := P.exists_ge_zero_eq_rootForm S x.1 x.2

Premises used: RootPairing.exists_ge_zero_eq_rootForm, Subtype.val, Subtype.property
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
s : S
left : s ≥ 0
hs :
  Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
⊢ s =
    (((RootPositiveForm.posForm (P.posRootForm S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
            x :
          LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
            (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
        (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
      x

Tactic:
have : s = (P.posRootForm S).posForm x x :=
    FaithfulSMul.algebraMap_injective S R <| (P.algebraMap_posRootForm_posForm S x x) ▸ hs
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
s : S
left : s ≥ 0
hs :
  Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
this :
  s =
    (((RootPositiveForm.posForm (P.posRootForm S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
            x :
          LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
            (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
        (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
      x
rwa rwa₁ rwa₂ rwa₃ : 0 ≤ s
⊢ LE.le.{u_5} (α := S) (0 : S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        x :
      S)

Tactic:
rwa [← this]
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
⊢ 0 < P.pairingIn S i j ↔ 0 < P.pairingIn S j i

Tactic:
let _i : Fintype ι := Fintype.ofFinite ι
  zero_lt_pairingIn_iff (P.posRootForm S) i j

Premises used: Fintype.ofFinite, RootPairing.zero_lt_pairingIn_iff, RootPairing.posRootForm
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
⊢ P.pairingIn S i j < 0 ↔ P.pairingIn S j i < 0

Tactic:
simpa using P.zero_lt_pairingIn_iff' S (i := i) (j := P.reflectionPerm j j)

Premises used: RootPairing.zero_lt_pairingIn_iff'
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
inl : ∀ (hij : P.pairingIn S i j = 0), P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
inr : ∀ (hij : P.pairingIn S i j ≠ 0), P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0

Tactic:
rcases eq_or_ne (P.pairingIn S i j) 0 with hij | hij

Premises used: RootPairing.pairingIn, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
hij : P.pairingIn S i j = 0
inl : ∀ (hji : P.pairingIn S j i = 0), P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
inl₁ : ∀ (hji : P.pairingIn S j i ≠ 0), P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0

Tactic:
rcases eq_or_ne (P.pairingIn S j i) 0 with hji | hji

Premises used: RootPairing.pairingIn, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
inr : ∀ (hji : P.pairingIn S j i = 0), P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
inr₁ : ∀ (hji : P.pairingIn S j i ≠ 0), P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0

Tactic:
rcases eq_or_ne (P.pairingIn S j i) 0 with hji | hji

Premises used: RootPairing.pairingIn, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
hij : P.pairingIn S i j = 0
hji : P.pairingIn S j i = 0
inl : LE.le.{u_5} (α := S) 0 0 ↔ P.pairingIn S j i ≤ 0
inl₁ inl₂ : LE.le.{u_5} (α := S) 0 0 ↔ LE.le.{u_5} (α := S) 0 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0

Tactic:
rw [hij, hji]
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
hij : P.pairingIn S i j = 0
hji : P.pairingIn S j i ≠ 0
inl : LE.le.{u_5} (α := S) 0 0 ↔ P.pairingIn S j i ≤ 0
inl₁ inl₂ : LE.le.{u_5} (α := S) 0 0 ↔ LE.le.{u_5} (α := S) 0 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0

Tactic:
rw [hij, P.pairingIn_eq_zero_iff.mp hij]

Premises used: RootPairing.pairingIn_eq_zero_iff, Iff.mp