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

Goal state before:
pp: case h
ι : 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✝⁶ : Finite ι
inst✝⁵ : P.IsRootSystem
k : Type u_5
inst✝⁴ : Field k
inst✝³ : CharZero k
inst✝² : Module k M
inst✝¹ : Module k N
p : M →ₗ[k] N →ₗ[k] k
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hsp : span k (range ⇑root) = ⊤
i j : ι
⊢ (preReflection (root i) (p.flip (coroot i))) (root j) = (preReflection (root i) (p.flip (coroot i))) (root j)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: case refine_3
ι : 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
i j : ι
inst✝¹ : NeZero 2
inst✝ : IsAddTorsionFree M
hl : ∀ (s t : R), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
hc : P.coxeterWeight i j = 4
⊢ (P.flip (P.coroot i)) (P.root j) • P.root i ≠ 2 • P.root j

Tactic:
]

Goal state after:
case refine_3
ι : 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
i j : ι
inst✝¹ : NeZero 2
inst✝ : IsAddTorsionFree M
hl : ∀ (s t : R), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
hc : P.coxeterWeight i j = 4
⊢ (P.flip (P.coroot i)) (P.root j) • P.root i ≠ 2 • P.root j
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✝⁴ : Field R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsAnisotropic
inst✝ : P.IsRootSystem
i : ι
h₀ : (P.RootForm (P.root i)) (P.root i) ≠ 0
⊢ 2 • P.Polarization (P.root i) = 2 • P.Polarization (P.root i)

Tactic:
]

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✝⁴ : Field R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsAnisotropic
inst✝ : P.IsRootSystem
i : ι
h₀ : (P.RootForm (P.root i)) (P.root i) ≠ 0
⊢ 2 • P.Polarization (P.root i) = 2 • P.Polarization (P.root i)
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: case refine_3
ι : 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
i j : ι
inst✝¹ : NeZero 2
inst✝ : IsAddTorsionFree M
hc : P.coxeterWeight i j = 4
hl : ¬P.pairing j i • P.root i + -(2 • P.root j) = 0
⊢ ¬P.pairing j i • P.root i + -(2 • P.root j) = 0

Tactic:
]

Goal state after:
case refine_3
ι : 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
i j : ι
inst✝¹ : NeZero 2
inst✝ : IsAddTorsionFree M
hc : P.coxeterWeight i j = 4
hl : ¬P.pairing j i • P.root i + -(2 • P.root j) = 0
⊢ ¬P.pairing j i • P.root i + -(2 • P.root j) = 0
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
hx' : ¬x = 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
this : ⁅e, x⁆ ∈ genWeightSpace L (⇑α + ⇑(chainTop (⇑α) β))
⊢ ⁅↑(coroot α), x⁆ = ⁅coroot α, x⁆

Tactic:
]

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
hx' : ¬x = 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
this : ⁅e, x⁆ ∈ genWeightSpace L (⇑α + ⇑(chainTop (⇑α) β))
⊢ ⁅↑(coroot α), x⁆ = ⁅coroot α, x⁆
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
i j : ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ¬∀ (s t : R), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
⊢ P.pairing j i • P.root i = 2 • P.root j

Tactic:
]

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
i j : ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ¬∀ (s t : R), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
⊢ P.pairing j i • P.root i = 2 • P.root j
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
hx' : ¬x = 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
this : ⁅e, x⁆ ∈ ⊥
⊢ ⁅e, x⁆ = 0

Tactic:
]

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
hx' : ¬x = 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
this : ⁅e, x⁆ ∈ ⊥
⊢ ⁅e, x⁆ = 0
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
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : LinearOrder S
inst✝⁶ : IsStrictOrderedRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : ↥(span S (range ⇑P.root))
s : S
left✝ : s ≥ 0
hs : (algebraMap S R) s = (P.RootForm ↑x) ↑x
this : s = ((P.posRootForm S).posForm x) x
⊢ 0 ≤ s

Tactic:
]

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
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : LinearOrder S
inst✝⁶ : IsStrictOrderedRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : ↥(span S (range ⇑P.root))
s : S
left✝ : s ≥ 0
hs : (algebraMap S R) s = (P.RootForm ↑x) ↑x
this : s = ((P.posRootForm S).posForm x) x
⊢ 0 ≤ s
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✝⁵ : Field R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsAnisotropic
inst✝¹ : P.IsRootSystem
inst✝ : NeZero 2
s : Set ι
h : LinearIndepOn R (⇑P.root) s
f : ↑s → Rˣ
hf : ∀ (i : ↑s), P.coroot ↑i = f i • P.PolarizationEquiv (P.root ↑i)
this : s.domRestrict ⇑P.coroot = ⇑↑P.PolarizationEquiv ∘ (f • s.domRestrict ⇑P.root)
⊢ LinearIndependent (ι := ↑s) R (f • s.domRestrict ⇑P.root)

Tactic:
]

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✝⁵ : Field R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsAnisotropic
inst✝¹ : P.IsRootSystem
inst✝ : NeZero 2
s : Set ι
h : LinearIndepOn R (⇑P.root) s
f : ↑s → Rˣ
hf : ∀ (i : ↑s), P.coroot ↑i = f i • P.PolarizationEquiv (P.root ↑i)
this : s.domRestrict ⇑P.coroot = ⇑↑P.PolarizationEquiv ∘ (f • s.domRestrict ⇑P.root)
⊢ LinearIndependent (ι := ↑s) R (f • s.domRestrict ⇑P.root)
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
hx' : ¬x = 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
this : isSl2.HasPrimitiveVectorWith x ((chainTop (⇑α) β) (coroot α))
μ : ℕ
hμ : (chainTop (⇑α) β) (coroot α) = ↑μ
⊢ (chainTop (⇑α) β) (coroot α) • x = (chainTop (⇑α) β) (coroot α) • x

Tactic:
]

Goal state after:
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
i j : ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
s t : R
h₁ : s • P.root i = -t • P.root j
h₂ : s ≠ 0
h₃ : t ≠ 0
⊢ s • P.root i = -t • P.root j

Tactic:
]

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
i j : ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
s t : R
h₁ : s • P.root i = -t • P.root j
h₂ : s ≠ 0
h₃ : t ≠ 0
⊢ s • P.root i = -t • P.root j
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
i j : ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₁ : s • P.root i = -t • P.root j
h₄ : s * 2 = -(t * P.pairing j i)
⊢ 2 • -t • P.root j = 2 • -t • P.root j

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ⋃ i ∈ s, ↑(p i) = univ
this : ↑(p j) ⊆ ⋃ i ∈ s, ↑(p i)
⊢ ⋃ i ∈ s, ↑(p i) = univ

Tactic:
]

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ⋃ i ∈ s, ↑(p i) = univ
this : ↑(p j) ⊆ ⋃ i ∈ s, ↑(p i)
⊢ ⋃ i ∈ s, ↑(p i) = univ
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
hα : α.IsZero
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

Goal state before:
pp: case inl.inl
ι : 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
S : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : IsStrictOrderedRing S
inst✝⁸ : Algebra S R
inst✝⁷ : FaithfulSMul S R
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : P.IsValuedIn S
i j : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j = 0
hji : P.pairingIn S j i = 0
⊢ 0 ≤ 0 ↔ 0 ≤ 0

Tactic:
]

Goal state after:
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
i j : ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₄ : s * 2 = -(t * P.pairing j i)
h₁ : -t • P.pairing j i • P.root i = -t • 2 • P.root j
⊢ P.pairing j i • P.root i = 2 • P.root j

Tactic:
]

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
i j : ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₄ : s * 2 = -(t * P.pairing j i)
h₁ : -t • P.pairing j i • P.root i = -t • 2 • P.root j
⊢ P.pairing j i • P.root i = 2 • P.root j
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

Goal state before:
pp: case inl.inr
ι : 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
S : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : IsStrictOrderedRing S
inst✝⁸ : Algebra S R
inst✝⁷ : FaithfulSMul S R
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : P.IsValuedIn S
i j : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j = 0
hji : P.pairingIn S j i ≠ 0
⊢ 0 ≤ 0 ↔ 0 ≤ 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 | ∃ t, ∃ (_ : t ≠ 0), x + t • y = x_1}
⊢ sxy ∩ ↑(p j) ⊆ ∅

Tactic:
]

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 | ∃ t, ∃ (_ : t ≠ 0), x + t • y = x_1}
⊢ sxy ∩ ↑(p j) ⊆ ∅
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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
this : IsAddTorsionFree M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
⊢ P.coxeterWeight i j = 4

Tactic:
]

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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
this : IsAddTorsionFree M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
⊢ P.coxeterWeight i j = 4
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

Goal state before:
pp: case inr.inl
ι : 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
S : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : IsStrictOrderedRing S
inst✝⁸ : Algebra S R
inst✝⁷ : FaithfulSMul S R
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : P.IsValuedIn S
i j : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
hji : P.pairingIn S j i = 0
⊢ 0 ≤ 0 ↔ 0 ≤ 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : ¬α.IsZero
x' : L := ⋯.choose
h : x' ∈ rootSpace H ⇑(chainTop (⇑α) β) ∧ x' ≠ 0
k : K
hx : k • x' ∈ rootSpace H ⇑(chainTop (⇑α) β)
⊢ k • ⁅coroot α, x'⁆ = k • ⁅coroot α, x'⁆

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
⊢ ⁅coroot α, x⁆ = ⁅coroot α, x⁆

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 | ∃ t, ∃ (_ : t ≠ 0), x + t • y = x_1}
t : K
ht₀ : t ≠ 0
ht : y ∈ p j
⊢ x + t • y ∈ ∅

Tactic:
]

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 | ∃ t, ∃ (_ : t ≠ 0), x + t • y = x_1}
t : K
ht₀ : t ≠ 0
ht : y ∈ p j
⊢ x + t • y ∈ ∅
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

Goal state before:
pp: case inr.inr
ι : 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
S : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : IsStrictOrderedRing S
inst✝⁸ : Algebra S R
inst✝⁷ : FaithfulSMul S R
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : P.IsValuedIn S
i j : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
hji : P.pairingIn S j i ≠ 0
⊢ P.pairingIn S i j < 0 ↔ P.pairingIn S j i < 0

Tactic:
]

Goal state after:
case inr.inr
ι : 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
S : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : IsStrictOrderedRing S
inst✝⁸ : Algebra S R
inst✝⁷ : FaithfulSMul S R
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : P.IsValuedIn S
i j : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
hji : P.pairingIn S j i ≠ 0
⊢ P.pairingIn S i j < 0 ↔ P.pairingIn S j i < 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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
this : IsAddTorsionFree M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
h₂ : P.pairing i j • P.root j = 2 • P.root i
⊢ P.pairing i j • 2 • P.root j = P.pairing i j • 2 • P.root j

Tactic:
]

Goal state after:
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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
this : IsAddTorsionFree M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
h₂ : P.pairing i j • P.root j = 2 • P.root i
⊢ (2 * 2) • P.root i = 4 • P.root i

Tactic:
]

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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
this : IsAddTorsionFree M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
h₂ : P.pairing i j • P.root j = 2 • P.root i
⊢ (2 * 2) • P.root i = 4 • P.root i
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsZero
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : OrzechProperty R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
b : ι → M
spans : Function.Surjective ⇑(Finsupp.linearCombination R b)
card_le : Fintype.card ι ≤ finrank R M
⊢ LinearIndependent R b

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : OrzechProperty R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
b : ι → M
spans : Function.Surjective ⇑(Finsupp.linearCombination R b)
card_le : Fintype.card ι ≤ finrank R M
⊢ LinearIndependent R b
Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : OrzechProperty R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
ι : Type u_3
inst✝ : Fintype ι
b : ι → M
hc : Fintype.card ι = Set.finrank R (Set.range b)
x✝¹ : ↥(span R (Set.range b))
val✝ : M
property✝ : val✝ ∈ span R (Set.range b)
x✝ : ⟨val✝, property✝⟩ ∈ ⊤
⊢ (span R (Set.range b)).subtype ⟨val✝, property✝⟩ ∈
    ↑(span R (Set.range (⇑(span R (Set.range b)).subtype ∘ fun i ↦ ⟨b i, ⋯⟩)))

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : OrzechProperty R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
ι : Type u_3
inst✝ : Fintype ι
b : ι → M
hc : Fintype.card ι = Set.finrank R (Set.range b)
x✝¹ : ↥(span R (Set.range b))
val✝ : M
property✝ : val✝ ∈ span R (Set.range b)
x✝ : ⟨val✝, property✝⟩ ∈ ⊤
⊢ (span R (Set.range b)).subtype ⟨val✝, property✝⟩ ∈
    ↑(span R (Set.range (⇑(span R (Set.range b)).subtype ∘ fun i ↦ ⟨b i, ⋯⟩)))
Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : OrzechProperty R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
ι : Type u_3
inst✝ : Fintype ι
b : ι → M
⊢ Fintype.card ι = Set.finrank R (Set.range b) ↔ Fintype.card ι = Set.finrank R (Set.range b)

Tactic:
]

Goal state after: