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

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
_i5 : IsNoetherian R ↥L'
K : LieSubalgebra R ↥L'
hK₁ : K ∈ s
hK₂ : ∀ x ∈ s, ¬K < x
⊢ K = ⊤

Tactic:
grind

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

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R (↥I) (↥I) k) ≤ ↑(lowerCentralSeries R L (↥I) k)
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
apply Submodule.span_mono

Goal state after:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R (↥I) (↥I) k) ≤ ↑(lowerCentralSeries R L (↥I) k)
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : LieRing.IsNilpotent (L ⧸ I)
⊢ LieRing.IsNilpotent L

Tactic:
suffices LieModule.IsNilpotent L (L ⧸ I) by
    exact LieModule.nilpotentOfNilpotentQuotient R L L h₁ this
  simp only [LieRing.IsNilpotent, LieModule.isNilpotent_iff R] at h₂ ⊢
  peel h₂ with k hk
  simp [← LieSubmodule.toSubmodule_inj, coe_lowerCentralSeries_ideal_quot_eq, hk]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ IsSeparable (↥(subfield G F)) x

Tactic:
IsSeparable,

Goal state after:
case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ (_root_.minpoly (↥(subfield G F)) x).Separable
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
| IsIntegral F α

Tactic:
rw [← AdjoinSimple.algebraMap_gen F α]

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
| IsIntegral F ((algebraMap (↥F⟮α⟯) E) (gen F α))
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f✝ : G →* Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f✝.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f✝)
this : FaithfulSMul Q F
f : Gal(F/↥(subfield G F))
⊢ ∃ a, (MulSemiringAction.toAlgAut G (↥(subfield G F)) F) a = f

