awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 j_1 : ι
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
x_1 x_2 : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
y : M
hy : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) y
i j : ι
⊢ Membership.mem (α := R) (γ := Submodule S R) (LinearMap.range (Algebra.linearMap S R))
    ((((LinearMap.restrictScalarsₗ S R M R S ∘ₗ
                  (↑S :
                      {S_1 : Type u_2} →
                        {M : Type u_4} →
                          {M₂ : Type (max u_2 u_4)} →
                            [inst : Semiring S] →
                              [inst_12 : Semiring S_1] →
                                [inst_13 : AddCommMonoid M] →
                                  [inst_14 : AddCommMonoid M₂] →
                                    [inst_15 : Module S M] →
                                      [inst_16 : Module S M₂] →
                                        [inst_17 : Module S_1 M] →
                                          [inst_18 : Module S_1 M₂] →
                                            [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                    B.form :
                (a : M) → M →ₗ[S] R)
              ((P.root : (a : ι) → M) i) :
            M →ₗ[S] R) :
          (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)

Tactic:
simpa using B.exists_eq i j

Premises used: RootPairing.RootPositiveForm.exists_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
i j : ι
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
x_1 x_2 : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
y : M
hy : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) y
⊢ Membership.mem (α := M) (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
    ((Submodule.subtype (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → M)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x
          hx) :
      M)

Tactic:
simpa
-- 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
inst_10 : Module S M
inst_11 : IsScalarTower S R M
x_1 x_2 : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
y : M
hy : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) y
⊢ Membership.mem (α := M) (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
    ((Submodule.subtype (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → M)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) y
          hy) :
      M)

Tactic:
simpa
-- 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
inst_10 : Module S M
inst_11 : IsScalarTower S R M
x y : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
change :
  Eq.{u_2 + 1} (α := R)
    ((Algebra.linearMap S R : (a : S) → R)
        ((((B.posForm :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  x :
                LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                  (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            y :
          S) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((((B.posForm :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  x :
                LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                  (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            y :
          S) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)

Tactic:
change Algebra.linearMap S R _ = _

Premises used: Algebra.linearMap, 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
inst_10 : Module S M
inst_11 : IsScalarTower S R M
x y : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
⊢ Eq.{u_2 + 1} (α := R)
    ((Algebra.linearMap S R : (a : S) → R)
        ((((B.posForm :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  x :
                LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                  (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            y :
          S) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)

Tactic:
simp [posForm]

Premises used: RootPairing.RootPositiveForm.posForm
-- 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
inst_10 : Module S M
inst_11 : IsScalarTower S R M
x y : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
s : S
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
      ((((B.form : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R) ↔
    s =
      (((B.posForm :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
              (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        y

Tactic:
simp [RootPositiveForm.posForm]

Premises used: RootPairing.RootPositiveForm.posForm
-- 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
inst_10 : Module S M
inst_11 : IsScalarTower S R M
x y : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
h :
  LT.lt.{u_3} (α := S) (0 : S)
    ((((B.posForm : (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
              (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        y :
      S)
⊢ Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((((B.posForm :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  x :
                LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                  (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            y :
          S) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)

Tactic:
simp
-- 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
inst_10 : Module S M
inst_11 : IsScalarTower S R M
x y : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
refine :
  (∃ s > 0,
      Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
        ((((B.form : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)) →
    ∀ (s : S) (h : s > 0)
      (h' :
        Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
          ((((B.form : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)),
      LT.lt.{u_3} (α := S) (0 : S)
        ((((B.posForm :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  x :
                LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                  (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            y :
          S)
⊢ LT.lt.{u_3} (α := S) (0 : S)
      ((((B.posForm :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                x :
              LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
            (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
          y :
        S) ↔
    ∃ s > 0,
      Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
        ((((B.form : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)

Tactic:
refine ⟨fun h ↦ ⟨B.posForm x y, h, by simp⟩, fun ⟨s, h, h'⟩ ↦ ?_⟩
-- 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
inst_10 : Module S M
inst_11 : IsScalarTower S R M
x y : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
h_1 :
  ∃ s > 0,
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
      ((((B.form : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
s : S
h : s > 0
h' :
  Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
    ((((B.form : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
    ((algebraMap S R : (a : S) → R)
        ((((B.posForm :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  x :
                LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                  (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            y :
          S) :
      R)

Tactic:
rw [← B.algebraMap_posForm] at h'

Premises used: RootPairing.RootPositiveForm.algebraMap_posForm
-- 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
inst_10 : Module S M
inst_11 : IsScalarTower S R M
x y : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
h_1 :
  ∃ s > 0,
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
      ((((B.form : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
s : S
h : s > 0
h' :
  Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
    ((algebraMap S R : (a : S) → R)
        ((((B.posForm :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  x :
                LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                  (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            y :
          S) :
      R)
rwa rwa₁ rwa₂ rwa₃ : 0 < s
⊢ LT.lt.{u_3} (α := S) (0 : S)
    ((((B.posForm : (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
              (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        y :
      S)

Tactic:
rwa [← FaithfulSMul.algebraMap_injective S R h']

Premises used: FaithfulSMul.algebraMap_injective
-- 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
inst_10 : Module S M
inst_11 : IsScalarTower S R M
i : ι
hi :
  Membership.mem.{u_4, u_4} (α := M) (γ := Submodule S M)
    (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) ((P.root : (a : ι) → M) i : M)
⊢ LT.lt.{u_3} (α := S) (0 : S)
    ((((B.posForm : (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_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
                ((P.root : (a : ι) → M) i) hi) :
            LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
              (↥(span S (range.{u_4, 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_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
            ((P.root : (a : ι) → M) i) hi :
          ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) :
      S)

Tactic:
simpa only [zero_lt_posForm_iff] using B.exists_pos_eq i

Premises used: RootPairing.RootPositiveForm.zero_lt_posForm_iff, 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
inst_10 : Module S M
inst_11 : IsScalarTower S R M
x y : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
a :
  Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((RingHom.id S : (a : S) → S)
            ((((B.posForm :
                        (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) →
                          ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                      x :
                    LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                      (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
                y :
              S) :
          S) :
      R)
    ((algebraMap S R : (a : S) → R)
        ((((B.posForm :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  y :
                LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                  (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            x :
          S) :
      R)
⊢ Eq (α := S)
    ((RingHom.id S : (a : S) → S)
        ((((B.posForm :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  x :
                LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                  (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            y :
          S) :
      S)
    ((((B.posForm : (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              y :
            LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
              (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        x :
      S)

Tactic:
apply FaithfulSMul.algebraMap_injective S R

Premises used: FaithfulSMul.algebraMap_injective
-- 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
inst_10 : Module S M
inst_11 : IsScalarTower S R M
x y : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
⊢ Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((RingHom.id S : (a : S) → S)
            ((((B.posForm :
                        (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) →
                          ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                      x :
                    LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                      (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
                y :
              S) :
          S) :
      R)
    ((algebraMap S R : (a : S) → R)
        ((((B.posForm :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  y :
                LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                  (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            x :
          S) :
      R)

Tactic:
simpa using B.symm.eq x y

Premises used: RootPairing.RootPositiveForm.symm, LinearMap.IsSymm.eq, Subtype.val
-- 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
inst_10 : Module S M
inst_11 : IsScalarTower S R M
i : ι
⊢ 0 < B.rootLength i

Tactic:
simpa using B.zero_lt_posForm_apply_root i

Premises used: Set.mem_range_self, RootPairing.RootPositiveForm.zero_lt_posForm_apply_root, Submodule.subset_span
-- 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
inst_10 : Module S M
inst_11 : IsScalarTower S R M
i : ι
⊢ B.rootLength ((P.reflectionPerm i : (a : ι) → ι) i) = B.rootLength i

Tactic:
simp [rootLength, rootSpanMem_reflectionPerm_self]

Premises used: RootPairing.RootPositiveForm.rootLength, RootPairing.rootSpanMem_reflectionPerm_self
-- 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
inst_10 : Module S M
inst_11 : IsScalarTower S R M
i : ι
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (B.rootLength i) : 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)

Tactic:
simp [rootLength]

Premises used: RootPairing.RootPositiveForm.rootLength
-- 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
inst_10 : Module S M
inst_11 : IsScalarTower S R M
⊢ P.pairingIn S j i * B.rootLength i = P.pairingIn S i j * B.rootLength j

Tactic:
simpa only [← (algebraMap_injective S R).eq_iff, algebraMap_pairingIn, map_mul,
    B.algebraMap_rootLength] using B.toInvariantForm.pairing_mul_eq_pairing_mul_swap i j

Premises used: RootPairing.RootPositiveForm.algebraMap_rootLength, RootPairing.InvariantForm.pairing_mul_eq_pairing_mul_swap, Function.Injective.eq_iff, RootPairing.algebraMap_pairingIn, map_mul, FaithfulSMul.algebraMap_injective, RootPairing.RootPositiveForm.toInvariantForm