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

Goal state before:
pp: case lie.hx.a.a
ι : 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
y : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅v, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
yc : L
hyc : yc ∈ H
yl : L
hyl : yl ∈ lieSpan R L (range b.f)
yu : L
hyu : yu ∈ lieSpan R L (range b.e)
aux : yc + yl + yu = ⁅v, z⁆
⊢ ⁅yc, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
]

Goal state after:
case lie.hx.a.a
ι : 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
y : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅v, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
yc : L
hyc : yc ∈ H
yl : L
hyl : yl ∈ lieSpan R L (range b.f)
yu : L
hyu : yu ∈ lieSpan R L (range b.e)
aux : yc + yl + yu = ⁅v, z⁆
⊢ ⁅yc, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝² : Field k
K : Type ?u.6
inst✝¹ : Field K
inst✝ : DecidableEq K
i : k →+* K
f : Monics k
hf : (map i ↑f).roots.toEnumFinset.card = (↑f).natDegree
⊢ (map i ↑f).roots.toEnumFinset.card = (↑f).natDegree

Tactic:
]

Goal state after:
k : Type u
inst✝² : Field k
K : Type ?u.6
inst✝¹ : Field K
inst✝ : DecidableEq K
i : k →+* K
f : Monics k
hf : (map i ↑f).roots.toEnumFinset.card = (↑f).natDegree
⊢ (map i ↑f).roots.toEnumFinset.card = (↑f).natDegree
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 (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f -
          (Multiset.map (fun x ↦ X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod).coeff
      n =
    0

Tactic:
]

Goal state after:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f -
          (Multiset.map (fun x ↦ X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod).coeff
      n =
    0
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 : ℕ
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
⊢ ¬∃ l ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ,
      (Finsupp.linearCombination (MvPolynomial (Vars k) k) fun fn ↦ (subProdXSubC fn.1).coeff fn.2) l = 1

Tactic:
]

Goal state after:
k : Type u
inst✝ : Field k
⊢ ¬∃ l ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ,
      (Finsupp.linearCombination (MvPolynomial (Vars k) k) fun fn ↦ (subProdXSubC fn.1).coeff fn.2) l = 1
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : 0 = 1
⊢ False

pp: k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : ∑ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 1
⊢ ∀ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 0

Tactic:
]

Goal state after:
k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : 0 = 1
⊢ False

k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : ∑ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 1
⊢ ∀ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 0
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : ∑ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 1
j : Monics k × ℕ
hj : j ∈ v.support
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
q : ℚ
⊢ ↑q.num / ↑q.den = ↑q.num / ↑q.den

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : CommSemiring A
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Algebra R A
inst✝⁹ : Module R M₁
inst✝⁸ : Module A M₁
inst✝⁷ : Module R N₁
inst✝⁶ : Module A N₁
inst✝⁵ : SMulCommClass R A M₁
inst✝⁴ : IsScalarTower R A M₁
inst✝³ : SMulCommClass R A N₁
inst✝² : IsScalarTower R A N₁
inst✝¹ : Module R M₂
inst✝ : Module R N₂
B₁ : BilinMap A M₁ N₁
B₂ : BilinMap R M₂ N₂
hB₁ : ∀ (x y : M₁), (B₁ x) y = (B₁ y) x
hB₂ : ∀ (x y : M₂), (B₂ x) y = (B₂ y) x
⊢ B₁.tmul B₂ = flip (B₁.tmul B₂)

Tactic:
]

Goal state after:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : CommSemiring A
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Algebra R A
inst✝⁹ : Module R M₁
inst✝⁸ : Module A M₁
inst✝⁷ : Module R N₁
inst✝⁶ : Module A N₁
inst✝⁵ : SMulCommClass R A M₁
inst✝⁴ : IsScalarTower R A M₁
inst✝³ : SMulCommClass R A N₁
inst✝² : IsScalarTower R A N₁
inst✝¹ : Module R M₂
inst✝ : Module R N₂
B₁ : BilinMap A M₁ N₁
B₂ : BilinMap R M₂ N₂
hB₁ : ∀ (x y : M₁), (B₁ x) y = (B₁ y) x
hB₂ : ∀ (x y : M₂), (B₂ x) y = (B₂ y) x
⊢ B₁.tmul B₂ = flip (B₁.tmul B₂)
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Algebra R A
inst✝⁴ : Module R M₁
inst✝³ : Module A M₁
inst✝² : SMulCommClass R A M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ B₁.tmul B₂ = LinearMap.flip (B₁.tmul B₂)

Tactic:
]

Goal state after:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Algebra R A
inst✝⁴ : Module R M₁
inst✝³ : Module A M₁
inst✝² : SMulCommClass R A M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ B₁.tmul B₂ = LinearMap.flip (B₁.tmul B₂)
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (subProdXSubC f).coeff n✝ ∈ maxIdeal k

Tactic:
]

Goal state after:
k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (subProdXSubC f).coeff n✝ ∈ maxIdeal k
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
z : AlgebraicClosure k
p : MvPolynomial (Vars k) k
hp : (Ideal.Quotient.mk (maxIdeal k)) p = z
⊢ IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)

Tactic:
]

Goal state after:
k : Type u
inst✝ : Field k
z : AlgebraicClosure k
p : MvPolynomial (Vars k) k
hp : (Ideal.Quotient.mk (maxIdeal k)) p = z
⊢ IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)
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
I : LieIdeal R L
inst✝ : IsLieAbelian ↥I
⊢ I ≤ LieIdeal.killingCompl R L ⊤

Tactic:
]

Goal state after:
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
I : LieIdeal R L
inst✝ : IsLieAbelian ↥I
⊢ I ≤ LieIdeal.killingCompl R L ⊤
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie.hx.a
ι : 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
y : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅v, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
yc : L
hyc : yc ∈ H
yl : L
hyl : yl ∈ lieSpan R L (range b.f)
yu : L
hyu : yu ∈ lieSpan R L (range b.e)
aux : yc + yl + yu = ⁅v, z⁆
⊢ ⁅yu, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
]

Goal state after:
case lie.hx.a
ι : 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
y : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅v, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
yc : L
hyc : yc ∈ H
yl : L
hyl : yl ∈ lieSpan R L (range b.f)
yu : L
hyu : yu ∈ lieSpan R L (range b.e)
aux : yc + yl + yu = ⁅v, z⁆
⊢ ⁅yu, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: case mul_X
k : Type u
inst✝ : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k), (Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X fi) = z
⊢ IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p * (Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi))

Tactic:
]

Goal state after:
case mul_X
k : Type u
inst✝ : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k), (Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X fi) = z
⊢ IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p * (Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi))
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: 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
h : center R L = ⊤
⊢ Subsingleton L

Tactic:
]

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
h : center R L = ⊤
⊢ Subsingleton 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
inst✝⁴ : IsKilling R L
inst✝³ : Module.Free R L
inst✝² : Module.Finite R L
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
h : center R L = ⊤
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: case mul_X
k : Type u
inst✝ : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k), (Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X fi) = z
⊢ eval ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi)) (map (Ideal.Quotient.mk (maxIdeal k)) X) -
      eval ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi))
        (C ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X ⟨fi.fst, fi.snd⟩))) =
    0

Tactic:
]

Goal state after:
case mul_X
k : Type u
inst✝ : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k), (Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X fi) = z
⊢ eval ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi)) (map (Ideal.Quotient.mk (maxIdeal k)) X) -
      eval ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi))
        (C ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X ⟨fi.fst, fi.snd⟩))) =
    0
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: case mul_X
k : Type u
inst✝ : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k), (Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X fi) = z
⊢ eval ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi)) (map (Ideal.Quotient.mk (maxIdeal k)) X) -
      (Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X ⟨fi.fst, fi.snd⟩) =
    0

Tactic:
]

Goal state after:
case mul_X
k : Type u
inst✝ : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k), (Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X fi) = z
⊢ eval ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi)) (map (Ideal.Quotient.mk (maxIdeal k)) X) -
      (Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X ⟨fi.fst, fi.snd⟩) =
    0
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
f : k[X]
hf : f.Monic
x✝ : Irreducible f
⊢ (∏ i, map (Ideal.Quotient.mk (maxIdeal k)) (X - C (MvPolynomial.X ⟨⟨f, hf⟩, i⟩))).Splits

Tactic:
]

Goal state after:
k : Type u
inst✝ : Field k
f : k[X]
hf : f.Monic
x✝ : Irreducible f
⊢ (∏ i, map (Ideal.Quotient.mk (maxIdeal k)) (X - C (MvPolynomial.X ⟨⟨f, hf⟩, i⟩))).Splits
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'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
this : e.symm x' ∈ ⊥
⊢ x' ∈ ⊥

Tactic:
]

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'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
this : e.symm x' ∈ ⊥
⊢ x' ∈ ⊥
Module: Mathlib.Algebra.Lie.Derivation.Killing

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
⊢ killingForm R ↥(ad R L).idealRange =
    killingForm R ↥(LieIdeal.toLieSubalgebra R (LieDerivation R L L) (ad R L).idealRange)

Tactic:
]

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
⊢ killingForm R ↥(ad R L).idealRange =
    killingForm R ↥(LieIdeal.toLieSubalgebra R (LieDerivation R L L) (ad R L).idealRange)
Module: Mathlib.Algebra.Lie.Derivation.Killing

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : Field R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
this :
  (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule =
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule
hD :
  D ∈
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule
⊢ ⁅x, D⁆ ∈
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule

Tactic:
]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : Field R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
this :
  (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule =
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule
hD :
  D ∈
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule
⊢ ⁅x, D⁆ ∈
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule
Module: Mathlib.Algebra.Lie.Derivation.Killing

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : Field R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
this :
  (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule =
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule
hD :
  D ∈
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule
⊢ ⁅(ad R L) x, D⁆ ∈
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule

Tactic:
]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : Field R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
this :
  (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule =
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule
hD :
  D ∈
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule
⊢ ⁅(ad R L) x, D⁆ ∈
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule
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'
x' : L'
y : L
hx' : ((killingForm R L) (e.symm x')) y = 0
⊢ ((killingForm R L) (e.symm x')) y = 0 y

Tactic:
]

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'
x' : L'
y : L
hx' : ((killingForm R L) (e.symm x')) y = 0
⊢ ((killingForm R L) (e.symm x')) y = 0 y
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
this : Disjoint I (killingCompl K L I)
⊢ Disjoint I (killingCompl K L I)

Tactic:
]

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
this : Disjoint I (killingCompl K L I)
⊢ Disjoint I (killingCompl K L I)
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
this : IsLieAbelian ↥(I ⊓ killingCompl K L I)
⊢ I ⊓ killingCompl K L I = ⊥

Tactic:
]

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
this : IsLieAbelian ↥(I ⊓ killingCompl K L I)
⊢ I ⊓ killingCompl K L I = ⊥
Module: Mathlib.Algebra.Lie.Derivation.Killing

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ (ad R L) (D x) ∈
    Submodule.map (ad R L).range.subtype
      (LinearMap.ker ((killingForm R (LieDerivation R L L)).restrict (ad R L).range.toSubmodule))

Tactic:
]

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ (ad R L) (D x) ∈
    Submodule.map (ad R L).range.subtype
      (LinearMap.ker ((killingForm R (LieDerivation R L L)).restrict (ad R L).range.toSubmodule))
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
this : ∀ (x y z : L), x ∈ killingCompl K L I → y ∈ I → ((LieModule.traceForm K L L) ⁅x, y⁆) z = 0
⊢ ∀ x ∈ I ⊓ killingCompl K L I, ∀ m ∈ I ⊓ killingCompl K L I, ⁅x, m⁆ = 0

Tactic:
]

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
this : ∀ (x y z : L), x ∈ killingCompl K L I → y ∈ I → ((LieModule.traceForm K L L) ⁅x, y⁆) z = 0
⊢ ∀ x ∈ I ⊓ killingCompl K L I, ∀ m ∈ I ⊓ killingCompl K L I, ⁅x, m⁆ = 0
Module: Mathlib.Algebra.Lie.Derivation.Killing

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
x : L
h : x = 0
⊢ x = 0

Tactic:
]

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
x : L
h : x = 0
⊢ x = 0
Module: Mathlib.Algebra.Lie.Derivation.Killing

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
⊢ (ad R L).range.toSubmodule = ⊤.toSubmodule

Tactic:
]

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
⊢ (ad R L).range.toSubmodule = ⊤.toSubmodule
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
x y z : L
hx : x ∈ killingCompl K L I
hy : y ∈ I
⊢ ((LieModule.traceForm K L L) ⁅y, z⁆) x = 0

Tactic:
]

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
x y z : L
hx : x ∈ killingCompl K L I
hy : y ∈ I
⊢ ((LieModule.traceForm K L L) ⁅y, z⁆) x = 0