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

Goal state before:
pp: 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
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
x : ↥H
hx : x ∈ corootSpace α
N : ℤ → Submodule R M := fun k ↦ ↑(genWeightSpace M (k • α + χ))
h₁ : iSupIndep fun i ↦ N ↑i
h₂ : ∀ (i : ℤ), MapsTo ⇑((toEnd R (↥H) M) x) ↑(N i) ↑(N i)
h₃ : ↑(genWeightSpaceChain M α χ p q) = ⨆ i ∈ Finset.Ioo p q, N i
⊢ (a • α + ↑b • χ) x = (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) (LinearMap.restrict ((toEnd R (↥H) M) x) ⋯)

Tactic:
subst a b N

Goal state after:
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
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x : ↥H
hx : x ∈ corootSpace α
hb : 0 < ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
h₁ : iSupIndep fun i ↦ (fun k ↦ ↑(genWeightSpace M (k • α + χ))) ↑i
h₂ :
  ∀ (i : ℤ),
    MapsTo ⇑((toEnd R (↥H) M) x) ↑((fun k ↦ ↑(genWeightSpace M (k • α + χ))) i)
      ↑((fun k ↦ ↑(genWeightSpace M (k • α + χ))) i)
h₃ : ↑(genWeightSpaceChain M α χ p q) = ⨆ i ∈ Finset.Ioo p q, (fun k ↦ ↑(genWeightSpace M (k • α + χ))) i
⊢ ((∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i) • α +
        ↑(∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))) • χ)
      x =
    (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) (LinearMap.restrict ((toEnd R (↥H) M) x) ⋯)
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 = 1

Tactic:
simpa [IsPeriodicPt, IsFixedPt] using hk

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

Goal state before:
pp: case succ
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
B : LinearMap.BilinForm R M
hB : ∀ (x : L) (m n : M), (B ⁅x, m⁆) n = -(B m) ⁅x, n⁆
m₀ m₁ : M
hm₀ : m₀ ∈ genWeightSpace M 0
hm₁ : m₁ ∈ posFittingComp R L M
x : L
k : ℕ
ih : ∀ (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
⊢ ∀ (m n : M), (B m) ((φ x ^ (k + 1)) n) = (-1) ^ (k + 1) • (B ((φ x ^ (k + 1)) m)) n

Tactic:
intro m n

Goal state after:
case succ
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
B : LinearMap.BilinForm R M
hB : ∀ (x : L) (m n : M), (B ⁅x, m⁆) n = -(B m) ⁅x, n⁆
m₀ m₁ : M
hm₀ : m₀ ∈ genWeightSpace M 0
hm₁ : m₁ ∈ posFittingComp R L M
x : L
k : ℕ
ih : ∀ (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
m n : M
⊢ (B m) ((φ x ^ (k + 1)) n) = (-1) ^ (k + 1) • (B ((φ x ^ (k + 1)) m)) n
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : IsKilling R L
inst✝² : IsNoetherian R L
inst✝¹ : IsArtinian R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
h : Codisjoint H.toSubmodule ↑(LieModule.posFittingComp R (↥H) L)
⊢ ∀ m₀ ∈ H, ∀ m₁ ∈ LieModule.posFittingComp R (↥H) L, ((killingForm R L) m₀) m₁ = 0

Tactic:
intro m₀

Goal state after:
R : Type u_1
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : IsKilling R L
inst✝² : IsNoetherian R L
inst✝¹ : IsArtinian R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
h : Codisjoint H.toSubmodule ↑(LieModule.posFittingComp R (↥H) L)
m₀ : L
⊢ m₀ ∈ H → ∀ m₁ ∈ LieModule.posFittingComp R (↥H) L, ((killingForm R L) m₀) m₁ = 0
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✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ (LieIdeal.toLieSubalgebra R L (lowerCentralSeries R L L 1 ⊓ LieAlgebra.center R L)).toSubmodule ≤
    LinearMap.ker (traceForm R L M)

Tactic:
rintro z ⟨hz : z ∈ lowerCentralSeries R L L 1, hzc : z ∈ LieAlgebra.center R L⟩

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✝¹ : Free R M
inst✝ : Module.Finite R M
z : L
hz : z ∈ lowerCentralSeries R L L 1
hzc : z ∈ LieAlgebra.center R L
⊢ z ∈ LinearMap.ker (traceForm R L 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
⊢ LinearMap.range (traceForm K L M) ≤ span K (range (Weight.toLinear K L M))

Tactic:
by
  rintro - ⟨x, rfl⟩
  rw [LieModule.traceForm_eq_sum_finrank_nsmul, LinearMap.coe_sum, Finset.sum_apply]
  refine Submodule.sum_mem _ fun χ _ ↦ ?_
  simp_rw [LinearMap.smul_apply, LinearMap.coe_smulRight, Weight.toLinear_apply,
    ← Nat.cast_smul_eq_nsmul K]
  exact Submodule.smul_mem _ _ <| Submodule.smul_mem _ _ <| subset_span <| mem_range_self χ

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

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

Tactic:
simpa using congr_arg (Polynomial.eval t) (S_sq_add_S_sq R k)

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

Goal state before:
pp: case mem
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
x y z : ↥H
u : L
hu : u ∈ rootSpace H ⇑α
v : L
huv : ⁅u, v⁆ = ↑z
hx : α x = 0
⊢ ((killingForm K L) ↑x) ⁅u, v⁆ = 0

Tactic:
← traceForm_apply_lie_apply,

Goal state after:
case mem
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
x y z : ↥H
u : L
hu : u ∈ rootSpace H ⇑α
v : L
huv : ⁅u, v⁆ = ↑z
hx : α x = 0
⊢ ((traceForm K L L) ⁅↑x, u⁆) v = 0
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
⊢ 2 - 1 = 1

Tactic:
norm_num

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
⊢ 2 - 1 = 1

Tactic:
norm_num

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
⊢ 2 * ↑↑(↑n).negOnePow - ↑↑(↑n).negOnePow = ↑↑((↑n).negOnePow * (-1) ^ 2)

Tactic:
norm_num

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
hn : Even n
⊢ eval 0 (T R n) = ↑↑(n / 2).negOnePow

Tactic:
simp [T_eval_zero, hn]

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) = -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:
have h₁ := U_eq R n
    have h₂ := U_sub_two R (-n)
    linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂

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

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
⊢ 2 = 1 + 1

Tactic:
norm_num

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

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
⊢ -2 = -1 + -1

Tactic:
norm_num

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)
⊢ -(2 * ↑(↑((↑n).negOnePow * Int.negOnePow 1) * ↑(n + 1 + 1))) - ↑(↑(↑n).negOnePow * ↑(n + 1)) =
    ↑(↑((↑n).negOnePow * (-1) ^ 2) * ↑(n + 2 + 1))

Tactic:
norm_num

Goal state after:
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)
⊢ 2 * ((-1) ^ n * (↑n + 1 + 1)) - (-1) ^ n * (↑n + 1) = (-1) ^ n * (↑n + 2 + 1)
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)
⊢ -(2 * (↑↑(↑n).negOnePow * (-↑n + 1))) - ↑↑((↑n).negOnePow * Int.negOnePow 1) * (-↑n + 1 + 1) =
    ↑(-(↑((↑n).negOnePow * Int.negOnePow 1) * ↑n))

Tactic:
norm_num

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

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

Tactic:
eval_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R ↑n) = ↑↑(↑n).negOnePow * eval x (U R ↑n)
ih2 : eval (-x) (U R (↑n + 1)) = ↑↑(↑n + 1).negOnePow * eval x (U R (↑n + 1))
⊢ eval (-x) (2 * X) * eval (-x) (U R (↑n + 1)) - eval (-x) (U R ↑n) =
    ↑↑(↑n + 2).negOnePow * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
eval_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R ↑n) = ↑↑(↑n).negOnePow * eval x (U R ↑n)
ih2 : eval (-x) (U R (↑n + 1)) = ↑↑(↑n + 1).negOnePow * eval x (U R (↑n + 1))
⊢ eval (-x) 2 * eval (-x) X * eval (-x) (U R (↑n + 1)) - eval (-x) (U R ↑n) =
    ↑↑(↑n + 2).negOnePow * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑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α : α.IsNonZero
contra : 1 < finrank K ↥(rootSpace H ⇑α)
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
F : ↥(rootSpace H ⇑α) →ₗ[K] K := (killingForm K L) f ∘ₗ (↑(rootSpace H ⇑α)).subtype
hF : F.ker ≠ ⊥
y : L
hyα : y ∈ rootSpace H ⇑α
hy₀ : ⟨y, hyα⟩ ≠ 0
hy : ⁅y, f⁆ = 0
⊢ ⁅-h, y⁆ = -2 • y

Tactic:
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α]

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

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
⊢ U R (1 + 1) = X * U R 1 + T R (1 + 1)

Tactic:
simp [U_two, T_two]

Goal state after:
case one
R : Type u_1
inst✝ : CommRing R
⊢ 4 * X ^ 2 - 1 = X * (2 * X) + (2 * X ^ 2 - 1)
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
⊢ 2 * 2 - 2 = 2

Tactic:
norm_num

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
⊢ 2 * 2 - 2 = 2

Tactic:
norm_num

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
⊢ ↑(2 * (2 * ↑(↑n).negOnePow) - 2 * ↑(↑n).negOnePow) = ↑(2 * ↑((↑n).negOnePow * (-1) ^ 2))

Tactic:
norm_num

Goal state after:
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
⊢ 2 * (2 * (-1) ^ n) - 2 * (-1) ^ n = 2 * (-1) ^ n
Module: Mathlib.LinearAlgebra.Reflection

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

Tactic:
ext z

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
m : ℕ
t : R
ht : t = f y * g x - 2
z : M
⊢ ↑((reflection hf * reflection hg) ^ m) z =
    (LinearMap.id +
          (Polynomial.eval t (S R ((↑m - 2) / 2)) *
              (Polynomial.eval t (S R ((↑m - 1) / 2)) + Polynomial.eval t (S R ((↑m - 3) / 2)))) •
            (LinearMap.smulRight (g x • f - g) y - LinearMap.smulRight f x) +
        (Polynomial.eval t (S R ((↑m - 1) / 2)) *
            (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
          (LinearMap.smulRight (f y • g - f) x - LinearMap.smulRight g y))
      z
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)
⊢ ↑(-(2 * (↑((↑n).negOnePow * Int.negOnePow 1) * ↑(n + 1 + 1))) - ↑(↑n).negOnePow * ↑(n + 1)) =
    ↑(↑((↑n).negOnePow * (-1) ^ 2) * ↑(n + 2 + 1))

Tactic:
norm_num

Goal state after:
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)
⊢ 2 * ((-1) ^ n * (↑n + 1 + 1)) - (-1) ^ n * (↑n + 1) = (-1) ^ n * (↑n + 2 + 1)
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)
⊢ -(2 * (↑↑(↑n).negOnePow * (-↑n + 1))) - ↑↑((↑n).negOnePow * Int.negOnePow 1) * (-↑n + 1 + 1) =
    ↑(-(↑((↑n).negOnePow * Int.negOnePow 1) * ↑n))

Tactic:
norm_num

Goal state after:
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)
⊢ -(2 * ((-1) ^ n * (-↑n + 1))) + (-1) ^ n * (-↑n + 1 + 1) = (-1) ^ n * ↑n
Module: Mathlib.LinearAlgebra.Reflection

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

Tactic:
ext z

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℤ
⊢ map f (U R n) = U R' n

Tactic:
by
  induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [U_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [U_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
H₁ : (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)
H₂ : derivative (T R (n + 1)) = ↑(n + 1) * U R (n + 1 - 1)
h₁ : T R (n + 2) = 2 * X * T R (n + 1) - T R n
⊢ (1 - X ^ 2) * derivative (T R (n + 1)) = (↑n + 1) * (T R n - X * T R (n + 1))

Tactic:
linear_combination (norm := (push_cast; ring_nf))
    (-n - 1) * h₁ + (-(X : R[X]) ^ 2 + 1) * H₂ + (n + 1) * H₁

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: case refine_1.mem
ι : 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 : P.reflectionPerm i = P.reflectionPerm j
x : M
k : ι
⊢ (P.reflection i) (P.root k) = (P.reflection j) (P.root k)

Tactic:
simp only [← root_reflectionPerm, h]

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst✝ : IsAddTorsionFree M
Φ : Set M
hΦ : Φ.Finite
hfx : f x = 2
hgy : g y = 2
hgx : g x = 2
hfy : f y = 2
hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ
hyΦ : y ∈ Φ
h : 2 • x = 2 • y
⊢ x = y

Tactic:
exact smul_right_injective _ two_ne_zero h

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

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

Tactic:
simp [T_derivative_eq_U, sq]

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module L M
inst✝⁹ : Module L N
inst✝⁸ : Module K M
inst✝⁷ : Module K N
inst✝⁶ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝⁵ : p.IsPerfPair
M' : Type u_5
N' : Type u_6
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup N'
inst✝² : Module K M'
inst✝¹ : Module K N'
inst✝ : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (span L ↑i.range) (span L ↑j.range)
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range
this : (p.compl₁₂ (span L (Set.range ⇑i)).subtype (span L (Set.range ⇑j)).subtype).IsPerfPair
⊢ span L ↑(Submodule.inclusionSpan L i.range).range = ⊤

Tactic:
exact (LinearMap.range i).span_range_inclusionSpan L

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ length R M = Order.coheight ⊥

Tactic:
apply WithBot.coe_injective
  rw [Module.coe_length, Order.coheight_bot_eq_krullDim]

Goal state after:
Module: Mathlib.Algebra.Ring.Torsion

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : IsDomain R
inst✝ : CharZero R
n : ℕ
h : n ≠ 0
a b : R
w : (fun a ↦ n • a) a = (fun a ↦ n • a) b
⊢ a = b

Tactic:
simp only [nsmul_eq_mul, mul_eq_mul_left_iff, Nat.cast_eq_zero] at w
    grind

Goal state after:
Module: Mathlib.Algebra.Ring.Torsion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
f : R →* M
x : R
⊢ f (-x) = f x

Tactic:
rw [← neg_one_mul, map_mul, map_neg_one, one_mul]

Goal state after: