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

Goal state before:
pp: 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
⊢ sSup {J | IsAtom J ∧ J ≤ I} = I

Tactic:
apply le_antisymm

Goal state after:
case a
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
⊢ sSup {J | IsAtom J ∧ J ≤ I} ≤ I

case a
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
⊢ I ≤ sSup {J | IsAtom J ∧ J ≤ I}
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case h.right
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
⊢ sSup C = sSup (sSup {x | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})

Tactic:
apply le_antisymm

Goal state after:
case h.right.a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
⊢ sSup C ≤ sSup (sSup {x | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})

case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
⊢ sSup (sSup {x | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}) ≤ sSup C
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
hT : ∅ ⊆ S
ha : IsAtom (sSup ∅)
haS : sSup ∅ ≤ sSup S
⊢ sSup ∅ ∈ S

pp: case inr
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
⊢ sSup T ∈ S

Tactic:
· simp only [sSup_empty] at ha
    exact (ha.1 rfl).elim

Goal state after:
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
⊢ sSup T ∈ S
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
⊢ sSup (T₁ ∩ T₂) = sSup T₁ ⊓ sSup T₂

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
⊢ sSup (T₁ ∩ T₂) ≤ sSup T₁ ⊓ sSup T₂

case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
⊢ sSup T₁ ⊓ sSup T₂ ≤ sSup (T₁ ∩ T₂)
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
⊢ sSup (T₁ ∩ T₂) ≤ sSup T₂

Tactic:
· apply sSup_le_sSup Set.inter_subset_right

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ S = {a | IsAtom a}

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ S ⊆ {a | IsAtom a}

case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ {a | IsAtom a} ⊆ S
Module: Mathlib.Algebra.Lie.Weights.Linear

Goal state before:
pp: R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : LinearWeights R L M
χ : Weight R L M
h : χ.IsZero
x✝ : L
⊢ (toLinear R L M χ) x✝ = 0 x✝

Tactic:
simp [h.eq]

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

Goal state before:
pp: case right
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map ↑I.incl ↑J;
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : J' = I
⊢ J = ⊤

Tactic:
eq_top_iff

Goal state after:
case right
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map ↑I.incl ↑J;
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : J' = I
⊢ ⊤ ≤ J
Module: Mathlib.Algebra.Lie.Weights.Linear

Goal state before:
pp: k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
χ : L → R
inst✝ : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
a✝ : Nontrivial ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x, ↑(t • m)⁆ - χ x • ↑(t • m) = ↑(t • ⁅x, m⁆)

Tactic:
simp only [SetLike.val_smul, lie_smul]

Goal state after:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
χ : L → R
inst✝ : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
a✝ : Nontrivial ↥(shiftedGenWeightSpace R L M χ)
⊢ t • ⁅x, ↑m⁆ - χ x • t • ↑m = t • ↑⁅x, m⁆
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: case pos
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
⊢ factor 0 ∣ 0

Tactic:
exact dvd_zero _

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian ↥I
⊢ ¬∃ a, IsAtom a ∧ a ≤ I

Tactic:
rintro ⟨J, hJ, hJ'⟩

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
⊢ False
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
q : ℚ≥0
⊢ (algebraMap K f.SplittingField) ↑q.num / (algebraMap K f.SplittingField) ↑q.den = ↑q.num / ↑q.den

Tactic:
map_natCast

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
q : ℚ≥0
⊢ (algebraMap K f.SplittingField) ↑q = ↑q.num / ↑q.den

Tactic:
simp_rw [NNRat.cast_def, map_div₀, map_natCast]

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
q : ℚ
⊢ ↑q.num / (algebraMap K f.SplittingField) ↑q.den = ↑q.num / ↑q.den

Tactic:
map_natCast

Goal state after:
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
q : ℚ
⊢ ↑q.num / ↑q.den = ↑q.num / ↑q.den
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
q : ℚ≥0
⊢ (algebraMap k (AlgebraicClosure k)) ↑q.num / (algebraMap k (AlgebraicClosure k)) ↑q.den = ↑q.num / ↑q.den

Tactic:
map_natCast

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
q : ℚ≥0
⊢ (algebraMap k (AlgebraicClosure k)) ↑q = ↑q.num / ↑q.den

Tactic:
simp_rw [NNRat.cast_def, map_div₀, map_natCast]

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
q : ℚ
⊢ ↑q.num / (algebraMap k (AlgebraicClosure k)) ↑q.den = ↑q.num / ↑q.den

Tactic:
map_natCast

Goal state after:
k : Type u
inst✝ : Field k
q : ℚ
⊢ ↑q.num / ↑q.den = ↑q.num / ↑q.den
Module: Mathlib.RingTheory.Finiteness.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
A : Matrix ι ι R
h : ∀ (v : ι → R), ∃ n, Aᵀ ^ n *ᵥ v = 0
i : ι
n : ℕ
hn : Aᵀ ^ n *ᵥ Pi.single i 1 = 0
⊢ (A ^ n).row i = 0

Tactic:
simpa [← transpose_pow] using hn

Goal state after:
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
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
⊢ genWeightSpaceChain M (-χ₁) χ₂ (-q) (-p) = genWeightSpaceChain M χ₁ χ₂ p q

Tactic:
by
  let e : ℤ ≃ ℤ := neg_involutive.toPerm
  simp_rw [genWeightSpaceChain, ← e.biSup_comp (Ioo p q)]
  simp [e, -mem_Ioo]

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
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
x✝ : ↥H
⊢ (-α) x✝ = 0 x✝

Tactic:
coe_neg,

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
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
x✝ : ↥H
⊢ (-⇑α) x✝ = 0 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
hn : n < m
u : R
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (↑S '' Set.Iio m)
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq_natDegree : head.degree = ↑head.natDegree
p_ne_zero : ¬P = 0
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
tail_eq_zero : ¬tail = 0
head_degree_eq : P.natDegree = head.natDegree
⊢ P.leadingCoeff = P.leadingCoeff • u • (↑S n).coeff (↑S n).natDegree

Tactic:
coeff_natDegree,

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
hn : n < m
u : R
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (↑S '' Set.Iio m)
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq_natDegree : head.degree = ↑head.natDegree
p_ne_zero : ¬P = 0
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
tail_eq_zero : ¬tail = 0
head_degree_eq : P.natDegree = head.natDegree
⊢ P.leadingCoeff = P.leadingCoeff • u • (↑S n).leadingCoeff
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
x : M
f : Dual R M
inst✝² : IsDomain R
inst✝¹ : NeZero 2
inst✝ : IsTorsionFree R M
h : f x = 2
p : Submodule R M
hp : Disjoint p (R ∙ x)
y : M
h' : y ∈ Submodule.comap (↑(reflection h)) p
hy : y ∈ p
hx : x ≠ 0
⊢ f y • x ∈ p

Tactic:
simp only [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply] at h'

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
x : M
f : Dual R M
inst✝² : IsDomain R
inst✝¹ : NeZero 2
inst✝ : IsTorsionFree R M
h : f x = 2
p : Submodule R M
hp : Disjoint p (R ∙ x)
y : M
hy : y ∈ p
hx : x ≠ 0
h' : y - f y • x ∈ p
⊢ f y • x ∈ p
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
⊢ α (coroot α) = 2

Tactic:
rw [← Weight.coe_coe]
  simpa [coroot] using inv_mul_cancel₀ (root_apply_cartanEquivDual_symm_ne_zero hα)

Goal state after:
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 ι
i : ι
x : ↥H
⊢ (b.baseSupp i) x • b.e i = ⁅x, b.e i⁆

Tactic:
obtain ⟨x, hx⟩ := x

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 ι
i : ι
x : L
hx : x ∈ H
⊢ (b.baseSupp i) ⟨x, hx⟩ • b.e i = ⁅⟨x, hx⟩, b.e i⁆
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:
by
  obtain ⟨m, rfl | rfl⟩ := n.eq_nat_or_neg
  case inl => rw [degree_U_natCast R m]; norm_cast
  case inr =>
    rw [U_neg, degree_neg]
    cases m with
    | zero => simp
    | succ m =>
      cases m with
      | zero => contradiction
      | succ m =>
        trans (U R m).degree
        · congr; omega
        · rw [degree_U_natCast R m]; norm_cast

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:
simp_rw [C_sub_one, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]

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

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

Tactic:
by
  induction k
  case zero =>
    rw [Function.iterate_zero_apply]
    exact Submodule.mem_span_of_mem ⟨n, by simp⟩
  case succ k ih =>
    rw [Function.iterate_succ_apply']
    suffices Submodule.span ℕ ((fun m : ℕ => derivative (T R m)) '' Set.Icc 0 (n - k)) ≤
      Submodule.span ℕ ((fun m : ℕ => T R m) '' Set.Icc 0 (n - (k + 1))) by
      apply this
      convert! Submodule.apply_mem_span_image_of_mem_span (derivative.restrictScalars ℕ) ih using 2
      simp [Set.image]
    refine Submodule.span_le.mpr (fun x hx => ?_)
    obtain ⟨m, hm, rfl⟩ := hx
    refine (Submodule.span_mono (by grind)) (T_derivative_mem_span_T (R := R) m)

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

Goal state before:
pp: case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
hj : j ≠ (p.scaleRoots ↑(den A r)).natDegree
h : (p.scaleRoots ↑(den A r)).natDegree ≤ j
⊢ ↑(den A r) ∣ 0

Tactic:
exact dvd_zero _

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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : C R m * C R (↑k + 1) = C R (m + (↑k + 1)) + C R (m - (↑k + 1))
ih2 : C R m * C R ↑k = C R (m + ↑k) + C R (m - ↑k)
⊢ C R m * C R (↑k + 2) = C R (m + (↑k + 2)) + C R (m - (↑k + 2))

Tactic:
have h₁ := C_add_two R (m + k)

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : C R m * C R (↑k + 1) = C R (m + (↑k + 1)) + C R (m - (↑k + 1))
ih2 : C R m * C R ↑k = C R (m + ↑k) + C R (m - ↑k)
h₁ : C R (m + ↑k + 2) = X * C R (m + ↑k + 1) - C R (m + ↑k)
⊢ C R m * C R (↑k + 2) = C R (m + (↑k + 2)) + C R (m - (↑k + 2))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m n : ℤ
⊢ T R (m * n) = (T R m).comp (T R n)

Tactic:
induction m using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two m ih1 ih2 =>
    have h₁ := T_mul_T R ((m + 1) * n) n
    have h₂ := congr_arg (comp · (T R n)) <| T_add_two R m
    simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1
  | neg_add_one m ih1 ih2 =>
    have h₁ := T_mul_T R ((-m) * n) n
    have h₂ := congr_arg (comp · (T R n)) <| T_add_two R (-m - 1)
    simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1

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
s : CompositionSeries (Submodule R M)
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
H : IsFiniteLength R M
this✝ : IsNoetherian R M
this : IsArtinian R M
⊢ ↑↑s.length = Order.krullDim (Submodule R M)

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
H : IsFiniteLength R M
this✝ : IsNoetherian R M
this : IsArtinian R M
⊢ ↑↑s.length ≤ Order.krullDim (Submodule R M)

case a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
H : IsFiniteLength R M
this✝ : IsNoetherian R M
this : IsArtinian R M
⊢ Order.krullDim (Submodule R M) ≤ ↑↑s.length
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
ι : Type u_5
h✝ : Infinite ι
a✝ : Nontrivial M
m : ℕ
s : Finset ι
hs : s.card = m
this : length R (↥s →₀ M) = ↑m * length R M
⊢ ↑m ≤ ↑m * length R M

Tactic:
exact ENat.self_le_mul_right _ length_pos.ne'

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

Goal state before:
pp: case succ
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
n : ℕ
⊢ f (n + 1) ≡ f 1 [SMOD ⊥ ^ (n + 1) • ⊤]

Tactic:
specialize hf (Nat.le_add_left 1 n)

Goal state after:
case succ
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
n : ℕ
hf : f 1 ≡ f (n + 1) [SMOD ⊥ ^ 1 • ⊤]
⊢ f (n + 1) ≡ f 1 [SMOD ⊥ ^ (n + 1) • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_6
s : Finset ι
f : ι → AdicCompletion I M
⊢ ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

Tactic:
← funext (incl_apply _ _ _),

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_6
s : Finset ι
f : ι → AdicCompletion I M
⊢ (incl I M) (∑ i ∈ s, f i) = ∑ x ∈ s, (incl I M) (f x)
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P, P ≠ ⊥ ∧ P.IsPrime
⊢ IsDiscreteValuationRing R

Tactic:
have : IsLocalRing R := IsLocalRing.of_unique_nonzero_prime Punique

Goal state after:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P, P ≠ ⊥ ∧ P.IsPrime
this : IsLocalRing R
⊢ IsDiscreteValuationRing R
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case neg
𝒪 : Type u
K : Type v
inst✝² : CommRing 𝒪
inst✝¹ : Field K
inst✝ : Algebra 𝒪 K
h : ∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
hinj : Function.Injective ⇑(algebraMap 𝒪 K)
this✝¹ : IsDomain 𝒪
this✝ : FaithfulSMul 𝒪 K
this : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
h0 : ¬a = 0
⊢ ∃ x_1, x * (algebraMap 𝒪 K) ↑x_1.2 = (algebraMap 𝒪 K) x_1.1

Tactic:
· have : algebraMap 𝒪 K a ≠ 0 := by simpa using h0
    rw [inv_eq_iff_eq_inv, ← one_div, eq_div_iff this] at ha
    cases ha with
    | inl ha => exact ⟨⟨a, 1⟩, by simpa⟩
    | inr ha => exact ⟨⟨1, ⟨a, mem_nonZeroDivisors_of_ne_zero h0⟩⟩, by simpa using ha⟩

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

Goal state before:
pp: 𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
⊢ ValuationRing 𝒪

Tactic:
have := hh.hom_inj.isDomain
  suffices PreValuationRing 𝒪 from .mk
  constructor
  intro a b
  rcases le_total (v (algebraMap 𝒪 K a)) (v (algebraMap 𝒪 K b)) with h | h
  · obtain ⟨c, hc⟩ := Valuation.Integers.dvd_of_le hh h
    use c; exact Or.inr hc.symm
  · obtain ⟨c, hc⟩ := Valuation.Integers.dvd_of_le hh h
    use c; exact Or.inl hc.symm

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

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
ex : ∃ n, p ^ n ∈ I
⊢ I = span {p ^ Nat.find ex}

Tactic:
apply le_antisymm

Goal state after:
case h.a
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
ex : ∃ n, p ^ n ∈ I
⊢ I ≤ span {p ^ Nat.find ex}

case a
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
ex : ∃ n, p ^ n ∈ I
⊢ span {p ^ Nat.find ex} ≤ I