mathlib-initiative/mathlib-tactics huggingface dataset:
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✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
x y : ↥(rootSpace H χ₁)
m : ↥(genWeightSpace M χ₂)
⊢ ↑({ toFun := fun m ↦ ⟨⁅↑(x + y), ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } m) =
    ↑(({ toFun := fun m ↦ ⟨⁅↑x, ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } +
          { toFun := fun m ↦ ⟨⁅↑y, ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ })
        m)

Tactic:
simp only [LieSubmodule.coe_add, add_lie, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply,
      AddMemClass.mk_add_mk]

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

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✝ : IsNoetherian R M
χ : L → R
x : L
this :
  (toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x) =
    LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯
⊢ _root_.IsNilpotent ((toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x))

Tactic:
obtain ⟨k, hk⟩ := exists_genWeightSpace_le_ker_of_isNoetherian M χ x

Goal state after:
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✝ : IsNoetherian R M
χ : L → R
x : L
this :
  (toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x) =
    LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯
k : ℕ
hk : ↑(genWeightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)
⊢ _root_.IsNilpotent ((toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x))
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
k : ℕ
hk : rootSpace H 0 ≤ LieSubmodule.ucs k ⊥
⊢ rootSpace H 0 ≤ H.toLieSubmodule

Tactic:
exact hk.trans (LieSubmodule.ucs_le_of_normalizer_eq_self (by simp) k)

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

Goal state before:
pp: case h
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
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective ⇑f
m : M
hm : ∀ (x : L), ∃ k, (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
x : L
h : ((toEnd R L M₂) x - χ x • 1) ∘ₗ ↑f = ↑f ∘ₗ ((toEnd R L M) x - χ x • 1)
k : ℕ
hk : (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
⊢ (((toEnd R L M) x - χ x • 1) ^ k) m = 0

Tactic:
suffices f (((toEnd R L M x - χ x • ↑1) ^ k) m) = 0 by
      rw [← map_zero f] at this; exact hf this

Goal state after:
case h
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
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective ⇑f
m : M
hm : ∀ (x : L), ∃ k, (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
x : L
h : ((toEnd R L M₂) x - χ x • 1) ∘ₗ ↑f = ↑f ∘ₗ ((toEnd R L M) x - χ x • 1)
k : ℕ
hk : (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
⊢ f ((((toEnd R L M) x - χ x • 1) ^ k) m) = 0
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case mem
ι : 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 u : L
hu : u ∈ range b.f
⊢ ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
obtain ⟨j, rfl⟩ := hu

Goal state after:
case mem
ι : 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
j : ι
⊢ ⁅b.e i, b.f j⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
Module: Mathlib.Algebra.Lie.Weights.Basic

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✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
χ₁ : L → R
a✝ : χ₁ ∈ {χ | genWeightSpace M χ ≠ ⊥}
χ₂ : L → R
hχ₂ : χ₂ ∈ {χ | genWeightSpace M χ ≠ ⊥}
hχ₁₂ : genWeightSpace M χ₁ = genWeightSpace M χ₂
⊢ χ₁ = χ₂

Tactic:
contrapose! hχ₂

Goal state after:
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✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
χ₁ : L → R
a✝ : χ₁ ∈ {χ | genWeightSpace M χ ≠ ⊥}
χ₂ : L → R
hχ₁₂ : genWeightSpace M χ₁ = genWeightSpace M χ₂
hχ₂ : χ₁ ≠ χ₂
⊢ χ₂ ∉ {χ | genWeightSpace M χ ≠ ⊥}
Module: Mathlib.Algebra.Lie.Weights.Basic

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✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
x : L
⊢ iSupIndep fun χ ↦ genWeightSpaceOf M χ x

Tactic:
rw [← LieSubmodule.iSupIndep_toSubmodule]
  dsimp [genWeightSpaceOf]
  exact (toEnd R L M x).independent_genEigenspace _

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

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✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
χ : L → R
x : L
⊢ (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x) = finrank R ↥(genWeightSpace M χ) • χ x

Tactic:
by
  suffices _root_.IsNilpotent ((toEnd R L (genWeightSpace M χ) x) - χ x • LinearMap.id) by
    replace this := (isNilpotent_trace_of_isNilpotent this).eq_zero
    rwa [map_sub, map_smul, trace_id, sub_eq_zero, smul_eq_mul, mul_comm,
      ← nsmul_eq_mul] at this
  rw [← Module.algebraMap_end_eq_smul_id]
  exact isNilpotent_toEnd_sub_algebraMap M χ x

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
B : BilinForm K V
W : Subspace K V
⊢ Submodule.map (Submodule.subtype W) (domRestrict B W).ker = W ⊓ ker B

Tactic:
ext x; constructor <;> intro hx
  · rcases hx with ⟨⟨x, hx⟩, hker, rfl⟩
    constructor
    · simp [hx]
    · simpa
  · simp_rw [Submodule.mem_map, LinearMap.mem_ker]
    exact ⟨⟨x, hx.1⟩, hx.right, rfl⟩

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
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.orthogonal W = ⊥
⊢ W = ⊤

Tactic:
have := (B.isCompl_orthogonal_of_restrict_nondegenerate b₁ b₂).sup_eq_top

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
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.orthogonal W = ⊥
this : W ⊔ B.orthogonal W = ⊤
⊢ W = ⊤
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ m.toEnumFinset.card = m.card

Tactic:
rw [Finset.card, ← Multiset.card_map Prod.fst m.toEnumFinset.val]
  congr
  exact m.map_toEnumFinset_fst

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

Goal state before:
pp: k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (map (Ideal.Quotient.mk (maxIdeal k))
          (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f - ∏ i, (X - C (MvPolynomial.X ⟨f, i⟩)))).coeff
      n✝ =
    0

Tactic:
← subProdXSubC,

Goal state after:
k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (map (Ideal.Quotient.mk (maxIdeal k)) (subProdXSubC f)).coeff n✝ = 0
Module: Mathlib.Algebra.Lie.Derivation.Killing

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
x : L
h : (ad R L) x = 0
⊢ x = 0

Tactic:
rwa [← LieHom.mem_ker, ad_ker_eq_center, LieAlgebra.center_eq_bot, LieSubmodule.mem_bot] at h

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
⊢ 1 ≤ k

Tactic:
exact Order.one_le_iff_pos.mpr hk

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

Goal state before:
pp: case mem
ι : 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 u : L
hu : u ∈ range b.e ∪ range b.f
⊢ u ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
rcases (mem_union _ _ _).mpr hu with hu | hu
    · exact LieSubmodule.mem_sup_right <| subset_lieSpan hu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| subset_lieSpan hu

Goal state after:
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✝⁵ : Free R M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
this :
  (trace R ↥(genWeightSpace M χ))
      (((toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id) ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y -
        ((toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id) ∘ₗ (χ y • LinearMap.id)) =
    0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)

Tactic:
LinearMap.sub_comp,

Goal state after:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : Free R M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
this :
  (trace R ↥(genWeightSpace M χ))
      ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y -
          (χ x • LinearMap.id) ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y -
        ((toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id) ∘ₗ (χ y • LinearMap.id)) =
    0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)
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✝⁵ : Free R M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
this :
  (trace R ↥(genWeightSpace M χ))
      ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y -
          (χ x • LinearMap.id) ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y -
        ((toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id) ∘ₗ (χ y • LinearMap.id)) =
    0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)

Tactic:
LinearMap.sub_comp,

Goal state after:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : Free R M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
this :
  (trace R ↥(genWeightSpace M χ))
      ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y -
          (χ x • LinearMap.id) ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y -
        ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (χ y • LinearMap.id) - (χ x • LinearMap.id) ∘ₗ (χ y • LinearMap.id))) =
    0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 - h₁ + h₂

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

Goal state before:
pp: case refine_1
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α : ¬α.IsZero
x : ↥H
hx : x ∈ (traceForm K (↥H) L).orthogonal (K ∙ coroot α)
⊢ x ∈ Weight.ker

Tactic:
simp only [LinearMap.BilinForm.mem_orthogonal_iff] at hx

Goal state after:
case refine_1
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α : ¬α.IsZero
x : ↥H
hx : ∀ n ∈ K ∙ coroot α, ((traceForm K (↥H) L) n) x = 0
⊢ x ∈ Weight.ker
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:
rw [Matrix.nondegenerate_iff_det_ne_zero, ← RingHom.map_det]

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) b.A.det ≠ 0
Module: Mathlib.Algebra.Lie.Basis.Basic

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

Tactic:
obtain ⟨j, rfl⟩ := hu

Goal state after:
case mem
ι : 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
j : ι
hx : b.h j ∈ H
⊢ (b.baseSupp i) ⟨b.h j, hx⟩ • b.e i = ⁅b.h j, b.e i⁆
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case add
ι : 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 u v : L
hu : u ∈ H
hv : v ∈ H
hu' : ∀ (hx : u ∈ H), (b.baseSupp i) ⟨u, hx⟩ • b.e i = ⁅u, b.e i⁆
hv' : ∀ (hx : v ∈ H), (b.baseSupp i) ⟨v, hx⟩ • b.e i = ⁅v, b.e i⁆
hx : u + v ∈ H
⊢ (b.baseSupp i) (⟨u, hu⟩ + ⟨v, hv⟩) • b.e i = ⁅u + v, b.e i⁆

Tactic:
simp only [map_add, add_smul, add_lie] at hu' hv' ⊢

Goal state after:
case add
ι : 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 u v : L
hu : u ∈ H
hv : v ∈ H
hu' : ∀ (hx : u ∈ H), (b.baseSupp i) ⟨u, hx⟩ • b.e i = ⁅u, b.e i⁆
hv' : ∀ (hx : v ∈ H), (b.baseSupp i) ⟨v, hx⟩ • b.e i = ⁅v, b.e i⁆
hx : u + v ∈ H
⊢ (b.baseSupp i) ⟨u, hu⟩ • b.e i + (b.baseSupp i) ⟨v, hv⟩ • b.e i = ⁅u, b.e i⁆ + ⁅v, b.e i⁆
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
by
  simpa [sub_eq_add_neg, add_comm] using U_neg R (n + 2)

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

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

Tactic:
simp [U_eval_zero, hn]

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

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

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

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 l : ι
x y : R
h : P.root k = x • P.root i + y • P.root l
⊢ P.pairing k j = x • P.pairing i j + y • P.pairing l j

Tactic:
simp only [← root_coroot_eq_pairing, h, map_add, map_smul, LinearMap.add_apply,
    LinearMap.smul_apply, smul_eq_mul]

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

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ 2 * T R m * T R 1 = T R (m + 1) + T R (m - 1)

Tactic:
T_add_one,

Goal state after:
case one
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ 2 * T R m * T R 1 = 2 * X * T R m - T R (m - 1) + T R (m - 1)
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯) (x (m + 1))
k : ℕ
ih : ∀ {m n : ℕ} (g : m ≤ n), n = m + (n - m) → n - m = k → x m = (factor ⋯) (x n)
m : ℕ
g : m ≤ m + k + 1
hmn : m + k + 1 - m = k + 1
⊢ m + k - m = k

Tactic:
· lia

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

Goal state before:
pp: case zero
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 • ⊤]
⊢ f 0 ≡ f 1 [SMOD ⊥ ^ 0 • ⊤]

Tactic:
rw [pow_zero, Ideal.one_eq_top, top_smul]

Goal state after:
case zero
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 • ⊤]
⊢ f 0 ≡ f 1 [SMOD ⊤]
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mp
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
⊢ ValuationRing R → ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

Tactic:
intro H x

Goal state after:
case mp
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 : K
⊢ IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case neg.inl
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 : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : (algebraMap R K) a ≠ 0
hb : (algebraMap R K) b ≠ 0
c : R
e : (algebraMap R K) c = (algebraMap R K) a / (algebraMap R K) b
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
eq_div_iff hb,

Goal state after:
case neg.inl
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 : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : (algebraMap R K) a ≠ 0
hb : (algebraMap R K) b ≠ 0
c : R
e : (algebraMap R K) c * (algebraMap R K) b = (algebraMap R K) a
⊢ ∃ c, a * c = b ∨ b * c = a
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 := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
⊢ Prime q

Tactic:
have hpq := Multiset.eq_of_mem_replicate hq

Goal state after:
case h.left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
⊢ Prime q
Module: Mathlib.RingTheory.Jacobson.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
t : ⊥.jacobson = ⊥
⊢ (map C j).jacobson = map C j

Tactic:
jacobson_eq_iff_jacobson_quotient_eq_bot

Goal state after:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
t : ⊥.jacobson = ⊥
⊢ ⊥.jacobson = ⊥
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
⊢ P.jacobson = P

Tactic:
jacobson_eq_iff_jacobson_quotient_eq_bot

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
⊢ ⊥.jacobson = ⊥