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

Goal state before:
pp: case pos
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₀)
⊢ m μ ∈ p

Tactic:
let g : End K V := (m.support.erase μ).noncommProd _ fun μ₁ _ μ₂ _ _ ↦ h_comm μ₁ μ₂

Goal state after:
case pos
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₀) ⋯
⊢ m μ ∈ p
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
K : IntermediateField F E
⊢ finrank F ↥K = 1 ↔ K.toSubalgebra = ⊥.toSubalgebra

Tactic:
← finrank_eq_finrank_subalgebra,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
⊢ finrank F ↥K.toSubalgebra = 1 ↔ K.toSubalgebra = ⊥.toSubalgebra
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
⊢ finrank F ↥⊥ = 1

Tactic:
by
  rw [finrank_eq_one_iff]

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

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

Tactic:
replace hy : ∀ φ, finrank K ((f i).maxGenEigenspace φ) < n := fun φ ↦ by
      simp_rw [not_exists, ← lt_top_iff_ne_top] at hy; exact h_dim ▸ Submodule.finrank_lt (hy φ).ne

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

Goal state before:
pp: F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} #↥(adjoin F s).toSubfield ≤ max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀

Tactic:
adjoin_toSubfield

Goal state after:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} #↥(Subfield.closure (Set.range ⇑(algebraMap F E) ∪ s)) ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case inl
ι : Type u_1
K : Type u_3
M : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun i j ↦ Commute (f i) (f j)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
j : ι
⊢ Commute (f j) (f j)

Tactic:
tauto

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

Goal state before:
pp: case inr
ι : Type u_1
K : Type u_3
M : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun i j ↦ Commute (f i) (f j)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
i j : ι
hij : j ≠ i
⊢ Commute (f j) (f i)

Tactic:
tauto

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

Goal state before:
pp: case succ
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✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
n : ℕ
hn : μ = ↑n
n✝ : ℕ
a✝ : n✝ ≤ n → ((toEnd R L M) f ^ n✝) m = 0 → False
hi : n✝ + 1 ≤ n
H : ((toEnd R L M) f ^ (n✝ + 1)) m = 0
⊢ False

Tactic:
next i IH =>
    have : ((i + 1) * (n - i) : ℤ) • (toEnd R L M f ^ i) m = 0 := by
      have := congr_arg (⁅e, ·⁆) H
      simpa [← Int.cast_smul_eq_zsmul R, P.lie_e_pow_succ_toEnd_f, hn] using this
    rw [← Int.cast_smul_eq_zsmul R, smul_eq_zero, Int.cast_eq_zero, mul_eq_zero, sub_eq_zero,
      Nat.cast_inj, ← @Nat.cast_one ℤ, ← Nat.cast_add, Nat.cast_eq_zero] at this
    simp only [add_eq_zero, one_ne_zero, and_false, false_or] at this
    exact (hi.trans_eq (this.resolve_right (IH (i.le_succ.trans hi)))).not_gt i.lt_succ_self

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
B : BilinForm R M
r : S
x y : M
⊢ (B x) (r • y) = r • (B x) y

Tactic:
rw [← IsScalarTower.algebraMap_smul R r, smul_right, Algebra.smul_def]

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✝¹ : Nontrivial M
inst✝ : IsTriangularizable R L M
x : L
this : ∀ (φ : R), ((toEnd R L M) x).maxGenEigenspace φ = ⊥
⊢ ⨆ φ, ((toEnd R L M) x).maxGenEigenspace φ ≠ ⊤

Tactic:
simp [this]

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

Goal state before:
pp: case a
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
⊢ ∀ (a : LieIdeal K L), IsAtom a → a ≤ J' → a ≤ I → IsAtom a ∧ a ≤ I

Tactic:
tauto

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x✝ : α
⊢ (x✝ ∈ Ta ∨ x✝ ∈ Tb) ∧ (x✝ ∈ Ta ∨ x✝ ∈ Tc) ↔ x✝ ∈ Ta ∨ x✝ ∈ Tb ∧ x✝ ∈ Tc

Tactic:
tauto

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case hT₁
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
⊢ Ta ⊆ S ∧ Tb ⊆ S

Tactic:
tauto

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case hT₂
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
⊢ Ta ⊆ S ∧ Tc ⊆ S

Tactic:
tauto

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : Type u_3
m : Multiset α
f : α → β
⊢ map (f ∘ fun x ↦ x.fst) Finset.univ.val = map f m

Tactic:
rw [← Multiset.map_map, Multiset.map_univ_coe]

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

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

Tactic:
Finset.card,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ m.toEnumFinset.val.card = m.card
Module: Mathlib.Algebra.Lie.Weights.Linear

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
inst✝ : LinearWeights R L M
x : L
⊢ (toEnd R L ↥(shiftedGenWeightSpace R L M χ)) x =
    (shift R L M χ).conj ((toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id)

Tactic:
tauto

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
f : α → β
l : List α
a : α
s : List α
x✝ : { v // ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst }
v : ToType ⟦s⟧ ≃ (map f ⟦s⟧).ToType
hv : ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst
x : ToType ⟦a :: s⟧
⊢ ((((consEquiv.trans v.optionCongr).trans consEquiv.symm).trans (cast ⋯).symm) x).fst = f x.fst

Tactic:
simp only [consEquiv, Equiv.trans_apply, Equiv.coe_fn_mk, Equiv.optionCongr_apply,
            Equiv.coe_fn_symm_mk]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
f : α → β
l : List α
a : α
s : List α
x✝ : { v // ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst }
v : ToType ⟦s⟧ ≃ (map f ⟦s⟧).ToType
hv : ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst
x : ToType ⟦a :: s⟧
⊢ ((cast ⋯).symm
        ((Option.map (⇑v) (if h : x.fst = a ∧ ↑x.snd = count a ⟦s⟧ then none else some ⟨x.fst, ⟨↑x.snd, ⋯⟩⟩)).elim
          ⟨f a, ⟨count (f a) (map f ⟦s⟧), ⋯⟩⟩ fun x ↦ ⟨x.fst, Fin.castLE ⋯ x.snd⟩)).fst =
    f x.fst
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: K : Type v
inst✝ : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
⊢ eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) (f.factor * g) = 0

Tactic:
eval₂_mul,

Goal state after:
K : Type v
inst✝ : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
⊢ eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) f.factor *
      eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) g =
    0
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝² : Field k
K : Type ?u.6
inst✝¹ : Field K
inst✝ : DecidableEq K
i : k →+* K
f : Monics k
hf : (map i ↑f).Splits
⊢ (map i ↑f).roots.toEnumFinset.card = (↑f).natDegree

Tactic:
splits_iff_card_roots,

Goal state after:
k : Type u
inst✝² : Field k
K : Type ?u.6
inst✝¹ : Field K
inst✝ : DecidableEq K
i : k →+* K
f : Monics k
hf : (map i ↑f).roots.card = (map i ↑f).natDegree
⊢ (map i ↑f).roots.toEnumFinset.card = (↑f).natDegree
Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple

Goal state before:
pp: case mpr.inr
K : Type u_3
V : Type u_4
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
h : ∀ (μ : K), f.HasEigenvalue μ → μ = 0
μ : K
hμ : μ ≠ 0
this : f.eigenspace μ = ⊥
⊢ f.eigenspace μ ≤ f.eigenspace 0

Tactic:
simp [this]

Goal state after:
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
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ chainTopCoeff α β + 1 = Nat.find ⋯

Tactic:
chainTopCoeff,

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
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ (if hα : α = 0 then 0 else (Nat.find ⋯).pred) + 1 = Nat.find ⋯
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
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
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x : L
hx : x ∈ LieAlgebra.derivedSeries R L 1
⊢ x ∈ Submodule.span R {x | ∃ u v, ⁅u, v⁆ = x}

Tactic:
rw [← LieAlgebra.coe_derivedSeries_one_eq]

Goal state after:
R : Type u_1
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
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x : L
hx : x ∈ LieAlgebra.derivedSeries R L 1
⊢ x ∈ (LieIdeal.toLieSubalgebra R L (LieAlgebra.derivedSeries R L 1)).toSubmodule
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: case succ
R : Type u_1
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
k : ℕ
ih : ∀ {x y : L}, x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((traceForm R L M) x) y = 0
x y : L
hx : x ∈ ⊤.lcs L (k + 1)
hy : ∀ (x : L), ⁅x, y⁆ ∈ LieSubmodule.ucs k ⊥
⊢ ((traceForm R L M) x) y = 0

Tactic:
LieIdeal.lcs_succ,

Goal state after:
case succ
R : Type u_1
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
k : ℕ
ih : ∀ {x y : L}, x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((traceForm R L M) x) y = 0
x y : L
hy : ∀ (x : L), ⁅x, y⁆ ∈ LieSubmodule.ucs k ⊥
hx : x ∈ ⁅⊤, ⊤.lcs L k⁆
⊢ ((traceForm R L M) x) y = 0
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: case succ
R : Type u_1
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
k : ℕ
ih : ∀ {x y : L}, x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((traceForm R L M) x) y = 0
x y : L
hx : x ∈ ⊤.lcs L (k + 1)
hy : y ∈ LieSubmodule.ucs (k + 1) ⊥
⊢ ((traceForm R L M) x) y = 0

Tactic:
rw [LieSubmodule.ucs_succ, LieSubmodule.mem_normalizer] at hy
    simp_rw [LieIdeal.lcs_succ, ← LieSubmodule.mem_toSubmodule,
      LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_top, true_and] at hx
    refine Submodule.span_induction ?_ ?_ (fun z w _ _ hz hw ↦ ?_) (fun t z _ hz ↦ ?_) hx
    · rintro - ⟨z, w, hw, rfl⟩
      rw [← lie_skew, map_neg, LinearMap.neg_apply, neg_eq_zero, traceForm_apply_lie_apply]
      exact ih hw (hy _)
    · simp
    · simp [hz, hw]
    · simp [hz]

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
⊢ corootSpace 0 = ⊥

Tactic:
refine eq_bot_iff.mpr fun x hx ↦ ?_

Goal state after:
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
x : ↥H
hx : x ∈ corootSpace 0
⊢ x ∈ ⊥
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
α : Weight K (↥H) L
⊢ α.IsZero ∨ ∃ x, x.IsNonZero ∧ Weight.toLinear K (↥H) L x = Weight.toLinear K (↥H) L α

Tactic:
tauto

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

Goal state before:
pp: R : Type u_1
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✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
hy' : ∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N
this✝ : ∀ (m : M), ⁅x, ⁅y, m⁆⁆ ∈ N
this : (trace R ↥N) ((φ x ∘ₗ φ y).restrict ⋯) = (trace R M) (φ x ∘ₗ φ y)
⊢ (trace R M) (φ x ∘ₗ φ y) = (trace R ↥N) ((φ x ∘ₗ φ y).restrict hy')

Tactic:
simp [this]

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

Goal state before:
pp: R : Type u_1
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✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
inst✝ : LieModule.IsTrivial ↥I ↥N
hy' : ∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N := fun m x_1 ↦ N.lie_mem ((mem_idealizer N).mp (h hy) m)
n : ↥N
this : ⁅y, ↑n⁆ = 0
⊢ ↑(((φ x ∘ₗ φ y).restrict hy') n) = ↑(0 n)

Tactic:
simp [this]

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

Goal state before:
pp: K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
this :
  ∑ χ with χ.IsZero, finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ) =
    0
⊢ ∑ x with x.IsNonZero,
        finrank K ↥(genWeightSpace M ⇑x) • (Weight.toLinear K L M x).smulRight (Weight.toLinear K L M x) +
      ∑ x with ¬x.IsNonZero,
        finrank K ↥(genWeightSpace M ⇑x) • (Weight.toLinear K L M x).smulRight (Weight.toLinear K L M x) =
    ∑ χ with χ.IsNonZero,
      finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ)

Tactic:
simp [this]

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

Goal state before:
pp: case refine_2
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✝ : PerfectField K
α : Weight K (↥H) L
⊢ (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) ∈ corootSpace ⇑α

Tactic:
exact cartanEquivDual_symm_apply_mem_corootSpace α

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
inst✝ : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
this : IsUnit (2 * (α α')⁻¹)
⊢ K ∙ 2 • (α α')⁻¹ • α' = K ∙ α'

Tactic:
simpa [← Nat.cast_smul_eq_nsmul K, smul_smul] using Submodule.span_singleton_smul_eq this _

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
inst✝ : CharZero K
α : Weight K (↥H) L
h₀ : ¬α.IsZero
t : K
h_two : α (t • coroot α) = 2
h_mem : t • coroot α ∈ K ∙ coroot α
this : t = 1
⊢ t • coroot α = coroot α

Tactic:
simp [this]

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

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
⊢ T R (-1) = T R 1

Tactic:
simp only [T_neg_one, T_one]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
x : L
hx : x ∈ lieSpan R L (range b.e ∪ range b.f)
⊢ x ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
induction hx using lieSpan_induction with
  | mem u hu =>
    rcases (mem_union _ _ _).mpr hu with hu | hu
    · exact LieSubmodule.mem_sup_right <| subset_lieSpan hu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| subset_lieSpan hu
  | zero => simp
  | add u v _ _ hu hv => exact add_mem hu hv
  | smul t u _ hu => exact SMulMemClass.smul_mem t hu
  | lie u v _ _ hu hv =>
    obtain ⟨yc, hyc, yl, hyl, yu, hyu, rfl⟩ :
        ∃ᵉ (yc ∈ H) (yl ∈ lieSpan R L (range b.f)) (yu ∈ lieSpan R L (range b.e)),
          yc + yl + yu = u := by simpa [LieSubmodule.mem_sup] using! hu
    obtain ⟨zc, hzc, zl, hzl, zu, hzu, rfl⟩ :
        ∃ᵉ (zc ∈ H) (zl ∈ lieSpan R L (range b.f)) (zu ∈ lieSpan R L (range b.e)),
          zc + zl + zu = v := by simpa [LieSubmodule.mem_sup] using! hv
    simp only [lie_add, add_lie, ← add_assoc]
    repeat apply add_mem
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_left <| lie_mem _ hyc hzc
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨zc, hzc⟩) hyl
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨zc, hzc⟩) hyu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨yc, hyc⟩) hzl
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| lie_mem _ hyl hzl
    · exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hyu hzl
    · exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hzu
    · rw [← lie_skew, neg_mem_iff]
      exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hzu hyl
    · exact LieSubmodule.mem_sup_right <| lie_mem _ hyu hzu

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁴ : Finite ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝ : Fintype ι
i j : ι
e : ↥H.toSubmodule ≃ₗ[R] ↥(Submodule.span R (range b.h)) :=
  LinearEquiv.ofEq H.toSubmodule (Submodule.span R (range b.h)) ⋯
f : ι → R := fun k ↦ b.A i k • ((Basis.span ⋯).repr (e (b.h' j))) k
this : f = fun k ↦ if j = k then ↑(b.A i k) else 0
⊢ ∑ k, f k = ↑(b.A i j)

Tactic:
simp [this]

Goal state after: