mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: case h
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)
f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)
h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0
k₂ : ℕ
hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0
hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0
hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0
hf_comm : Commute f₁ f₂
⊢ ∑ x ∈ Finset.antidiagonal (k₁ + k₂ - 1), (k₁ + k₂ - 1).choose x.1 • (f₁ ^ x.1 * f₂ ^ x.2) (m₁ ⊗ₜ[R] m₂) = 0

Tactic:
apply Finset.sum_eq_zero

Goal state after:
case h
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := ⋯
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) := ⋯
f₂ : Module.End R (M₁ ⊗[R] M₂) := ⋯
h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0
k₂ : ℕ
hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0
hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0
hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0
hf_comm : Commute f₁ f₂
⊢ ∀ x ∈ Finset.antidiagonal (k₁ + k₂ - 1), (k₁ + k₂ - 1).choose x.1 • (f₁ ^ x.1 * f₂ ^ x.2) (m₁ ⊗ₜ[R] m₂) = 0
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: case h.inl
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)
f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)
h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0
k₂ : ℕ
hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0
hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0
hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal (k₁ + k₂ - 1)
hi : k₁ ≤ (i, j).1
⊢ (f₂ ^ j) ((f₁ ^ i) (m₁ ⊗ₜ[R] m₂)) = 0

Tactic:
Module.End.pow_map_zero_of_le hi hf₁,

Goal state after:
case h.inl
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)
f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)
h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0
k₂ : ℕ
hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0
hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0
hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal (k₁ + k₂ - 1)
hi : k₁ ≤ (i, j).1
⊢ (f₂ ^ j) 0 = 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
⊢ H.toLieSubmodule ≤ rootSpace H 0

Tactic:
intro x hx
  simp only [LieSubalgebra.mem_toLieSubmodule] at hx
  simp only [mem_genWeightSpace, Pi.zero_apply, sub_zero, zero_smul]
  intro y
  obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R H H
  use k
  let f : Module.End R H := toEnd R H H y
  let g : Module.End R L := toEnd R H L y
  have hfg : g.comp (H : Submodule R L).subtype = (H : Submodule R L).subtype.comp f := rfl
  change (g ^ k).comp (H : Submodule R L).subtype ⟨x, hx⟩ = 0
  rw [Module.End.commute_pow_left_of_commute hfg k]
  have h := iterate_toEnd_mem_lowerCentralSeries R H H y ⟨x, hx⟩ k
  rw [hk, LieSubmodule.mem_bot] at h
  simp only [Submodule.subtype_apply, Function.comp_apply, Module.End.pow_apply, LinearMap.coe_comp,
    Submodule.coe_eq_zero]
  exact h

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

Goal state before:
pp: case zero
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
hm : ⁅h, m⁆ = μ • m
⊢ ⁅h, ((toEnd R L M) e ^ 0) m⁆ = (μ + 2 * ↑0) • ((toEnd R L M) e ^ 0) m

Tactic:
simpa using hm

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
y : M
⊢ y ∈ orthogonal Φ hΦ_inv N ↔ ∀ x ∈ N, (Φ x) y = 0

Tactic:
simp [orthogonal, LinearMap.BilinForm.mem_orthogonal_iff]

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✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
χ : L → R
x : L
this : (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x) = χ x * ↑(finrank R ↥(genWeightSpace M χ))
⊢ (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x) = finrank R ↥(genWeightSpace M χ) • χ x

Tactic:
mul_comm,

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✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
χ : L → R
x : L
this : (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x) = ↑(finrank R ↥(genWeightSpace M χ)) * χ x
⊢ (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x) = finrank R ↥(genWeightSpace M χ) • χ x
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: K : Type u_1
L : Type u_3
M : Type u_4
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieRing.IsNilpotent L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
inst✝ : IsTriangularizable K L M
N : LieSubmodule K L M
⊢ ⨆ i, LieSubmodule.map N.incl (genWeightSpace ↥N ⇑i) ≤ ⨆ χ, N ⊓ genWeightSpace M ⇑χ

Tactic:
refine iSup_le fun χ_N ↦ ?_

Goal state after:
K : Type u_1
L : Type u_3
M : Type u_4
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieRing.IsNilpotent L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
inst✝ : IsTriangularizable K L M
N : LieSubmodule K L M
χ_N : Weight K L ↥N
⊢ LieSubmodule.map N.incl (genWeightSpace ↥N ⇑χ_N) ≤ ⨆ χ, N ⊓ genWeightSpace M ⇑χ
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 := ⋯
this : I ≤ J ⊔ J' ⊓ I
⊢ J ≤ sSup {J | IsAtom J ∧ J ≤ I}

Tactic:
exact le_sSup ⟨hJ, hJI⟩

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

Goal state before:
pp: case mp
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 ∈ (domRestrict B W).range.dualCoannihilator
⊢ ∀ n ∈ W, (B n) x = 0

Tactic:
intro y hy
    rw [Submodule.mem_dualCoannihilator] at hx
    exact hx (B.domRestrict W ⟨y, hy⟩) ⟨⟨y, hy⟩, rfl⟩

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
hB : B.Nondegenerate
hB₀ : B.IsRefl
W : Submodule K V
⊢ B.orthogonal (B.orthogonal W) = W

Tactic:
by
  apply (eq_of_le_of_finrank_le (LinearMap.BilinForm.le_orthogonal_orthogonal hB₀) _).symm
  simp only [finrank_orthogonal hB]
  lia

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
x : α
i : ℕ
⊢ (∃ a ∈ m, ∃ a_1 < count a m, { toFun := Prod.mk a, inj' := ⋯ } a_1 = (x, i)) ↔ (x, i) ∈ {p | p.2 < count p.1 m}

Tactic:
Function.Embedding.coeFn_mk,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
x : α
i : ℕ
⊢ (∃ a ∈ m, ∃ a_1 < count a m, (a, a_1) = (x, i)) ↔ (x, i) ∈ {p | p.2 < count p.1 m}
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: case pos
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
⊢ f.factor ∣ f

pp: case neg
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ f.factor ∣ f

Tactic:
· rw [hf2]; exact dvd_zero _

Goal state after:
case neg
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ f.factor ∣ f
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (1 * (Multiset.map (fun x ↦ X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod -
          (Multiset.map (fun x ↦ X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod).coeff
      n =
    0

Tactic:
one_mul,

Goal state after:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ ((Multiset.map (fun x ↦ X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod -
          (Multiset.map (fun x ↦ X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod).coeff
      n =
    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'
e : L ≃ₗ⁅R⁆ L'
x y : L
⊢ ((killingForm R L') (e x)) (e y) = ((killingForm R L) x) y

Tactic:
killingForm_apply_apply,

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'
e : L ≃ₗ⁅R⁆ L'
x y : L
⊢ (LinearMap.trace R L') ((ad R L') (e x) ∘ₗ (ad R L') (e y)) = (LinearMap.trace R L) ((ad R L) x ∘ₗ (ad R L) y)
Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple

Goal state before:
pp: 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
this : f.eigenspace 0 = ⊤
⊢ f = 0

Tactic:
by rwa [eigenspace_zero, LinearMap.ker_eq_top] at this

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

Goal state before:
pp: case mem
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y : M
k : Subtype (Membership.mem (Ioo p q))
z : M
hz : z ∈ genWeightSpace M (↑k • α + χ)
⊢ ⁅x, z⁆ ∈ genWeightSpaceChain M α χ p q

Tactic:
| mem k z hz =>

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
x y : L
hx : x ∈ lowerCentralSeries R L L 1
hy : y ∈ LieAlgebra.center R L
⊢ ((traceForm R L M) x) y = 0

Tactic:
apply traceForm_eq_zero_if_mem_lcs_of_mem_ucs R L M 1

Goal state after:
case hx
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
x y : L
hx : x ∈ lowerCentralSeries R L L 1
hy : y ∈ LieAlgebra.center R L
⊢ x ∈ ⊤.lcs L 1

case hy
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
x y : L
hx : x ∈ lowerCentralSeries R L L 1
hy : y ∈ LieAlgebra.center R L
⊢ y ∈ LieSubmodule.ucs 1 ⊥
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie.a.a.a.a.a.a.a.a
ι : 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 yc : L
hyc : yc ∈ H
yl : L
hyl : yl ∈ lieSpan R L (range b.f)
yu : L
hyu : yu ∈ lieSpan R L (range b.e)
hx✝ : yc + yl + yu ∈ lieSpan R L (range b.e ∪ range b.f)
hu : yc + yl + yu ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ H
zl : L
hzl : zl ∈ lieSpan R L (range b.f)
zu : L
hzu : zu ∈ lieSpan R L (range b.e)
hy✝ : zc + zl + zu ∈ lieSpan R L (range b.e ∪ range b.f)
hv : zc + zl + zu ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅zc, yl⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨zc, hzc⟩) hyl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ eval 1 (T R n) = 1

Tactic:
by
  induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 => simp [T_add_two, ih1, ih2]; norm_num
  | neg_add_one n ih1 ih2 => simp [T_sub_one, -T_neg, ih1, ih2]; norm_num

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (T R (↑n + 1)).degree = ↑(↑n + 1).natAbs
ih2 : (T R ↑n).degree = ↑(↑n).natAbs
⊢ (X * T R (↑n + 1)).degree = ↑(n + 2)

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (T R (↑n + 1)).degree = ↑(↑n + 1).natAbs
ih2 : (T R ↑n).degree = ↑(↑n).natAbs
⊢ (T R (↑n + 1) * X).degree = ↑(n + 2)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (T R (↑n + 1)).leadingCoeff = 2 ^ ((↑n + 1).natAbs - 1)
ih2 : (T R ↑n).leadingCoeff = 2 ^ ((↑n).natAbs - 1)
this : leadingCoeff 2 = 2
⊢ (T R ↑n).degree < (X * T R (↑n + 1)).degree

Tactic:
mul_comm,

Goal state after:
case add_two
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (T R (↑n + 1)).leadingCoeff = 2 ^ ((↑n + 1).natAbs - 1)
ih2 : (T R ↑n).leadingCoeff = 2 ^ ((↑n).natAbs - 1)
this : leadingCoeff 2 = 2
⊢ (T R ↑n).degree < (T R (↑n + 1) * X).degree
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (U R ↑n).degree = ↑n
ih2 : (U R (↑n + 1)).degree = ↑n + 1
⊢ (X * U R (↑n + 1)).degree = ↑(n + 2)

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (U R ↑n).degree = ↑n
ih2 : (U R (↑n + 1)).degree = ↑n + 1
⊢ (U R (↑n + 1) * X).degree = ↑(n + 2)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ (U R ↑n).degree < (X * U R ↑(n + 1)).degree

Tactic:
mul_comm,

Goal state after:
case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ (U R ↑n).degree < (U R ↑(n + 1) * X).degree
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α : α.IsNonZero
⊢ finrank K ↥(rootSpace H ⇑α) = 1

Tactic:
suffices ¬ 1 < finrank K (rootSpace H α) by
    have h₀ : finrank K (rootSpace H α) ≠ 0 := by
      convert_to! finrank K (rootSpace H α).toSubmodule ≠ 0
      simpa using! α.genWeightSpace_ne_bot
    lia
  intro contra
  obtain ⟨h, e, f, ht, heα, hfα⟩ := exists_isSl2Triple_of_weight_isNonZero hα
  let F : rootSpace H α →ₗ[K] K := killingForm K L f ∘ₗ (rootSpace H α).subtype
  have hF : LinearMap.ker F ≠ ⊥ := F.ker_ne_bot_of_finrank_lt <| by rwa [finrank_self]
  obtain ⟨⟨y, hyα⟩, hy, hy₀⟩ := (Submodule.ne_bot_iff _).mp hF
  replace hy : ⁅y, f⁆ = 0 := by
    have : killingForm K L y f = 0 := by simpa [F, traceForm_comm] using! hy
    simpa [this] using! lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg hyα hfα
  have P : ht.symm.HasPrimitiveVectorWith y (-2 : K) :=
    { ne_zero := by simpa [LieSubmodule.mk_eq_zero] using! hy₀
      lie_h := by simp only [neg_smul, neg_lie, ht.h_eq_coroot hα heα hfα,
        ← H.coe_bracket_of_module, lie_eq_smul_of_mem_rootSpace hyα (coroot α),
        root_apply_coroot hα]
      lie_e := by rw [← lie_skew, hy, neg_zero] }
  obtain ⟨n, hn⟩ := P.exists_nat
  assumption_mod_cast

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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (C R (↑n + 1)).comp (2 * X) = 2 * T R (↑n + 1)
ih2 : (C R ↑n).comp (2 * X) = 2 * T R ↑n
⊢ (C R (↑n + 2)).comp (2 * X) = 2 * T R (↑n + 2)

Tactic:
simp_rw [C_add_two, T_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (C R (↑n + 1)).comp (2 * X) = 2 * T R (↑n + 1)
ih2 : (C R ↑n).comp (2 * X) = 2 * T R ↑n
⊢ 2 * X * (2 * T R (↑n + 1)) - 2 * T R ↑n = 2 * (2 * X * T R (↑n + 1) - T R ↑n)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (C R n).comp (1 * X) = Polynomial.C 2 * (T R n).comp (Polynomial.C ⅟2 * X)
⊢ C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)

Tactic:
one_mul,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (C R n).comp X = Polynomial.C 2 * (T R n).comp (Polynomial.C ⅟2 * X)
⊢ C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (S R n).comp (1 * X) = (U R n).comp (Polynomial.C ⅟2 * X)
⊢ S R n = (U R n).comp (Polynomial.C ⅟2 * X)

Tactic:
one_mul,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (S R n).comp X = (U R n).comp (Polynomial.C ⅟2 * X)
⊢ S R n = (U R n).comp (Polynomial.C ⅟2 * X)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k] (1 * (⇑derivative)^[2] (T R n)) - (⇑derivative)^[k] (X ^ 2 * (⇑derivative)^[2] (T R n)) =
    (⇑derivative)^[k] (X * derivative (T R n) - ↑(n ^ 2) * T R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (T R n) =
    (2 * ↑k + 1) * X * (⇑derivative)^[k + 1] (T R n) - (↑n ^ 2 - ↑k ^ 2) * (⇑derivative)^[k] (T R n)

Tactic:
one_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k] ((⇑derivative)^[2] (T R n)) - (⇑derivative)^[k] (X ^ 2 * (⇑derivative)^[2] (T R n)) =
    (⇑derivative)^[k] (X * derivative (T R n) - ↑(n ^ 2) * T R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (T R n) =
    (2 * ↑k + 1) * X * (⇑derivative)^[k + 1] (T R n) - (↑n ^ 2 - ↑k ^ 2) * (⇑derivative)^[k] (T R n)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k] (1 * (⇑derivative)^[2] (U R n)) - (⇑derivative)^[k] (X ^ 2 * (⇑derivative)^[2] (U R n)) =
    (⇑derivative)^[k] (3 * X * derivative (U R n) - ↑((n + 2) * n) * U R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (U R n) =
    (2 * ↑k + 3) * X * (⇑derivative)^[k + 1] (U R n) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * (⇑derivative)^[k] (U R n)

Tactic:
one_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k] ((⇑derivative)^[2] (U R n)) - (⇑derivative)^[k] (X ^ 2 * (⇑derivative)^[2] (U R n)) =
    (⇑derivative)^[k] (3 * X * derivative (U R n) - ↑((n + 2) * n) * U R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (U R n) =
    (2 * ↑k + 3) * X * (⇑derivative)^[k + 1] (U R n) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * (⇑derivative)^[k] (U R n)
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 ⇑(tensorToSpan A p)

Tactic:
rw [← LinearMap.coe_restrictScalars R, this, coe_comp]

Goal state after:
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)