mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: case neg
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
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq : (P.leadingCoeff • u • ↑S n).degree = (u • ↑S n).degree
⊢ tail.degree < ↑n

Tactic:
u_degree_same,

Goal state after:
case neg
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
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq : (P.leadingCoeff • u • ↑S n).degree = (↑S n).degree
⊢ tail.degree < ↑n
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ α : Weight K (↥H) L
hα : ¬α.IsZero
e : genWeightSpace L (-⇑α) = ⊥
x : L
hx : x ∈ genWeightSpace L ⇑α
x_ne0 : x ≠ 0
y : L
hy : y ∈ rootSpace H (-⇑α)
⊢ ((killingForm K L) x) y = 0

Tactic:
rootSpace,

Goal state after:
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ α : Weight K (↥H) L
hα : ¬α.IsZero
e : genWeightSpace L (-⇑α) = ⊥
x : L
hx : x ∈ genWeightSpace L ⇑α
x_ne0 : x ≠ 0
y : L
hy : y ∈ genWeightSpace L (-⇑α)
⊢ ((killingForm K L) x) y = 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
y : L
hy : y ∈ H
z : L
hz : z ∈ H
⊢ ⁅y, z⁆ = 0

Tactic:
suffices ⁅(⟨y, hy⟩ : H), (⟨z, hz⟩ : H)⁆ = 0 by
    simpa only [Subtype.ext_iff, LieSubalgebra.coe_bracket, ZeroMemClass.coe_zero] using this

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
x : ↥H
hx : x ∈ corootSpace 0
y : L
hy : y ∈ H
z : L
hz : z ∈ H
⊢ ⁅⟨y, hy⟩, ⟨z, hz⟩⁆ = 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
z x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1
hzc : ∀ (x : L), ⁅x, z⁆ = 0
y : A ⊗[R] L
a : A
u : L
⊢ ⁅a ⊗ₜ[R] u, 1 ⊗ₜ[R] z⁆ = 0

Tactic:
by simp [hzc u]

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

Goal state before:
pp: case zero
ι : 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 ι
i : ι
x : L
hx : 0 ∈ H
⊢ (b.baseSupp i) ⟨0, hx⟩ • b.e i = ⁅0, b.e i⁆

Tactic:
change b.baseSupp i 0 • _ = _; simp

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

Goal state before:
pp: case refine_1
ι : 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 u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
n₁ n₂ : ↑{n | n ≠ 0}
h : (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) n₁ = (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) n₂
⊢ n₁ = n₂

pp: case refine_2
ι : 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 u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
χ : ↑s
⊢ ∃ a, (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) a = χ

Tactic:
· ext i
        have := b.linearIndependent_baseSupp.restrict_scalars' ℕ
        refine Fintype.linearIndependent_iffₛ.mp this n₁ n₂ ?_ i
        ext v
        rw [Subtype.mk.injEq] at h
        simpa using congr_fun h v

Goal state after:
case refine_2
ι : 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 u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
χ : ↑s
⊢ ∃ a, (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) a = χ
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
⊢ h = coroot α

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

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
⊢ h = coroot α
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:
simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case pred
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
t : R
ht : t = f y * g x - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ (-↑m)) x =
    (Polynomial.eval t (S R (-↑m)) + Polynomial.eval t (S R (-↑m - 1))) • x +
      (Polynomial.eval t (S R (-↑m - 1)) * -g x) • y
⊢ ((reflection hf * reflection hg) ^ (-1 + -↑m)) x =
    (Polynomial.eval t (S R (-1 + -↑m)) + Polynomial.eval t (S R (-1 + -↑m - 1))) • x +
      (Polynomial.eval t (S R (-1 + -↑m - 1)) * -g x) • y

Tactic:
zpow_add,

Goal state after:
case pred
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
t : R
ht : t = f y * g x - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ (-↑m)) x =
    (Polynomial.eval t (S R (-↑m)) + Polynomial.eval t (S R (-↑m - 1))) • x +
      (Polynomial.eval t (S R (-↑m - 1)) * -g x) • y
⊢ ((reflection hf * reflection hg) ^ (-1) * (reflection hf * reflection hg) ^ (-↑m)) x =
    (Polynomial.eval t (S R (-1 + -↑m)) + Polynomial.eval t (S R (-1 + -↑m - 1))) • x +
      (Polynomial.eval t (S R (-1 + -↑m - 1)) * -g x) • y
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
inst✝¹ : Finite ι
inst✝ : IsAddTorsionFree N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
x x✝ : N
⊢ (P.root' j) x✝ = (t • P.root' i) x✝