Tactic:
obtain ⟨q, hq⟩ := (toAlgAut_bijective Q F).surjective
    (AlgEquiv.ofRingEquiv (f := f) (fun ⟨x, hx⟩ ↦ f.commutes' ⟨x, fun g ↦ hx g⟩))

Goal state after:
G : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f✝ : G →* Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f✝.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f✝)
this : FaithfulSMul Q F
f : Gal(F/↥(subfield G F))
q : Q
hq : (MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F) q = AlgEquiv.ofRingEquiv ⋯
⊢ ∃ a, (MulSemiringAction.toAlgAut G (↥(subfield G F)) F) a = f
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

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_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
⊢ (adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L

Tactic:
let i' : E ≃ₐ[F] E' := AlgEquiv.ofInjectiveField i

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i
⊢ (adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

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_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i
x : E
⊢ (algebraMap E K) x = (⇑(algebraMap (↥E') K) ∘ ⇑i') x

Tactic:
rfl

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

Goal state before:
pp: F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑g).range = g.range.toSubring

Tactic:
rfl

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
f : K[X]
inst✝ : IsSplittingField K L f
hf : (Polynomial.map (algebraMap K F) f).Splits
hf0 : ¬f = 0
⊢ ↥(Algebra.adjoin K (f.rootSet L)) →ₐ[K] F

Tactic:
exact Classical.choice (lift_of_splits _ fun y hy =>
      have : aeval y f = 0 := (eval₂_eq_eval_map _).trans <|
        (mem_roots <| map_ne_zero hf0).1 (Multiset.mem_toFinset.mp hy)
    ⟨IsAlgebraic.isIntegral ⟨f, hf0, this⟩, hf.of_dvd (map_ne_zero hf0)
      ((map_dvd_map' _).mpr (minpoly.dvd K y this))⟩)

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

Goal state before:
pp: case e'_2
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ + x✝², ⋯⟩ = φ₁ (⟨x✝³, x✝¹⟩ + ⟨x✝², x✝⟩)

Tactic:
rfl

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

Goal state before:
pp: case e'_3
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₂ ⟨x✝³ + x✝², ⋯⟩ = φ₂ (⟨x✝³, x✝¹⟩ + ⟨x✝², x✝⟩)

Tactic:
rfl

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

Goal state before:
pp: case e'_2
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ * x✝², ⋯⟩ = φ₁ (⟨x✝³, x✝¹⟩ * ⟨x✝², x✝⟩)

Tactic:
rfl

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

Goal state before:
pp: case e'_3
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₂ ⟨x✝³ * x✝², ⋯⟩ = φ₂ (⟨x✝³, x✝¹⟩ * ⟨x✝², x✝⟩)

Tactic:
rfl

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 : Set E
α : E
A : Type u_3
B : Type u_4
C : Type u_5
inst✝⁶ : Field A
inst✝⁵ : Field B
inst✝⁴ : Field C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
b : B
x : ↥A⟮b⟯
⊢ (algebraMap B C) b = (AlgHom.restrictScalars A (Algebra.ofId B C)) b

Tactic:
rfl

Goal state after:
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
S : Set E
L : Lifts F E K
x : F
⊢ L.emb ((inclusion ⋯) ((botEquiv F E).symm x)) = (Algebra.ofId F K) (↑(botEquiv F E) ((botEquiv F E).symm x))

Tactic:
AlgEquiv.coe_toAlgHom,

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
S : Set E
L : Lifts F E K
x : F
⊢ L.emb ((inclusion ⋯) ((botEquiv F E).symm x)) = (Algebra.ofId F K) ((botEquiv F E) ((botEquiv F E).symm x))
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
L₁ L₂ : Lifts F E K
⊢ L₁ ≤ L₂ ↔ ∃ (h : L₁.carrier ≤ L₂.carrier), ∀ (x : ↥L₁.carrier), (L₂.emb.comp (inclusion ⋯)) x = L₁.emb x

Tactic:
rfl

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

Goal state before:
pp: k : Type u
inst✝¹⁶ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹⁵ : Field K
inst✝¹⁴ : Field J
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Field L
inst✝¹⁰ : Field M
inst✝⁹ : Algebra R M
inst✝⁸ : IsTorsionFree R M
inst✝⁷ : IsAlgClosure R M
inst✝⁶ : Algebra K M
inst✝⁵ : IsAlgClosure K M
inst✝⁴ : Algebra S L
inst✝³ : IsTorsionFree S L
inst✝² : IsAlgClosure S L
inst✝¹ : IsDomain R
inst✝ : IsDomain S
hSR : S ≃+* R
⊢ { e // e.toRingHom.comp (algebraMap S L) = (algebraMap R M).comp hSR.toRingHom }

Tactic:
letI : Algebra R S := RingHom.toAlgebra hSR.symm.toRingHom
  letI : Algebra S R := RingHom.toAlgebra hSR.toRingHom
  letI : Algebra R L := RingHom.toAlgebra ((algebraMap S L).comp (algebraMap R S))
  haveI : IsScalarTower R S L := .of_algebraMap_eq fun _ => rfl
  haveI : IsScalarTower S R L := .of_algebraMap_eq (by simp [RingHom.algebraMap_toAlgebra])
  have : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr hSR.symm.injective
  have : Algebra.IsAlgebraic R L := (IsAlgClosure.isAlgebraic.extendScalars
    (show Function.Injective (algebraMap S R) from hSR.injective))
  refine ⟨equivOfAlgebraic' R S L M, ?_⟩
  ext x
  simp only [RingEquiv.toRingHom_eq_coe, Function.comp_apply, RingHom.coe_comp,
    AlgEquiv.coe_ringEquiv, RingEquiv.coe_toRingHom]
  conv_lhs => rw [← hSR.symm_apply_apply x]
  change equivOfAlgebraic' R S L M (algebraMap R L (hSR x)) = _
  rw [AlgEquiv.commutes]

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
| aeval α

Tactic:
rw [← AdjoinSimple.algebraMap_gen F α]

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
| aeval ((algebraMap (↥F⟮α⟯) E) (AdjoinSimple.gen F α))
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case right.refine_2
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⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (minpoly F α))
⊢ F⟮α⟯.toSubfield.subtype (AdjoinSimple.gen F α) = α

Tactic:
rfl

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

Goal state before:
pp: K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ (powerBasis hx).dim = (minpoly K x).natDegree

Tactic:
rfl

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

Goal state before:
pp: K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)
x : L
hx✝ : x ∈ ⨆ i, t i
s : Finset ((i : ι) × ↥(t i))
hx : x ∈ ⨆ i ∈ s, K⟮↑i.snd⟯
⊢ IsAlgebraic K x

Tactic:
← Subtype.coe_mk (p := (· ∈ _)) x hx,

Goal state after:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)
x : L
hx✝ : x ∈ ⨆ i, t i
s : Finset ((i : ι) × ↥(t i))
hx : x ∈ ⨆ i ∈ s, K⟮↑i.snd⟯
⊢ IsAlgebraic K ↑⟨x, hx⟩
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case h_dim
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst : AddCommGroup M] [inst_1 : Module K M] [FiniteDimensional K M] (f : ι → End K M),
      (∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)) →
        (∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤) → finrank K M = m → ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
φ : K
⊢ finrank K ↥((f i).maxGenEigenspace φ) = finrank K ↥((f i).maxGenEigenspace φ)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
this : Submodule.comap p.subtype p = Submodule.comap p.subtype (⨆ μ, p ⊓ (f.genEigenspace μ) k)
h_inj : Injective ⇑p.subtype
⊢ ⨆ μ, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤

Tactic:
simp_rw [Submodule.inf_genEigenspace f p h, Submodule.comap_subtype_self,
    ← Submodule.map_iSup, Submodule.comap_map_eq_of_injective h_inj] at this

Goal state after:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
h_inj : Injective ⇑p.subtype
this : ⊤ = ⨆ i, (genEigenspace (LinearMap.restrict f h) i) k
⊢ ⨆ μ, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
⊢ LieRing.IsNilpotent ↥H

Tactic:
dsimp only [LieRing.IsNilpotent]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
⊢ LieModule.IsNilpotent ↥H ↥H
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
⊢ LieSubmodule.lcs k H.toLieSubmodule = ⊥

Tactic:
_root_.eq_bot_iff,

Goal state after:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
⊢ LieSubmodule.lcs k H.toLieSubmodule ≤ ⊥
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✝ : IsNoetherian R M
χ : L → R
x : L
⊢ (toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x) =
    LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯

Tactic:
rfl

Goal state after:
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
⊢ (∃ m,
      (LieModuleHom.codRestrict H.toLieSubmodule
            ((rootSpace H 0).incl.comp (rootSpaceWeightSpaceProduct R L H L α (-α) 0 ⋯)) ⋯)
          m =
        x) ↔
    ∃ m,
      (LieModuleHom.codRestrict H.toLieSubmodule
            ((rootSpace H 0).incl.comp (rootSpaceWeightSpaceProduct R L H L α (-α) 0 ⋯)) ⋯)
          m =
        x

Tactic:
rfl

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
m : M
⊢ m ∈ posFittingComp R L M ↔ m ∈ ⨆ x, posFittingCompOf R M x

Tactic:
rfl

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
B : BilinForm R M
r : M →ₗ[R] M
x✝ y✝ : M
⊢ ((B.comp id r) x✝) y✝ = ((B.compRight r) x✝) y✝

Tactic:
rfl

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
B : BilinForm R M
l : M →ₗ[R] M
x✝ y✝ : M
⊢ ((B.comp l id) x✝) y✝ = ((B.compLeft l) x✝) y✝

Tactic:
rfl

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
B : BilinForm R M
x✝ y✝ : M
⊢ ((B.compLeft id) x✝) y✝ = (B x✝) y✝

Tactic:
rfl

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
B : BilinForm R M
x✝ y✝ : M
⊢ ((B.compRight id) x✝) y✝ = (B x✝) y✝

Tactic:
rfl

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
B : BilinForm R M
x✝ y✝ : M
⊢ ((B.comp id id) x✝) y✝ = (B x✝) y✝

Tactic:
rfl

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
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
m : M
hm : m ∈ genWeightSpace M χ
x : L
this : ((toEnd R L M₂) x - χ x • 1) ∘ₗ ↑f = ↑f ∘ₗ ((toEnd R L M) x - χ x • 1)
⊢ ∃ k, (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0

Tactic:
obtain ⟨k, h⟩ := (mem_genWeightSpace _ _ _).mp hm x

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
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
m : M
hm : m ∈ genWeightSpace M χ
x : L
this : ((toEnd R L M₂) x - χ x • 1) ∘ₗ ↑f = ↑f ∘ₗ ((toEnd R L M) x - χ x • 1)
k : ℕ
h : (((toEnd R L M) x - χ x • 1) ^ k) m = 0
⊢ ∃ k, (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
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 u_7
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
e : M ≃ₗ[R] M'
⊢ (congr e).symm = congr e.symm

Tactic:
rfl

Goal state after:
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
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
this : (B (∑ i ∈ s, w i • v i)) (v i) = 0
⊢ ∑ j ∈ s, w j * (B (v j)) (v i) = w i * (B (v i)) (v i)

Tactic:
apply Finset.sum_eq_single_of_mem i hi

Goal state after:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
this : (B (∑ i ∈ s, w i • v i)) (v i) = 0
⊢ ∀ b ∈ s, b ≠ i → w b * (B (v b)) (v i) = 0
Module: Mathlib.Algebra.Lie.Weights.Basic

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✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
inst✝ : IsTriangularizable K L M
N : LieSubmodule K L M
⊢ N = ⨆ χ, N ⊓ genWeightSpace M ⇑χ

Tactic:
by
  refine le_antisymm ?_ (iSup_le fun χ ↦ inf_le_left)
  conv_lhs => rw [← N.map_incl_top, ← iSup_genWeightSpace_eq_top' K L N, LieSubmodule.map_iSup]
  refine iSup_le fun χ_N ↦ ?_
  have hN := (LieSubmodule.map_mono (le_top : genWeightSpace N χ_N ≤ ⊤)).trans N.map_incl_top.le
  exact (le_inf hN (map_genWeightSpace_le _)).trans <| by
    by_cases h : genWeightSpace M (χ_N : L → K) = ⊥
    · simp [h]
    · exact le_iSup_of_le ⟨_, h⟩ le_rfl

Goal state after: