mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
h : (fun i ↦ ⟨P.coroot i, ⋯⟩) i = (fun i ↦ ⟨P.coroot i, ⋯⟩) j
⊢ i = j

Tactic:
simpa using

Goal state after:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
h : (fun i ↦ ⟨P.coroot i, ⋯⟩) i = (fun i ↦ ⟨P.coroot i, ⋯⟩) j
⊢ i = j
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
⊢ ↑({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } j -
        (((span K (range ⇑P.root)).subtype.restrictScalarsRange₂ (span K (range ⇑P.coroot)).subtype
                (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯)
              ({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } j))
            ({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } i) •
          { toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } i) =
    ↑({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } ((P.reflectionPerm i) j))

Tactic:
simpa using

Goal state after:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
⊢ P.root j - (algebraMap L L) (P.pairing j i) • P.root i = (P.reflection i) (P.root j)
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : FaithfulSMul S R
inst✝ : P.IsValuedIn S
i j k l : ι
h : P.root k = P.root i + P.root l
⊢ (algebraMap S R) (P.pairingIn S k j) = (algebraMap S R) (P.pairingIn S i j + P.pairingIn S l j)

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : FaithfulSMul S R
inst✝ : P.IsValuedIn S
i j k l : ι
h : P.root k = P.root i + P.root l
⊢ (algebraMap S R) (P.pairingIn S k j) = (algebraMap S R) (P.pairingIn S i j) + (algebraMap S R) (P.pairingIn S l j)
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
⊢ ↑({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } j -
        (((span K (range ⇑P.root)).subtype.restrictScalarsRange₂ (span K (range ⇑P.coroot)).subtype
                (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯)
              ({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } i))
            ({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } j) •
          { toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } i) =
    ↑({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } ((P.reflectionPerm i) j))

Tactic:
simpa using

Goal state after:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
⊢ P.coroot j - (algebraMap L L) (P.pairing i j) • P.coroot i = (P.coreflection i) (P.coroot j)
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : P.IsValuedIn S
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i j k l : ι
x y : S
h : P.root k = (algebraMap S R) x • P.root i + (algebraMap S R) y • P.root l
⊢ (algebraMap S R) (P.pairingIn S k j) = (algebraMap S R) (x • P.pairingIn S i j + y • P.pairingIn S l j)

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : P.IsValuedIn S
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i j k l : ι
x y : S
h : P.root k = (algebraMap S R) x • P.root i + (algebraMap S R) y • P.root l
⊢ (algebraMap S R) (P.pairingIn S k j) =
    (algebraMap S R) x * (algebraMap S R) (P.pairingIn S i j) +
      (algebraMap S R) y * (algebraMap S R) (P.pairingIn S l j)
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: R : Type u_1
inst✝¹ : AddZeroClass R
inst✝ : Mul R
a : R
⊢ IsSumSq (a * a)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : AddZeroClass R
inst✝ : Mul R
a : R
⊢ IsSumSq (a * a)
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : Mul R
ι : Type u_2
I : Finset ι
s : ι → R
hs : ∀ i ∈ I, IsSumSq (s i)
⊢ IsSumSq (∑ i ∈ I, s i)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : Mul R
ι : Type u_2
I : Finset ι
s : ι → R
hs : ∀ i ∈ I, IsSumSq (s i)
⊢ IsSumSq (∑ i ∈ I, s i)
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalCommSemiring R
s₁ s₂ : R
h₁ : IsSumSq s₁
h₂ : IsSumSq s₂
⊢ IsSumSq (s₁ * s₂)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : NonUnitalCommSemiring R
s₁ s₂ : R
h₁ : IsSumSq s₁
h₂ : IsSumSq s₂
⊢ IsSumSq (s₁ * s₂)
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
I : Finset ι
x : ι → R
hx : ∀ i ∈ I, IsSumSq (x i)
⊢ IsSumSq (∏ i ∈ I, x i)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
I : Finset ι
x : ι → R
hx : ∀ i ∈ I, IsSumSq (x i)
⊢ IsSumSq (∏ i ∈ I, x i)
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝³ : CommRing S
inst✝² : Module S M
inst✝¹ : Nonempty ι
inst✝ : NeZero 2
⊢ P.rootSpan S ≠ ⊥

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝³ : CommRing S
inst✝² : Module S M
inst✝¹ : Nonempty ι
inst✝ : NeZero 2
⊢ ∃ x, ¬P.root x = 0
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: case add
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
x y z : M
hy : y ∈ span R (range ⇑P.root)
hz : z ∈ span R (range ⇑P.root)
hy' : y ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))
hz' : z ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))
⊢ y + z ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))

Tactic:
simpa using

Goal state after:
case add
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
x y z : M
hy : y ∈ span R (range ⇑P.root)
hz : z ∈ span R (range ⇑P.root)
hy' : y ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))
hz' : z ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))
⊢ (P.reflection i) y + (P.reflection i) z ∈ span R (range ⇑P.root)
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: case smul
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
x : M
y : R
t : M
hy : t ∈ span R (range ⇑P.root)
hy' : t ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))
⊢ y • t ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))

Tactic:
simpa using

Goal state after:
case smul
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
x : M
y : R
t : M
hy : t ∈ span R (range ⇑P.root)
hy' : t ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))
⊢ y • (P.reflection i) t ∈ span R (range ⇑P.root)
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
P : RootPairing ι R M N
S : Type u_7
inst✝⁶ : CommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : P.IsValuedIn S
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : NeZero 2
i j : ι
⊢ P.pairingIn S i j = 0 ↔ P.pairingIn S j i = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
P : RootPairing ι R M N
S : Type u_7
inst✝⁶ : CommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : P.IsValuedIn S
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : NeZero 2
i j : ι
⊢ P.pairing i j = 0 ↔ P.pairing j i = 0
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : P.IsValuedIn S
inst✝³ : Module S M
inst✝² : Module S N
inst✝¹ : IsScalarTower S R M
inst✝ : IsScalarTower S R N
x : M
hx : x ∈ P.rootSpan S
y : N
hy : y ∈ P.corootSpan S
⊢ ∀ x ∈ range ⇑P.root,
    ∀ y ∈ range ⇑P.coroot,
      ((LinearMap.restrictScalarsₗ S R N R S ∘ₗ ↑S P.toLinearMap) x) y ∈ (Algebra.linearMap S R).range

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : P.IsValuedIn S
inst✝³ : Module S M
inst✝² : Module S N
inst✝¹ : IsScalarTower S R M
inst✝ : IsScalarTower S R N
x : M
hx : x ∈ P.rootSpan S
y : N
hy : y ∈ P.corootSpan S
⊢ ∀ (a a_1 : ι), ∃ y, (algebraMap S R) y = P.pairing a a_1
Module: Mathlib.LinearAlgebra.RootSystem.RootPositive

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : LinearOrder 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
inst✝ : FaithfulSMul S R
i : ι
s : S
hs : s > 0
hs' : (algebraMap S R) s = (B.form (P.root i)) (P.root i)
⊢ (B.form (P.root i)) (P.root i) ≠ 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : LinearOrder 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
inst✝ : FaithfulSMul S R
i : ι
s : S
hs : s > 0
hs' : (algebraMap S R) s = (B.form (P.root i)) (P.root i)
⊢ ¬s = 0
Module: Mathlib.LinearAlgebra.RootSystem.RootPositive

Goal state before:
pp: case hB
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder 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✝¹ : Module S M
inst✝ : IsScalarTower S R M
x✝¹ x✝ : ↥(span S (range ⇑P.root))
x : M
hx : x ∈ span S (range ⇑P.root)
y : M
hy : y ∈ span S (range ⇑P.root)
i j : ι
⊢ ((LinearMap.restrictScalarsₗ S R M R S ∘ₗ ↑S B.form) (P.root i)) (P.root j) ∈ (Algebra.linearMap S R).range

Tactic:
simpa using

Goal state after:
case hB
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder 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✝¹ : Module S M
inst✝ : IsScalarTower S R M
x✝¹ x✝ : ↥(span S (range ⇑P.root))
x : M
hx : x ∈ span S (range ⇑P.root)
y : M
hy : y ∈ span S (range ⇑P.root)
i j : ι
⊢ ∃ y, (algebraMap S R) y = (B.form (P.root i)) (P.root j)
Module: Mathlib.LinearAlgebra.RootSystem.RootPositive

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder 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
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ι
hi : P.root i ∈ span S (range ⇑P.root)
⊢ 0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root i, hi⟩

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder 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
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ι
hi : P.root i ∈ span S (range ⇑P.root)
⊢ ∃ s > 0, (algebraMap S R) s = (B.form (P.root i)) (P.root i)
Module: Mathlib.LinearAlgebra.RootSystem.RootPositive

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder 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
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
⊢ (algebraMap S R) ((RingHom.id S) ((B.posForm x) y)) = (algebraMap S R) ((B.posForm y) x)

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder 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
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
⊢ (B.form ↑x) ↑y = (B.form ↑y) ↑x
Module: Mathlib.LinearAlgebra.RootSystem.RootPositive

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : LinearOrder 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✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : IsStrictOrderedRing S
hi : P.root i ∈ span S (range ⇑P.root)
hj : P.root j ∈ span S (range ⇑P.root)
ri : ↥(span S (range ⇑P.root)) := ⋯
rj : ↥(span S (range ⇑P.root)) := ⋯
⊢ (algebraMap S R) (2 * (B.posForm ri) rj) = (algebraMap S R) (P.pairingIn S i j * (B.posForm rj) rj)

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : LinearOrder 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✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : IsStrictOrderedRing S
hi : P.root i ∈ span S (range ⇑P.root)
hj : P.root j ∈ span S (range ⇑P.root)
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, hj⟩
⊢ 2 * (B.form ↑ri) ↑rj = P.pairing i j * (B.form ↑rj) ↑rj
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

Goal state before:
pp: ι : 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✝ : Fintype ι
m : M
h : P.flip.toPerfPair (P.Polarization m) = 0
⊢ P.Polarization m = 0

Tactic:
simpa using

Goal state after:
ι : 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✝ : Fintype ι
m : M
h : P.flip.toPerfPair (P.Polarization m) = 0
⊢ P.Polarization m = 0
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case neg.mp.inl
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x < 1 ↔ v' x < 1
x : K
hx : ¬x = 0
hh : v x = 1
h_1 : ¬v' x = 1
h_2 : v' x < 1
⊢ False

Tactic:
simpa using

Goal state after:
case neg.mp.inl
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x < 1 ↔ v' x < 1
x : K
hx : ¬x = 0
hh : v x = 1
h_1 : ¬v' x = 1
h_2 : v' x < 1
⊢ False
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case neg.mpr.inl
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x < 1 ↔ v' x < 1
x : K
hx : ¬x = 0
hh : v' x = 1
h_1 : ¬v x = 1
h_2 : v x < 1
⊢ False

Tactic:
simpa using

Goal state after:
case neg.mpr.inl
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x < 1 ↔ v' x < 1
x : K
hx : ¬x = 0
hh : v' x = 1
h_1 : ¬v x = 1
h_2 : v x < 1
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : AddCommGroup N
inst✝¹³ : CommRing R
inst✝¹² : Module R M
inst✝¹¹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : LinearOrder S
inst✝⁸ : IsStrictOrderedRing S
inst✝⁷ : IsDomain R
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : P.IsValuedIn S
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
x : ↥(P.rootSpan S)
hx : x ≠ 0
⊢ 0 < (LinearMap.BilinMap.toQuadraticMap (P.RootFormIn S)) x

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : AddCommGroup N
inst✝¹³ : CommRing R
inst✝¹² : Module R M
inst✝¹¹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : LinearOrder S
inst✝⁸ : IsStrictOrderedRing S
inst✝⁷ : IsDomain R
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : P.IsValuedIn S
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
x : ↥(P.rootSpan S)
hx : x ≠ 0
⊢ 0 < ((P.RootFormIn S) x) x
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Fintype ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsAnisotropic
inst✝ : P.IsRootSystem
⊢ P.RootForm.Nondegenerate

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Fintype ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsAnisotropic
inst✝ : P.IsRootSystem
⊢ LinearMap.ker P.RootForm = ⊥
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: ι : 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✝³ : CharZero R
inst✝² : IsAddTorsionFree M
inst✝¹ : P.IsReduced
n : ℕ
inst✝ : n.AtLeastTwo
i : ι
⊢ ¬LinearIndependent R ![n • P.root i, P.root i]

Tactic:
simpa using

Goal state after:
ι : 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✝³ : CharZero R
inst✝² : IsAddTorsionFree M
inst✝¹ : P.IsReduced
n : ℕ
inst✝ : n.AtLeastTwo
i : ι
⊢ ∃ x x_1, ∃ (_ : x • n • P.root i + x_1 • P.root i = 0), ¬(x = 0 ∧ x_1 = 0)
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: ι : 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✝³ : CharZero R
inst✝² : IsAddTorsionFree M
inst✝¹ : P.IsReduced
n : ℕ
inst✝ : n.AtLeastTwo
i : ι
this : ¬LinearIndependent R ![n • P.root i, P.root i]
j : ι
hj : P.root j = n • P.root i
⊢ j = i ∨ P.root j = -P.root i

Tactic:
simpa using

Goal state after:
ι : 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✝³ : CharZero R
inst✝² : IsAddTorsionFree M
inst✝¹ : P.IsReduced
n : ℕ
inst✝ : n.AtLeastTwo
i : ι
this : ¬LinearIndependent R ![n • P.root i, P.root i]
j : ι
hj : P.root j = n • P.root i
⊢ j = i ∨ P.root j = -P.root i