mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
pb : PowerBasis K L
⊢ (adjoin.powerBasis ⋯).gen = AdjoinSimple.gen K pb.gen

Tactic:
adjoin.powerBasis_gen

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
pb : PowerBasis K L
⊢ AdjoinSimple.gen K pb.gen = AdjoinSimple.gen K pb.gen
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) ≤ max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀

Tactic:
by
  rw [show ↥(adjoin F s) = (adjoin F s).toSubfield from rfl, adjoin_toSubfield]
  apply (Cardinal.lift_le.mpr (Subfield.cardinalMk_closure_le_max _)).trans
  rw [lift_max, sup_le_iff, lift_aleph0]
  refine ⟨(Cardinal.lift_le.mpr ((mk_union_le _ _).trans <| add_le_max _ _)).trans ?_, le_sup_right⟩
  simp_rw [lift_max, lift_aleph0]
  grw [mk_range_le_lift]

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

Goal state before:
pp: R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
⊢ H.toLieSubmodule.normalizer = H.toLieSubmodule

Tactic:
rw [← LieSubmodule.toSubmodule_inj, coe_normalizer_eq_normalizer,
    IsCartanSubalgebra.self_normalizing, coe_toLieSubmodule]

Goal state after:
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
m✝ : M
μ : R
t : IsSl2Triple h✝ e f
P : t.HasPrimitiveVectorWith m✝ μ
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : IsNoetherian R M
inst✝ : IsTorsionFree R M
n : ℕ
hn : μ = ↑n
h : ¬((toEnd R L M) f ^ (n + 1)) m✝ = 0
this : t.HasPrimitiveVectorWith (((toEnd R L M) f ^ (n + 1)) m✝) (↑n - 2 * (↑n + 1))
m : ℕ
hm : ↑n - 2 * (↑n + 1) = ↑m
⊢ False

Tactic:
have : (n : ℤ) < m + 2 * (n + 1) := by lia

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
m✝ : M
μ : R
t : IsSl2Triple h✝ e f
P : t.HasPrimitiveVectorWith m✝ μ
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : IsNoetherian R M
inst✝ : IsTorsionFree R M
n : ℕ
hn : μ = ↑n
h : ¬((toEnd R L M) f ^ (n + 1)) m✝ = 0
this✝ : t.HasPrimitiveVectorWith (((toEnd R L M) f ^ (n + 1)) m✝) (↑n - 2 * (↑n + 1))
m : ℕ
hm : ↑n - 2 * (↑n + 1) = ↑m
this : ↑n < ↑m + 2 * (↑n + 1)
⊢ False
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)
this : P ⊤
e : ↥⊤ ≃ₗ⁅R,L⁆ M := LieModuleEquiv.ofTop R L M
⊢ IsCompl (genWeightSpace M 0) (posFittingComp R L M)

Tactic:
rw [← map_genWeightSpace_eq e, ← map_posFittingComp_eq e]

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)
this : P ⊤
e : ↥⊤ ≃ₗ⁅R,L⁆ M := LieModuleEquiv.ofTop R L M
⊢ IsCompl (LieSubmodule.map e.toLieModuleHom (genWeightSpace (↥⊤) 0))
    (LieSubmodule.map e.toLieModuleHom (posFittingComp R L ↥⊤))
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
⊢ InjOn (fun χ ↦ genWeightSpace M χ) {χ | genWeightSpace M χ ≠ ⊥}

Tactic:
by
  rintro χ₁ _ χ₂ hχ₂ (hχ₁₂ : genWeightSpace M χ₁ = genWeightSpace M χ₂)
  contrapose! hχ₂
  simpa [hχ₁₂] using disjoint_genWeightSpace R L M hχ₂

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✝ : Module.IsTorsionFree R M
⊢ iSupIndep fun χ ↦ genWeightSpace M χ

Tactic:
simp only [← LieSubmodule.iSupIndep_toSubmodule, genWeightSpace,
    LieSubmodule.iInf_toSubmodule]
  exact Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo (toEnd R L M)
    (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem)

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

Goal state before:
pp: case refine_2
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
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
h : Φ ∈ LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)
x : L
y z : M
⊢ (Φ ⁅x, y⁆) z = -(Φ y) ⁅x, z⁆

Tactic:
replace h := LinearMap.congr_fun₂ (h x) y z

Goal state after:
case refine_2
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
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
x : L
y z : M
h : (⁅x, Φ⁆ y) z = (0 y) z
⊢ (Φ ⁅x, y⁆) z = -(Φ y) ⁅x, z⁆
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
x : V
hx : x ∈ W ⊓ B.orthogonal W
hx₁ : x ∈ W
hx₂ : x ∈ B.orthogonal W
⊢ ∀ (y : ↥W), ((B.restrict W) ⟨x, hx₁⟩) y = 0

Tactic:
rintro ⟨n, hn⟩

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
hx₁ : x ∈ W
hx₂ : x ∈ B.orthogonal W
n : V
hn : n ∈ W
⊢ ((B.restrict W) ⟨x, hx₁⟩) ⟨n, hn⟩ = 0
Module: Mathlib.Data.Multiset.Fintype

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

Tactic:
by
  simp_rw [← Function.comp_apply (f := f)]
  exact map_univ_comp_coe m f

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
⊢ False

Tactic:
apply IsSemisimple.non_abelian_of_isAtom J hJ

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
⊢ IsLieAbelian ↥J
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih : ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → (map (algebraMap K (SplittingFieldAux n f)) f).Splits
K : Type u
x✝ : Field K
f : K[X]
hf : f.natDegree = n.succ
⊢ (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
      ((X - C (AdjoinRoot.root f.factor)) * f.removeFactor)).Splits

Tactic:
rw [Polynomial.map_mul]

Goal state after:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih : ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → (map (algebraMap K (SplittingFieldAux n f)) f).Splits
K : Type u
x✝ : Field K
f : K[X]
hf : f.natDegree = n.succ
⊢ (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) *
      map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor).Splits
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie.hy.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
y : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅v, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
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)
aux : yc + yl + yu = ⁅u, z⁆
⊢ ⁅v, yu⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
· rw [← lie_skew, neg_mem_iff]
        exact LieSubmodule.mem_sup_right <| LieSubalgebra.lie_mem _ hyu hv

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
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
⊢ (-α).IsZero

Tactic:
ext; rw [coe_neg, h, neg_zero]

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✝⁵ : LieRing.IsNilpotent L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsTorsionFree R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z x y : L
hxy : ∀ (χ : R), MapsTo ⇑(φ x ∘ₗ φ y) ↑(genWeightSpaceOf M χ z) ↑(genWeightSpaceOf M χ z)
⊢ {χ | ↑(genWeightSpaceOf M χ z) ≠ ⊥}.Finite

Tactic:
ne_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
inst✝⁵ : LieRing.IsNilpotent L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsTorsionFree R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z x y : L
hxy : ∀ (χ : R), MapsTo ⇑(φ x ∘ₗ φ y) ↑(genWeightSpaceOf M χ z) ↑(genWeightSpaceOf M χ z)
⊢ {χ | ¬↑(genWeightSpaceOf M χ z) = ⊥}.Finite
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case hx
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
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e
α' : ↥H := ⋯
⊢ ⁅e, f⁆ - ((killingForm K L) e) f • ↑α' ∈ rootSpace H 0

Tactic:
simp only [rootSpace_zero_eq, LieSubalgebra.mem_toLieSubmodule]

Goal state after:
case hx
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
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ ⁅e, f⁆ - ((killingForm K L) e) f • ↑α' ∈ H
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
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆
S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }
y : L
hy' : y ∈ H
hy : S = (ad K L) y
⊢ _root_.IsNilpotent (N + (ad K L) y - (ad K L) y)

Tactic:
add_sub_cancel_right,

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
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆
S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }
y : L
hy' : y ∈ H
hy : S = (ad K L) y
⊢ _root_.IsNilpotent N
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α : corootSpace ⇑α ≠ ⊥
⊢ (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule ≠ ⊥

Tactic:
ne_eq,

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
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : ¬corootSpace ⇑α = ⊥
⊢ (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule ≠ ⊥
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
| add_two n ih1 ih2 =>

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

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

Tactic:
| add_two n ih1 ih2 =>

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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-1) (T R (↑n + 1)) = ↑↑(↑n + 1).negOnePow
ih2 : eval (-1) (T R ↑n) = ↑↑(↑n).negOnePow
⊢ eval (-1) (T R (↑n + 2)) = ↑↑(↑n + 2).negOnePow

Tactic:
| add_two n ih1 ih2 =>

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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 0 (T R (↑n + 1)) = ↑(if Even (↑n + 1) then ↑((↑n + 1) / 2).negOnePow else 0)
ih2 : eval 0 (T R ↑n) = ↑(if Even ↑n then ↑(↑n / 2).negOnePow else 0)
⊢ eval 0 (T R (↑n + 2)) = ↑(if Even (↑n + 2) then ↑((↑n + 2) / 2).negOnePow else 0)

Tactic:
| add_two n ih1 ih2 =>

Goal state after:
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)).degree = ↑(↑n + 1).natAbs
ih2 : (T R ↑n).degree = ↑(↑n).natAbs
⊢ (T R (↑n + 2)).degree = ↑(↑n + 2).natAbs

Tactic:
| add_two n ih1 ih2 =>

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α : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
this : h = ((killingForm K L) e) f' • (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ ((killingForm K L) e) f' * α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) ≠ 0

Tactic:
ne_eq,

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
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
this : h = ((killingForm K L) e) f' • (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ ¬((killingForm K L) e) f' * α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) = 0
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)
⊢ (T R (↑n + 2)).leadingCoeff = 2 ^ ((↑n + 2).natAbs - 1)

Tactic:
| add_two n ih1 ih2 =>

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

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

Tactic:
| add_two n ih1 ih2 =>

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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : U R (-(↑n + 1) - 1) = -U R (↑n + 1 - 1)
ih2 : U R (-↑n - 1) = -U R (↑n - 1)
⊢ U R (-(↑n + 2) - 1) = -U R (↑n + 2 - 1)

Tactic:
| add_two n ih1 ih2 =>

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ U R (-n) = -U R (n - 2)

Tactic:
simpa [sub_sub] using U_neg_sub_one R (n - 1)

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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 1 (U R (↑n + 1)) = ↑(↑n + 1) + 1
ih2 : eval 1 (U R ↑n) = ↑↑n + 1
⊢ eval 1 (U R (↑n + 2)) = ↑(↑n + 2) + 1

Tactic:
| add_two n ih1 ih2 =>

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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-1) (U R (↑n + 1)) = ↑↑(↑n + 1).negOnePow * (↑(↑n + 1) + 1)
ih2 : eval (-1) (U R ↑n) = ↑↑(↑n).negOnePow * (↑↑n + 1)
⊢ eval (-1) (U R (↑n + 2)) = ↑↑(↑n + 2).negOnePow * (↑(↑n + 2) + 1)

Tactic:
| add_two n ih1 ih2 =>

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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 0 (U R (↑n + 1)) = ↑(if Even (↑n + 1) then ↑((↑n + 1) / 2).negOnePow else 0)
ih2 : eval 0 (U R ↑n) = ↑(if Even ↑n then ↑(↑n / 2).negOnePow else 0)
⊢ eval 0 (U R (↑n + 2)) = ↑(if Even (↑n + 2) then ↑((↑n + 2) / 2).negOnePow else 0)

Tactic:
| add_two n ih1 ih2 =>

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α : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
this : ⁅↑h, e⁆ = α h • e
⊢ α h = 2

Tactic:
ht.lie_h_e_smul K

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
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
this : 2 • e = α h • e
⊢ α h = 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)
⊢ ↑(2 * 1 * (2 ^ n * 2 ^ 1)) = ↑(2 ^ (n + 2))

Tactic:
pow_add

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)
⊢ ↑(2 * 1 * (2 ^ n * 2 ^ 1)) = ↑(2 ^ n * 2 ^ 2)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
| add_two n ih1 ih2 =>

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)) = C R (↑n + 1)
ih2 : C R (-↑n) = C R ↑n
⊢ C R (-(↑n + 2)) = C R (↑n + 2)

Tactic:
| add_two n ih1 ih2 =>

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:
| add_two n ih1 ih2 =>

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

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

Tactic:
| add_two n ih1 ih2 =>

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

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

Tactic:
| add_two n ih1 ih2 =>

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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : S R (-(↑n + 1) - 1) = -S R (↑n + 1 - 1)
ih2 : S R (-↑n - 1) = -S R (↑n - 1)
⊢ S R (-(↑n + 2) - 1) = -S R (↑n + 2 - 1)

Tactic:
| add_two n ih1 ih2 =>

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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (S R (↑n + 1)) = ↑(↑n + 1) + 1
ih2 : eval 2 (S R ↑n) = ↑↑n + 1
⊢ eval 2 (S R (↑n + 2)) = ↑(↑n + 2) + 1

Tactic:
| add_two n ih1 ih2 =>

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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-2) (S R (↑n + 1)) = ↑↑(↑n + 1).negOnePow * (↑(↑n + 1) + 1)
ih2 : eval (-2) (S R ↑n) = ↑↑(↑n).negOnePow * (↑↑n + 1)
⊢ eval (-2) (S R (↑n + 2)) = ↑↑(↑n + 2).negOnePow * (↑(↑n + 2) + 1)

Tactic:
| add_two n ih1 ih2 =>

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

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

Tactic:
| add_two n ih1 ih2 =>

Goal state after: