mathlib-initiative/mathlib-tactics huggingface dataset:
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:
smul_mul',

Goal state after:
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 * m • Polynomial.X ^ (n + 1) = Polynomial.C x * Polynomial.X ^ (n + 1)
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case refine_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieRing.IsNilpotent ↥(ad R L).range
⊢ LieRing.IsNilpotent L

pp: case refine_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ LieRing.IsNilpotent L → LieRing.IsNilpotent ↥(ad R L).range

Tactic:
· have : (ad R L).ker = center R L := by simp
    exact
      LieAlgebra.nilpotent_of_nilpotent_quotient (le_of_eq this)
        ((ad R L).quotKerEquivRange.nilpotent_iff_equiv_nilpotent.mpr h)

Goal state after:
case refine_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ LieRing.IsNilpotent L → LieRing.IsNilpotent ↥(ad R L).range
Module: Mathlib.FieldTheory.Normal.Defs

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

Tactic:
rw [IsScalarTower.AlgEquiv.restrictNormalHom_comp F K₁ K₂ K₃, MonoidHom.comp_apply]

Goal state after:
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
⊢ FiniteDimensional K L

Tactic:
by
  classical
  exact ⟨@Algebra.top_toSubmodule K L _ _ _ ▸
    adjoin_rootSet L f ▸ fg_adjoin_of_finite (Finset.finite_toSet _) fun y hy ↦
      if hf : f = 0 then by rw [hf, rootSet_zero] at hy; cases hy
      else IsAlgebraic.isIntegral ⟨f, hf, (mem_rootSet'.mp hy).2⟩⟩

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 (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
⊢ (sSup S).toSubfield = Subfield.closure (⋃₀ (SetLike.coe '' S))

Tactic:
sSup_def,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
⊢ (adjoin F (⋃₀ (SetLike.coe '' S))).toSubfield = Subfield.closure (⋃₀ (SetLike.coe '' S))
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
⊢ ⨆ t ∈ S, {t} = S

Tactic:
exact S.biUnion_of_singleton

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

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
a✝ : Nontrivial A
h : p.degree ≤ 0
⊢ σ ((aeval a) p) = (fun k ↦ eval k p) '' σ a

Tactic:
rw [eq_C_of_degree_le_zero h]

Goal state after:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
a✝ : Nontrivial A
h : p.degree ≤ 0
⊢ σ ((aeval a) (C (p.coeff 0))) = (fun k ↦ eval k (C (p.coeff 0))) '' σ a
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : A
hp : IsIdempotentElem p
⊢ spectrum 𝕜 p ⊆ {0, 1}

Tactic:
by
  nontriviality A
  apply Set.image_subset_iff.mp (spectrum.subset_polynomial_aeval p (X ^ 2 - X)) |>.trans
  refine fun a ha => eq_zero_or_one_of_sq_eq_self ?_
  simpa [pow_two p, hp.eq, sub_eq_zero] using ha

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
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst✝ : Nonempty ↑c
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
⊢ ∃ τ ≥ union c hc, ↑S ⊆ ↑τ.carrier

Tactic:
let Ω := adjoin F (S : Set E) →ₐ[F] K

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
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst✝ : Nonempty ↑c
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := ↥(adjoin F ↑S) →ₐ[F] K
⊢ ∃ τ ≥ union c hc, ↑S ⊆ ↑τ.carrier
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
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
inst✝¹ : FiniteDimensional K ↥E1
inst✝ : FiniteDimensional K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
⊢ g.range = (E1 ⊔ E2).toSubalgebra

Tactic:
rw [Algebra.TensorProduct.productMap_range, E1.range_val, E2.range_val, sup_toSubalgebra_of_left]

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]

Goal state after:
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 < n + 1
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
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
⊢ 0 < finrank K ↥((f.genEigenspace μ₀) ↑(finrank K V))

Tactic:
rw [h_dim]

Goal state after:
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
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
⊢ 0 < finrank K ↥((f.genEigenspace μ₀) ↑(n + 1))
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: F : Type u_1
F' : Type u_2
E : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field F'
inst✝⁴ : Field E
inst✝³ : Algebra F F'
inst✝² : Algebra F E
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : IsAlgClosed F'
h : finrank F F' = 2
emb : E →ₐ[F] F'
e : E ≃ₐ[F] ↥emb.range
this : IsSimpleOrder (Subalgebra F F')
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')

Tactic:
obtain h | h := IsSimpleOrder.eq_bot_or_eq_top emb.range <;> rw [h] at e

Goal state after:
case inl
F : Type u_1
F' : Type u_2
E : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field F'
inst✝⁴ : Field E
inst✝³ : Algebra F F'
inst✝² : Algebra F E
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : IsAlgClosed F'
h✝ : finrank F F' = 2
emb : E →ₐ[F] F'
e : E ≃ₐ[F] ↥⊥
this : IsSimpleOrder (Subalgebra F F')
h : emb.range = ⊥
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')

case inr
F : Type u_1
F' : Type u_2
E : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field F'
inst✝⁴ : Field E
inst✝³ : Algebra F F'
inst✝² : Algebra F E
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : IsAlgClosed F'
h✝ : finrank F F' = 2
emb : E →ₐ[F] F'
e : E ≃ₐ[F] ↥⊤
this : IsSimpleOrder (Subalgebra F F')
h : emb.range = ⊤
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_1
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
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst✝ : Nonempty ↑c
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := ↥(adjoin F ↑S) →ₐ[F] K
ω : Ω
θ : ↑c → Lifts F E K
ge : ∀ (π : ↑c), θ π ≥ ↑π
hθ : ∀ (π : ↑c), { carrier := adjoin F ↑S, emb := ω } ≤ θ π
eq : ∀ (π : ↑c), (θ π).carrier = adjoin F (↑(↑π).carrier ∪ ↑S)
π₁ π₂ : ↑c
h : π₁ ≤ π₂
⊢ (θ π₁).carrier ≤ (θ π₂).carrier

Tactic:
eq,

Goal state after:
case refine_1
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
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst✝ : Nonempty ↑c
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := ↥(adjoin F ↑S) →ₐ[F] K
ω : Ω
θ : ↑c → Lifts F E K
ge : ∀ (π : ↑c), θ π ≥ ↑π
hθ : ∀ (π : ↑c), { carrier := adjoin F ↑S, emb := ω } ≤ θ π
eq : ∀ (π : ↑c), (θ π).carrier = adjoin F (↑(↑π).carrier ∪ ↑S)
π₁ π₂ : ↑c
h : π₁ ≤ π₂
⊢ adjoin F (↑(↑π₁).carrier ∪ ↑S) ≤ (θ π₂).carrier
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: case h.succ
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
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K ↥ES
h_dim_add : finrank K ↥ER + finrank K ↥ES = finrank K V
h_dim_ER : finrank K ↥ER < n.succ
ih_ER : ⨆ μ, f'.maxGenEigenspace μ = ⊤
ih_ER' : ⨆ μ, Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
hff' : ∀ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ
hER : ER ≤ ⨆ μ, f.maxGenEigenspace μ
hES : ES ≤ ⨆ μ, f.maxGenEigenspace μ
h_disjoint : Disjoint ER ES
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤

Tactic:
rw [← top_le_iff, ← Submodule.eq_top_of_disjoint ER ES h_dim_add.ge h_disjoint]

Goal state after:
case h.succ
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
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K ↥ES
h_dim_add : finrank K ↥ER + finrank K ↥ES = finrank K V
h_dim_ER : finrank K ↥ER < n.succ
ih_ER : ⨆ μ, f'.maxGenEigenspace μ = ⊤
ih_ER' : ⨆ μ, Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
hff' : ∀ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ
hER : ER ≤ ⨆ μ, f.maxGenEigenspace μ
hES : ES ≤ ⨆ μ, f.maxGenEigenspace μ
h_disjoint : Disjoint ER ES
⊢ ER ⊔ ES ≤ ⨆ μ, f.maxGenEigenspace μ
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)⟮α⟯
L : Λ → Lifts F E K := fun σ ↦ { carrier := restrictScalars F (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max : ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ S, ∀ τ ≥ y, ¬↑S ⊆ ↑τ.carrier
S : Λ → Finset E
hS : ∀ (σ : Λ), ∀ τ ≥ L σ, ¬↑(S σ) ⊆ ↑τ.carrier
θ : Lifts F E K
hθϕ : θ ≥ ϕ
hθ : ↑({α} ∪ Finset.univ.biUnion S) ⊆ ↑θ.carrier
⊢ False

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

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 σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max : ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ S, ∀ τ ≥ y, ¬↑S ⊆ ↑τ.carrier
S : Λ → Finset E
hS : ∀ (σ : Λ), ∀ τ ≥ L σ, ¬↑(S σ) ⊆ ↑τ.carrier
θ : Lifts F E K
hθϕ : θ ≥ ϕ
hθ : α ∈ ↑θ.carrier ∧ ∀ (i : Λ), ↑(S i) ⊆ ↑θ.carrier
⊢ False
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: L : Type u_2
inst✝ : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ ⁅-h, e⁆ = -(2 • e)

Tactic:
rw [neg_lie, neg_inj, ht.lie_h_e_nsmul]

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
x : L
⊢ weightSpace M χ ≤ genWeightSpaceOf M (χ x) x

Tactic:
← (LieSubmodule.toSubmodule_orderEmbedding R L M).le_iff_le

Goal state after:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
⊢ (LieSubmodule.toSubmodule_orderEmbedding R L M) (weightSpace M χ) ≤
    (LieSubmodule.toSubmodule_orderEmbedding R L M) (genWeightSpaceOf M (χ x) x)
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) (g : n → K), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0

Tactic:
intro s w hs 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
⊢ w i = 0
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ I ≤ sSup T₁

Tactic:
· exact (_root_.le_sSup hI).trans (hX'.ge.trans inf_le_left)

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

Goal state before:
pp: case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ ↑↑J
a : L
ha : a ∈ I
b : L
hb : b ∈ sSup ({I' | IsAtom I'} \ {I})
⊢ ⁅b, ↑y⁆ ∈ ⊥

Tactic:
← (IsSemisimple.sSupIndep_isAtom hI).eq_bot

Goal state after:
case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ ↑↑J
a : L
ha : a ∈ I
b : L
hb : b ∈ sSup ({I' | IsAtom I'} \ {I})
⊢ ⁅b, ↑y⁆ ∈ I ⊓ sSup ({I | IsAtom I} \ {I})
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
h : ¬(x.fst = v ∧ ↑x.snd = count v m)
hv : x.fst = v
⊢ ↑x.snd < count x.fst m

Tactic:
simp only [hv, true_and] at h ⊢

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hv : x.fst = v
h : ¬↑x.snd = count v m
⊢ ↑x.snd < count v m
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsKilling R L
⊢ LinearMap.SeparatingLeft (LieModule.traceForm R L L)

Tactic:
simp [LinearMap.separatingLeft_iff_ker_eq_bot]

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

Goal state before:
pp: case hΦ_inv
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
⊢ LinearMap.BilinForm.lieInvariant L (killingForm K L)

pp: case hΦ_refl
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
⊢ (killingForm K L).IsRefl

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:
· exact LieModule.traceForm_lieInvariant _ _ _

Goal state after:
case hΦ_refl
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
⊢ (killingForm K L).IsRefl

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

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
⊢ x' ∈ LieIdeal.killingCompl R L' ⊤ ↔ x' ∈ ⊥

Tactic:
LieIdeal.mem_killingCompl,

Goal state after:
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
⊢ (∀ y ∈ ⊤, ((killingForm R L') y) x' = 0) ↔ x' ∈ ⊥
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: 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
hp : genWeightSpace M (p • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : y ∈ genWeightSpaceChain M α χ p q
⊢ genWeightSpace M (-p • -α + χ) = ⊥

Tactic:
rwa [smul_neg, neg_smul, neg_neg]

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

Goal state before:
pp: case zero
L : Type u_2
inst✝¹⁰ : LieRing L
M : Type u_3
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
K : Type u_4
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L
H : LieSubalgebra K L
inst✝⁴ : LieRing.IsNilpotent ↥H
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : IsTriangularizable K (↥H) M
inst✝ : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
⊢ ∃ n, ((toEnd K L M) x ^ n) 0 = 0

Tactic:
exact ⟨0, map_zero _⟩

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

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

Tactic:
by_cases! p_ne_zero : P = 0

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

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

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

Tactic:
by_cases! p_ne_zero : P = 0

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

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
⊢ corootSpace ⇑α = ⊥ ↔ α.IsZero

Tactic:
by
  simp [← LieSubmodule.toSubmodule_eq_bot, coe_corootSpace_eq_span_singleton α]

Goal state after: