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

Goal state before:
pp: case neg
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ¬∃ s, Nonempty (Basis (↥s) A M)
this : finrank A M = 0
⊢ LinearMap.det (c • f) = c ^ finrank A M * LinearMap.det f

Tactic:
simp [coe_det, H, this]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : LinearMap.det f ≠ 1
H : ∃ s, Nonempty (Basis (↥s) R M)
⊢ Module.Finite R M

Tactic:
rcases H with ⟨s, ⟨hs⟩⟩

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : LinearMap.det f ≠ 1
s : Finset M
hs : Basis (↥s) R M
⊢ Module.Finite R M
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : Free R M
inst✝² : Free R M'
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
f : End R M
f' : End R M'
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M') R M' := Free.chooseBasis R M'
⊢ ((toMatrix (b.prod b') (b.prod b')) (prodMap f f')).det = ((toMatrix b b) f).det * ((toMatrix b' b') f').det

Tactic:
toMatrix_prodMap,

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : Free R M
inst✝² : Free R M'
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
f : End R M
f' : End R M'
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M') R M' := Free.chooseBasis R M'
⊢ (fromBlocks ((toMatrix b b) f) 0 0 ((toMatrix b' b') f')).det = ((toMatrix b b) f).det * ((toMatrix b' b') f').det
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
⊢ f ∣ g - 0 ↔ f ∣ g

Tactic:
by rw [sub_zero]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
⊢ Function.LeftInverse ⇑(mk g) ⇑(modByMonicHom hg)

Tactic:
intro f
  induction f using AdjoinRoot.induction_on
  rw [modByMonicHom_mk hg, mk_eq_mk, modByMonic_eq_sub_mul_div, sub_sub_cancel_left, dvd_neg]
  apply dvd_mul_right

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
this : ∑ i ∈ Ico k (nilpotencyClass a), ((↑i !)⁻¹ • a ^ i) • m = 0
⊢ ∑ k ∈ range k, ((↑k !)⁻¹ • a ^ k) • m + ∑ k ∈ Ico k (nilpotencyClass a), ((↑k !)⁻¹ • a ^ k) • m =
    ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m

Tactic:
by
    simp_rw [this, add_zero, smul_assoc]

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

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
⊢ D (k + 1) I ≤ D l J

Tactic:
have h : l = k.succ ∨ l ≤ k := by rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂
    rcases h with h | h
    · rw [h, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]
      exact LieSubmodule.mono_lie (ih (le_refl k)) (ih (le_refl k))
    · rw [derivedSeriesOfIdeal_succ]; exact le_trans (LieSubmodule.lie_le_left _ _) (ih h)

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

Goal state before:
pp: case refine_3
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
⊢ ((bracket' R A L L) z₂) z₂ = 0 → ((bracket' R A L L) (z₁ + z₂)) (z₁ + z₂) = 0

Tactic:
h₂

Goal state after:
case refine_3
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
h₂ : ((bracket' R A L L) z₂) z₂ = 0
⊢ ((bracket' R A L L) (z₁ + z₂)) (z₁ + z₂) = 0
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y : L ⧸ I
x₁ x₂ y₁ y₂ : L
h₁ : (↑I).quotientRel x₁ y₁
⊢ (↑I).quotientRel x₂ y₂ → mk ⁅x₁, x₂⁆ = mk ⁅y₁, y₂⁆

Tactic:
h₂

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y : L ⧸ I
x₁ x₂ y₁ y₂ : L
h₁ : (↑I).quotientRel x₁ y₁
h₂ : (↑I).quotientRel x₂ y₂
⊢ mk ⁅x₁, x₂⁆ = mk ⁅y₁, y₂⁆
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x : L
⊢ ⁅Quotient.mk'' x, Quotient.mk'' x⁆ = 0

Tactic:
| _ x
     => 

Goal state after:
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x : L
⊢ ⁅Quotient.mk'' x, Quotient.mk'' x⁆ = 0
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
k : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective ⇑f
⊢ LieSubmodule.map f (lowerCentralSeries R L M k) = lowerCentralSeries R L M₂ k

Tactic:
apply le_antisymm (map_lowerCentralSeries_le k f)
  induction k with
  | zero =>
    rwa [lowerCentralSeries_zero, lowerCentralSeries_zero, top_le_iff, f.map_top,
      f.range_eq_top]
  | succ =>
    simp only [lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
    apply LieSubmodule.mono_lie_right
    assumption

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
b : P
⊢ map (↑g) (m • C b) = (MonoidHom.id M) m • map (↑g) (C b)

Tactic:
by rw [MonoidHom.id_apply, smul_C, map_C, coe_fn_coe, g.map_smul, map_C,
          coe_fn_coe, smul_C]

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

Goal state before:
pp: case h
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 = ⊥
⊢ lowerCentralSeries R L M k ≤ N

Tactic:
rw [← LieSubmodule.Quotient.map_mk'_eq_bot_le, ← le_bot_iff, ← hk]

Goal state after:
case h
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 = ⊥
⊢ LieSubmodule.map (LieSubmodule.Quotient.mk' N) (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L (M ⧸ N) k
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: M : Type u
inst✝² : Monoid M
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction M F
m : M
p : Polynomial ↥(subfield M F)
n : ℕ
x : ↥(subfield M F)
x✝ : m • (Polynomial.C x * Polynomial.X ^ n) = Polynomial.C x * Polynomial.X ^ n
⊢ m • (Polynomial.C x * Polynomial.X ^ (n + 1)) = Polynomial.C x * Polynomial.X ^ (n + 1)

Tactic:
rw [smul_mul', Polynomial.smul_C, smul, smul_pow', Polynomial.smul_X]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case h
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)
g₁ g₂ : G
h : ∀ (a : F), ⟦g₁⟧ • a = ⟦g₂⟧ • a
⊢ g₁⁻¹ * g₂ ∈ f.ker

Tactic:
MonoidHom.mem_ker,

Goal state after:
case h
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)
g₁ g₂ : G
h : ∀ (a : F), ⟦g₁⟧ • a = ⟦g₂⟧ • a
⊢ f (g₁⁻¹ * g₂) = 1
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝² : Field k
R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsAlgClosed k
f : R →+* k
hf : Function.Injective ⇑f
p : R[X]
hp : p.degree ≠ 0
x : k
hx : (map f p).IsRoot x
⊢ eval₂ f x p = 0

Tactic:
eval₂_eq_eval_map,

Goal state after:
k : Type u
inst✝² : Field k
R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsAlgClosed k
f : R →+* k
hf : Function.Injective ⇑f
p : R[X]
hp : p.degree ≠ 0
x : k
hx : (map f p).IsRoot x
⊢ eval x (map f p) = 0
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
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
⊢ ∀ μ' ∈ m.support, g (m μ') = if μ' = μ then g (m μ) else 0

Tactic:
rintro μ' hμ'

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
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
μ' : K
hμ' : μ' ∈ m.support
⊢ g (m μ') = if μ' = μ then g (m μ) else 0
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
⊢ Nonempty (E →ₐ[F] K)

Tactic:
have : (⊥ : Lifts F E K).IsExtendible := fun S ↦ have ⟨σ, hσ⟩ := h S; ⟨σ, bot_le, hσ⟩
  have ⟨ϕ, hϕ⟩ := zorn_le₀ {ϕ : Lifts F E K | ϕ.IsExtendible}
    fun c hext hc ↦ (isEmpty_or_nonempty c).elim
      (fun _ ↦ ⟨⊥, this, fun ϕ hϕ ↦ isEmptyElim (⟨ϕ, hϕ⟩ : c)⟩)
      fun _ ↦ ⟨_, union_isExtendible c hc hext, le_union c hc⟩
  suffices ϕ.carrier = ⊤ from ⟨ϕ.emb.comp <| ((equivOfEq this).trans topEquiv).symm⟩
  by_contra!
  obtain ⟨α, -, hα⟩ := SetLike.exists_of_lt this.lt_top
  let _ : Algebra ϕ.carrier K := ϕ.emb.toAlgebra
  let Λ := ϕ.carrier⟮α⟯ →ₐ[ϕ.carrier] K
  have := finiteDimensional_adjoin (S := {α}) fun _ _ ↦ ((alg.tower_top ϕ.carrier).isIntegral).1 _
  let L (σ : Λ) : Lifts F E K := ⟨ϕ.carrier⟮α⟯.restrictScalars F, σ.restrictScalars F⟩
  have hL (σ : Λ) : ϕ < L σ := lt_iff.mpr
    ⟨by simpa only [L, restrictScalars_adjoin_eq_sup, left_lt_sup, adjoin_simple_le_iff],
      AlgHom.coe_ringHom_injective σ.comp_algebraMap⟩
  have ⟨(ϕ_ext : ϕ.IsExtendible), ϕ_max⟩ := maximal_iff_forall_gt.mp hϕ
  simp_rw [Set.mem_ofPred, IsExtendible] at ϕ_max; push Not at ϕ_max
  choose S hS using fun σ : Λ ↦ ϕ_max (hL σ)
  classical
  have ⟨θ, hθϕ, hθ⟩ := ϕ_ext ({α} ∪ Finset.univ.biUnion S)
  simp_rw [Finset.coe_union, Set.union_subset_iff, Finset.coe_singleton, Set.singleton_subset_iff,
    Finset.coe_biUnion, Finset.coe_univ, Set.mem_univ, Set.iUnion_true, Set.iUnion_subset_iff] at hθ
  have : ϕ.carrier⟮α⟯.restrictScalars F ≤ θ.carrier := by
    rw [restrictScalars_adjoin_eq_sup, sup_le_iff, adjoin_simple_le_iff]; exact ⟨hθϕ.1, hθ.1⟩
  exact hS ⟨(θ.emb.comp <| inclusion this).toRingHom, hθϕ.2⟩ θ ⟨this, fun _ ↦ rfl⟩ (hθ.2 _)

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
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
μ' : K
x✝ : μ' ∈ m.support.erase μ
this : MapsTo ⇑(f - (algebraMap K (End K V)) μ') ↑p ↑p
⊢ MapsTo ⇑((f - (algebraMap K (End K V)) μ') ^ l₀) ↑p ↑p

Tactic:
by
      simp only [Module.End.coe_pow, this.iterate l₀]

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra F K
hA : ∀ (x : K), (map (algebraMap F L) (minpoly F x)).Splits
inst✝ : Algebra.IsAlgebraic F K
x : K
a : L
⊢ (a ∈ Set.range fun ψ ↦ ψ x) ↔ a ∈ (minpoly F x).rootSet L

Tactic:
mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x))

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra F K
hA : ∀ (x : K), (map (algebraMap F L) (minpoly F x)).Splits
inst✝ : Algebra.IsAlgebraic F K
x : K
a : L
⊢ (a ∈ Set.range fun ψ ↦ ψ x) ↔ (aeval a) (minpoly F x) = 0
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
h : f.comp g = 0
⊢ False

Tactic:
by simpa [hf', hg', natDegree_comp] using congr_arg natDegree h

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

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

Tactic:
rcases hv with rfl | rfl | rfl

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

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

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}
Module: Mathlib.Algebra.Lie.Sl2

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

Tactic:
rcases hv with rfl | rfl | rfl

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

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

case mem.mem.inr.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
e x y u v : L
t : IsSl2Triple v e u
__spread✝⁻⁰ : Submodule R L := span R {e, u, v}
⊢ ⁅u, v⁆ ∈ span R {e, u, v}
Module: Mathlib.Algebra.Lie.Sl2

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

Tactic:
rcases hv with rfl | rfl | rfl

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

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

case mem.mem.inr.inr.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
e f x y v : L
t : IsSl2Triple v e f
__spread✝⁻⁰ : Submodule R L := span R {e, f, v}
⊢ ⁅v, v⁆ ∈ span R {e, f, v}
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
k : ℕ
hk : genWeightSpace M 0 ≤ LieSubmodule.ucs k ⊥
⊢ LieSubmodule.ucs k ⊥ ≤ ⨆ k, LieSubmodule.ucs k ⊥

Tactic:
exact le_iSup (fun k ↦ (⊥ : LieSubmodule R L M).ucs k) k

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case h.left
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
c : α
h₁ : IsCompactElement c
h₂ : c ≤ sSup S
⊢ T c h₁ h₂ ⊆ S

Tactic:
apply hT₁

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

Goal state before:
pp: case mp
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsSolvable ↥I → I = ⊥
I : LieIdeal R L
⊢ IsLieAbelian ↥I → I = ⊥

Tactic:
h₂

Goal state after:
case mp
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsSolvable ↥I → I = ⊥
I : LieIdeal R L
h₂ : IsLieAbelian ↥I
⊢ I = ⊥
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: case mpr
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian ↥I → I = ⊥
I : LieIdeal R L
⊢ IsSolvable ↥I → I = ⊥

Tactic:
h₂

Goal state after:
case mpr
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian ↥I → I = ⊥
I : LieIdeal R L
h₂ : IsSolvable ↥I
⊢ I = ⊥
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: case mp
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
⊢ IsLieAbelian ↥(radical R L) → ∀ (I : LieIdeal R L), IsSolvable ↥I → IsLieAbelian ↥I

pp: case mpr
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
⊢ (∀ (I : LieIdeal R L), IsSolvable ↥I → IsLieAbelian ↥I) → IsLieAbelian ↥(radical R L)

Tactic:
· rintro h₁ I h₂
    rw [LieIdeal.solvable_iff_le_radical] at h₂
    exact (LieIdeal.inclusion_injective h₂).isLieAbelian h₁

Goal state after:
case mpr
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
⊢ (∀ (I : LieIdeal R L), IsSolvable ↥I → IsLieAbelian ↥I) → IsLieAbelian ↥(radical R L)
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
h₁ : IsAtom I
⊢ ¬IsLieAbelian ↥I

Tactic:
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