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

Goal state before:
pp: case lie.a.a
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
x yc : L
hyc : yc ∈ H
yl : L
hyl : yl ∈ lieSpan R L (range b.f)
yu : L
hyu : yu ∈ lieSpan R L (range b.e)
hx✝ : yc + yl + yu ∈ lieSpan R L (range b.e ∪ range b.f)
hu : yc + yl + yu ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ H
zl : L
hzl : zl ∈ lieSpan R L (range b.f)
zu : L
hzu : zu ∈ lieSpan R L (range b.e)
hy✝ : zc + zl + zu ∈ lieSpan R L (range b.e ∪ range b.f)
hv : zc + zl + zu ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ -⁅zu, yl⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
neg_mem_iff

Goal state after:
case lie.a.a
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
x yc : L
hyc : yc ∈ H
yl : L
hyl : yl ∈ lieSpan R L (range b.f)
yu : L
hyu : yu ∈ lieSpan R L (range b.e)
hx✝ : yc + yl + yu ∈ lieSpan R L (range b.e ∪ range b.f)
hu : yc + yl + yu ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ H
zl : L
hzl : zl ∈ lieSpan R L (range b.f)
zu : L
hzu : zu ∈ lieSpan R L (range b.e)
hy✝ : zc + zl + zu ∈ lieSpan R L (range b.e ∪ range b.f)
hv : zc + zl + zu ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅zu, yl⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : 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
⊢ ((Int.castRingHom R).mapMatrix b.A).Nondegenerate

Tactic:
Matrix.nondegenerate_iff_det_ne_zero,

Goal state after:
ι : 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
⊢ ((Int.castRingHom R).mapMatrix b.A).det ≠ 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
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 ≠ 0

Tactic:
have : h = killingForm K L e f' • (cartanEquivDual H).symm α := by
      simp only [h, Subtype.ext_iff, hef]
      rw [Submodule.coe_smul_of_tower]

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 α)
⊢ α h ≠ 0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
by
  linear_combination (norm := ring_nf) U_add_two R (n - 1)

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

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

Tactic:
by
  linear_combination (norm := ring_nf) U_add_two R (n - 1)

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

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

Tactic:
push_cast

Goal state after:
case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (U R ↑n).degree = ↑n
ih2 : (U R ↑(n + 1)).degree = ↑(n + 1)
⊢ (U R (↑n + 2)).degree = ↑n + 2
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 : ℕ
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)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (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
k : ℤ := ↑m / 2
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 k) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
e : ℤ
he : e = 0 ∨ e = 1
⊢ -(g z * 1) +
        Polynomial.eval t (S R ((e - 2) / 2 + k)) *
            (Polynomial.eval t (S R ((e - 1) / 2 + k)) + Polynomial.eval t (S R ((e - 3) / 2 + k))) *
          ((g x * f z - g z) * (1 - 2 * 1) - f z * -(g x * 1)) +
      Polynomial.eval t (S R ((e - 1) / 2 + k)) *
          (Polynomial.eval t (S R (e / 2 + k)) + Polynomial.eval t (S R ((e - 2) / 2 + k))) *
        ((f y * g z - f z) * -(g x * 1) - g z * (1 - 2 * 1)) =
    Polynomial.eval t (S R ((e + 1 - 2) / 2 + k)) *
          (Polynomial.eval t (S R ((e + 1 - 1) / 2 + k)) + Polynomial.eval t (S R ((e + 1 - 3) / 2 + k))) *
        ((g x * f z - g z) * 1) +
      Polynomial.eval t (S R ((e + 1 - 1) / 2 + k)) *
          (Polynomial.eval t (S R ((e + 1) / 2 + k)) + Polynomial.eval t (S R ((e + 1 - 2) / 2 + k))) *
        -(g z * 1)

Tactic:
linear_combination (norm := skip)
          g z * (S R (e - 1 + k)).eval t * S_eval_t_sub_two (e + k) +
          g z * S_eval_t_sq_add_S_eval_t_sq (k - 1)
      subst ht
      obtain rfl | rfl : e = 0 ∨ e = 1 := he <;> ring_nf

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

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

Tactic:
push_cast

Goal state after:
case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R ↑(n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ (U R (↑n + 2)).leadingCoeff = 2 ^ (n + 2)
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
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
⊢ h = ↑(coroot α)

Tactic:
have hef := lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg heα hfα
  lift h to H using by simpa only [← ht.lie_e_f, hef] using H.smul_mem _ (Submodule.coe_mem _)
  congr 1
  have key : α h = 2 := by
    have := lie_eq_smul_of_mem_rootSpace heα h
    rw [LieSubalgebra.coe_bracket_of_module, ht.lie_h_e_smul K] at this
    exact smul_left_injective K ht.e_ne_zero this.symm
  suffices ∃ s : K, s • h = coroot α by
    obtain ⟨s, hs⟩ := this
    replace this : s = 1 := by simpa [root_apply_coroot hα, key] using congr_arg α hs
    rwa [this, one_smul] at hs
  set α' := (cartanEquivDual H).symm α with hα'
  have h_eq : h = killingForm K L e f • α' := by
    simp only [hα', Subtype.ext_iff, ← ht.lie_e_f, hef]
    rw [Submodule.coe_smul_of_tower]
  use (2 • (α α')⁻¹) * (killingForm K L e f)⁻¹
  have hef₀ : killingForm K L e f ≠ 0 := by
    have := ht.h_ne_zero
    contrapose this
    simpa [this] using h_eq
  rw [h_eq, smul_smul, mul_assoc, inv_mul_cancel₀ hef₀, mul_one, smul_assoc, coroot]

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) (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) (U R ↑(n + 2)) = ↑↑(↑n + 2).negOnePow * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n))

Tactic:
push_cast

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) (U R (↑n + 2)) = ↑↑(↑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: case more
R : Type u_1
inst✝ : CommRing R
n : ℕ
h₀ : U R ↑n ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 n)
a✝ : U R ↑(n + 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 1))
⊢ U R ↑(n + 2) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 2))

Tactic:
push_cast

Goal state after:
case more
R : Type u_1
inst✝ : CommRing R
n : ℕ
h₀ : U R ↑n ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 n)
a✝ : U R ↑(n + 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 1))
⊢ U R (↑n + 2) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 2))
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
h e f : L
t : IsSl2Triple h e f
hte : e ∈ rootSpace H ⇑α
htf : f ∈ rootSpace H (-⇑α)
x : L
pf✝² : LieRing.IsNilpotent ↥H
pf✝¹ : LieModule K (↥H) L
pf✝ : ∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
he : ∃ e f, IsSl2Triple (Classical.choose pf✝) e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
hf :
  ∃ f,
    IsSl2Triple (Classical.choose pf✝) (Classical.choose he) f ∧
      Classical.choose he ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
ce : K
hce : he.choose = ce • e
cf : K
hcf : hf.choose = cf • f
⊢ ce ≠ 0

Tactic:
rintro rfl

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
h e f : L
t : IsSl2Triple h e f
hte : e ∈ rootSpace H ⇑α
htf : f ∈ rootSpace H (-⇑α)
x : L
pf✝² : LieRing.IsNilpotent ↥H
pf✝¹ : LieModule K (↥H) L
pf✝ : ∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
he : ∃ e f, IsSl2Triple (Classical.choose pf✝) e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
hf :
  ∃ f,
    IsSl2Triple (Classical.choose pf✝) (Classical.choose he) f ∧
      Classical.choose he ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
cf : K
hcf : hf.choose = cf • f
hce : he.choose = 0 • e
⊢ False
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
h e f : L
t : IsSl2Triple h e f
hte : e ∈ rootSpace H ⇑α
htf : f ∈ rootSpace H (-⇑α)
x : L
pf✝² : LieRing.IsNilpotent ↥H
pf✝¹ : LieModule K (↥H) L
pf✝ : ∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
he : ∃ e f, IsSl2Triple (Classical.choose pf✝) e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
hf :
  ∃ f,
    IsSl2Triple (Classical.choose pf✝) (Classical.choose he) f ∧
      Classical.choose he ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
ce : K
hce : he.choose = ce • e
cf : K
hcf : hf.choose = cf • f
hce₀ : ce ≠ 0
⊢ cf ≠ 0

Tactic:
rintro rfl

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
h e f : L
t : IsSl2Triple h e f
hte : e ∈ rootSpace H ⇑α
htf : f ∈ rootSpace H (-⇑α)
x : L
pf✝² : LieRing.IsNilpotent ↥H
pf✝¹ : LieModule K (↥H) L
pf✝ : ∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
he : ∃ e f, IsSl2Triple (Classical.choose pf✝) e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
hf :
  ∃ f,
    IsSl2Triple (Classical.choose pf✝) (Classical.choose he) f ∧
      Classical.choose he ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
ce : K
hce : he.choose = ce • e
hce₀ : ce ≠ 0
hcf : hf.choose = 0 • f
⊢ False
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ C R (-1) = X

Tactic:
change C R (Int.negSucc 0) = X
  rw [C]
  suffices X * 2 - X = X by simpa
  ring

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

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

Tactic:
comp_assoc,

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

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

Tactic:
comp_assoc,

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

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

Tactic:
push_cast

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : derivative (T R (↑n + 1)) = ↑(↑n + 1) * U R (↑n + 1 - 1)
ih2 : derivative (T R ↑n) = ↑↑n * U R (↑n - 1)
h₂ : U R (↑n - 1) = 2 * X * U R ↑n - U R (↑n + 1)
h₃ : T R (↑n + 1) = U R (↑n + 1) - X * U R (↑n + 1 - 1)
h₁ :
  derivative (T R (↑n + 2)) = (0 * X + 2 * 1) * T R (↑n + 1) + 2 * X * derivative (T R (↑n + 1)) - derivative (T R ↑n)
⊢ derivative (T R (↑n + 2)) +
        ((0 * X + 2 * 1) * T R (↑n + 1) + 2 * X * derivative (T R (↑n + 1)) - derivative (T R ↑n) +
                derivative (T R ↑n) +
              2 * X * ((↑n + 1) * U R (↑n + 1 - 1)) +
            2 * (U R (↑n + 1) - X * U R (↑n + 1 - 1)) +
          ↑n * U R (↑n - 1)) -
      ((↑n + 2) * U R (↑n + 2 - 1) +
        (derivative (T R (↑n + 2)) + ↑n * U R (↑n - 1) + 2 * X * derivative (T R (↑n + 1)) + 2 * T R (↑n + 1) +
          ↑n * (2 * X * U R ↑n - U R (↑n + 1)))) =
    0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
push_cast

Goal state after:
case a
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)
h₂ : U R (-↑n - 2) = 2 * X * U R (-↑n - 1) - U R (-↑n)
h₃ : T R (-↑n) = U R (-↑n) - X * U R (-↑n - 1)
h₁ :
  derivative (T R (-↑n - 1)) = (0 * X + 2 * 1) * T R (-↑n) + 2 * X * derivative (T R (-↑n)) - derivative (T R (-↑n + 1))
⊢ derivative (T R (-↑n - 1)) +
        (derivative (T R (-↑n + 1)) + 2 * X * (-↑n * U R (-↑n - 1)) +
              ((0 * X + 2 * 1) * T R (-↑n) + 2 * X * derivative (T R (-↑n)) - derivative (T R (-↑n + 1))) +
            2 * (U R (-↑n) - X * U R (-↑n - 1)) +
          (↑n + 1) * (2 * X * U R (-↑n - 1) - U R (-↑n))) -
      ((-↑n - 1) * U R (-↑n - 1 - 1) +
        ((-↑n + 1) * U R (-↑n + 1 - 1) + 2 * X * derivative (T R (-↑n)) + derivative (T R (-↑n - 1)) + 2 * T R (-↑n) +
          (↑n + 1) * U R (-↑n - 2))) =
    0
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 : ι
⊢ P.root ((P.reflectionPerm i ^ 2) j) = P.root (1 j)

Tactic:
simp only [sq, Equiv.Perm.mul_apply, root_reflectionPerm, reflection_same, Equiv.Perm.one_apply]

Goal state after:
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 : ι
⊢ MapsTo (⇑(P.coreflection i)) (range ⇑P.coroot) (range ⇑P.coroot)

Tactic:
rintro - ⟨j, rfl⟩
  exact P.coroot_reflectionPerm i j ▸ mem_range_self (P.reflectionPerm i j)

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

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

Tactic:
push_cast

Goal state after:
case a
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) * (2 * X * T R (n + 1) - T R n) + (-X ^ 2 + 1) * ((↑n + 1) * U R (n + 1 - 1)) +
          (↑n + 1) * (X * T R (n + 1) - T R (n + 2))) -
      ((↑n + 1) * (T R n - X * T R (n + 1)) +
        ((-↑n - 1) * T R (n + 2) + (-X ^ 2 + 1) * derivative (T R (n + 1)) + (↑n + 1) * ((1 - X ^ 2) * U R n))) =
    0
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
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
⊢ x ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f 0 = 2
hf₂ : MapsTo (⇑(preReflection 0 f)) Φ Φ
hg₁ : g 0 = 2
hg₂ : MapsTo (⇑(preReflection 0 g)) Φ Φ
⊢ False
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : 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
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
f : ↥H → R
hf : f ∈ sU
g : ↥H → R
hg : g ∈ sV
⊢ f ≠ g

Tactic:
rintro rfl

Goal state after:
ι : 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
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
f : ↥H → R
hf : f ∈ sU
hg : f ∈ sV
⊢ False