Tactic:
simp [h, root']

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 j k : ι
hij : P.reflectionPerm i = P.reflectionPerm j
⊢ P.pairing k i • P.root i = P.pairing k j • P.root j

Tactic:
by
  have h : P.reflection i (P.root k) = P.reflection j (P.root k) := by
    simp only [← root_reflectionPerm, hij]
  simpa only [reflection_apply_root, sub_right_inj] using h

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

Goal state before:

Tactic:
2 • P.toLinearMap x (P.coroot i) • P.root i
      = P.toLinearMap x (P.coroot i) • ((2 : R) • P.root i) := ?_
    _ = P.toLinearMap x (P.coroot i) • (P.pairing i j • P.root j) := ?_
    _ = P.toLinearMap x (P.pairing i j • P.coroot i) • (P.root j) := ?_
    _ = P.toLinearMap x ((2 : R) • P.coroot j) • (P.root j) := ?_
    _ = 2 • P.toLinearMap x (P.coroot j) • P.root j := ?_

Goal state after:
case calc_1
ι : 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ 2 • (P.toLinearMap x) (P.coroot i) • P.root i = (P.toLinearMap x) (P.coroot i) • 2 • P.root i

case calc_2
ι : 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.toLinearMap x) (P.coroot i) • 2 • P.root i = (P.toLinearMap x) (P.coroot i) • P.pairing i j • P.root j

case calc_3
ι : 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.toLinearMap x) (P.coroot i) • P.pairing i j • P.root j = (P.toLinearMap x) (P.pairing i j • P.coroot i) • P.root j

case calc_4
ι : 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.toLinearMap x) (P.pairing i j • P.coroot i) • P.root j = (P.toLinearMap x) (2 • P.coroot j) • P.root j

case calc_5
ι : 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.toLinearMap x) (2 • P.coroot j) • P.root j = 2 • (P.toLinearMap x) (P.coroot j) • P.root j
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 ↑Φ
hx : x ∈ 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)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
x' : ↥(span R Φ) := ⟨x, hx⟩
F : Dual R M
hF : MapsTo (⇑(preReflection x F)) Φ Φ
y : M
hy : y ∈ span R Φ
⊢ ⟨y, hy⟩ ∈ Φ' → (preReflection x' ((span R Φ).subtype.dualMap F)) ⟨y, hy⟩ ∈ Φ'

Tactic:
hy'

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
x : M
Φ : Set M
hΦ₁ : Finite ↑Φ
hx : x ∈ 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)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
x' : ↥(span R Φ) := ⟨x, hx⟩
F : Dual R M
hF : MapsTo (⇑(preReflection x F)) Φ Φ
y : M
hy : y ∈ span R Φ
hy' : ⟨y, hy⟩ ∈ Φ'
⊢ (preReflection x' ((span R Φ).subtype.dualMap F)) ⟨y, hy⟩ ∈ Φ'
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k] ((1 - X ^ 2) * (⇑derivative)^[2] (U R n)) =
    (⇑derivative)^[k] (3 * X * derivative (U R n) - ↑((n + 2) * n) * U R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (U R n) =
    (2 * ↑k + 3) * X * (⇑derivative)^[k + 1] (U R n) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * (⇑derivative)^[k] (U R n)

Tactic:
rw [sub_mul, iterate_derivative_sub, one_mul, ← Function.iterate_add_apply, mul_comm (X ^ 2),
    iterate_derivative_sub, mul_assoc 3, ← Nat.cast_three, iterate_derivative_natCast_mul,
    mul_comm X, iterate_derivative_intCast_mul, iterate_derivative_derivative_mul_X_sq,
    iterate_derivative_derivative_mul_X] at h

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (U R n) -
      ((⇑derivative)^[k + 2] (U R n) * X ^ 2 + (2 * k) • (⇑derivative)^[k + 1] (U R n) * X +
        (k * (k - 1)) • (⇑derivative)^[k] (U R n)) =
    ↑3 * ((⇑derivative)^[k + 1] (U R n) * X + k • (⇑derivative)^[k] (U R n)) -
      ↑((n + 2) * n) * (⇑derivative)^[k] (U R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (U R n) =
    (2 * ↑k + 3) * X * (⇑derivative)^[k + 1] (U R n) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * (⇑derivative)^[k] (U R n)
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
inst✝ : IsNoetherian R L
⊢ H.IsCartanSubalgebra

Tactic:
by
  let := b.isLieAbelian_cartan
  rw [← eq_rootSpace_zero_iff_isCartan, b.cartan_eq]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
b : R ⧸ I ^ n
hb : (factorPow I ⋯) a * b = 1
right✝ : b * (factorPow I ⋯) a = 1
⊢ IsUnit a

Tactic:
rcases factor_surjective (pow_le_pow_right n.le_succ) b with ⟨b', hb'⟩

Goal state after:
R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
b : R ⧸ I ^ n
hb : (factorPow I ⋯) a * b = 1
right✝ : b * (factorPow I ⋯) a = 1
b' : R ⧸ I ^ n.succ
hb' : (factor ⋯) b' = b
⊢ IsUnit a
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c : ℕ
h : c = b + a
N : Submodule R M
⊢ Function.Injective ⇑(powSMulQuotInclusion I M h N)

Tactic:
rw [← LinearMap.ker_eq_bot]
  simp [powSMulQuotInclusion, mapQ, ← le_bot_iff, ker_liftQ, LinearMap.ker_comp, pow_add, mul_smul,
    map_le_iff_le_comap, ← Submodule.map_le_map_iff_of_injective (I ^ a • N).subtype_injective, h]

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case inl.intro
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_5
h✝ : Finite ι
val✝ : Fintype ι
⊢ length R (ι →₀ M) = ENat.card ι * length R M

Tactic:
simp [(Finsupp.linearEquivFunOnFinite R M ι).length_eq]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mpr
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) ((⇑v ∘ ⇑(algebraMap O F)) a)
b : O
⊢ b ∈ I ↔ a ∣ b

Tactic:
exact ⟨fun hb ↦ dvd_of_le hv (hx.2 <| mem_image_of_mem _ hb), fun hb ↦ I.mem_of_dvd hb ha⟩

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case neg.inr
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
b : A
hb : b ∈ β
c : A
h : b * c = a
⊢ b ∈ α

Tactic:
exfalso

Goal state after:
case neg.inr
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
b : A
hb : b ∈ β
c : A
h : b * c = a
⊢ False
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
x s : R
hy : x * s ∈ nonZeroDivisors R
this : (algebraMap R K) (x * s) ≠ 0
⊢ (algebraMap R K) s * ((algebraMap R K) x / (algebraMap R K) (x * s)) = 1

Tactic:
by rwa [mul_div, div_eq_one_iff_eq, map_mul, mul_comm]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ (fun a ↦ a * g) (x * a + y * b) = (fun a ↦ a * g) 1

Tactic:
convert! e' using 1 <;> ring

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsHausdorff I M
x : M
hx : (of I M) x = 0
n : ℕ
⊢ x ≡ 0 [SMOD I ^ n • ⊤]

Tactic:
Subtype.ext_iff

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsHausdorff I M
x : M
hx : ↑((of I M) x) = ↑0
n : ℕ
⊢ x ≡ 0 [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I : Ideal R
inst✝ : IsJacobsonRing R
⊢ Function.Surjective ⇑(Ideal.Quotient.mk I)

Tactic:
by
    rintro ⟨x⟩
    use x
    rfl

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O K
v : Valuation K Γ₀
hv : v.Integers O
this✝ : IsDomain O := Function.Injective.isDomain (algebraMap O K) hv.hom_inj
inst✝ : IsDiscreteValuationRing O
ϖ : O
h : Irreducible ϖ
n : ℕ
this : v ((algebraMap O K) ϖ) ^ n = v ((algebraMap O K) (ϖ ^ n))
⊢ ↑(maximalIdeal O ^ n) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ) ^ n}

Tactic:
rw [this, ← hv.coe_span_singleton_eq_setOfPred_le_v_algebraMap,
      ← Ideal.span_singleton_pow, ← h.maximalIdeal_eq]

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x✝¹ x✝ : Associates R
⊢ (associatesEquivIsPrincipal R).toFun (x✝¹ * x✝) =
    (associatesEquivIsPrincipal R).toFun x✝¹ * (associatesEquivIsPrincipal R).toFun x✝

Tactic:
Subtype.ext_iff

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x✝¹ x✝ : Associates R
⊢ ↑((associatesEquivIsPrincipal R).toFun (x✝¹ * x✝)) =
    ↑((associatesEquivIsPrincipal R).toFun x✝¹ * (associatesEquivIsPrincipal R).toFun x✝)
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
f : R[X]
n : ℕ
hf : ((Ideal.Quotient.mk I).comp C).rangeRestrict (f.coeff n) = 0
⊢ f.coeff n ∈ comap C I

Tactic:
Subtype.ext_iff

Goal state after:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
f : R[X]
n : ℕ
hf : ↑(((Ideal.Quotient.mk I).comp C).rangeRestrict (f.coeff n)) = ↑0
⊢ f.coeff n ∈ comap C I
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
P' : Ideal R := comap C P
this✝ : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
hPJ : P = comap f (Ideal.map f P)
this : (Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P).IsMaximal
⊢ IsJacobsonRing (R ⧸ P')

pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
P' : Ideal R := comap C P
this✝ : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
hPJ : P = comap f (Ideal.map f P)
this : (Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P).IsMaximal
x : R ⧸ P'
hx : C x ∈ Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P
⊢ x = 0

Tactic:
any_goals exact isJacobsonRing_quotient

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
P' : Ideal R := comap C P
this✝ : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
hPJ : P = comap f (Ideal.map f P)
this : (Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P).IsMaximal
x : R ⧸ P'
hx : C x ∈ Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P
⊢ x = 0