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 (↑g (m • b)) * map (↑g) (X ^ (n + 1)) = m • map (↑g) (C b * X ^ (n + 1))

Tactic:
Polynomial.map_pow,

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 (↑g (m • b)) * map (↑g) X ^ (n + 1) = m • map (↑g) (C b * X ^ (n + 1))
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) = m • (C (↑g b) * map (↑g) (X ^ (n + 1)))

Tactic:
Polynomial.map_pow,

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) = m • (C (↑g b) * map (↑g) X ^ (n + 1))
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNilpotent L M
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k = ⊥

Tactic:
by simp [hk]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ ∑ x ∈ s, g • l x * (toFun G F) x g' = ∑ x ∈ s, l x • (toFun G F) x g'

Tactic:
conv_lhs =>
    congr
    · skip
    · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]

Goal state after:
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ ∑ x ∈ s, g • (l x * (toFun G F) x (g⁻¹ * g')) = ∑ x ∈ s, l x • (toFun G F) x g'
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x f = 0 ∨ Polynomial.eval₂ (subfield G F).subtype x g = 0
⊢ f = 1 ∨ g = 1

Tactic:
rcases this with this | this

Goal state after:
case inl
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x f = 0
⊢ f = 1 ∨ g = 1

case inr
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x g = 0
⊢ f = 1 ∨ g = 1
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ (Polynomial.map (subfield G F).subtype ((prodXSubSMul G F x).toSubring (subfield G F).toSubring ⋯)).Splits

Tactic:
Polynomial.map_toSubring _ (subfield G F).toSubring,

Goal state after:
case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ (prodXSubSMul G F x).Splits
Module: Mathlib.RingTheory.Adjoin.Dimension

Goal state before:
pp: case neg.inr
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
this✝ :
  ∀ (A B : Subalgebra R S) [Free R ↥A] [Free R ↥B],
    ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B) → ¬Module.Finite R ↥A → finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B
hA : ¬¬Module.Finite R ↥A
this : finrank R ↥(B ⊔ A) ≤ finrank R ↥B * finrank R ↥A
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
rwa [sup_comm, mul_comm] at this

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: 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✝² : Algebra.IsAlgebraic F K
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
⊢ Algebra.IsAlgebraic F L

Tactic:
by
  have : FiniteDimensional K L := IsSplittingField.finiteDimensional L f
  exact Algebra.IsAlgebraic.trans F K L

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

Goal state before:
pp: case neg
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → ∃ x, eval x p = 0
p : k[X]
hp0 : ¬p = 0
u : k[X]ˣ
hu : (UniqueFactorizationMonoid.factors p).prod * ↑u = p
f : k[X]
hf : f ∈ UniqueFactorizationMonoid.factors p
h : Irreducible f := UniqueFactorizationMonoid.irreducible_of_factor f hf
x : k
hx : eval x f = 0
⊢ f.Splits

Tactic:
exact Splits.of_degree_eq_one (degree_eq_one_of_irreducible_of_root h hx)

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

Goal state before:
pp: k : Type u
inst✝¹⁸ : Field k
K✝ : Type u
inst✝¹⁷ : Field K✝
L : Type v
M : Type w
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra K✝ L
inst✝¹⁴ : Field M
inst✝¹³ : Algebra K✝ M
inst✝¹² : IsAlgClosed M
inst✝¹¹ : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type v
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R M
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree R M
inst✝² : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := X ^ (n + 1) - 1
hfsep : f.Separable
hroot : n.succ = Fintype.card ↑(f.rootSet K)
⊢ (Fintype.card K).succ ≤ Fintype.card K

Tactic:
hroot

Goal state after:
k : Type u
inst✝¹⁸ : Field k
K✝ : Type u
inst✝¹⁷ : Field K✝
L : Type v
M : Type w
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra K✝ L
inst✝¹⁴ : Field M
inst✝¹³ : Algebra K✝ M
inst✝¹² : IsAlgClosed M
inst✝¹¹ : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type v
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R M
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree R M
inst✝² : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := X ^ (n + 1) - 1
hfsep : f.Separable
hroot : n.succ = Fintype.card ↑(f.rootSet K)
⊢ Fintype.card ↑(f.rootSet K) ≤ Fintype.card K
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (i j : ι) (φ : R), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
l : ι
χ : ι → R
⊢ MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))

Tactic:
intro x hx

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (i j : ι) (φ : R), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
l : ι
χ : ι → R
x : M
hx : x ∈ ⨅ i, ↑((f i).maxGenEigenspace (χ i))
⊢ (f l) x ∈ ⨅ i, ↑((f i).maxGenEigenspace (χ i))
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ Module.finrank K ↥K⟮x⟯ = (minpoly K x).natDegree

Tactic:
by
  rw [PowerBasis.finrank (adjoin.powerBasis hx :)]
  rfl

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 μ
⊢ MapsTo ⇑(f - (algebraMap K (End K V)) μ') ↑p ↑p

Tactic:
intro x hx

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
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
μ' : K
x✝ : μ' ∈ m.support.erase μ
x : V
hx : x ∈ ↑p
⊢ (f - (algebraMap K (End K V)) μ') x ∈ ↑p
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
x : E
y : K
hx : x ∈ adjoin F S
hy : (aeval y) (minpoly F x) = 0
this : Algebra.IsAlgebraic F ↥(adjoin F S)
⊢ ∃ φ, φ ⟨x, hx⟩ = y

Tactic:
have ix : IsAlgebraic F _ := Algebra.IsAlgebraic.isAlgebraic (⟨x, hx⟩ : adjoin F S)

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
x : E
y : K
hx : x ∈ adjoin F S
hy : (aeval y) (minpoly F x) = 0
this : Algebra.IsAlgebraic F ↥(adjoin F S)
ix : IsAlgebraic F ⟨x, hx⟩
⊢ ∃ φ, φ ⟨x, hx⟩ = y
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 μ
x : V
hx : x ∈ ↑p
⊢ f x - μ' • x ∈ ↑p

Tactic:
exact p.sub_mem (h _ hx) (smul_mem p μ' hx)

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

Goal state before:
pp: case none
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
m : K →₀ V
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
μ : K
hμ : μ ∈ m.support
l : 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 μ)
hg₁ : MapsTo ⇑g ↑p ↑p
μ' : K
_hμ' : μ' ∈ m.support.erase μ
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) none
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) none
hlk : ∀ (i : K), ↑(l i) ≤ none
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) none) ↑((f.genEigenspace μ) none)
this : iSupIndep fun x ↦ (f.genEigenspace x) none
⊢ ↑l₀ ≤ none

pp: case some
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
m : K →₀ V
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
μ : K
hμ : μ ∈ m.support
l : 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 μ)
hg₁ : MapsTo ⇑g ↑p ↑p
μ' : K
_hμ' : μ' ∈ m.support.erase μ
k : ℕ
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) (some k)
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) (some k)
hlk : ∀ (i : K), ↑(l i) ≤ some k
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) (some k)) ↑((f.genEigenspace μ) (some k))
this : iSupIndep fun x ↦ (f.genEigenspace x) (some k)
⊢ ↑l₀ ≤ some k

Tactic:
· exact le_top

Goal state after:
case some
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
m : K →₀ V
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
μ : K
hμ : μ ∈ m.support
l : 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 μ)
hg₁ : MapsTo ⇑g ↑p ↑p
μ' : K
_hμ' : μ' ∈ m.support.erase μ
k : ℕ
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) (some k)
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) (some k)
hlk : ∀ (i : K), ↑(l i) ≤ some k
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) (some k)) ↑((f.genEigenspace μ) (some k))
this : iSupIndep fun x ↦ (f.genEigenspace x) (some k)
⊢ ↑l₀ ≤ some k
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
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
⊢ p = p ⊓ ⨆ μ, (f.genEigenspace μ) k

Tactic:
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
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
⊢ p = p ⊓ ⊤
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
⊢ H.toLieSubmodule ≤ rootSpace H 0

Tactic:
intro x hx

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
x : L
hx : x ∈ H.toLieSubmodule
⊢ x ∈ rootSpace H 0
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
⊢ (zeroRootSubalgebra R L H).normalizer ≤ zeroRootSubalgebra R L H

Tactic:
intro x hx

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
x : L
hx : x ∈ (zeroRootSubalgebra R L H).normalizer
⊢ x ∈ zeroRootSubalgebra R L H
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✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
x : L
φ₁ φ₂ : R
h : φ₁ ≠ φ₂
⊢ Disjoint (((toEnd R L M) x).maxGenEigenspace φ₁) (((toEnd R L M) x).maxGenEigenspace φ₂)

Tactic:
exact Module.End.disjoint_genEigenspace _ h _ _

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

Goal state before:
pp: case mp.right
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 : x ∈ W
hker : ⟨x, hx⟩ ∈ ↑(domRestrict B W).ker
⊢ (Submodule.subtype W) ⟨x, hx⟩ ∈ ↑(ker B)

Tactic:
· simpa

Goal state after:
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
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
⊢ W ⊓ B.orthogonal W ≤ ⊥

Tactic:
intro x hx

Goal state after:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
x : V
hx : x ∈ W ⊓ B.orthogonal W
⊢ x ∈ ⊥
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
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map ↑I.incl ↑J;
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
this : J' ≤ ⊥
⊢ J ≤ ⊥

Tactic:
intro x hx

Goal state after:
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
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map ↑I.incl ↑J;
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
this : J' ≤ ⊥
x : ↥I
hx : x ∈ J
⊢ x ∈ ⊥
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x ↦ a = x.1) s.val).card > 0
h : {x ∈ s | x.1 = a} ⊆ {a} ×ˢ Finset.range ((filter (fun x ↦ a = x.1) s.val).card - 1)
⊢ (filter (fun x ↦ a = x.1) s.val).card ≤ (filter (fun x ↦ a = x.1) s.val).card - 1

Tactic:
simpa [Finset.card, eq_comm] using Finset.card_mono h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p ∈ m₁.toEnumFinset → p ∈ m₂.toEnumFinset

Tactic:
simp only [Multiset.mem_toEnumFinset]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p.2 < count p.1 m₁ → p.2 < count p.1 m₂
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p.2 < count p.1 m₁ → p.2 < count p.1 m₂

Tactic:
exact lt_of_le_of_lt' (Multiset.le_iff_count.mp h p.1)

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

Goal state before:
pp: case inr
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
⊢ I ≤ K

Tactic:
intro x hx

Goal state after:
case inr
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
x : L
hx : x ∈ I
⊢ x ∈ K
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
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
x y : ↥J
⊢ ⁅↑x, ↑y⁆ = 0

Tactic:
have : (⁅(⟨x, hJ' x.2⟩ : I), ⟨y, hJ' y.2⟩⁆ : I) = 0 := trivial_lie_zero _ _ _ _

Goal state after:
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 : IsLieAbelian ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
x y : ↥J
this : ⁅⟨↑x, ⋯⟩, ⟨↑y, ⋯⟩⁆ = 0
⊢ ⁅↑x, ↑y⁆ = 0
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'
⊢ (∀ y ∈ ⊤, ((killingForm R L') y) x' = 0) ↔ x' ∈ ⊥

Tactic:
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' ∈ ⊥