mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
this : (toMatrix b b) e = fromBlocks A B 0 D
⊢ (fromBlocks A B 0 D).det = ((toMatrix bW bW) (e.restrict he)).det * LinearMap.det (W.mapQ W e he)

Tactic:
← LinearMap.det_toMatrix bQ,

Goal state after:
R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
this : (toMatrix b b) e = fromBlocks A B 0 D
⊢ (fromBlocks A B 0 D).det = ((toMatrix bW bW) (e.restrict he)).det * ((toMatrix bQ bQ) (W.mapQ W e he)).det
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
I : Ideal R
x : R
⊢ (aeval (root (minpoly R pb.gen))) (minpoly R pb.gen) = 0

Tactic:
by rw [AdjoinRoot.aeval_eq, AdjoinRoot.mk_self]

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ IsLieAbelian ↥(D k I) ↔ D (k + 1) I = ⊥

Tactic:
rw [add_comm, derivedSeriesOfIdeal_add I 1 k, abelian_iff_derived_one_eq_bot]

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

Goal state before:
pp: R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSolvable L
⊢ radical R L = ⊤

Tactic:
rw [eq_top_iff]

Goal state after:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSolvable L
⊢ ⊤ ≤ radical R L
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
this : ⁅⊤, lowerCentralSeries R L M k⁆ ≤ ⁅⊤, maxTrivSubmodule R L M⁆
⊢ ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥

Tactic:
ideal_oper_maxTrivSubmodule_eq_bot,

Goal state after:
R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
this : ⁅⊤, lowerCentralSeries R L M k⁆ ≤ ⊥
⊢ ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥
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
K : LieSubalgebra R L
hK₁ : IsEngelian R ↥K
hK₂ : K < K.normalizer
⊢ ∃ K', IsEngelian R ↥K' ∧ K < K'

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := SetLike.exists_of_lt hK₂
  let K' : LieSubalgebra R L :=
    { (R ∙ x) ⊔ (K : Submodule R L) with
      lie_mem' := fun {y z} => LieSubalgebra.lie_mem_sup_of_mem_normalizer hx₁ }
  have hxK' : x ∈ K' := Submodule.mem_sup_left (Submodule.subset_span (Set.mem_singleton _))
  have hKK' : K ≤ K' := (LieSubalgebra.toSubmodule_le_toSubmodule K K').mp le_sup_right
  have hK' : K' ≤ K.normalizer := by
    rw [← LieSubalgebra.toSubmodule_le_toSubmodule]
    exact sup_le ((Submodule.span_singleton_le_iff_mem _ _).mpr hx₁) hK₂.le
  refine ⟨K', ?_, lt_iff_le_and_ne.mpr ⟨hKK', fun contra => hx₂ (contra.symm ▸ hxK')⟩⟩
  intro M _i1 _i2 _i3 _i4 h
  obtain ⟨I, hI₁ : (I : LieSubalgebra R K') = LieSubalgebra.ofLe hKK'⟩ :=
    LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer hKK' hK'
  have hI₂ : R ∙ (⟨x, hxK'⟩ : K') ⊔ LieSubmodule.toSubmodule I = ⊤ := by
    rw [← LieIdeal.toLieSubalgebra_toSubmodule R K' I, hI₁]
    apply Submodule.map_injective_of_injective (K' : Submodule R L).injective_subtype
    simp only [LieSubalgebra.coe_ofLe, Submodule.map_sup, Submodule.map_subtype_range_inclusion,
      Submodule.map_top, Submodule.range_subtype]
    rw [Submodule.map_subtype_span_singleton]
  have e : K ≃ₗ⁅R⁆ I :=
    (LieSubalgebra.equivOfLe hKK').trans
      (LieEquiv.ofEq _ _ ((LieSubalgebra.coe_set_eq _ _).mpr hI₁.symm))
  have hI₃ : LieAlgebra.IsEngelian R I := e.isEngelian_iff.mp hK₁
  exact LieSubmodule.isNilpotentOfIsNilpotentSpanSupEqTop hI₂ (h _) (hI₃ _ fun x => h x)

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

Goal state before:
pp: R : Type u₁
L : Type u₂
M : Type u₄
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✝ : IsNoetherian R M
⊢ IsNilpotent L M ↔ ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)

Tactic:
rw [← isNilpotent_range_toEnd_iff (R := R), LieModule.isNilpotent_iff_forall (R := R)]

Goal state after:
R : Type u₁
L : Type u₂
M : Type u₄
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✝ : IsNoetherian R M
⊢ (∀ (x : ↥(toEnd R L M).range), _root_.IsNilpotent ((toEnd R (↥(toEnd R L M).range) M) x)) ↔
    ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
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✝ : IsNilpotent L M
⊢ maxNilpotentSubmodule R L M = ⊤

Tactic:
rw [eq_top_iff]

Goal state after:
R : Type u
L : Type v
M : Type w
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✝ : IsNilpotent L M
⊢ ⊤ ≤ maxNilpotentSubmodule R L M
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
R : Type u_1
A : 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✝¹ : CommRing A
inst✝ : Algebra R A
k : ℕ
ih : lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k = baseChange A (lowerCentralSeries R L M k)
⊢ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) (k + 1) = baseChange A (lowerCentralSeries R L M (k + 1))

Tactic:
simp only [lowerCentralSeries_succ, ih, ← baseChange_top, lie_baseChange]

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Algebraic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
H : F < E
this✝ : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L < finrank (↥F) L

Tactic:
refine lt_of_le_of_ne ?_ ?_

Goal state after:
case refine_1
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
H : F < E
this✝ : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ≤ finrank (↥F) L

case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
H : F < E
this✝ : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ≠ finrank (↥F) L
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: case mp
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s : Finset E
hs : adjoin F ↑s = ⊤
this✝¹ : Algebra.FiniteType F ↥(Algebra.adjoin F ↑s)
this✝ : Algebra.EssFiniteType ↥(Algebra.adjoin F ↑s) ↥(adjoin F ↑s)
this : Algebra.EssFiniteType F ↥(adjoin F ↑s)
⊢ Algebra.EssFiniteType F E

Tactic:
rw [hs] at this

Goal state after:
case mp
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s : Finset E
hs : adjoin F ↑s = ⊤
this✝¹ : Algebra.FiniteType F ↥(Algebra.adjoin F ↑s)
this✝ : Algebra.EssFiniteType ↥(Algebra.adjoin F ↑s) ↥(adjoin F ↑s)
this : Algebra.EssFiniteType F ↥⊤
⊢ Algebra.EssFiniteType F E
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
x : K
hxy : (algebraMap K L) x = y
⊢ y ∈ ↑⊥

Tactic:
← hxy

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
x : K
hxy : (algebraMap K L) x = y
⊢ (algebraMap K L) x ∈ ↑⊥
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Algebra.adjoin F (↑(f.aroots L).toFinset ∪ ↑(g.aroots L).toFinset) = ⊤

Tactic:
Algebra.adjoin_union_eq_adjoin_adjoin,

Goal state after:
case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Subalgebra.restrictScalars F (Algebra.adjoin ↥(Algebra.adjoin F ↑(f.aroots L).toFinset) ↑(g.aroots L).toFinset) = ⊤
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
⊢ (Polynomial.map (algebraMap K ↥F) p).Splits →
    (Algebra.adjoin K (p.rootSet ↥F) = ⊤ ↔ F.toSubalgebra = Algebra.adjoin K (p.rootSet L))

Tactic:
refine fun hp ↦ (hp.adjoin_rootSet_eq_range F.val).symm.trans ?_

Goal state after:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
hp : (Polynomial.map (algebraMap K ↥F) p).Splits
⊢ Algebra.adjoin K (p.rootSet L) = F.val.range ↔ F.toSubalgebra = Algebra.adjoin K (p.rootSet L)
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra R K
x : L
inst✝ : Algebra R L
int : IsIntegral R x
h : (Polynomial.map (algebraMap R K) (minpoly R x)).Splits
f : K →ₐ[R] L
⊢ x ∈ ⇑f '' (minpoly R x).rootSet K

Tactic:
rw [h.image_rootSet, mem_rootSet']

Goal state after:
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra R K
x : L
inst✝ : Algebra R L
int : IsIntegral R x
h : (Polynomial.map (algebraMap R K) (minpoly R x)).Splits
f : K →ₐ[R] L
⊢ Polynomial.map (algebraMap R L) (minpoly R x) ≠ 0 ∧ (aeval x) (minpoly R x) = 0
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ ∃ z, z ^ n = x

Tactic:
have : degree (X ^ n - C x) ≠ 0 := by
    rw [degree_X_pow_sub_C hn x]
    exact ne_of_gt (WithBot.coe_lt_coe.2 hn)
  obtain ⟨z, hz⟩ := exists_root (X ^ n - C x) this
  use z
  simp only [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def] at hz
  exact sub_eq_zero.1 hz

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
⊢ 0 < finrank ?m.80 V

Tactic:
rw [h_dim]; apply Nat.zero_lt_succ

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

Goal state before:
pp: case empty
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst✝ : ∀ (i : ι), FiniteDimensional K ↥(t i)
x✝ : Set ι
⊢ FiniteDimensional K ↥⊥

Tactic:
exact (botEquiv K L).symm.toLinearEquiv.finiteDimensional

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

Goal state before:
pp: case refine_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hp : Nat.Prime (finrank F E)
⊢ ∀ (a : IntermediateField F E), a = ⊥ ∨ a = ⊤

Tactic:
intro K

Goal state after:
case refine_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hp : Nat.Prime (finrank F E)
K : IntermediateField F E
⊢ K = ⊥ ∨ K = ⊤
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
dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯
⊢ ∀ (K : IntermediateField F E), finrank (↥K) E = (minpoly (↥K) α).natDegree

Tactic:
intro 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 : IntermediateField F E
⊢ finrank (↥K) E = (minpoly (↥K) α).natDegree
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 : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
⊢ ∃ φ, AlgHom.domRestrict L φ = f

Tactic:
let f' : L' →ₐ[F] K := f.comp (AlgEquiv.ofInjectiveField _).symm.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 : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
⊢ ∃ φ, AlgHom.domRestrict L φ = f
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 : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
⊢ ∃ φ, AlgHom.domRestrict L φ = f

Tactic:
by
  let L' := (IsScalarTower.toAlgHom F L E).fieldRange
  let f' : L' →ₐ[F] K := f.comp (AlgEquiv.ofInjectiveField _).symm.toAlgHom
  have := exists_algHom_adjoin_of_splits'' f' (S := S) fun s hs ↦ ?_
  · obtain ⟨φ, hφ⟩ := this; refine ⟨φ.comp <|
      inclusion (?_ : (adjoin L S).restrictScalars F ≤ (adjoin L' S).restrictScalars F), ?_⟩
    · simp_rw [← SetLike.coe_subset_coe, coe_restrictScalars, adjoin_subset_adjoin_iff]
      exact ⟨subset_adjoin_of_subset_left S (F := L'.toSubfield) le_rfl, subset_adjoin _ _⟩
    · ext x
      let y := (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x
      refine Eq.trans congr($hφ y) ?_
      simp only [AlgHom.coe_comp, Function.comp_apply, f']
      exact congr_arg f (AlgEquiv.symm_apply_apply _ _)
  let : Algebra L L' := (AlgEquiv.ofInjectiveField _).toRingHom.toAlgebra
  have : IsScalarTower L L' E := IsScalarTower.of_algebraMap_eq' rfl
  refine ⟨(hK s hs).1.tower_top, (hK s hs).1.minpoly_splits_tower_top' ?_⟩
  convert! (hK s hs).2
  ext
  simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
    AlgHom.coe_comp, Function.comp_apply, f']
  exact congr_arg f (AlgEquiv.symm_apply_apply _ _)

Goal state after:
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
inst✝ : H.IsCartanSubalgebra
⊢ H.toLieSubmodule.normalizer = H.toLieSubmodule

Tactic:
by
  rw [← LieSubmodule.toSubmodule_inj, coe_normalizer_eq_normalizer,
    IsCartanSubalgebra.self_normalizing, coe_toLieSubmodule]

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

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
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 φ)
ih : ∀ (φ : K), ⨆ χ, ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤
φ : K
χ : ι → K
hχ : χ i ≠ φ
⊢ (f i).maxGenEigenspace φ ⊓ ⨅ i, (f i).maxGenEigenspace (χ i) ≤ ⊥

Tactic:
← disjoint_iff_inf_le

Goal state after:
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
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 φ)
ih : ∀ (φ : K), ⨆ χ, ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤
φ : K
χ : ι → K
hχ : χ i ≠ φ
⊢ Disjoint ((f i).maxGenEigenspace φ) (⨅ i, (f i).maxGenEigenspace (χ i))
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: 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 μ
inst✝³ : IsNoetherian R M
inst✝² : IsTorsionFree R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : ∃ n, ((toEnd R L M) f ^ n) m = 0
⊢ ∃ n, μ = ↑n

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := Nat.exists_not_and_succ_of_not_zero_of_exists P.ne_zero this
    refine ⟨n, ?_⟩
    have := lie_e_pow_succ_toEnd_f P n
    rw [hn₂, lie_zero, eq_comm, smul_eq_zero_iff_left hn₁, mul_eq_zero, sub_eq_zero] at this
    exact this.resolve_left <| Nat.cast_add_one_ne_zero n

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

Goal state before:
pp: case h.mk
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
inst✝ : IsArtinian R M
x : L
k : ℕ
m : M
F : LieSubmodule R L M := posFittingComp R L M
x✝ : M ⧸ F
hk : ((toEnd R L M) x ^ k) m ∈ F
⊢ ((toEnd R L (M ⧸ F)) x ^ k) (LieSubmodule.Quotient.mk m) = LieSubmodule.Quotient.mk (((toEnd R L M) x ^ k) m)

Tactic:
have := LinearMap.congr_fun (Module.End.commute_pow_left_of_commute
    (LieSubmodule.Quotient.toEnd_comp_mk' F x) k) m

Goal state after:
case h.mk
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
inst✝ : IsArtinian R M
x : L
k : ℕ
m : M
F : LieSubmodule R L M := posFittingComp R L M
x✝ : M ⧸ F
hk : ((toEnd R L M) x ^ k) m ∈ F
this :
  (((toEnd R L (M ⧸ F)) x ^ k) ∘ₗ ↑(LieSubmodule.Quotient.mk' F)) m =
    (↑(LieSubmodule.Quotient.mk' F) ∘ₗ (toEnd R L M) x ^ k) m
⊢ ((toEnd R L (M ⧸ F)) x ^ k) (LieSubmodule.Quotient.mk m) = LieSubmodule.Quotient.mk (((toEnd R L M) x ^ k) m)
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: L : Type u_2
inst✝⁵ : LieRing L
K : Type u_4
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
⊢ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : α.IsNonZero), rootSpace H ⇑α = ⊤

Tactic:
by
  rw [eq_top_iff, ← LieModule.iSup_genWeightSpace_eq_top', iSup_le_iff]
  intro α
  by_cases hα : α.IsZero
  · simp [hα]
  · exact le_sup_of_le_right <| le_iSup₂_of_le α hα (le_refl _)

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₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ posFittingComp R L M₂ =
    LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))

Tactic:
← LieSubmodule.map_comp

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₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ posFittingComp R L M₂ = LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂)