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

Goal state before:
pp: G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
| (∑ x ∈ s, (g • l x - l x) • (toFun G F) x) g'

Tactic:
rw [Finset.sum_apply]

Goal state after:
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
| ∑ c ∈ s, ((g • l c - l c) • (toFun G F) c) g'
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
have : (adjoin E1 (E2 : Set L)).toSubalgebra = _ := adjoin_toSubalgebra_of_isAlgebraic fun x h ↦
    IsAlgebraic.tower_top _ (isAlgebraic_iff.mp (Algebra.IsAlgebraic.isAlgebraic (⟨x, h⟩ : E2)))
  apply_fun Subalgebra.restrictScalars K at this
  rw [← restrictScalars_toSubalgebra, restrictScalars_adjoin] at this
  -- TODO: rather than using `← coe_type_toSubalgebra` here, perhaps we should restate another
  -- version of `Algebra.restrictScalars_adjoin` for intermediate fields?
  simp only [← coe_type_toSubalgebra] at this
  rw [Algebra.restrictScalars_adjoin] at this
  exact this

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

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E1
this : (E2 ⊔ E1).toSubalgebra = E2.toSubalgebra ⊔ E1.toSubalgebra
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
sup_comm (a := E1),

Goal state after:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E1
this : (E2 ⊔ E1).toSubalgebra = E2.toSubalgebra ⊔ E1.toSubalgebra
⊢ (E2 ⊔ E1).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
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
f : K[X]
inst✝ : IsSplittingField K L f
h : f.Splits
y : L
⊢ y ∈ ↑(Multiset.map (⇑(algebraMap K L)) f.roots).toFinset → y ∈ ↑⊥

Tactic:
hy

Goal state after:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : f.Splits
y : L
hy : y ∈ ↑(Multiset.map (⇑(algebraMap K L)) f.roots).toFinset
⊢ y ∈ ↑⊥
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : (map (algebraMap F L) (minpoly F a)).Splits
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, (map (algebraMap F L) (minpoly F x)).Splits
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
this✝¹ : FiniteDimensional F ↥Ks
this✝ : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra (↥Ks) L := (↑f).toAlgebra
H5 : IsIntegral (↥Ks) a
H6 : (map (algebraMap (↥Ks) L) (minpoly (↥Ks) a)).Splits
⊢ (map (algebraMap (↥Ks) L) (minpoly (↥Ks) a)).degree ≠ 0

Tactic:
simp [(minpoly.degree_pos H5).ne']

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ ↑(adjoin (↥(adjoin F S)) T) = ↑(adjoin F (S ∪ T))

Tactic:
apply subset_antisymm <;> rw [adjoin_subset_adjoin_iff]

Goal state after:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ Set.range ⇑(algebraMap (↥(adjoin F S)) E) ⊆ ↑(adjoin F (S ∪ T)) ∧ T ⊆ ↑(adjoin F (S ∪ T))

case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ Set.range ⇑(algebraMap F E) ⊆ ↑(adjoin (↥(adjoin F S)) T) ∧ S ∪ T ⊆ ↑(adjoin (↥(adjoin F S)) T)
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝¹ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this✝ : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
⊢ False

Tactic:
let L (σ : Λ) : Lifts F E K := ⟨ϕ.carrier⟮α⟯.restrictScalars F, σ.restrictScalars F⟩

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝¹ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this✝ : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : Λ → Lifts F E K := fun σ ↦ { carrier := restrictScalars F (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
⊢ False
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case left
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := ⋯
this : Fact (Irreducible (minpoly F α))
⊢ Function.Injective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)

Tactic:
exact RingHom.injective f

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 : Type u
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
S : Set K
hprim : adjoin F S = ⊤
⊢ restrictScalars F (adjoin E S) = restrictScalars F ⊤

Tactic:
rw [restrictScalars_top, ← top_le_iff, ← hprim, adjoin_le_iff,
      coe_restrictScalars, ← adjoin_le_iff]

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

Goal state before:
pp: case mem.add
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
t : IsSl2Triple h e f
x y u✝ : L
hu✝ : u✝ ∈ {e, f, h}
u v : L
hu : u ∈ span R {e, f, h}
hv : v ∈ span R {e, f, h}
hu' : ⁅u✝, u⁆ ∈ span R {e, f, h}
hv' : ⁅u✝, v⁆ ∈ span R {e, f, h}
⊢ ⁅u✝, u + v⁆ ∈ span R {e, f, h}

Tactic:
simpa only [lie_add] using add_mem hu' hv'

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

Goal state before:
pp: case mem.mem.inl.inr.inr
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
f x y u v : L
t : IsSl2Triple v u f
__spread✝⁻⁰ : Submodule R L := span R {u, f, v}
⊢ ⁅u, v⁆ ∈ span R {u, f, v}

Tactic:
rw [← lie_skew, t.lie_h_e_nsmul, neg_mem_iff]
          apply nsmul_mem <| subset_span _
          simp

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

Goal state before:
pp: case pos.add
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i ∈ s, genWeightSpace M i
hy✝ : y✝ ∈ ⨆ i ∈ s, genWeightSpace M i
hv : ⁅u, x✝⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
hw : ⁅u, y✝⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
⊢ ⁅u, x✝ + y✝⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

Tactic:
lie_add

Goal state after:
case pos.add
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i ∈ s, genWeightSpace M i
hy✝ : y✝ ∈ ⨆ i ∈ s, genWeightSpace M i
hv : ⁅u, x✝⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
hw : ⁅u, y✝⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
⊢ ⁅u, x✝⁆ + ⁅u, y✝⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case mem
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : m ∈ ⨆ χ ∈ s, genWeightSpace M χ
χ₁ : ↥H → R
u : L
hu : u ∈ ⨆ (_ : χ₁ ∈ s), rootSpace H χ₁
⊢ ⁅u, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

Tactic:
| mem χ₁ u hu =>

Goal state after:
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
⊢ weightSpace M χ ≤ genWeightSpace M χ

Tactic:
by
  apply le_iInf
  intro x
  rw [← (LieSubmodule.toSubmodule_orderEmbedding R L M).le_iff_le]
  apply (iInf_le _ x).trans
  exact ((toEnd R L M x).genEigenspace (χ x)).monotone le_top

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B₁ B₂ : BilinForm R M'
l r : M →ₗ[R] M'
hₗ : Function.Surjective ⇑l
hᵣ : Function.Surjective ⇑r
⊢ B₁.comp l r = B₂.comp l r ↔ B₁ = B₂

Tactic:
constructor <;> intro h

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B₁ B₂ : BilinForm R M'
l r : M →ₗ[R] M'
hₗ : Function.Surjective ⇑l
hᵣ : Function.Surjective ⇑r
h : B₁.comp l r = B₂.comp l r
⊢ B₁ = B₂

case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B₁ B₂ : BilinForm R M'
l r : M →ₗ[R] M'
hₗ : Function.Surjective ⇑l
hᵣ : Function.Surjective ⇑r
h : B₁ = B₂
⊢ B₁.comp l r = B₂.comp l r
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case add
ι : 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)
i : ι
x u v : L
hx✝ : u ∈ lieSpan R L (range b.f)
hy✝ : v ∈ lieSpan R L (range b.f)
hu : ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
hv : ⁅b.e i, v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
⊢ ⁅b.e i, u + v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
lie_add

Goal state after:
case add
ι : 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)
i : ι
x u v : L
hx✝ : u ∈ lieSpan R L (range b.f)
hy✝ : v ∈ lieSpan R L (range b.f)
hu : ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
hv : ⁅b.e i, v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
⊢ ⁅b.e i, u⁆ + ⁅b.e i, v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
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✝¹ : Nontrivial M
inst✝ : IsTriangularizable R L M
x : L
⊢ ∃ φ, ((toEnd R L M) x).HasEigenvalue φ

Tactic:
suffices ∃ φ, (toEnd R L M x).maxGenEigenspace φ ≠ ⊥ by
    obtain ⟨φ, hφ⟩ := this
    exact ⟨φ, (Module.End.hasUnifEigenvalue_iff_hasUnifEigenvalue_one ENat.top_pos).mp hφ⟩

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✝¹ : Nontrivial M
inst✝ : IsTriangularizable R L M
x : L
⊢ ∃ φ, ((toEnd R L M) x).maxGenEigenspace φ ≠ ⊥
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
inst✝ : IsTriangularizable R L M
x : L
⊢ ↑(⨆ φ, genWeightSpaceOf M φ x) = ↑⊤

Tactic:
LieSubmodule.iSup_toSubmodule,

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
inst✝ : IsTriangularizable R L M
x : L
⊢ ⨆ i, ↑(genWeightSpaceOf M i x) = ↑⊤
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: case a
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := ⋯
this : I ≤ J ⊔ J' ⊓ I
⊢ J' ⊓ I ≤ sSup {J | IsAtom J ∧ J ≤ I}

Tactic:
rw [← atomistic (J' ⊓ I)]

Goal state after:
case a
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
⊢ sSup {J | IsAtom J ∧ J ≤ J' ⊓ I} ≤ sSup {J | IsAtom J ∧ J ≤ I}
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case mp
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
hx : x ∈ (domRestrict B W).range.dualCoannihilator
y : V
⊢ y ∈ W → (B y) x = 0

Tactic:
hy

Goal state after:
case mp
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
hx : x ∈ (domRestrict B W).range.dualCoannihilator
y : V
hy : y ∈ W
⊢ (B y) x = 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
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.Nondegenerate
h : W = ⊤
⊢ B.orthogonal ⊤ ≤ ⊥

Tactic:
exact fun x hx ↦ b₃.1 x fun y ↦ b₁ y x <| by simpa using! hx y

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

Goal state before:
pp: case hL
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : LieAlgebra K L
inst✝² : IsKilling R L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
⊢ ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I

Tactic:
intro I h₁ h₂

Goal state after:
case hL
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : LieAlgebra K L
inst✝² : IsKilling R L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
h₁ : IsAtom I
h₂ : IsLieAbelian ↥I
⊢ False
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
⊢ y ∈ I → ((LieModule.traceForm K L L) ⁅x, y⁆) z = 0

Tactic:
hy

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) ⁅x, y⁆) z = 0
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie.hy.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 = ⁅u, z⁆
⊢ ⁅v, yl⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
exact hv' hyl

Goal state after:
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: case add
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✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i, genWeightSpace M (↑i • α + χ)
hy✝ : y✝ ∈ ⨆ i, genWeightSpace M (↑i • α + χ)
hz₁ : ⁅x, x✝⁆ ∈ genWeightSpaceChain M α χ p q
hz₂ : ⁅x, y✝⁆ ∈ genWeightSpaceChain M α χ p q
⊢ ⁅x, x✝ + y✝⁆ ∈ genWeightSpaceChain M α χ p q

Tactic:
lie_add

Goal state after:
case add
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✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i, genWeightSpace M (↑i • α + χ)
hy✝ : y✝ ∈ ⨆ i, genWeightSpace M (↑i • α + χ)
hz₁ : ⁅x, x✝⁆ ∈ genWeightSpaceChain M α χ p q
hz₂ : ⁅x, y✝⁆ ∈ genWeightSpaceChain M α χ p q
⊢ ⁅x, x✝⁆ + ⁅x, y✝⁆ ∈ genWeightSpaceChain M α χ p q
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✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
this :
  (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y) -
        χ x • finrank R ↥(genWeightSpace M χ) • χ y -
      (χ y • finrank R ↥(genWeightSpace M χ) • χ x - χ y • χ x • (trace R ↥(genWeightSpace M χ)) LinearMap.id) =
    0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)

Tactic:
LinearMap.trace_id,

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✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
this :
  (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y) -
        χ x • finrank R ↥(genWeightSpace M χ) • χ y -
      (χ y • finrank R ↥(genWeightSpace M χ) • χ x - χ y • χ x • ↑(finrank R ↥(genWeightSpace M χ))) =
    0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ 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✝ : IsTrivial L M
x y : L
this : φ x ∘ₗ φ y = 0
⊢ ((traceForm R L M) x) y = (0 x) y

Tactic:
simp [traceForm_apply_apply, this]

Goal state after:
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₁ : M
hm₀ : m₀ ∈ genWeightSpace M 0
hm₁ : m₁ ∈ posFittingComp R L M
hB : ∀ (x : L) (k : ℕ) (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
⊢ (B m₀) m₁ = 0

Tactic:
suffices ∀ (x : L) m, m ∈ posFittingCompOf R M x → B m₀ m = 0 by
    refine LieSubmodule.iSup_induction (motive := fun m ↦ (B m₀) m = 0) _ hm₁ this (map_zero _) ?_
    simp_all

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₁ : M
hm₀ : m₀ ∈ genWeightSpace M 0
hm₁ : m₁ ∈ posFittingComp R L M
hB : ∀ (x : L) (k : ℕ) (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
⊢ ∀ (x : L), ∀ m ∈ posFittingCompOf R M x, (B m₀) m = 0