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

Goal state before:
pp: ι : 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 φ = ⊤
φ : K
⊢ finrank K ↥((f i).maxGenEigenspace φ) < n

Tactic:
simp_rw [not_exists, ← lt_top_iff_ne_top] at hy; exact h_dim ▸ Submodule.finrank_lt (hy φ).ne

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

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
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
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
ih : ∀ (φ : K), ⨆ χ, ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤
φ : K
this : ∀ (χ : ι → K), χ i ≠ φ → ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊥
⊢ ⨆ χ, ⨆ (_ : χ i = φ), ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤

Tactic:
specialize ih φ; rw [iSup_split, biSup_congr this] at ih; simpa using ih

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

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
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
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
ih : ∀ (φ : K), ⨆ χ, ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤
φ : K
χ : ι → K
hχ : χ i ≠ φ
⊢ Disjoint ((f i).maxGenEigenspace φ) (⨅ i, (f i).maxGenEigenspace (χ i))

Tactic:
exact ((f i).disjoint_genEigenspace hχ.symm _ _).mono_right (iInf_le _ i)

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
inst✝ : IsNilpotent L M
x : L
⊢ posFittingCompOf R M x ≤ ⊥

Tactic:
← iInf_lowerCentralSeries_eq_bot_of_isNilpotent,

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
inst✝ : IsNilpotent L M
x : L
⊢ posFittingCompOf R M x ≤ ⨅ k, lowerCentralSeries R L M k
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: 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
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Nontrivial M
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : IsTriangularizable R L M
t : IsSl2Triple h e f
μ₀ : R
hμ₀ : ((toEnd R L M) h).HasEigenvalue μ₀
m₀ : M
hm₀ : ((toEnd R L M) h).HasEigenvector μ₀ m₀
evals : ℕ → R := fun n ↦ μ₀ + 2 * ↑n
e_vecs : ℕ → M := fun n ↦ ((toEnd R L M) e ^ n) m₀
h_exists_zero : ∃ k, e_vecs k = 0
⊢ ∃ μ m, m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ

Tactic:
obtain ⟨n, hn_ne, hn_zero⟩ := Nat.exists_not_and_succ_of_not_zero_of_exists hm₀.2 h_exists_zero

Goal state after:
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
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Nontrivial M
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : IsTriangularizable R L M
t : IsSl2Triple h e f
μ₀ : R
hμ₀ : ((toEnd R L M) h).HasEigenvalue μ₀
m₀ : M
hm₀ : ((toEnd R L M) h).HasEigenvector μ₀ m₀
evals : ℕ → R := fun n ↦ μ₀ + 2 * ↑n
e_vecs : ℕ → M := fun n ↦ ((toEnd R L M) e ^ n) m₀
h_exists_zero : ∃ k, e_vecs k = 0
n : ℕ
hn_ne : ¬e_vecs n = 0
hn_zero : e_vecs (n + 1) = 0
⊢ ∃ μ m, m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: case refine_1
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
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective ⇑f
m : M
hm : ∀ (x : L), ∃ k, (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
⊢ m ∈ genWeightSpace M χ

Tactic:
simp only [mem_genWeightSpace]

Goal state after:
case refine_1
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
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective ⇑f
m : M
hm : ∀ (x : L), ∃ k, (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
⊢ ∀ (x : L), ∃ k, (((toEnd R L M) x - χ x • 1) ^ k) m = 0
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
⊢ B.dualBasis hB (B.flip.dualBasis ⋯ b) = b

Tactic:
ext i

Goal state after:
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
i : ι
⊢ (B.dualBasis hB (B.flip.dualBasis ⋯ b)) i = b i
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:
let e := LieSubmodule.equivMapOfInjective N' N.injective_incl

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
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'))
e : ↥N' ≃ₗ⁅R,L⁆ ↥(LieSubmodule.map N.incl N') := N'.equivMapOfInjective ⋯
⊢ IsCompl (genWeightSpace (↥N') 0) (posFittingComp R L ↥N')
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: case neg
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
⊢ I ≤ sSup {J | IsAtom J ∧ J ≤ I}

Tactic:
let J' := orthogonal Φ hΦ_inv J

Goal state after:
case neg
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
⊢ I ≤ sSup {J | IsAtom J ∧ J ≤ I}
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
this : a ≤ sSup T
⊢ sSup T = a

Tactic:
rwa [ha.le_iff_eq, eq_comm] at this

Goal state after:
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
this : a ≤ sSup T
⊢ a ≠ ⊥
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
⊢ sSup (T₁ ∩ T₂) ≤ sSup T₁ ⊓ sSup T₂

Tactic:
apply le_inf

Goal state after:
case a.a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
⊢ sSup (T₁ ∩ T₂) ≤ sSup T₁

case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
⊢ sSup (T₁ ∩ T₂) ≤ sSup T₂
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case a.left
α : 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 ∈ T₁

Tactic:
apply (hS.mono hT₁).mem_of_isAtom_of_le_sSup_atoms _ _ _

Goal state after:
α : 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
⊢ IsAtom I

α : 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₁
Module: Mathlib.Algebra.Lie.Weights.Linear

Goal state before:
pp: k : Type u_1
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✝² : IsLieAbelian L
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
aux : ∀ (χ : L → R), genWeightSpace M χ ≠ ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
χ : L → R
hχ : genWeightSpace M χ ≠ ⊥
t x : L
⊢ χ 0 = 0

Tactic:
← add_left_inj (χ 0),

Goal state after:
k : Type u_1
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✝² : IsLieAbelian L
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
aux : ∀ (χ : L → R), genWeightSpace M χ ≠ ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
χ : L → R
hχ : genWeightSpace M χ ≠ ⊥
t x : L
⊢ χ 0 + χ 0 = 0 + χ 0
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 α
⊢ IsEmpty (ToType ⟦[]⟧)

Tactic:
dsimp; infer_instance

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 α
⊢ IsEmpty (map f ⟦[]⟧).ToType

Tactic:
dsimp; infer_instance

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

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
change algebraMap K _ _ = _; rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]

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

Goal state before:
pp: case negSucc
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
n : ℕ
hn' : Int.negSucc n ≤ ↑(chainTopCoeff α β)
hn : n.succ ≤ chainBotCoeff α β
⊢ genWeightSpace M (↑n.succ • -α + ⇑β) ≠ ⊥

Tactic:
Nat.cast_smul_eq_nsmul

Goal state after:
case negSucc
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
n : ℕ
hn' : Int.negSucc n ≤ ↑(chainTopCoeff α β)
hn : n.succ ≤ chainBotCoeff α β
⊢ genWeightSpace M (n.succ • -α + ⇑β) ≠ ⊥
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : (s.sup fun i ↦ (g i • ↑S i).degree) = ⊥
⊢ g i = 0

Tactic:
have le_sup := Finset.le_sup hi (f := fun i ↦ (g i • S i).degree)
    exact (smul_eq_zero_iff_left (S.ne_zero i)).mp <| degree_eq_bot.mp (eq_bot_mono le_sup hsupzero)

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✝ : PerfectField K
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
h : ↥H
⊢ ⁅h, x⁆ = α h • x

Tactic:
by
  replace hx : x ∈ (ad K L h).maxGenEigenspace (α h) :=
    genWeightSpace_le_genWeightSpaceOf L h α hx
  rw [(isSemisimple_ad_of_mem_isCartanSubalgebra
    h.property).isFinitelySemisimple.maxGenEigenspace_eq_eigenspace,
    Module.End.mem_eigenspace_iff] at hx
  simpa using hx

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

Goal state before:
pp: motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
neg' : ∀ (n : ℤ), motive (-n) → motive n
n : ℕ
h₀ : motive (-↑n)
h₁ : motive (-↑n + 1)
⊢ motive (-↑n - 1)

Tactic:
cases n with
  | zero => exact neg 1 h₁
  | succ n =>
    apply neg (n + 2) (add_two n (neg' _ h₀) (neg' n ?_))
    convert! h₁ using 1; omega

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
⊢ (traceForm K (↥H) L).orthogonal (K ∙ coroot α) = Weight.ker

Tactic:
by
  if hα : α.IsZero then
    have hα' : coroot α = 0 := by simpa
    replace hα : α.ker = ⊤ := by ext; simp [hα]
    simp [hα, hα']
  else
    refine le_antisymm (fun x hx ↦ ?_) (fun x hx y hy ↦ ?_)
    · simp only [LinearMap.BilinForm.mem_orthogonal_iff] at hx
      specialize hx (coroot α) (Submodule.mem_span_singleton_self _)
      simp only [traceForm_coroot, smul_eq_mul, nsmul_eq_mul,
        Nat.cast_ofNat, mul_eq_zero, OfNat.ofNat_ne_zero, inv_eq_zero, false_or] at hx
      simpa using hx.resolve_left (root_apply_cartanEquivDual_symm_ne_zero hα)
    · have := traceForm_eq_zero_of_mem_ker_of_mem_span_coroot hx hy
      rwa [traceForm_comm] at this

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

Goal state before:
pp: case refine_1
ι : 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 ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
n₁ n₂ : ↑{n | n ≠ 0}
h : (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) n₁ = (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) n₂
⊢ n₁ = n₂

Tactic:
ext i

Goal state after:
case refine_1
ι : 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 ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
n₁ n₂ : ↑{n | n ≠ 0}
h : (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) n₁ = (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) n₂
i : ι
⊢ ↑n₁ i = ↑n₂ i
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case h
ι : 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 ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := ⋯
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := ⋯
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
χ : ↑s
⊢ (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) ⟨Exists.choose ⋯, ⋯⟩ = χ

Tactic:
ext i

Goal state after:
case h
ι : 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 ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
χ : ↑s
i : ↥H
⊢ ↑((fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) ⟨Exists.choose ⋯, ⋯⟩) i = ↑χ i
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
m : ℤ
t : R
ht : t = f y * g x - 2
⊢ ↑((reflection hf * reflection hg) ^ m) =
    LinearMap.id +
        (Polynomial.eval t (S R ((m - 2) / 2)) *
            (Polynomial.eval t (S R ((m - 1) / 2)) + Polynomial.eval t (S R ((m - 3) / 2)))) •
          (LinearMap.smulRight (g x • f - g) y - LinearMap.smulRight f x) +
      (Polynomial.eval t (S R ((m - 1) / 2)) *
          (Polynomial.eval t (S R (m / 2)) + Polynomial.eval t (S R ((m - 2) / 2)))) •
        (LinearMap.smulRight (f y • g - f) x - LinearMap.smulRight g y)

Tactic:
by
  ext z
  simpa using reflection_mul_reflection_zpow_apply hf hg m z t ht

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : n ≠ 0
⊢ n • U R (Int.subNatNat n 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Ico 0 n)

Tactic:
refine Submodule.smul_of_tower_mem _ n ?_

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : n ≠ 0
⊢ U R (Int.subNatNat n 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Ico 0 n)
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
i : ι
inst✝¹ : NeZero 2
inst✝ : IsDomain R
⊢ i ≠ -i

Tactic:
have := Module.IsReflexive.of_isPerfPair P.toLinearMap
  intro contra
  replace contra : P.root i = -P.root i := by simpa using congr_arg P.root contra
  simp [eq_neg_iff_add_eq_zero, ← two_smul R, NeZero.out, P.ne_zero i] at contra

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Finite ↑Φ
hx : x ∈ span R Φ
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
x' : ↥(span R Φ) := ⟨x, hx⟩
F : Dual R M
hF : MapsTo (⇑(preReflection x F)) Φ Φ
y : M
hy : y ∈ span R Φ
hy' : ⟨y, hy⟩ ∈ {x | ↑x ∈ Φ}
⊢ (preReflection x' ((span R Φ).subtype.dualMap F)) ⟨y, hy⟩ ∈ range (inclusion ⋯)

Tactic:
simp only [SetLike.coe_sort_coe, mem_ofPred_eq] at hy' ⊢

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Finite ↑Φ
hx : x ∈ span R Φ
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
x' : ↥(span R Φ) := ⟨x, hx⟩
F : Dual R M
hF : MapsTo (⇑(preReflection x F)) Φ Φ
y : M
hy : y ∈ span R Φ
hy' : y ∈ Φ
⊢ (preReflection x' ((span R Φ).subtype.dualMap F)) ⟨y, hy⟩ ∈ range (inclusion ⋯)
Module: Mathlib.LinearAlgebra.Span.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
p : Submodule R M
inst✝¹ : Algebra.IsEpi R A
inst✝ : Module.Flat R A
f : A ⊗[R] ↥(span A ↑p) →ₗ[A] ↥(span A ↑p) :=
  AlgebraTensorModule.lift (restrictScalarsₗ R A (↥(span A ↑p)) (↥(span A ↑p)) A ∘ₗ lsmul A ↥(span A ↑p))
g : A ⊗[R] ↥p →ₗ[R] A ⊗[R] ↥(span A ↑p) := lTensor A (inclusionSpan A p)
hf : Injective ⇑f
hg : Injective ⇑g
this : ↑R (tensorToSpan A p) = ↑R f ∘ₗ g
⊢ Injective (⇑(↑R f) ∘ ⇑g)

Tactic:
exact hf.comp hg

Goal state after: