mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
pX : R[X]
hpX : pX ∈ P
hp0 : map (Ideal.Quotient.mk (comap C P)) pX ≠ 0
a : R ⧸ P' := (map (Ideal.Quotient.mk P') pX).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hP'_prime : P'.IsPrime
hM : 0 ∉ M
M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M
this :
  (algebraMap (R[X] ⧸ P) (Localization M')).comp φ =
    (IsLocalization.map (Localization M') φ ⋯).comp (algebraMap (R ⧸ P') (Localization M))
⊢ (IsLocalization.map (Localization M') φ ⋯).IsIntegral

Tactic:
have isloc : IsLocalization M' (Localization M') := by infer_instance
        exact @isIntegral_isLocalization_polynomial_quotient R _
          (Localization M) (Localization M') _ _ P pX hpX _ _ _ isloc

Goal state after:
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
h✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], ValuationRing (Localization P.primeCompl)
h : IsTorsionFree R M
P : Ideal R
hP : P.IsMaximal
⊢ Flat R (LocalizedModule P.primeCompl M)

Tactic:
rw [← flat_iff_of_isLocalization (Localization P.primeCompl) P.primeCompl,
    Flat.flat_iff_torsion_eq_bot_of_isBezout, ← Submodule.isTorsionFree_iff_torsion_eq_bot]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
h✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], ValuationRing (Localization P.primeCompl)
h : IsTorsionFree R M
P : Ideal R
hP : P.IsMaximal
⊢ IsTorsionFree (Localization P.primeCompl) (LocalizedModule P.primeCompl M)
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 = x • P.root i + y • P.root l
⊢ P.root k = (algebraMap S R) x • P.root i + (algebraMap S R) y • P.root l

Tactic:
simpa

Goal state after:
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₂
⊢ s₁ ∈ NonUnitalSubsemiring.sumSq R

Tactic:
simpa

Goal state after:
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₂
⊢ s₂ ∈ NonUnitalSubsemiring.sumSq R

Tactic:
simpa

Goal state after:
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)
⊢ ∀ c ∈ I, x c ∈ Subsemiring.sumSq R

Tactic:
simpa

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

Goal state before:
pp: case hx
ι : 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)
⊢ (span S (range ⇑P.root)).subtype ⟨x, hx⟩ ∈ span S (range ⇑P.root)

Tactic:
simpa

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

Goal state before:
pp: case hy
ι : 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)
⊢ (span S (range ⇑P.root)).subtype ⟨y, hy⟩ ∈ span S (range ⇑P.root)

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: 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 : v x ≤ 1
hx' : v x < 1
⊢ v x < v 1

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: 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 : v' x ≤ 1
hx' : v' x < 1
⊢ v' x < v' 1

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case mp
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : v.IsEquiv v'
x : K
⊢ v x < 1 ↔ v' x < 1

Tactic:
h.lt_one_iff_lt_one

Goal state after:
case mp
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : v.IsEquiv v'
x : K
⊢ v' x < 1 ↔ v' x < 1
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✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i : ι
c : S
hc :
  ∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) =
    ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) * c
⊢ ∃ y, (P.PolarizationIn S) y = c • 2 • (P.PolarizationIn S) (P.rootSpanMem S i)

Tactic:
use c • 2 • (P.rootSpanMem S i)

Goal state after:
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
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i : ι
c : S
hc :
  ∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) =
    ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) * c
⊢ (P.PolarizationIn S) (c • 2 • P.rootSpanMem S i) = c • 2 • (P.PolarizationIn S) (P.rootSpanMem S i)
Module: Mathlib.LinearAlgebra.RootSystem.Basic

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✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)
i j : ι
⊢ coroot j - (p (root i)) (coroot j) • coroot i = coroot ((RootPairing.equiv_of_mapsTo p root coroot i hr hp) j)

Tactic:
by
    refine (coroot_eq_coreflection_of_root_eq' p root coroot hp hr hc ?_).symm
    rw [equiv_of_mapsTo_apply, (exist_eq_reflection_of_mapsTo p root coroot i j hr).choose_spec]

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
inst✝³ : CharZero R
inst✝² : IsAddTorsionFree M
inst✝¹ : P.IsReduced
n : ℕ
inst✝ : n.AtLeastTwo
j : ι
hj : P.root j = n • P.root j
⊢ 1 • P.root j = ↑n • P.root j

Tactic:
simpa

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
inst✝³ : CharZero R
inst✝² : IsAddTorsionFree M
inst✝¹ : P.IsReduced
n : ℕ
inst✝ : n.AtLeastTwo
i j : ι
hj : P.root j = n • P.root i
this : n • P.root i = -1 • P.root i
⊢ ↑n • P.root i = -1 • P.root i

Tactic:
simpa

Goal state after:
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
⊢ P.coroot i = (2 / (P.RootForm (P.root i)) (P.root i)) • P.Polarization (P.root i)

Tactic:
← (smul_right_injective N h₀).eq_iff,

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
⊢ (P.RootForm (P.root i)) (P.root i) • P.coroot i =
    (P.RootForm (P.root i)) (P.root i) • (2 / (P.RootForm (P.root i)) (P.root i)) • P.Polarization (P.root i)
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 ≤ ((P.posRootForm S).posForm x) x

Tactic:
← this

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:
simpa

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 (⇑α) β)
hα : ¬α.IsZero
x' : L := ⋯.choose
h : x' ∈ rootSpace H ⇑(chainTop (⇑α) β) ∧ x' ≠ 0
⊢ ⟨x', ⋯⟩ ≠ 0

Tactic:
by simpa using h.2

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
S : Type u_5
i j : ι
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : P.IsReduced
inst✝ : IsTorsionFree R N
⊢ P.flip.IsReduced

Tactic:
by
  refine ⟨fun i j h ↦ ?_⟩
  rcases eq_or_ne i j with rfl | hij; · tauto
  right
  rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight_flip,
    coxeterWeight_eq_four_iff_not_linearIndependent, IsReduced.linearIndependent_iff] at h
  push Not at h
  simp [P.root_eq_neg_iff.mp (h hij)]

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}
hsxy : sxy ⊆ ⋃ i ∈ s, ↑(p i)
f : ↑sxy → ι
hf : ∀ (z : ↑sxy), ↑z ∈ ⋃ (_ : f z ∈ s), ↑(p (f z))
hf' : MapsTo f univ ↑s
key : ↑s.card < sxy.encard
⊢ (↑s).encard < univ.encard

Tactic:
simpa

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
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
⊢ P.pairing i j = -1 ∧ P.pairing j i = -4 ↔ P.root j = -2 • P.root i

Tactic:
simpa [neg_smul, ← neg_eq_iff_eq_neg] using P.pairing_one_four_iff' i (P.reflectionPerm j j) h2

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
inst✝¹ : Finite ι
inst✝ : Infinite K
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
i : ι
contra : ∀ (x : Dual K M), ((Dual.eval K M) (v i)) x = 0
⊢ False

Tactic:
simp_rw [Dual.eval_apply, forall_dual_apply_eq_zero_iff] at contra

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝⁴ : Field K
inst✝³ : AddCommGroup M
inst✝² : Module K M
inst✝¹ : Finite ι
inst✝ : Infinite K
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
i : ι
contra : v i = 0
⊢ False
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case a
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
e : chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β < chainLength α β
⊢ rootSpace H (-↑((chainBotCoeff (⇑α) β).succ + chainTopCoeff (⇑α) β) • ⇑α + ↑(chainTopCoeff (⇑α) β) • ⇑α + ⇑β) = ⊥

Tactic:
← add_smul,

Goal state after:
case a
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
e : chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β < chainLength α β
⊢ rootSpace H ((-↑((chainBotCoeff (⇑α) β).succ + chainTopCoeff (⇑α) β) + ↑(chainTopCoeff (⇑α) β)) • ⇑α + ⇑β) = ⊥
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
n : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α) β
this : rootSpace H (-↑(n + chainTopCoeff (⇑α) β) • ⇑α + ↑(chainTopCoeff (⇑α) β) • ⇑α + ⇑β) = ⊥
⊢ rootSpace H (-↑n • ⇑α + ⇑β) = ⊥

Tactic:
← add_smul,

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
n : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α) β
this : rootSpace H ((-↑(n + chainTopCoeff (⇑α) β) + ↑(chainTopCoeff (⇑α) β)) • ⇑α + ⇑β) = ⊥
⊢ rootSpace H (-↑n • ⇑α + ⇑β) = ⊥
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case mpr
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
k : ℕ
h₁ : ↑(chainTopCoeff (⇑α) β) - ↑k ≤ ↑(chainTopCoeff (⇑α) β)
h₂ : k ≤ chainLength α β
this : rootSpace H (-↑k • ⇑α + ↑(chainTopCoeff (⇑α) β) • ⇑α + ⇑β) ≠ ⊥
⊢ rootSpace H ((↑(chainTopCoeff (⇑α) β) - ↑k) • ⇑α + ⇑β) ≠ ⊥

Tactic:
← add_smul,

Goal state after:
case mpr
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
k : ℕ
h₁ : ↑(chainTopCoeff (⇑α) β) - ↑k ≤ ↑(chainTopCoeff (⇑α) β)
h₂ : k ≤ chainLength α β
this : rootSpace H ((-↑k + ↑(chainTopCoeff (⇑α) β)) • ⇑α + ⇑β) ≠ ⊥
⊢ rootSpace H ((↑(chainTopCoeff (⇑α) β) - ↑k) • ⇑α + ⇑β) ≠ ⊥
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case a
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
β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
⊢ rootSpace H ((↑(chainTopCoeff (⇑α) β) - n) • ⇑α + n • ⇑α + ⇑β) ≠ ⊥

Tactic:
← add_smul,

Goal state after:
case a
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
β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
⊢ rootSpace H ((↑(chainTopCoeff (⇑α) β) - n + n) • ⇑α + ⇑β) ≠ ⊥
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case h₂
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
inst✝ : Nontrivial L
hα : α.IsNonZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) 0)
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α 0)
k : K
hk : k • f = ((toEnd K L L) f ^ (chainTopCoeff (⇑α) 0 + 1)) x
⊢ ¬1 < chainTopCoeff (⇑α) 0

Tactic:
apply_fun (⁅f, ·⁆) at hk

Goal state after:
case h₂
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
inst✝ : Nontrivial L
hα : α.IsNonZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) 0)
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α 0)
k : K
hk : ⁅f, k • f⁆ = ⁅f, ((toEnd K L L) f ^ (chainTopCoeff (⇑α) 0 + 1)) x⁆
⊢ ¬1 < chainTopCoeff (⇑α) 0
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case inr
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
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
H : k • 2 = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
rcases (chainLength α β).even_or_odd with (⟨n, hn⟩ | ⟨n, hn⟩)

Goal state after:
case inr.inl
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
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
H : k • 2 = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
n : ℕ
hn : chainLength α β = n + n
⊢ k = -1 ∨ k = 0 ∨ k = 1

case inr.inr
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
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
H : k • 2 = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
n : ℕ
hn : chainLength α β = 2 * n + 1
⊢ k = -1 ∨ k = 0 ∨ k = 1
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case weightMap
ι : 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
f g : P.End
hfg : MulOpposite.op f.coweightMap = MulOpposite.op g.coweightMap
x : M
⊢ f.weightMap x = g.weightMap x

Tactic:
rw [MulOpposite.op_inj] at hfg

Goal state after:
case weightMap
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
⊢ f.weightMap x = g.weightMap x
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case indexEquiv
ι : 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
f g : P.End
hfg : MulOpposite.op f.coweightMap = MulOpposite.op g.coweightMap
x : ι
⊢ f.indexEquiv x = g.indexEquiv x

Tactic:
rw [MulOpposite.op_inj] at hfg

Goal state after:
case indexEquiv
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
⊢ f.indexEquiv x = g.indexEquiv x