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

Goal state before:
pp: case pos
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
hN : LieSubmodule.map N.incl (genWeightSpace ↥N ⇑χ_N) ≤ N
h : genWeightSpace M ⇑χ_N = ⊥
⊢ N ⊓ genWeightSpace M ⇑χ_N ≤ ⨆ χ, N ⊓ genWeightSpace M ⇑χ

Tactic:
simp [h]

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
⊢ ∃ T ⊆ S, b = sSup T

Tactic:
obtain ⟨s, hs₁, hs₂⟩ := (isCompactElement_iff_exists_le_sSup_of_le_sSup α b).1 hb S hbS

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
b : α
hb : IsCompactElement b
hbS : b ≤ sSup S
s : Finset α
hs₁ : ↑s ⊆ S
hs₂ : b ≤ s.sup id
⊢ ∃ T ⊆ S, b = sSup T
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
hx : x ∈ W ⊓ ker B
⊢ x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker

Tactic:
simp_rw [Submodule.mem_map, LinearMap.mem_ker]

Goal state after:
case mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
hx : x ∈ W ⊓ ker B
⊢ ∃ y, (domRestrict B W) y = 0 ∧ (Submodule.subtype W) y = x
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
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
⊢ I ≤ sSup {J | IsAtom J ∧ J ≤ I}

Tactic:
suffices I ≤ J ⊔ (J' ⊓ I) by
    refine this.trans ?_
    apply sup_le
    · exact le_sSup ⟨hJ, hJI⟩
    rw [← atomistic (J' ⊓ I)]
    apply sSup_le_sSup
    simp only [le_inf_iff, Set.ofPred_subset_ofPred, and_imp]
    tauto

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 ≤ J ⊔ J' ⊓ I
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
h : W = ⊥
⊢ B.orthogonal W = ⊤

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m s t : Multiset α
h : s = t
x : s.ToType
⊢ count x.fst s = count x.fst t

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m s t : Multiset α
h : s = t
x : t.ToType
⊢ count x.fst t = count x.fst s

Tactic:
simp [h]

Goal state after:
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 → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 : map (algebraMap K (SplittingFieldAux n.succ f)) f ≠ 0
⊢ Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f)) = ⊤

Tactic:
rootSet_def,

Goal state after:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 : map (algebraMap K (SplittingFieldAux n.succ f)) f ≠ 0
⊢ Algebra.adjoin K ↑(f.aroots (SplittingFieldAux n.succ f)).toFinset = ⊤
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 → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 : map (algebraMap K (SplittingFieldAux n.succ f)) f ≠ 0
⊢ Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f)) = ⊤

Tactic:
rw [rootSet_def, aroots_def]

Goal state after:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 : map (algebraMap K (SplittingFieldAux n.succ f)) f ≠ 0
⊢ Algebra.adjoin K ↑(map (algebraMap K (SplittingFieldAux n.succ f)) f).roots.toFinset = ⊤
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 : ℕ
⊢ (C ((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 -
          (Multiset.map (fun x ↦ X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod).coeff
      n =
    0

Tactic:
f.2,

Goal state after:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (C ((algebraMap k (∏ f ∈ s, ↑f).SplittingField) 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
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Algebra R A
inst✝⁴ : Module R M₁
inst✝³ : Module A M₁
inst✝² : SMulCommClass R A M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ B₁.tmul B₂ = LinearMap.flip (B₁.tmul B₂)

Tactic:
ext x₁ x₂ y₁ y₂

Goal state after:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Algebra R A
inst✝⁴ : Module R M₁
inst✝³ : Module A M₁
inst✝² : SMulCommClass R A M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
x₁ : M₁
x₂ : M₂
y₁ : M₁
y₂ : M₂
⊢ ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (B₁.tmul B₂)) x₁) x₂)) y₁) y₂ =
    ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (LinearMap.flip (B₁.tmul B₂))) x₁) x₂)) y₁) y₂
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M₂
inst✝² : Algebra R A
inst✝¹ : Module R M₂
inst✝ : FaithfulSMul R A
B : BilinForm R M₂
h : B = 0
⊢ BilinForm.baseChange A B = 0

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.Killing

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
x : L
h : x = 0
⊢ (ad R L) x = 0

Tactic:
simp [h]

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 z : L
⊢ ((traceForm R L M) ⁅x, y⁆) z = (trace R M) (φ ⁅x, y⁆ ∘ₗ φ z)

Tactic:
by simp only [traceForm_apply_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteSpan

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e) Φ Φ
e' : ↑Φ ≃ ↑Φ := BijOn.equiv (⇑e) he
this : Finite ↑Φ
k : ℕ
hk₀ : k > 0
hk : IsPeriodicPt (fun x ↦ e' * x) k 1
m : M
hm : m ∈ span R Φ
x : M
hx : x ∈ Φ
⊢ (e ^ k) x = x

Tactic:
rw [LinearEquiv.pow_apply, ← he.1.coe_iterate_restrict ⟨x, hx⟩ k]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e) Φ Φ
e' : ↑Φ ≃ ↑Φ := BijOn.equiv (⇑e) he
this : Finite ↑Φ
k : ℕ
hk₀ : k > 0
hk : IsPeriodicPt (fun x ↦ e' * x) k 1
m : M
hm : m ∈ span R Φ
x : M
hx : x ∈ Φ
⊢ ↑((MapsTo.restrict (⇑e) Φ Φ ⋯)^[k] ⟨x, hx⟩) = x
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P ∈ degreeLT R m
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (↑S '' Set.Iio m)
tail_eq_zero : ¬tail = 0
this : tail.degree < ↑n
⊢ P - head ∈ degreeLT R m

Tactic:
(Nat.cast_lt (α := WithBot ℕ)).mpr hn

Goal state after:
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P ∈ degreeLT R m
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (↑S '' Set.Iio m)
tail_eq_zero : ¬tail = 0
this : tail.degree < ↑m
⊢ P - head ∈ degreeLT R m
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x : L
⊢ (∑ χ, finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ)) x ∈
    span K (range (Weight.toLinear K L M))

Tactic:
LinearMap.coe_sum,

Goal state after:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x : L
⊢ (∑ i, ⇑(finrank K ↥(genWeightSpace M ⇑i) • (Weight.toLinear K L M i).smulRight (Weight.toLinear K L M i))) x ∈
    span K (range (Weight.toLinear K L M))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
| neg_add_one 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'⁆, ⋯⟩
⊢ h = ((killingForm K L) e) f' • (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)

Tactic:
simp only [h, Subtype.ext_iff, hef]

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'⁆, ⋯⟩
⊢ ((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 α))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
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)
⊢ U R (-(-↑n - 1) - 1) = -U R (-↑n - 1 - 1)

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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 : ℤ
hn : n ≠ -1
⊢ (U R n).degree = ↑((n + 1).natAbs - 1)

Tactic:
obtain ⟨m, rfl | rfl⟩ := n.eq_nat_or_neg

Goal state after:
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : ↑m ≠ -1
⊢ (U R ↑m).degree = ↑((↑m + 1).natAbs - 1)

case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : -↑m ≠ -1
⊢ (U R (-↑m)).degree = ↑((-↑m + 1).natAbs - 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : ℤ
inst✝¹ : IsDomain R
inst✝ : NeZero 2
h : n = -1
⊢ U R n = 0

Tactic:
simp [h]

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
by
  linear_combination (norm := ring_nf) (T_eq_U_sub_X_mul_U R (n + 2)) + (T_eq_X_mul_U_sub_U R n)

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
simp_rw [C_sub_one, T_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
    ring

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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

Goal state before:
pp: case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (-↑n)) = T R' (-↑n)
ih2 : map f (T R (-↑n + 1)) = T R' (-↑n + 1)
⊢ map f (T R (-↑n - 1)) = T R' (-↑n - 1)

Tactic:
| neg_add_one n ih1 ih2 =>

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

Goal state before:
pp: case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (U R (-↑n)) = U R' (-↑n)
ih2 : map f (U R (-↑n + 1)) = U R' (-↑n + 1)
⊢ map f (U R (-↑n - 1)) = U R' (-↑n - 1)

Tactic:
| neg_add_one n ih1 ih2 =>

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

Goal state before:
pp: case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (C R (-↑n)) = C R' (-↑n)
ih2 : map f (C R (-↑n + 1)) = C R' (-↑n + 1)
⊢ map f (C R (-↑n - 1)) = C R' (-↑n - 1)

Tactic:
| neg_add_one n ih1 ih2 =>

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

Goal state before:
pp: case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (S R (-↑n)) = S R' (-↑n)
ih2 : map f (S R (-↑n + 1)) = S R' (-↑n + 1)
⊢ map f (S R (-↑n - 1)) = S R' (-↑n - 1)

Tactic:
| neg_add_one n ih1 ih2 =>

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

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

Tactic:
| neg_add_one n ih1 ih2 =>

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
⊢ U R (Int.subNatNat n 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Ico 0 n)

Tactic:
convert! U_mem_span_T R (n - 1) using 2

Goal state after:
case e'_4
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : n ≠ 0
⊢ (fun m ↦ T R ↑m) '' Set.Ico 0 n = (fun m ↦ T R ↑m) '' Set.Icc 0 (n - 1)

case e'_5
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : n ≠ 0
⊢ Int.subNatNat n 1 = ↑(n - 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n k : ℕ
ih : (⇑derivative)^[k] (T R ↑n) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - k))
⊢ (⇑derivative)^[k + 1] (T R ↑n) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - (k + 1)))

Tactic:
rw [Function.iterate_succ_apply']

Goal state after:
R : Type u_1
inst✝ : CommRing R
n k : ℕ
ih : (⇑derivative)^[k] (T R ↑n) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - k))
⊢ derivative ((⇑derivative)^[k] (T R ↑n)) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - (k + 1)))
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 j : ι
h : i = (P.reflectionPerm j) j
⊢ P.root i = -P.root j

Tactic:
simp [h]

Goal state after: