mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_6
K₁ : Type u_7
K₂ : Type u_8
K₃ : Type u_9
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K₁
inst✝¹³ : Field K₂
inst✝¹² : Field K₃
inst✝¹¹ : Algebra F K₁
inst✝¹⁰ : Algebra F K₂
inst✝⁹ : Algebra F K₃
inst✝⁸ : Algebra K₁ K₂
inst✝⁷ : Algebra K₁ K₃
inst✝⁶ : Algebra K₂ K₃
inst✝⁵ : IsScalarTower F K₁ K₃
inst✝⁴ : IsScalarTower F K₁ K₂
inst✝³ : IsScalarTower F K₂ K₃
inst✝² : IsScalarTower K₁ K₂ K₃
inst✝¹ : Normal F K₁
inst✝ : Normal F K₂
f : Gal(K₃/F)
x : K₁
⊢ (algebraMap K₁ K₃) (((AlgEquiv.restrictNormalHom K₁) f) x) =
    (algebraMap K₁ K₃) ((((AlgEquiv.restrictNormalHom K₁).comp (AlgEquiv.restrictNormalHom K₂)) f) x)

Tactic:
IsScalarTower.algebraMap_eq K₁ K₂ K₃

Goal state after:
F : Type u_6
K₁ : Type u_7
K₂ : Type u_8
K₃ : Type u_9
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K₁
inst✝¹³ : Field K₂
inst✝¹² : Field K₃
inst✝¹¹ : Algebra F K₁
inst✝¹⁰ : Algebra F K₂
inst✝⁹ : Algebra F K₃
inst✝⁸ : Algebra K₁ K₂
inst✝⁷ : Algebra K₁ K₃
inst✝⁶ : Algebra K₂ K₃
inst✝⁵ : IsScalarTower F K₁ K₃
inst✝⁴ : IsScalarTower F K₁ K₂
inst✝³ : IsScalarTower F K₂ K₃
inst✝² : IsScalarTower K₁ K₂ K₃
inst✝¹ : Normal F K₁
inst✝ : Normal F K₂
f : Gal(K₃/F)
x : K₁
⊢ ((algebraMap K₂ K₃).comp (algebraMap K₁ K₂)) (((AlgEquiv.restrictNormalHom K₁) f) x) =
    ((algebraMap K₂ K₃).comp (algebraMap K₁ K₂))
      ((((AlgEquiv.restrictNormalHom K₁).comp (AlgEquiv.restrictNormalHom K₂)) f) x)
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
⊢ IsSplittingField K (↥F) p ↔ (Polynomial.map (algebraMap K ↥F) p).Splits ∧ F = adjoin K (p.rootSet L)

Tactic:
by
  suffices _ → (Algebra.adjoin K (p.rootSet F) = ⊤ ↔ F = adjoin K (p.rootSet L)) by
    exact ⟨fun h ↦ ⟨h.1, (this h.1).mp h.2⟩, fun h ↦ ⟨h.1, (this h.1).mpr h.2⟩⟩
  rw [← toSubalgebra_injective.eq_iff,
      adjoin_toSubalgebra_of_isAlgebraic fun x ↦ isAlgebraic_of_mem_rootSet]
  refine fun hp ↦ (hp.adjoin_rootSet_eq_range F.val).symm.trans ?_
  rw [← F.range_val, eq_comm]

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
⊢ finrank F ↥K = 1 ↔ K = ⊥

Tactic:
by
  rw [← toSubalgebra_inj, ← finrank_eq_finrank_subalgebra, Subalgebra.finrank_eq_one_iff,
    bot_toSubalgebra]

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
⊢ K' = K

Tactic:
have dvd_g : minpoly K' α ∣ g.toSubring K'.toSubring (subset_adjoin F _) := by
    apply minpoly.dvd
    rw [aeval_def, eval₂_eq_eval_map]
    erw [g.map_toSubring K'.toSubring]
    rw [eval_map_algebraMap]
    exact minpoly.aeval K α

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯
⊢ K' = K
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case insert
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
⊢ ∀ (l : ι),
    ∃ k,
      ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) (y + z) ∈
        (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)

Tactic:
intro l

Goal state after:
case insert
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
⊢ ∃ k,
    ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) (y + z) ∈
      (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case succ
R : Type u_1
L : Type u_2
M : Type u_3
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 e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih : ⁅h, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((toEnd R L M) f ^ n) m
⊢ ⁅h, ⁅f, ((toEnd R L M) f ^ n) m⁆⁆ = (μ - 2 * (↑n + ↑1)) • ⁅f, ((toEnd R L M) f ^ n) m⁆

Tactic:
Nat.cast_one,

Goal state after:
case succ
R : Type u_1
L : Type u_2
M : Type u_3
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 e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih : ⁅h, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((toEnd R L M) f ^ n) m
⊢ ⁅h, ⁅f, ((toEnd R L M) f ^ n) m⁆⁆ = (μ - 2 * (↑n + 1)) • ⁅f, ((toEnd R L M) f ^ n) m⁆
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : Type u_2
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
χ : L → R
m : M
⊢ m ∈ ↑(genWeightSpace M (χ ∘ ⇑⊤.incl)) ↔ m ∈ ↑(genWeightSpace M χ)

Tactic:
simp only [mem_genWeightSpace, LieSubmodule.mem_toSubmodule, Subtype.forall]

Goal state after:
R : Type u_2
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
χ : L → R
m : M
⊢ (∀ (a : L) (b : a ∈ ⊤), ∃ k, (((toEnd R (↥⊤) M) ⟨a, b⟩ - (χ ∘ ⇑⊤.incl) ⟨a, b⟩ • 1) ^ k) m = 0) ↔
    ∀ (x : L), ∃ k, (((toEnd R L M) x - χ x • 1) ^ k) m = 0
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case succ
R : Type u_1
L : Type u_2
M : Type u_3
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 e f : L
m : M
μ : R
t : IsSl2Triple h e f
hm : ⁅h, m⁆ = μ • m
n : ℕ
ih : ⁅h, ((toEnd R L M) e ^ n) m⁆ = (μ + 2 * ↑n) • ((toEnd R L M) e ^ n) m
⊢ ⁅h, ⁅e, ((toEnd R L M) e ^ n) m⁆⁆ = (μ + 2 * (↑n + ↑1)) • ⁅e, ((toEnd R L M) e ^ n) m⁆

Tactic:
Nat.cast_one,

Goal state after:
case succ
R : Type u_1
L : Type u_2
M : Type u_3
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 e f : L
m : M
μ : R
t : IsSl2Triple h e f
hm : ⁅h, m⁆ = μ • m
n : ℕ
ih : ⁅h, ((toEnd R L M) e ^ n) m⁆ = (μ + 2 * ↑n) • ((toEnd R L M) e ^ n) m
⊢ ⁅h, ⁅e, ((toEnd R L M) e ^ n) m⁆⁆ = (μ + 2 * (↑n + 1)) • ⁅e, ((toEnd R L M) e ^ n) m⁆
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
inst✝² : LieRing.IsNilpotent ↥H
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
this : x ∈ corootSpace α ↔ ↑x ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α)
⊢ ↑x ∈
      Submodule.map (↑H.toLieSubmodule.incl)
        (Submodule.map
          (↑(LieModuleHom.codRestrict H.toLieSubmodule ((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯))
              ⋯))
          (Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t})) ↔
    ↑x ∈ Submodule.span R {x | ∃ y ∈ ↑(rootSpace H α), ∃ z ∈ ↑(rootSpace H (-α)), ⁅y, z⁆ = x}

Tactic:
LinearMap.map_span,

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
inst✝² : LieRing.IsNilpotent ↥H
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
this : x ∈ corootSpace α ↔ ↑x ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α)
⊢ ↑x ∈
      Submodule.span R
        (⇑↑H.toLieSubmodule.incl ''
          ⇑↑(LieModuleHom.codRestrict H.toLieSubmodule ((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯))
                  ⋯) ''
            {t | ∃ m n, m ⊗ₜ[R] n = t}) ↔
    ↑x ∈ Submodule.span R {x | ∃ y ∈ ↑(rootSpace H α), ∃ z ∈ ↑(rootSpace H (-α)), ⁅y, z⁆ = x}
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v : V
⊢ B₂ ((↑(B₂.toDual b₂).symm ∘ₗ B₁) v) = B₁ v

Tactic:
simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply]

Goal state after:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v : V
⊢ B₂ ((B₂.toDual b₂).symm (B₁ v)) = B₁ v
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ IsAtomistic α

Tactic:
refine CompleteLattice.isAtomistic_iff.2 fun a ↦ ?_

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
⊢ ∃ s, a = sSup s ∧ ∀ a ∈ s, IsAtom a
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
⊢ (B v).domRestrict W = 0 ∧ v ∈ W

Tactic:
refine ⟨?_, hv⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
⊢ (B v).domRestrict W = 0
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
| finrank K ↥(domRestrict B W).ker + finrank K ↥(domRestrict B W).range +
    finrank K ↥(domRestrict B W).range.dualCoannihilator

Tactic:
add_comm (finrank K (LinearMap.ker (B.domRestrict W))),

Goal state after:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
| finrank K ↥(domRestrict B W).range + finrank K ↥(domRestrict B W).ker +
    finrank K ↥(domRestrict B W).range.dualCoannihilator
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
hB₀ : B.IsRefl
h : Disjoint W (B.orthogonal W)
⊢ finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤) ≤ finrank K ↥(W ⊔ B.orthogonal W) + finrank K ↥(W ⊓ B.orthogonal W)

Tactic:
finrank_sup_add_finrank_inf_eq,

Goal state after:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
hB₀ : B.IsRefl
h : Disjoint W (B.orthogonal W)
⊢ finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤) ≤ finrank K ↥W + finrank K ↥(B.orthogonal W)
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
this : W ⊓ B.orthogonal W = ⊥
⊢ finrank K V ≤ finrank K ↥(W ⊔ B.orthogonal W) + finrank K ↥(W ⊓ B.orthogonal W)

Tactic:
finrank_sup_add_finrank_inf_eq,

Goal state after:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
this : W ⊓ B.orthogonal W = ⊥
⊢ finrank K V ≤ finrank K ↥W + finrank K ↥(B.orthogonal W)
Module: Mathlib.Algebra.Lie.Weights.Linear

Goal state before:
pp: k : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : LieRing L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieRing.IsNilpotent L
inst✝⁷ : Field k
inst✝⁶ : LieAlgebra k L
inst✝⁵ : Module k M
inst✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
⊢ ∃ χ, Nontrivial ↥(weightSpace M ⇑χ)

Tactic:
by
  obtain ⟨χ⟩ : Nonempty (Weight k L M) := by
    by_contra! contra
    simpa only [iSup_of_empty, bot_ne_top] using LieModule.iSup_genWeightSpace_eq_top' k L M
  obtain ⟨m, hm₀, hm⟩ := exists_forall_lie_eq_smul k L M χ
  simp only [LieSubmodule.nontrivial_iff_ne_bot, LieSubmodule.eq_bot_iff, ne_eq, not_forall]
  exact ⟨χ.toLinear, m, by simpa [mem_weightSpace], hm₀⟩

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : 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 z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
⊢ ⁅y, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
induction hy using lieSpan_induction generalizing z with
  | mem u hu =>
    obtain ⟨i, rfl⟩ := hu
    exact LieSubmodule.mem_sup_left <| this i z hz
  | zero => simp
  | add u v _ _ hu hv => rw [add_lie]; exact add_mem (hu hz) (hv hz)
  | smul t u _ hu => rw [smul_lie]; exact SMulMemClass.smul_mem t (hu hz)
  | lie u v hu hv hu' hv' =>
    rw [lie_lie]
    apply sub_mem
    · obtain ⟨yc, hyc, yl, hyl, yu, hyu, aux⟩ :
        ∃ᵉ (yc ∈ H) (yl ∈ lieSpan R L (range b.f)) (yu ∈ lieSpan R L (range b.e)),
        yc + yl + yu = ⁅v, z⁆ := by simpa [LieSubmodule.mem_sup] using! hv' hz
      simp only [← aux, lie_add]
      repeat apply add_mem
      · rw [← lie_skew, neg_mem_iff]
        exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hu
      · exact hu' hyl
      · rw [← lie_skew, neg_mem_iff]
        exact LieSubmodule.mem_sup_right <| LieSubalgebra.lie_mem _ hyu hu
    · obtain ⟨yc, hyc, yl, hyl, yu, hyu, aux⟩ :
        ∃ᵉ (yc ∈ H) (yl ∈ lieSpan R L (range b.f)) (yu ∈ lieSpan R L (range b.e)),
        yc + yl + yu = ⁅u, z⁆ := by simpa [LieSubmodule.mem_sup] using! hu' hz
      simp only [← aux, lie_add]
      repeat apply add_mem
      · rw [← lie_skew, neg_mem_iff]
        exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hv
      · exact hv' hyl
      · rw [← lie_skew, neg_mem_iff]
        exact LieSubmodule.mem_sup_right <| LieSubalgebra.lie_mem _ hyu hv

Goal state after:
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P ∈ degreeLT R m
hp : P.natDegree = n
p_ne_zero : P = 0
⊢ P ∈ span R (↑S '' Set.Iio m)

pp: case neg
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P ∈ degreeLT R m
hp : P.natDegree = n
p_ne_zero : P ≠ 0
⊢ P ∈ span R (↑S '' Set.Iio m)

Tactic:
· simp [p_ne_zero]

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P ∈ degreeLT R m
hp : P.natDegree = n
p_ne_zero : P ≠ 0
⊢ P ∈ span R (↑S '' Set.Iio m)
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
P : R[X]
p_ne_zero : P = 0
⊢ P ∈ span R (Set.range ↑S)

pp: case neg
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
P : R[X]
p_ne_zero : P ≠ 0
⊢ P ∈ span R (Set.range ↑S)

Tactic:
· simp [p_ne_zero]

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
P : R[X]
p_ne_zero : P ≠ 0
⊢ P ∈ span R (Set.range ↑S)
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i ↦ (g i • ↑S i).degree) = ⊥
x : ℕ
left✝¹ : x ∈ s
hx : g x • ↑S x ≠ 0
y : ℕ
left✝ : y ∈ s
hy : g y • ↑S y ≠ 0
xney : x ≠ y
zgx : g x ≠ 0
zgy : g y ≠ 0
⊢ (Ne on fun i ↦ (g i • ↑S i).degree) x y

Tactic:
have rx : IsRightRegular (S x).leadingCoeff := IsRegular.of_ne_zero (by simp) |>.right

Goal state after:
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i ↦ (g i • ↑S i).degree) = ⊥
x : ℕ
left✝¹ : x ∈ s
hx : g x • ↑S x ≠ 0
y : ℕ
left✝ : y ∈ s
hy : g y • ↑S y ≠ 0
xney : x ≠ y
zgx : g x ≠ 0
zgy : g y ≠ 0
rx : IsRightRegular (↑S x).leadingCoeff
⊢ (Ne on fun i ↦ (g i • ↑S i).degree) x y
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
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
z : L
hz : z ∈ lowerCentralSeries R L L 1
hzc : z ∈ LieAlgebra.center R L
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
this : (algebraMap R A) ((trace R M) (φ z ∘ₗ φ x)) = (algebraMap R A) 0
that : IsTorsionFree R A
⊢ (trace R M) (φ z ∘ₗ φ x) = 0

Tactic:
exact FaithfulSMul.algebraMap_injective R A this

Goal state after:
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
I : LieIdeal R L
inst✝⁴ : Free R L
inst✝³ : Module.Finite R L
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsLieAbelian ↥I
⊢ I ≤ killingCompl R L ⊤

Tactic:
intro x (hx : x ∈ I)

Goal state after:
R : Type u_1
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
I : LieIdeal R L
inst✝⁴ : Free R L
inst✝³ : Module.Finite R L
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsLieAbelian ↥I
x : L
hx : x ∈ I
⊢ x ∈ killingCompl R L ⊤
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
I : LieIdeal R L
inst✝⁴ : Free R L
inst✝³ : Module.Finite R L
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsLieAbelian ↥I
x : L
hx : x ∈ I
y : L
⊢ (trace R L) ((LieModule.toEnd R L L) y ∘ₗ (LieModule.toEnd R L L) x) = 0

Tactic:
exact LieSubmodule.traceForm_eq_zero_of_isTrivial I I (by simp) _ hx

Goal state after:
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x y : L
hxy : ∀ (χ : Weight K L M), MapsTo ⇑((toEnd K L M) x ∘ₗ (toEnd K L M) y) ↑(genWeightSpace M ⇑χ) ↑(genWeightSpace M ⇑χ)
hds : DirectSum.IsInternal fun i ↦ ↑(genWeightSpace M ⇑i)
⊢ ∑ i, (trace K ↥↑(genWeightSpace M ⇑i)) (((toEnd K L M) x ∘ₗ (toEnd K L M) y).restrict ⋯) =
    ∑ χ, finrank K ↥(genWeightSpace M ⇑χ) • (χ x * χ y)

Tactic:
← traceForm_genWeightSpace_eq K L M _ x y

Goal state after:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x y : L
hxy : ∀ (χ : Weight K L M), MapsTo ⇑((toEnd K L M) x ∘ₗ (toEnd K L M) y) ↑(genWeightSpace M ⇑χ) ↑(genWeightSpace M ⇑χ)
hds : DirectSum.IsInternal fun i ↦ ↑(genWeightSpace M ⇑i)
⊢ ∑ i, (trace K ↥↑(genWeightSpace M ⇑i)) (((toEnd K L M) x ∘ₗ (toEnd K L M) y).restrict ⋯) =
    ∑ x_1, ((traceForm K L ↥(genWeightSpace M ⇑x_1)) x) y
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
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
⊢ α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) ≠ 0

Tactic:
contrapose hα
  suffices (cartanEquivDual H).symm α ∈ α.ker ⊓ corootSpace α by
    rw [(disjoint_ker_weight_corootSpace α).eq_bot] at this
    simpa using this
  exact Submodule.mem_inf.mp ⟨hα, cartanEquivDual_symm_apply_mem_corootSpace α⟩

Goal state after: