mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
⊢ IsLieAbelian ↥(radical R L) ↔ ∀ (I : LieIdeal R L), IsSolvable ↥I → IsLieAbelian ↥I

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
⊢ IsLieAbelian ↥(radical R L) → ∀ (I : LieIdeal R L), IsSolvable ↥I → IsLieAbelian ↥I

case mpr
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
⊢ (∀ (I : LieIdeal R L), IsSolvable ↥I → IsLieAbelian ↥I) → IsLieAbelian ↥(radical R L)
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
q : ℚ≥0
x : f.SplittingField
p : MvPolynomial (SplittingFieldAux f.natDegree f) K
⊢ (fun x ↦ q • x) p = (fun x1 x2 ↦ x1 * x2) ((algebraMap K (MvPolynomial (SplittingFieldAux f.natDegree f) K)) ↑q) p

Tactic:
ext

Goal state after:
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
q : ℚ≥0
x : f.SplittingField
p : MvPolynomial (SplittingFieldAux f.natDegree f) K
m✝ : SplittingFieldAux f.natDegree f →₀ ℕ
⊢ MvPolynomial.coeff m✝ ((fun x ↦ q • x) p) =
    MvPolynomial.coeff m✝
      ((fun x1 x2 ↦ x1 * x2) ((algebraMap K (MvPolynomial (SplittingFieldAux f.natDegree f) K)) ↑q) p)
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
q : ℚ
x : f.SplittingField
p : MvPolynomial (SplittingFieldAux f.natDegree f) K
⊢ (fun x ↦ q • x) p = (fun x1 x2 ↦ x1 * x2) ((algebraMap K (MvPolynomial (SplittingFieldAux f.natDegree f) K)) ↑q) p

Tactic:
ext

Goal state after:
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
q : ℚ
x : f.SplittingField
p : MvPolynomial (SplittingFieldAux f.natDegree f) K
m✝ : SplittingFieldAux f.natDegree f →₀ ℕ
⊢ MvPolynomial.coeff m✝ ((fun x ↦ q • x) p) =
    MvPolynomial.coeff m✝
      ((fun x1 x2 ↦ x1 * x2) ((algebraMap K (MvPolynomial (SplittingFieldAux f.natDegree f) K)) ↑q) p)
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map (↑(MvPolynomial.aeval fun fi ↦ if hf : fi.fst ∈ s then (↑((finEquivRoots ⋯) fi.snd)).1 else 37))
            (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f) -
          ∏ x, (X - C (↑x).1)).coeff
      n =
    0

Tactic:
Finset.prod_coe_sort (f := fun x : _ × ℕ ↦ X - C x.1),

Goal state after:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map (↑(MvPolynomial.aeval fun fi ↦ if hf : fi.fst ∈ s then (↑((finEquivRoots ⋯) fi.snd)).1 else 37))
            (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f) -
          ∏ i ∈ (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots.toEnumFinset, (X - C i.1)).coeff
      n =
    0
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
q : ℚ≥0
x : AlgebraicClosure k
p : MvPolynomial (Vars k) k
⊢ (fun x ↦ q • x) p = (fun x1 x2 ↦ x1 * x2) ((algebraMap k (MvPolynomial (Vars k) k)) ↑q) p

Tactic:
ext

Goal state after:
k : Type u
inst✝ : Field k
q : ℚ≥0
x : AlgebraicClosure k
p : MvPolynomial (Vars k) k
m✝ : Vars k →₀ ℕ
⊢ MvPolynomial.coeff m✝ ((fun x ↦ q • x) p) =
    MvPolynomial.coeff m✝ ((fun x1 x2 ↦ x1 * x2) ((algebraMap k (MvPolynomial (Vars k) k)) ↑q) p)
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
q : ℚ
x : AlgebraicClosure k
p : MvPolynomial (Vars k) k
⊢ (fun x ↦ q • x) p = (fun x1 x2 ↦ x1 * x2) ((algebraMap k (MvPolynomial (Vars k) k)) ↑q) p

Tactic:
ext

Goal state after:
k : Type u
inst✝ : Field k
q : ℚ
x : AlgebraicClosure k
p : MvPolynomial (Vars k) k
m✝ : Vars k →₀ ℕ
⊢ MvPolynomial.coeff m✝ ((fun x ↦ q • x) p) =
    MvPolynomial.coeff m✝ ((fun x1 x2 ↦ x1 * x2) ((algebraMap k (MvPolynomial (Vars k) k)) ↑q) p)
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
f : Monics k
⊢ map (algebraMap k (AlgebraicClosure k)) ↑f = ∏ i, map (Ideal.Quotient.mk (maxIdeal k)) (X - C (MvPolynomial.X ⟨f, i⟩))

Tactic:
ext

Goal state after:
k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (map (algebraMap k (AlgebraicClosure k)) ↑f).coeff n✝ =
    (∏ i, map (Ideal.Quotient.mk (maxIdeal k)) (X - C (MvPolynomial.X ⟨f, i⟩))).coeff n✝
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : AddCommMonoid M₂
inst✝¹ : Algebra R A
inst✝ : Module R M₂
⊢ BilinForm.baseChange A 0 = 0

Tactic:
ext

Goal state after:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : AddCommMonoid M₂
inst✝¹ : Algebra R A
inst✝ : Module R M₂
x✝¹ x✝ : M₂
⊢ ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (BilinForm.baseChange A 0)) 1) x✝¹)) 1) x✝ =
    ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry 0) 1) x✝¹)) 1) x✝
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module.Free R M₁
inst✝² : Module.Finite R M₁
inst✝¹ : Module.Free R M₂
inst✝ : Module.Finite R M₂
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
⊢ ((AlgebraTensorModule.curry ↑(tensorDistribEquiv R)) B₁) B₂ = ((AlgebraTensorModule.curry (tensorDistrib R R)) B₁) B₂

Tactic:
ext

Goal state after:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module.Free R M₁
inst✝² : Module.Finite R M₁
inst✝¹ : Module.Free R M₂
inst✝ : Module.Finite R M₂
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
x✝³ : M₁
x✝² : M₂
x✝¹ : M₁
x✝ : M₂
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry (((AlgebraTensorModule.curry ↑(tensorDistribEquiv R)) B₁) B₂)) x✝³) x✝²))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (tensorDistrib R R)) B₁) B₂)) x✝³) x✝²))
        x✝¹)
      x✝
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : IsKilling R L
inst✝³ : Module.Free R L
inst✝² : Module.Finite R L
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ IsLieAbelian L ↔ Subsingleton L

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : IsKilling R L
inst✝³ : Module.Free R L
inst✝² : Module.Finite R L
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ IsLieAbelian L → Subsingleton L

case mpr
R : Type u_1
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : IsKilling R L
inst✝³ : Module.Free R L
inst✝² : Module.Finite R L
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ Subsingleton L → IsLieAbelian L
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
⊢ IsKilling R L'

Tactic:
constructor

Goal state after:
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
⊢ LieIdeal.killingCompl R L' ⊤ = ⊥
Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
⊢ f = 0 ↔ ∀ (μ : K), f.HasEigenvalue μ → μ = 0

Tactic:
constructor

Goal state after:
case mp
K : Type u_3
V : Type u_4
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
⊢ f = 0 → ∀ (μ : K), f.HasEigenvalue μ → μ = 0

case mpr
K : Type u_3
V : Type u_4
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
⊢ (∀ (μ : K), f.HasEigenvalue μ → μ = 0) → f = 0
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case mem.inr
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
x u : L
hu✝ : u ∈ range b.e ∪ range b.f
hu : u ∈ range b.f
⊢ u ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
· exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| subset_lieSpan hu

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = ↑u
f : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun x ↦
      match x with
      | ⟨m, hm⟩ => ⟨⁅y, m⁆, ⋯⟩,
    map_add' := ⋯, map_smul' := ⋯ }
g : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun x ↦
      match x with
      | ⟨m, hm⟩ => ⟨⁅z, m⁆, ⋯⟩,
    map_add' := ⋯, map_smul' := ⋯ }
⊢ (toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) u = ⁅f, g⁆

Tactic:
ext

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = ↑u
f : End R ↥(genWeightSpaceChain M α χ p q) := ⋯
g : End R ↥(genWeightSpaceChain M α χ p q) := ⋯
x✝ : ↥(genWeightSpaceChain M α χ p q)
⊢ ↑(((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) u) x✝) = ↑(⁅f, g⁆ x✝)
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Free R M
inst✝² : Module.Finite R M
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ traceForm A (A ⊗[R] L) (A ⊗[R] M) = LinearMap.BilinForm.baseChange A (traceForm R L M)

Tactic:
ext

Goal state after:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Free R M
inst✝² : Module.Finite R M
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Algebra R A
x✝¹ x✝ : L
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry (traceForm A (A ⊗[R] L) (A ⊗[R] M))) 1) x✝¹))
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry (LinearMap.BilinForm.baseChange A (traceForm R L M))) 1) x✝¹))
        1)
      x✝
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: case mem
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x a b c : L
hbc : ⁅φ b, y⁆ = -φ c
⊢ (trace R M) (⁅φ a, φ b⁆ * y) = 0

Tactic:
LinearMap.trace_lie_mul_eq,

Goal state after:
case mem
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x a b c : L
hbc : ⁅φ b, y⁆ = -φ c
⊢ (trace R M) (φ a * ⁅φ b, y⁆) = 0
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ chainTop (-α) β = chainBot α β

Tactic:
ext

Goal state after:
R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
x✝ : L
⊢ (chainTop (-α) β) x✝ = (chainBot α β) x✝
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ chainBot (-α) β = chainTop α β

Tactic:
ext

Goal state after:
R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
x✝ : L
⊢ (chainBot (-α) β) x✝ = (chainTop α β) x✝
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
β : Weight R L M
⊢ chainTop 0 β = β

Tactic:
ext

Goal state after:
R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
β : Weight R L M
x✝ : L
⊢ (chainTop 0 β) x✝ = β x✝
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
β : Weight R L M
⊢ chainBot 0 β = β

Tactic:
ext

Goal state after:
R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
β : Weight R L M
x✝ : L
⊢ (chainBot 0 β) x✝ = β x✝
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_4
N : Type u_5
N' : Type u_6
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup M'
inst✝⁶ : AddCommGroup N'
inst✝⁵ : CommRing R
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R N
inst✝¹ : Module R N'
eM : M' ≃ₗ[R] M
eN : N' ≃ₗ[R] N
q : M' →ₗ[R] N' →ₗ[R] R
inst✝ : (q.compl₁₂ ↑eM.symm ↑eN.symm).IsPerfPair
⊢ q = (q.compl₁₂ ↑eM.symm ↑eN.symm).compl₁₂ ↑eM ↑eN

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_3
M' : Type u_4
N : Type u_5
N' : Type u_6
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup M'
inst✝⁶ : AddCommGroup N'
inst✝⁵ : CommRing R
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R N
inst✝¹ : Module R N'
eM : M' ≃ₗ[R] M
eN : N' ≃ₗ[R] N
q : M' →ₗ[R] N' →ₗ[R] R
inst✝ : (q.compl₁₂ ↑eM.symm ↑eN.symm).IsPerfPair
x✝¹ : M'
x✝ : N'
⊢ (q x✝¹) x✝ = (((q.compl₁₂ ↑eM.symm ↑eN.symm).compl₁₂ ↑eM ↑eN) x✝¹) x✝
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
V : Submodule R N
h : p.IsPerfectCompl ⊤ V
⊢ V = ⊤

pp: case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
V : Submodule R N
h : V = ⊤
⊢ p.IsPerfectCompl ⊤ V

Tactic:
· exact eq_top_of_isCompl_bot <| by simpa using h.isCompl_right

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
V : Submodule R N
h : V = ⊤
⊢ p.IsPerfectCompl ⊤ V
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ ↑(e ≪≫ₗ e.flip.symm.dualMap) = Dual.eval R N

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
x✝¹ : N
x✝ : Dual R N
⊢ (↑(e ≪≫ₗ e.flip.symm.dualMap) x✝¹) x✝ = ((Dual.eval R N) x✝¹) x✝
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ IsReflexive R N

Tactic:
constructor

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ Bijective ⇑(Dual.eval R N)
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
h : IsReflexive R N
⊢ e.flip.flip = e

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
h : IsReflexive R N
x✝¹ : N
x✝ : M
⊢ (e.flip.flip x✝¹) x✝ = (e x✝¹) x✝
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] Dual R M
p : Submodule R M
⊢ (map (↑e).flip p).dualCoannihilator = map (↑e.symm) p.dualAnnihilator

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] Dual R M
p : Submodule R M
x✝ : N
⊢ x✝ ∈ (map (↑e).flip p).dualCoannihilator ↔ x✝ ∈ map (↑e.symm) p.dualAnnihilator
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
B : LinearMap.BilinForm R M
m₀ : M
hm₀ : m₀ ∈ genWeightSpace M 0
hB : ∀ (x : L) (k : ℕ) (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
x : L
m₁ : M
hm₁ : m₁ ∈ posFittingCompOf R M x
⊢ (B m₀) m₁ = 0

Tactic:
simp only [mem_genWeightSpace, Pi.zero_apply, zero_smul, sub_zero] at hm₀

Goal state after:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
B : LinearMap.BilinForm R M
m₀ : M
hB : ∀ (x : L) (k : ℕ) (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
x : L
m₁ : M
hm₁ : m₁ ∈ posFittingCompOf R M x
hm₀ : ∀ (x : L), ∃ k, (φ x ^ k) m₀ = 0
⊢ (B m₀) m₁ = 0
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ α : Weight K (↥H) L
⊢ { toFun := -⇑{ toFun := -⇑α, genWeightSpace_ne_bot' := ⋯ }, genWeightSpace_ne_bot' := ⋯ } = α

Tactic:
ext

Goal state after:
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ α : Weight K (↥H) L
x✝ : ↥H
⊢ { toFun := -⇑{ toFun := -⇑α, genWeightSpace_ne_bot' := ⋯ }, genWeightSpace_ne_bot' := ⋯ } x✝ = α x✝
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
⊢ (-α).IsZero

Tactic:
ext

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
x✝ : ↥H
⊢ (-α) x✝ = 0 x✝
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: case h_comm
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
z x : L
A : Type u_1 := ⋯
hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1
hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L)
⊢ Commute ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)) ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] z))

Tactic:
exact commute_toEnd_of_mem_center_right (A ⊗[R] M) hzc (1 ⊗ₜ x)

Goal state after: