mathlib-initiative/mathlib-tactics huggingface dataset:
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]
n : ℕ
b : P
x✝ : map (↑g) (m • (C b * X ^ n)) = (MonoidHom.id M) m • map (↑g) (C b * X ^ n)
⊢ C (m • g b) * X ^ (n + 1) = C (m • ↑g b) * (m • X) ^ (n + 1)

Tactic:
smul_X,

Goal state after:
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]
n : ℕ
b : P
x✝ : map (↑g) (m • (C b * X ^ n)) = (MonoidHom.id M) m • map (↑g) (C b * X ^ n)
⊢ C (m • g b) * X ^ (n + 1) = C (m • ↑g b) * X ^ (n + 1)
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
h : ∀ (x : L), IsNilpotent ((toEnd R L M) x)
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
⊢ LieModule.IsNilpotent (↥(toEnd R L M).range) M

Tactic:
replace h : ∀ y : L', IsNilpotent (y : Module.End R M) := by
    rintro ⟨-, ⟨y, rfl⟩⟩
    simp [h]

Goal state after:
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
⊢ LieModule.IsNilpotent (↥(toEnd R L M).range) M
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝¹⁶ : Field F
inst✝¹⁵ : Field K
inst✝¹⁴ : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝¹³ : Field K₁
inst✝¹² : Field K₂
inst✝¹¹ : Field K₃
inst✝¹⁰ : Algebra F K₁
inst✝⁹ : Algebra F K₂
inst✝⁸ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
inst✝⁵ : Algebra E K₁
inst✝⁴ : Algebra E K₂
inst✝³ : Algebra E K₃
inst✝² : IsScalarTower F E K₁
inst✝¹ : IsScalarTower F E K₂
inst✝ : IsScalarTower F E K₃
h : Normal F E
x : ↥(toAlgHom F E K₁).range
⊢ ϕ ↑x ∈ (toAlgHom F E K₂).range

Tactic:
suffices (toAlgHom F E K₁).range.map ϕ ≤ _ by exact this ⟨x, Subtype.mem x, rfl⟩

Goal state after:
F : Type u_1
K : Type u_2
inst✝¹⁶ : Field F
inst✝¹⁵ : Field K
inst✝¹⁴ : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝¹³ : Field K₁
inst✝¹² : Field K₂
inst✝¹¹ : Field K₃
inst✝¹⁰ : Algebra F K₁
inst✝⁹ : Algebra F K₂
inst✝⁸ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
inst✝⁵ : Algebra E K₁
inst✝⁴ : Algebra E K₂
inst✝³ : Algebra E K₃
inst✝² : IsScalarTower F E K₁
inst✝¹ : IsScalarTower F E K₂
inst✝ : IsScalarTower F E K₃
h : Normal F E
x : ↥(toAlgHom F E K₁).range
⊢ Subalgebra.map ϕ (toAlgHom F E K₁).range ≤ (toAlgHom F E K₂).range
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝¹⁷ : Field F
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝¹⁴ : Field K₁
inst✝¹³ : Field K₂
inst✝¹² : Field K₃
inst✝¹¹ : Algebra F K₁
inst✝¹⁰ : Algebra F K₂
inst✝⁹ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra E K₁
inst✝⁵ : Algebra E K₂
inst✝⁴ : Algebra E K₃
inst✝³ : IsScalarTower F E K₁
inst✝² : IsScalarTower F E K₂
inst✝¹ : IsScalarTower F E K₃
inst✝ : Normal F E
σ : E →ₐ[F] K₁
x✝ : E
⊢ ((fun σ ↦ (toAlgHom F E K₁).comp ↑σ) ((fun σ ↦ σ.restrictNormal' E) σ)) x✝ = σ x✝

Tactic:
simp [AlgHom.restrictNormal']

Goal state after:
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)
⊢ Subalgebra.restrictScalars F (Algebra.adjoin ↥(Algebra.adjoin F ↑(f.aroots L).toFinset) ↑(g.aroots L).toFinset) = ⊤

Tactic:
aroots_def,

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 ↑(Polynomial.map (algebraMap F L) f).roots.toFinset) ↑(g.aroots L).toFinset) =
    ⊤
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)
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin ↥(Algebra.adjoin F ↑(Polynomial.map (algebraMap F L) f).roots.toFinset) ↑(g.aroots L).toFinset) =
    ⊤

Tactic:
aroots_def,

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 ↑(Polynomial.map (algebraMap F L) f).roots.toFinset)
        ↑(Polynomial.map (algebraMap F L) g).roots.toFinset) =
    ⊤
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

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
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)
x✝³ : E
x✝² : Finset E
ha : x✝³ ∈ S
x✝¹ : x✝² ⊆ S
x✝ : x✝³ ∉ x✝²
h : P (adjoin F ↑x✝²)
⊢ P (adjoin F ↑(insert x✝³ x✝²))

Tactic:
rw [Finset.coe_insert, Set.insert_eq, Set.union_comm, ← adjoin_adjoin_left]

Goal state after:
case refine_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)
x✝³ : E
x✝² : Finset E
ha : x✝³ ∈ S
x✝¹ : x✝² ⊆ S
x✝ : x✝³ ∉ x✝²
h : P (adjoin F ↑x✝²)
⊢ P (restrictScalars F (↥(adjoin F ↑x✝²))⟮x✝³⟯)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case refine_1
K : Type u_1
L : Type u_2
E : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field E
inst✝³ : Algebra K L
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : adjoin K ↑s = restrictScalars K E'
⊢ adjoin L ↑s ≤ E'

Tactic:
rw [adjoin_le_iff]

Goal state after:
case refine_1
K : Type u_1
L : Type u_2
E : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field E
inst✝³ : Algebra K L
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : adjoin K ↑s = restrictScalars K E'
⊢ ↑s ⊆ ↑E'
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
this : ∀ (μ : K), m μ ∈ p
⊢ (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, p ⊓ (f.genEigenspace μ) k

Tactic:
by
    exact (mem_iSup_iff_exists_finsupp _ _).mpr ⟨m, fun μ ↦ mem_inf.mp ⟨this μ, hm₂ μ⟩, rfl⟩

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
K : Type u
inst✝³ : Field K
inst✝² : Algebra F K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
i : Fin (minpoly K x).natDegree
⊢ (powerBasisAux hx) i = AdjoinSimple.gen K x ^ ↑i

Tactic:
rw [powerBasisAux, Basis.reindex_apply, Basis.map_apply, PowerBasis.basis_eq_pow,
      finCongr_symm, finCongr_apply, Fin.cast_eq_self, AlgEquiv.toLinearEquiv_apply,
      map_pow, AdjoinRoot.powerBasis_gen, adjoinRootEquivAdjoin_apply_root]

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

Goal state before:
pp: case neg
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
hμμ' : ¬μ' = μ
hl₀ : ((f - (algebraMap K (End K V)) μ') ^ l₀) (m μ') = 0
⊢ g (m μ') = 0

Tactic:
have : _ = g := (m.support.erase μ).noncommProd_erase_mul (Finset.mem_erase.mpr ⟨hμμ', hμ'⟩)
      (fun μ ↦ (f - algebraMap K (End K V) μ) ^ l₀) (fun μ₁ _ μ₂ _ _ ↦ h_comm μ₁ μ₂)

Goal state after:
case neg
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
hμμ' : ¬μ' = μ
hl₀ : ((f - (algebraMap K (End K V)) μ') ^ l₀) (m μ') = 0
this :
  ((m.support.erase μ).erase μ').noncommProd (fun μ ↦ (f - (algebraMap K (End K V)) μ) ^ l₀) ⋯ *
      (f - (algebraMap K (End K V)) μ') ^ l₀ =
    g
⊢ g (m μ') = 0
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
⊢ ∃ k, ↑(genWeightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)

Tactic:
use (toEnd R L M x).maxGenEigenspaceIndex (χ x)

Goal state after:
case h
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
⊢ ↑(genWeightSpace M χ) ≤
    LinearMap.ker
      (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ ((toEnd R L M) x).maxGenEigenspaceIndex (χ x))
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
s : Set ↥H := {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
u : L
⊢ (∃ (x : u ∈ H), ⟨u, ⋯⟩ ∈ {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}) ↔
    ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u

Tactic:
refine ⟨fun ⟨_, y, hy, z, hz, hyz⟩ ↦ ⟨y, hy, z, hz, hyz⟩,
    fun ⟨y, hy, z, hz, hyz⟩ ↦ ⟨?_, y, hy, z, hz, hyz⟩⟩

Goal state after:
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
s : Set ↥H := {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
u : L
x✝ : ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = u
⊢ u ∈ H
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
s : Set ↥H := {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
u : L
x✝ : ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = u
⊢ u ∈ H

Tactic:
convert!
    (rootSpaceProduct R L H α (-α) 0 (add_neg_cancel α) (⟨y, hy⟩ ⊗ₜ[R] ⟨z, hz⟩)).property using 0

Goal state after:
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
s : Set ↥H := ⋯
u : L
x✝ : ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = u
⊢ u ∈ H ↔ ↑((rootSpaceProduct R L H α (-α) 0 ⋯) (⟨y, hy⟩ ⊗ₜ[R] ⟨z, hz⟩)) ∈ rootSpace H 0
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
inst✝ : IsArtinian R M
P : LieSubmodule R L M → Prop := fun N ↦ IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
N : LieSubmodule R L M
hN : ∀ y < N, P y
N' : LieSubmodule R L ↥N
hN' : N' < ⊤
this : IsCompl (genWeightSpace (↥(LieSubmodule.map N.incl N')) 0) (posFittingComp R L ↥(LieSubmodule.map N.incl N'))
⊢ IsCompl (genWeightSpace (↥N') 0) (posFittingComp R L ↥N')

Tactic:
by
    let e := LieSubmodule.equivMapOfInjective N' N.injective_incl
    rw [← map_genWeightSpace_eq e, ← map_posFittingComp_eq e] at this
    exact (LieSubmodule.orderIsoMapComap e).isCompl_iff.mpr this

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
x : ↥I
y : ↥I
z : L
hyz : ⁅↑x, z⁆ ∈ I
⊢ (Φ ↑y) ⁅↑x, z⁆ = 0

Tactic:
exact contra hyz y y.2

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

Goal state before:
pp: case mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
hx : ∀ n ∈ W, (B n) x = 0
w : V
hw : w ∈ W
⊢ ((domRestrict B W) ⟨w, hw⟩) x = 0

Tactic:
exact hx w hw

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
hT : ∅ ⊆ S
haS : sSup ∅ ≤ sSup S
ha : IsAtom ⊥
⊢ sSup ∅ ∈ S

Tactic:
exact (ha.1 rfl).elim

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

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

Tactic:
hasTrivialRadical_iff_no_solvable_ideals

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ (∀ (I : LieIdeal R L), IsSolvable ↥I → I = ⊥) ↔ ∀ (I : LieIdeal R L), IsLieAbelian ↥I → I = ⊥
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ Fintype.card m.ToType = m.card

Tactic:
rw [Fintype.card_congr m.coeEquiv]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ Fintype.card ↥m.toEnumFinset = m.card
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:
simp_rw [LieIdeal.mem_killingCompl, LieModule.traceForm_comm]

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 ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 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
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
hχ : Nontrivial ↥(genWeightSpace M χ)
⊢ 0 < b

Tactic:
refine Finset.sum_pos' (fun _ _ ↦ zero_le) ⟨0, Finset.mem_Ioo.mpr ⟨hp₀, hq₀⟩, ?_⟩

Goal state after:
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
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
hχ : Nontrivial ↥(genWeightSpace M χ)
⊢ 0 < finrank R ↥(genWeightSpace M (0 • α + χ))
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
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x : ↥H
hx : x ∈ corootSpace α
hb : 0 < ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
h₁ : iSupIndep fun i ↦ (fun k ↦ ↑(genWeightSpace M (k • α + χ))) ↑i
h₂ :
  ∀ (i : ℤ),
    MapsTo ⇑((toEnd R (↥H) M) x) ↑((fun k ↦ ↑(genWeightSpace M (k • α + χ))) i)
      ↑((fun k ↦ ↑(genWeightSpace M (k • α + χ))) i)
h₃ : ↑(genWeightSpaceChain M α χ p q) = ⨆ i ∈ Finset.Ioo p q, (fun k ↦ ↑(genWeightSpace M (k • α + χ))) i
⊢ ((∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i) • α +
        ↑(∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))) • χ)
      x =
    (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) (LinearMap.restrict ((toEnd R (↥H) M) x) ⋯)

Tactic:
LinearMap.trace_eq_sum_trace_restrict_of_eq_biSup _ h₁ h₂ (genWeightSpaceChain M α χ p q) h₃

Goal state after:
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
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x : ↥H
hx : x ∈ corootSpace α
hb : 0 < ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
h₁ : iSupIndep fun i ↦ (fun k ↦ ↑(genWeightSpace M (k • α + χ))) ↑i
h₂ :
  ∀ (i : ℤ),
    MapsTo ⇑((toEnd R (↥H) M) x) ↑((fun k ↦ ↑(genWeightSpace M (k • α + χ))) i)
      ↑((fun k ↦ ↑(genWeightSpace M (k • α + χ))) i)
h₃ : ↑(genWeightSpaceChain M α χ p q) = ⨆ i ∈ Finset.Ioo p q, (fun k ↦ ↑(genWeightSpace M (k • α + χ))) i
⊢ ((∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i) • α +
        ↑(∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))) • χ)
      x =
    ∑ i ∈ Finset.Ioo p q,
      (LinearMap.trace R ↥↑(genWeightSpace M (i • α + χ))) (LinearMap.restrict ((toEnd R (↥H) M) x) ⋯)
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R N
⊢ map (↑e.flip.symm) p.dualAnnihilator = (map (↑e) p).dualCoannihilator

Tactic:
have : IsReflexive R N := e.isReflexive_of_equiv_dual_of_isReflexive
  rw [← dualCoannihilator_map_linearEquiv_flip, ← LinearEquiv.coe_toLinearMap_flip,
    LinearEquiv.flip_flip]

Goal state after:
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
⊢ span K (range (Weight.toLinear K (↥H) L)) = ⊤

Tactic:
by
  refine eq_top_iff.mpr (le_trans ?_ (LieModule.range_traceForm_le_span_weight K H L))
  rw [← traceForm_flip K H L, ← LinearMap.dualAnnihilator_ker_eq_range_flip,
    ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.dualAnnihilator_bot]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ T R (-↑(k + 1) + 2) + (2 * X * T R (-↑k) - T R (-↑k + 1)) -
      (2 * X * T R (-↑(k + 1) + 1) - T R (-↑(k + 1)) + T R (Int.negSucc k)) =
    0

Tactic:
simp [Int.negSucc_eq]

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ T R (-1 + -↑k + 2) + (2 * X * T R (-↑k) - T R (-↑k + 1)) - 2 * X * T R (-↑k) = 0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ U R (-↑(k + 1) + 2) + (2 * X * U R (-↑k) - U R (-↑k + 1)) -
      (2 * X * U R (-↑(k + 1) + 1) - U R (-↑(k + 1)) + U R (Int.negSucc k)) =
    0

Tactic:
simp [Int.negSucc_eq]

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ U R (-1 + -↑k + 2) + (2 * X * U R (-↑k) - U R (-↑k + 1)) - 2 * X * U R (-↑k) = 0