mathlib-initiative/mathlib-tactics huggingface dataset:
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
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this✝ : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra
this : SMul ↥L ↥φ.carrier := this✝.toSMul
⊢ s ∈ ↑(extendScalars ⋯)

Tactic:
have : IsScalarTower L φ.carrier E := ⟨fun x y ↦ smul_assoc x (y : E)⟩

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
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this✝¹ : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra
this✝ : SMul ↥L ↥φ.carrier := this✝¹.toSMul
this : IsScalarTower (↥L) (↥φ.carrier) E
⊢ s ∈ ↑(extendScalars ⋯)
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_2
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
L : IntermediateField F E
f : ↥L →ₐ[F] K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
⊢ (φ.emb.comp (inclusion ⋯)).comp (inclusion hL) = f

Tactic:
· ext; apply hfφ.2

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 μ)
hg₁ : MapsTo ⇑g ↑p ↑p
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
this : iSupIndep fun x ↦ (f.genEigenspace x) k
⊢ Disjoint ((f.genEigenspace μ) k) (LinearMap.ker g)

Tactic:
have aux (μ') (_hμ' : μ' ∈ m.support.erase μ) :
        (f.genEigenspace μ') ↑l₀ ≤ (f.genEigenspace μ') k := by
      apply (f.genEigenspace μ').mono
      obtain _ | k := k
      · exact le_top
      · exact Nat.cast_le.2 <| Finset.sup_le fun i _ ↦ Nat.cast_le.1 <| hlk i

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 μ)
hg₁ : MapsTo ⇑g ↑p ↑p
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
this : iSupIndep fun x ↦ (f.genEigenspace x) k
aux : ∀ μ' ∈ m.support.erase μ, (f.genEigenspace μ') ↑l₀ ≤ (f.genEigenspace μ') k
⊢ Disjoint ((f.genEigenspace μ) k) (LinearMap.ker g)
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case ind.inl
ι : 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
this : ∀ (a : ι), ∃ φ, (f a).maxGenEigenspace φ = ⊤
⊢ ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤

Tactic:
choose χ hχ using this

Goal state after:
case ind.inl
ι : 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
χ : ι → K
hχ : ∀ (a : ι), (f a).maxGenEigenspace (χ a) = ⊤
⊢ ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
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
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
this✝ : FiniteDimensional K ↥K⟮x⟯
this : FiniteDimensional K ↥K⟮y⟯
⊢ FiniteDimensional K ↥K⟮x, y⟯

Tactic:
rw [← Set.singleton_union, adjoin_union]

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
this✝ : FiniteDimensional K ↥K⟮x⟯
this : FiniteDimensional K ↥K⟮y⟯
⊢ FiniteDimensional K ↥(K⟮x⟯ ⊔ K⟮y⟯)
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
x : L
⊢ x ∈ zeroRootSubalgebra R L H ↔ ∀ (y : ↥H), ∃ k, ((toEnd R (↥H) L) y ^ k) x = 0

Tactic:
by
  change x ∈ rootSpace H 0 ↔ _
  simp only [mem_genWeightSpace, Pi.zero_apply, zero_smul, sub_zero]

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

Goal state before:
pp: case h
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 y : L
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
hy : y ∈ H
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0
⊢ ((toEnd R (↥H) L) ⟨y, hy⟩ ^ (k + 1)) x = 0

Tactic:
Module.End.iterate_succ,

Goal state after:
case h
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 y : L
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
hy : y ∈ H
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0
⊢ (((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ∘ₗ (toEnd R (↥H) L) ⟨y, hy⟩) x = 0
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommMonoid M
R : Type u_8
inst✝² : Field R
inst✝¹ : NeZero 2
inst✝ : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
⊢ (B x) y = ((B x) x + (B x) y + ((B x) y + (B y) y) - (B x) x - (B y) y) / 2

Tactic:
ring_nf

Goal state after:
M : Type u_2
inst✝³ : AddCommMonoid M
R : Type u_8
inst✝² : Field R
inst✝¹ : NeZero 2
inst✝ : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
⊢ (B x) y = (B x) y * 2⁻¹ * 2
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case smul
ι : 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 z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x : L
t : R
u : L
hx✝ : u ∈ lieSpan R L (range b.f)
hu : ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
⊢ t • ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
exact SMulMemClass.smul_mem t hu

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

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✝⁶ : LieRing.IsNilpotent L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
N : LieSubmodule K L M
inst✝ : IsTriangularizable K L M
y : L
⊢ ⨆ φ, End.maxGenEigenspace (LinearMap.restrict ((toEnd K L M) y) ⋯) φ = ⊤

Tactic:
exact Module.End.genEigenspace_restrict_eq_top _ (IsTriangularizable.maxGenEigenspace_eq_top y)

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
b : α
hb : IsCompactElement b
hbS : b ≤ sSup S
s : Finset α
hs₁ : ↑s ⊆ S
hs₂ : b ≤ s.sup id
⊢ ∃ T ⊆ S, b = sSup T

Tactic:
obtain ⟨t, ht, rfl⟩ := hS.finitelyAtomistic s b hs₁ hb hs₂

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
s : Finset α
hs₁ : ↑s ⊆ S
t : Finset α
ht : t ⊆ s
hb : IsCompactElement (t.sup id)
hbS : t.sup id ≤ sSup S
hs₂ : t.sup id ≤ s.sup id
⊢ ∃ T ⊆ S, t.sup id = sSup T
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✝ : IsSimple R L
hI : IsLieAbelian L
⊢ False

Tactic:
exact IsSimple.non_abelian R (L := L) hI

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

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

Tactic:
have := m.map_toEnumFinset_fst

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
this : map Prod.fst m.toEnumFinset.val = m
⊢ map (fun x ↦ x.fst) Finset.univ.val = m
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: case non_abelian_of_isAtom
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
⊢ ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I

Tactic:
· intro I hI₁ hI₂
    apply IsSimple.non_abelian (R := R) (L := L)
    rw [IsSimple.isAtom_iff_eq_top] at hI₁
    rwa [hI₁, lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv] at hI₂

Goal state after:
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 : ℕ
| map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f

Tactic:
Splits.eq_prod_roots (Monics.splits_finsetProd h)

Goal state after:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
| C (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).leadingCoeff *
    (Multiset.map (fun x ↦ X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod
Module: Mathlib.Algebra.Lie.Basis.Basic

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

Tactic:
exact SMulMemClass.smul_mem t hu

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

Goal state before:
pp: case add
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x u v : L
hx✝ : u ∈ Submodule.span R {x | ∃ u v, ⁅u, v⁆ = x}
hy✝ : v ∈ Submodule.span R {x | ∃ u v, ⁅u, v⁆ = x}
hu : (trace R M) (φ u * y) = 0
hv : (trace R M) (φ v * y) = 0
⊢ (trace R M) (φ (u + v) * y) = 0

Tactic:
simp [add_mul, hu, hv]

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

Goal state before:
pp: case add
L : Type u_2
inst✝¹⁰ : LieRing L
M : Type u_3
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
K : Type u_4
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L
H : LieSubalgebra K L
inst✝⁴ : LieRing.IsNilpotent ↥H
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : IsTriangularizable K (↥H) M
inst✝ : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ : m₁ ∈ ⨆ i, genWeightSpace M ⇑i
hm₂ : m₂ ∈ ⨆ i, genWeightSpace M ⇑i
n₁ : ℕ
hn₁ : ((toEnd K L M) x ^ n₁) m₁ = 0
n₂ : ℕ
hn₂ : ((toEnd K L M) x ^ n₂) m₂ = 0
⊢ ((toEnd K L M) x ^ max n₁ n₂) m₁ + ((toEnd K L M) x ^ max n₁ n₂) m₂ = 0

Tactic:
Module.End.pow_map_zero_of_le le_sup_left hn₁,

Goal state after:
case add
L : Type u_2
inst✝¹⁰ : LieRing L
M : Type u_3
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
K : Type u_4
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L
H : LieSubalgebra K L
inst✝⁴ : LieRing.IsNilpotent ↥H
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : IsTriangularizable K (↥H) M
inst✝ : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ : m₁ ∈ ⨆ i, genWeightSpace M ⇑i
hm₂ : m₂ ∈ ⨆ i, genWeightSpace M ⇑i
n₁ : ℕ
hn₁ : ((toEnd K L M) x ^ n₁) m₁ = 0
n₂ : ℕ
hn₂ : ((toEnd K L M) x ^ n₂) m₂ = 0
⊢ 0 + ((toEnd K L M) x ^ max n₁ n₂) m₂ = 0
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
x : ↥H
hx : x ∈ corootSpace 0
this : {x | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} = {0}
⊢ x ∈ ⊥

Tactic:
by simpa [mem_corootSpace, this] 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 + 1))
h₁ : motive (-↑(n + 1) + 1)
⊢ motive (-↑n)

Tactic:
convert! h₁ using 1

Goal state after:
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 + 1))
h₁ : motive (-↑(n + 1) + 1)
⊢ -↑n = -↑(n + 1) + 1
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ T R (-1 + -↑k + 2) + (2 * X * T R (-↑k) - T R (-↑k + 1)) - 2 * X * T R (-↑k) = 0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R (n + 1) + (2 * X * T R (n - 1 + 1) - T R (n - 1)) - (2 * X * T R n - T R (n - 1) + T R (n - 1 + 2)) = 0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R (n - 2) + (2 * X * T R (n - 2 + 1) - T R (n - 2)) - (2 * X * T R (n - 1) - T R n + T R (n - 2 + 2)) = 0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R (n - 1) + (2 * X * T R (n - 1 + 1) - T R (n - 1)) - (2 * X * T R n - T R (n + 1) + T R (n - 1 + 2)) = 0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R n + (2 * X * T R (n - 2 + 1) - T R (n - 2)) - (2 * X * T R (n - 1) - T R (n - 2) + T R (n - 2 + 2)) = 0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : T R (-(↑n + 1)) = T R (↑n + 1)
ih2 : T R (-↑n) = T R ↑n
h₁ : T R (↑n + 2) = 2 * X * T R (↑n + 1) - T R ↑n
h₂ : T R (-↑n - 2) = 2 * X * T R (-↑n - 1) - T R (-↑n)
⊢ T R (-(↑n + 2)) + (2 * X * T R (↑n + 1) + T R (-↑n) + T R (↑n + 2) + (2 * X * T R (-↑n - 1) - T R (-↑n))) -
      (T R (↑n + 2) + (2 * X * T R (-(↑n + 1)) + T R ↑n + (2 * X * T R (↑n + 1) - T R ↑n) + T R (-↑n - 2))) =
    0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : T R (- -↑n) = T R (-↑n)
ih2 : T R (-(-↑n + 1)) = T R (-↑n + 1)
h₁ : T R (↑n + 1) = 2 * X * T R ↑n - T R (↑n - 1)
h₂ : T R (-↑n - 1) = 2 * X * T R (-↑n) - T R (-↑n + 1)
⊢ T R (-(-↑n - 1)) + (2 * X * T R (-↑n) + T R (-(-↑n + 1)) + (2 * X * T R ↑n - T R (↑n - 1)) + T R (-↑n - 1)) -
      (T R (-↑n - 1) + (2 * X * T R (- -↑n) + T R (-↑n + 1) + T R (↑n + 1) + (2 * X * T R (-↑n) - T R (-↑n + 1)))) =
    0

Tactic:
ring_nf

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

Goal state before:
pp: 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)
⊢ -(2 * x) * (-↑↑((↑n).negOnePow * 1) * eval x (T R (↑n + 1))) - ↑↑(↑n).negOnePow * eval x (T R ↑n) =
    ↑↑((↑n).negOnePow * 1) * (2 * x * eval x (T R (↑n + 1)) - eval x (T R ↑n))

Tactic:
ring_nf

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

Goal state before:
pp: case smul
ι : 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 : L
t : R
x✝ : L
hx✝ : x✝ ∈ lieSpan R L (range b.e)
hu : x✝ ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
⊢ t • x✝ ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))

Tactic:
exact SMulMemClass.smul_mem t hu

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ U R (-1 + -↑k + 2) + (2 * X * U R (-↑k) - U R (-↑k + 1)) - 2 * X * U R (-↑k) = 0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ U R (n + 1) + (2 * X * U R (n - 1 + 1) - U R (n - 1)) - (2 * X * U R n - U R (n - 1) + U R (n - 1 + 2)) = 0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ U R (n - 2) + (2 * X * U R (n - 2 + 1) - U R (n - 2)) - (2 * X * U R (n - 1) - U R n + U R (n - 2 + 2)) = 0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ U R (n - 1) + (2 * X * U R (n - 1 + 1) - U R (n - 1)) - (2 * X * U R n - U R (n + 1) + U R (n - 1 + 2)) = 0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ U R n + (2 * X * U R (n - 2 + 1) - U R (n - 2)) - (2 * X * U R (n - 1) - U R (n - 2) + U R (n - 2 + 2)) = 0

Tactic:
ring_nf

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

Goal state before:
pp: case a
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)
h₁ : U R (↑n + 1) = 2 * X * U R ↑n - U R (↑n - 1)
h₂ : U R (-↑n - 1 - 2) = 2 * X * U R (-↑n - 1 - 1) - U R (-↑n - 1)
⊢ U R (-(↑n + 2) - 1) +
        (2 * X * -U R (↑n + 1 - 1) + U R (-↑n - 1) + (2 * X * U R ↑n - U R (↑n - 1)) +
          (2 * X * U R (-↑n - 1 - 1) - U R (-↑n - 1))) -
      (-U R (↑n + 2 - 1) + (2 * X * U R (-(↑n + 1) - 1) + -U R (↑n - 1) + U R (↑n + 1) + U R (-↑n - 1 - 2))) =
    0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : U R (- -↑n - 1) = -U R (-↑n - 1)
ih2 : U R (-(-↑n + 1) - 1) = -U R (-↑n + 1 - 1)
h₁ : U R ↑n = 2 * X * U R (↑n - 1) - U R (↑n - 2)
h₂ : U R (-↑n - 2) = 2 * X * U R (-↑n - 1) - U R (-↑n)
⊢ U R (-(-↑n - 1) - 1) +
        (2 * X * -U R (-↑n - 1) + U R (-(-↑n + 1) - 1) + (2 * X * U R (↑n - 1) - U R (↑n - 2)) +
          (2 * X * U R (-↑n - 1) - U R (-↑n))) -
      (-U R (-↑n - 1 - 1) + (2 * X * U R (- -↑n - 1) + -U R (-↑n + 1 - 1) + U R ↑n + U R (-↑n - 2))) =
    0

Tactic:
ring_nf

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
key : α h = 2
s : K
hs : s • h = coroot α
⊢ s = 1

Tactic:
simpa [root_apply_coroot hα, key] using congr_arg α hs

Goal state after: