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

Goal state before:
pp: case succ
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih : ⁅h, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((toEnd R L M) f ^ n) m
⊢ ⁅h, ⁅f, ((toEnd R L M) f ^ n) m⁆⁆ = (μ - 2 * (↑n + 1)) • ⁅f, ((toEnd R L M) f ^ n) m⁆

Tactic:
leibniz_lie h,

Goal state after:
case succ
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih : ⁅h, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((toEnd R L M) f ^ n) m
⊢ ⁅⁅h, f⁆, ((toEnd R L M) f ^ n) m⁆ + ⁅f, ⁅h, ((toEnd R L M) f ^ n) m⁆⁆ =
    (μ - 2 * (↑n + 1)) • ⁅f, ((toEnd R L M) f ^ n) m⁆
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
⊢ ↑(rootSpace H 0) = ↑H.toLieSubmodule

Tactic:
← coe_zeroRootSubalgebra,

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
⊢ (zeroRootSubalgebra R L H).toSubmodule = ↑H.toLieSubmodule
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case succ
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
hm : ⁅h, m⁆ = μ • m
n : ℕ
ih : ⁅h, ((toEnd R L M) e ^ n) m⁆ = (μ + 2 * ↑n) • ((toEnd R L M) e ^ n) m
⊢ ⁅h, ⁅e, ((toEnd R L M) e ^ n) m⁆⁆ = (μ + 2 * (↑n + 1)) • ⁅e, ((toEnd R L M) e ^ n) m⁆

Tactic:
leibniz_lie h,

Goal state after:
case succ
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
hm : ⁅h, m⁆ = μ • m
n : ℕ
ih : ⁅h, ((toEnd R L M) e ^ n) m⁆ = (μ + 2 * ↑n) • ((toEnd R L M) e ^ n) m
⊢ ⁅⁅h, e⁆, ((toEnd R L M) e ^ n) m⁆ + ⁅e, ⁅h, ((toEnd R L M) e ^ n) m⁆⁆ =
    (μ + 2 * (↑n + 1)) • ⁅e, ((toEnd R L M) e ^ n) m⁆
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w v : M₁
⊢ ((B.compLeft φ) w) v - ((B.compLeft ψ) w) v = 0

Tactic:
← h,

Goal state after:
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w v : M₁
⊢ ((B.compLeft φ) w) v - ((B.compLeft φ) w) v = 0
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
i j : ι
h : i ≠ j
⊢ ⁅b.f i, b.e j⁆ = 0

Tactic:
rw [← lie_skew, neg_eq_zero, b.lie_e_f_ne j i h.symm]

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

Goal state before:
pp: case mem.inl
ι : 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
y z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x : L
⊢ b.h i ∈ lieSpan R L (range b.h)

Tactic:
exact LieSubalgebra.subset_lieSpan <| mem_range_self i

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
v : ι → V
h : ⇑(B.dualBasis hB b) = v
x✝¹ x✝ : ι
⊢ (B (v x✝¹)) (b x✝) = if x✝ = x✝¹ then 1 else 0

Tactic:
← h,

Goal state after:
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
v : ι → V
h : ⇑(B.dualBasis hB b) = v
x✝¹ x✝ : ι
⊢ (B ((B.dualBasis hB b) x✝¹)) (b x✝) = if x✝ = x✝¹ then 1 else 0
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ G.IsOrtho x (a • y) ↔ G.IsOrtho x y

Tactic:
dsimp only [IsOrtho]
  rw [map_smul]
  simp only [smul_eq_mul, mul_eq_zero, or_iff_right_iff_imp]
  exact fun a ↦ (ha a).elim

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
b₁ : B.IsRefl
W : Submodule K V
⊢ finrank K ↥W + finrank K ↥(B.orthogonal W) = finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤)

Tactic:
orthogonal_top_eq_ker b₁

Goal state after:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
b₁ : B.IsRefl
W : Submodule K V
⊢ finrank K ↥W + finrank K ↥(B.orthogonal W) = finrank K V + finrank K ↥(W ⊓ ker B)
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (toSplittingField s) ((subProdXSubC f).coeff n) = 0

Tactic:
by
  classical
  simp_rw [← AlgHom.coe_toRingHom, ← coeff_map, subProdXSubC, Polynomial.map_sub,
    Polynomial.map_prod, Polynomial.map_sub, map_X, map_C, toSplittingField,
    AlgHom.coe_toRingHom, MvPolynomial.aeval_X, dif_pos h,
    ← (finEquivRoots (Monics.splits_finsetProd h)).symm.prod_comp, Equiv.apply_symm_apply]
  rw [Finset.prod_coe_sort (f := fun x : _ × ℕ ↦ X - C x.1), (Multiset.toEnumFinset _)
    |>.prod_eq_multiset_prod, ← Function.comp_def (X - C ·) Prod.fst, ← Multiset.map_map,
    Multiset.map_toEnumFinset_fst, map_map, AlgHom.comp_algebraMap]
  conv in map _ _ => rw [Splits.eq_prod_roots (Monics.splits_finsetProd h)]
  rw [leadingCoeff_map, f.2, map_one, C_1, one_mul, sub_self, coeff_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple

Goal state before:
pp: case mp
K : Type u_3
V : Type u_4
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
⊢ f = 0 → ∀ (μ : K), f.HasEigenvalue μ → μ = 0

Tactic:
rintro rfl μ hμ

Goal state after:
case mp
K : Type u_3
V : Type u_4
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hf : IsSemisimple 0
μ : K
hμ : HasEigenvalue 0 μ
⊢ μ = 0
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
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ ⇑(chainTop α β) = ↑(chainTopCoeff α β) • α + ⇑β

Tactic:
rw [Nat.cast_smul_eq_nsmul ℤ]; rfl

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
inst✝² : IsDomain R
inst✝¹ : NeZero 2
inst✝ : IsTorsionFree R M
h : f x = 2
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ∈ End.invtSubmodule ↑(reflection h)
y : M
hy : y ∈ p
hx : x ≠ 0
this : f y • x ∈ p
aux : f y • x = 0
⊢ y ∈ LinearMap.ker f

Tactic:
smul_eq_zero

Goal state after:
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)
h' : p ∈ End.invtSubmodule ↑(reflection h)
y : M
hy : y ∈ p
hx : x ≠ 0
this : f y • x ∈ p
aux : f y = 0 ∨ x = 0
⊢ y ∈ LinearMap.ker f
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
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
hα : α ≠ 0
β : Weight K (↥H) L
⊢ x ∈ Weight.ker

Tactic:
obtain ⟨a, b, hb, hab⟩ :=
      exists_forall_mem_corootSpace_smul_add_eq_zero L α β hα β.genWeightSpace_ne_bot

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
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
hα : α ≠ 0
β : Weight K (↥H) L
a b : ℤ
hb : 0 < b
hab : ∀ x ∈ corootSpace α, (a • α + b • ⇑β) x = 0
⊢ x ∈ Weight.ker
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
induction n using Nat.twoStepInduction with
  | zero => simp
  | one => simp
  | more n ih1 ih2 =>
    trans (n + 2 : ℤ).negOnePow * (2 * x * (U R (n + 1)).eval x - (U R n).eval x)
    · push_cast; push_cast at ih2
      rw [U_add_two, eval_sub, eval_mul, eval_mul, ih1, ih2,
        Int.negOnePow_succ, Int.negOnePow_add, Int.negOnePow_even 2 even_two]
      simp; ring
    · simp

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

Goal state before:
pp: case refine_2
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 (-⇑α)
aux :
  ∀ {β : Weight K (↥H) L},
    β.IsNonZero → ∀ {y g : L}, y ∈ genWeightSpace L ⇑β → g ∈ rootSpace H ⇑β → g ≠ 0 → ∃ c, y = c • g
c₁ : K
hx_pos : c₁ • e ∈ ↑(genWeightSpace L ⇑α)
c₂ : K
hx_neg : c₂ • f ∈ ↑(genWeightSpace L (-⇑α))
hx_αneg : c₁ • e + c₂ • f ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
c₃ : K
hy_coroot : c₃ • coroot α ∈ ↑↑(corootSpace ⇑α)
hx :
  c₁ • e + c₂ • f + ↑H.toLieSubmodule.incl (c₃ • coroot α) ∈
    genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
⊢ c₁ • e + c₂ • f + ↑H.toLieSubmodule.incl (c₃ • coroot α) ∈ sl2SubalgebraOfRoot hα

Tactic:
rw [mem_sl2SubalgebraOfRoot_iff hα ht heα hfα]

Goal state after:
case refine_2
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 (-⇑α)
aux :
  ∀ {β : Weight K (↥H) L},
    β.IsNonZero → ∀ {y g : L}, y ∈ genWeightSpace L ⇑β → g ∈ rootSpace H ⇑β → g ≠ 0 → ∃ c, y = c • g
c₁ : K
hx_pos : c₁ • e ∈ ↑(genWeightSpace L ⇑α)
c₂ : K
hx_neg : c₂ • f ∈ ↑(genWeightSpace L (-⇑α))
hx_αneg : c₁ • e + c₂ • f ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
c₃ : K
hy_coroot : c₃ • coroot α ∈ ↑↑(corootSpace ⇑α)
hx :
  c₁ • e + c₂ • f + ↑H.toLieSubmodule.incl (c₃ • coroot α) ∈
    genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
⊢ ∃ c₁_1 c₂_1 c₃_1, c₁ • e + c₂ • f + ↑H.toLieSubmodule.incl (c₃ • coroot α) = c₁_1 • e + c₂_1 • f + c₃_1 • ⁅e, f⁆
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.reflection i) (P.root k) = (P.reflection j) (P.root k)

Tactic:
simp only [← root_reflectionPerm, hij]

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
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 ∈ Φ
⊢ (preReflection x' ((span R Φ).subtype.dualMap F)) ⟨y, hy⟩ ∈ {x | ↑x ∈ Φ}

Tactic:
exact hF hy'

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 : f y • x = 2 • y
⊢ x = y

Tactic:
rw [hfy, two_smul R x, two_smul R y, ← two_zsmul, ← two_zsmul] at h

Goal state after:
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
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
have h := congr_arg (fun (p : R[X]) => p.eval x) <|
    one_sub_X_sq_mul_iterate_derivative_U_eq_poly_in_U n k
  simp only [eval_mul, eval_sub, eval_one, eval_pow,
    eval_X, eval_add, eval_ofNat, eval_natCast, eval_intCast] at h
  linear_combination (norm := (push_cast; ring_nf)) h

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

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

Tactic:
one_pow,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (1 - 1) * eval 1 ((⇑derivative)^[k + 2] (T R n)) =
    (2 * ↑k + 1) * 1 * eval 1 ((⇑derivative)^[k + 1] (T R n)) - (↑n ^ 2 - ↑k ^ 2) * eval 1 ((⇑derivative)^[k] (T R n))
⊢ (2 * ↑k + 1) * eval 1 ((⇑derivative)^[k + 1] (T R n)) = (↑n ^ 2 - ↑k ^ 2) * eval 1 ((⇑derivative)^[k] (T R n))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
one_pow,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (1 - 1) * eval 1 ((⇑derivative)^[k + 2] (U R n)) =
    (2 * ↑k + 3) * 1 * eval 1 ((⇑derivative)^[k + 1] (U R n)) -
      ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 1 ((⇑derivative)^[k] (U R n))
⊢ (2 * ↑k + 3) * eval 1 ((⇑derivative)^[k + 1] (U R n)) =
    ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 1 ((⇑derivative)^[k] (U R n))
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: case h
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
d : Aˣ
hd : ↑d = ↑(den A x)
d_ne_zero : (algebraMap A K) ↑(den A x) ≠ 0
⊢ (algebraMap A K) ↑d⁻¹ * (algebraMap A K) (num A x) = mk' K (num A x) (den A x)

Tactic:
map_units_inv,

Goal state after:
case h
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
d : Aˣ
hd : ↑d = ↑(den A x)
d_ne_zero : (algebraMap A K) ↑(den A x) ≠ 0
⊢ ((algebraMap A K) ↑d)⁻¹ * (algebraMap A K) (num A x) = mk' K (num A x) (den A x)
Module: Mathlib.RingTheory.Polynomial.RationalRoot

Goal state before:
pp: case e
A : Type u_1
S : Type u_4
inst✝³ : CommRing A
inst✝² : CommRing S
M : Submonoid A
inst✝¹ : Algebra A S
inst✝ : IsLocalization M S
p : A[X]
r : A
s : ↥M
hr : (aeval (mk' S r s)) p = 0
⊢ ⇑(aeval ((algebraMap A S) r)) = eval₂ (algebraMap A S) ((algebraMap A S) ↑s * mk' S r s)

Tactic:
funext

Goal state after:
case e
A : Type u_1
S : Type u_4
inst✝³ : CommRing A
inst✝² : CommRing S
M : Submonoid A
inst✝¹ : Algebra A S
inst✝ : IsLocalization M S
p : A[X]
r : A
s : ↥M
hr : (aeval (mk' S r s)) p = 0
x✝ : A[X]
⊢ (aeval ((algebraMap A S) r)) x✝ = eval₂ (algebraMap A S) ((algebraMap A S) ↑s * mk' S r s) x✝
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
⊢ (i.restrictScalarsRange₂ j (Algebra.linearMap K L) ⋯ p hp).IsPerfPair

Tactic:
by
  have : (p.compl₁₂ (span L <| .range i).subtype (span L <| .range j).subtype).IsPerfPair :=
    .restrict _ _ _ (by simp) (by simp) (by simpa)
  exact restrictScalars_field_aux
    (p.compl₁₂ (span L <| .range i).subtype (span L <| .range j).subtype)
    ((LinearMap.range i).inclusionSpan L ∘ₗ i.rangeRestrict)
    ((LinearMap.range j).inclusionSpan L ∘ₗ j.rangeRestrict)
    (((LinearMap.range i).injective_inclusionSpan L).comp (by simpa))
    (((LinearMap.range j).injective_inclusionSpan L).comp (by simpa))
    (by rw [LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_rangeRestrict _)]
        exact (LinearMap.range i).span_range_inclusionSpan L)
    (by rw [LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_rangeRestrict _)]
        exact (LinearMap.range j).span_range_inclusionSpan L)
    fun x y ↦ LinearMap.BilinMap.apply_apply_mem_of_mem_span
      (LinearMap.range <| Algebra.linearMap K L) (range i) (range j)
      ((LinearMap.restrictScalarsₗ K L _ _ _).comp (p.restrictScalars K))
      (by simpa) (i x) (j y) (subset_span <| by simp) (subset_span <| by simp)

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
⊢ InfiniteDimensionalOrder (Submodule R M) ↔ InfiniteDimensionalOrder (Submodule R M)

Tactic:
← not_finiteDimensionalOrder_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ¬FiniteDimensionalOrder (Submodule R M) ↔ ¬FiniteDimensionalOrder (Submodule R M)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk.mk.mk.inr
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b✝ : ValueGroup A K
b : K
c✝ : ValueGroup A K
c : K
d : A
ha : ¬Quot.mk (⇑(MulAction.orbitRel Aˣ K)) 0 ≤ 0
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b

Tactic:
cases ha le_rfl

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

Goal state before:
pp: case mp.inl
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
y : ↥v.integer
hy : v ↑y ≤ γ
h : min 1 γ = 1
right✝ : 1 ≤ γ
⊢ v ((algebraMap (↥v.integer) K) y) ≤ min 1 γ

Tactic:
rw [h]
      exact y.prop

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

Goal state before:
pp: case h.left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := ⋯
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x := ⋯
x : R
hx : x ≠ 0
⊢ ∀ b ∈ Multiset.replicate (Classical.choose ⋯) p, Prime b

Tactic:
intro q hq
      have hpq := Multiset.eq_of_mem_replicate hq
      rw [hpq]
      refine ⟨spec.1.ne_zero, spec.1.not_isUnit, ?_⟩
      intro a b h
      by_cases ha : a = 0
      · rw [ha]
        simp only [true_or, dvd_zero]
      obtain ⟨m, u, rfl⟩ := spec.2 ha
      rw [mul_assoc, mul_left_comm, Units.dvd_mul_left] at h
      rw [Units.dvd_mul_right]
      by_cases hm : m = 0
      · simp only [hm, one_mul, pow_zero] at h ⊢
        right
        exact h
      left
      obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hm
      rw [pow_succ']
      apply dvd_mul_of_dvd_left dvd_rfl _

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : Nontrivial Γ₀
v : Valuation K Γ₀
x : K
hx : IsUnit x
⊢ v x ≠ 0

Tactic:
by
  simpa [hx.choose_spec] using ne_zero_of_unit v hx.choose

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
m n : ℕ
h : m ≤ n
⊢ -∑ x_1 ∈ range (n - m), (x * y) ^ (m + x_1) ∈ I ^ m

Tactic:
@neg_mem_iff

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
m n : ℕ
h : m ≤ n
⊢ ∑ x_1 ∈ range (n - m), (x * y) ^ (m + x_1) ∈ I ^ m
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : KrullDimLE 0 R
inst✝ : IsLocalRing R
I : Ideal R
hI : I ≠ ⊤
⊢ ∀ b ∈ {J | I ≤ J ∧ J.IsPrime}, IsLocalRing.maximalIdeal R ≤ b

Tactic:
rintro J ⟨h₁, h₂⟩

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : KrullDimLE 0 R
inst✝ : IsLocalRing R
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
h₁ : I ≤ J
h₂ : J.IsPrime
⊢ IsLocalRing.maximalIdeal R ≤ J
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case empty
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
hf₂ : 0 ≠ ∅
this : ∀ b ∈ 0, Associated x b
⊢ ∃ n, Associated (x ^ n) (Multiset.prod 0)

Tactic:
exact (hf₂ rfl).elim

Goal state after: