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

Goal state before:
pp: case refine_2
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
x : L
y z : M
h : (⁅x, Φ⁆ y) z = (0 y) z
⊢ (Φ ⁅x, y⁆) z = -(Φ y) ⁅x, z⁆

Tactic:
simp only [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply,
      LinearMap.zero_apply, sub_eq_zero] at h

Goal state after:
case refine_2
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
x : L
y z : M
h : -(Φ y) ⁅x, z⁆ = (Φ ⁅x, y⁆) z
⊢ (Φ ⁅x, y⁆) z = -(Φ y) ⁅x, z⁆
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
hB : B.IsRefl
⊢ B.orthogonal ⊤ = ker B

Tactic:
by
  ext; simp [LinearMap.ext_iff, hB.eq_iff]

Goal state after:
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
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
⊢ I ≤ sSup {J | IsAtom J ∧ J ≤ I}

Tactic:
refine this.trans ?_
    apply sup_le
    · exact le_sSup ⟨hJ, hJI⟩
    rw [← atomistic (J' ⊓ I)]
    apply sSup_le_sSup
    simp only [le_inf_iff, Set.ofPred_subset_ofPred, and_imp]
    tauto

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 = ⊤
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c

Tactic:
obtain ⟨Ta, hTa, rfl⟩ := hS.atomistic a (h ▸ le_top)

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
b c : α
Ta : Set α
hTa : Ta ⊆ S
⊢ (sSup Ta ⊔ b) ⊓ (sSup Ta ⊔ c) ≤ sSup Ta ⊔ b ⊓ c
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
x y : L
m : ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x, ⁅y, m⁆ - χ y • m⁆ - χ x • (⁅y, m⁆ - χ y • m) =
    ⁅⁅x, y⁆, m⁆ - χ ⁅x, y⁆ • m + (⁅y, ⁅x, m⁆ - χ x • m⁆ - χ y • (⁅x, m⁆ - χ x • m))

Tactic:
nontriviality shiftedGenWeightSpace R L M χ
    simp only [lie_sub, lie_smul, lie_lie, LinearWeights.map_lie χ (aux R L M χ), zero_smul,
      sub_zero, smul_sub, smul_comm (χ x)]
    abel

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

Goal state before:
pp: case inr
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
⊢ ⁅j, ⟨y, hy⟩⁆ = 0

Tactic:
suffices ⁅(j : L), z⁆ = 0 ∧ ⁅(j : L), y + z⁆ = 0 by
    rw [lie_add, this.1, add_zero] at this
    ext
    exact this.2

Goal state after:
case inr
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
⊢ ⁅↑j, z⁆ = 0 ∧ ⁅↑j, y + z⁆ = 0
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
z : AlgebraicClosure k
⊢ IsIntegral k z

Tactic:
let ⟨p, hp⟩ := Ideal.Quotient.mk_surjective z
      rw [← hp]
      induction p using MvPolynomial.induction_on generalizing z with
        | C => exact isIntegral_algebraMap
        | add _ _ ha hb => exact (ha _ rfl).add (hb _ rfl)
        | mul_X p fi ih =>
          rw [map_mul]
          refine (ih _ rfl).mul ⟨_, fi.1.2, ?_⟩
          simp_rw [← eval_map, Monics.map_eq_prod, eval_prod, Polynomial.map_sub, eval_sub]
          apply Finset.prod_eq_zero (Finset.mem_univ fi.2)
          rw [map_C]
          -- The `erw` is needed here because the `R` in `eval` is `AlgebraicClosure k`,
          -- but this has been unfolded in the arguments of `eval`.
          erw [eval_C]
          simp

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
k : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ lowerCentralSeries R L L 1
⊢ (trace R M) (φ x) = 0

Tactic:
replace hx : x ∈ Submodule.span R {m | ∃ u v : L, ⁅u, v⁆ = m} := by
    rw [lowerCentralSeries_succ, ← LieSubmodule.mem_toSubmodule,
      LieSubmodule.lieIdeal_oper_eq_linear_span'] at hx
    simpa using hx

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
k : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
⊢ (trace R M) (φ x) = 0
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
this :
  ∑ χ with χ.IsZero, finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ) =
    0
⊢ traceForm K L M =
    ∑ χ with χ.IsNonZero,
      finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ)

Tactic:
traceForm_eq_sum_finrank_nsmul,

Goal state after:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
this :
  ∑ χ with χ.IsZero, finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ) =
    0
⊢ ∑ χ, finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ) =
    ∑ χ with χ.IsNonZero,
      finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ)
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✝ : PerfectField K
α : Weight K (↥H) L
⊢ ↑(corootSpace ⇑α) ≤ K ∙ (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)

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✝ : PerfectField K
α : Weight K (↥H) L
⊢ K ∙ (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) ≤ ↑(corootSpace ⇑α)

Tactic:
· intro ⟨x, hx⟩ hx'
    have : {⁅y, z⁆ | (y ∈ rootSpace H α) (z ∈ rootSpace H (-α))} ⊆
        K ∙ ((cartanEquivDual H).symm α : L) := by
      rintro - ⟨e, heα, f, hfα, rfl⟩
      rw [lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg heα hfα, SetLike.mem_coe,
        Submodule.mem_span_singleton]
      exact ⟨killingForm K L e f, rfl⟩
    simp only [LieSubmodule.mem_toSubmodule, mem_corootSpace] at hx'
    replace this := Submodule.span_mono this hx'
    rw [Submodule.span_span] at this
    rw [Submodule.mem_span_singleton] at this ⊢
    obtain ⟨t, rfl⟩ := this
    solve_by_elim

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✝ : PerfectField K
α : Weight K (↥H) L
⊢ K ∙ (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) ≤ ↑(corootSpace ⇑α)
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
I : LieIdeal K L
⊢ LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H ⇑α ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : rootSpace H ⇑↑α ≤ LieSubmodule.restr I H), rootSpace H ⇑↑α

Tactic:
refine sup_le_sup_left (iSup₂_le fun α hα ↦ ?_) _

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
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsNonZero
⊢ LieSubmodule.restr I H ⊓ rootSpace H ⇑α ≤ ⨆ α, ⨆ (_ : rootSpace H ⇑↑α ≤ LieSubmodule.restr I H), rootSpace H ⇑↑α
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.root i = -P.root j ↔ i = (P.reflectionPerm j) j

Tactic:
refine ⟨fun h ↦ P.root.injective ?_, fun h ↦ by simp [h]⟩

Goal state after:
ι : 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 : ι
h : P.root i = -P.root j
⊢ P.root i = P.root ((P.reflectionPerm j) j)
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: 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
⊢ (P.toLinearMap x) (P.coroot i) • 2 • P.root i = (P.toLinearMap x) (P.coroot i) • 2 • P.root i

Tactic:
← Nat.cast_smul_eq_nsmul R,

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
⊢ (P.toLinearMap x) (P.coroot i) • ↑2 • P.root i = (P.toLinearMap x) (P.coroot i) • 2 • P.root i
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
T_derivative_eq_U

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : T R (n - 1 + 2) = X * U R (n - 1 + 1) - U R (n - 1)
⊢ (↑n + 1) * ↑n * T R (n + 1) = ↑n * X * (↑(n + 1) * U R (n + 1 - 1)) - (↑n + 1) * (↑n * U R (n - 1))
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: 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
⊢ 2 • (P.toLinearMap x) (P.coroot j) • P.root j = 2 • (P.toLinearMap x) (P.coroot j) • P.root j

Tactic:
← Nat.cast_smul_eq_nsmul R,

Goal state after:
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
⊢ 2 • (P.toLinearMap x) (P.coroot j) • P.root j = ↑2 • (P.toLinearMap x) (P.coroot j) • P.root j
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
n : ι → ℕ
hn : n ≠ 0
m : ι → ℕ
hm : m ≠ 0
hf : ⇑(∑ i, m i • b.baseSupp i) ∈ sU
hg : ⇑(∑ i, m i • b.baseSupp i) ∈ sV
hn' : ⇑(∑ i, m i • b.baseSupp i) = -⇑(∑ i, n i • b.baseSupp i)
⊢ ∑ i, (Nat.cast ∘ (m + n)) i • b.baseSupp i = 0

Tactic:
rw [eq_neg_iff_add_eq_zero] at hn'

Goal state after:
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
n : ι → ℕ
hn : n ≠ 0
m : ι → ℕ
hm : m ≠ 0
hf : ⇑(∑ i, m i • b.baseSupp i) ∈ sU
hg : ⇑(∑ i, m i • b.baseSupp i) ∈ sV
hn' : ⇑(∑ i, m i • b.baseSupp i) + ⇑(∑ i, n i • b.baseSupp i) = 0
⊢ ∑ i, (Nat.cast ∘ (m + n)) i • b.baseSupp i = 0
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
h : IsFiniteLength R M
⊢ IsFiniteLength R N

Tactic:
induction h generalizing N with
  | of_subsingleton =>
    have := e.symm.toEquiv.subsingleton; exact .of_subsingleton
  | @of_simple_quotient M _ _ S _ _ ih =>
    have : IsSimpleModule R (N ⧸ Submodule.map (e : M →ₗ[R] N) S) :=
      IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm
    exact .of_simple_quotient (ih <| e.submoduleMap S)

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: 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
t : LTSeries (Submodule R M)
t' : RelSeries {(a, b) | a ⋖ b}
i : Fin (t.length + 1) ↪ Fin (t'.length + 1)
hi : t'.toFun ∘ ⇑i = t.toFun
ht₁ : t'.head = ⊥
ht₂ : t'.last = ⊤
⊢ ↑t.length ≤ ↑s.length

Tactic:
have := (s.jordan_holder t' (h₁.trans ht₁.symm) (h₂.trans ht₂.symm)).choose

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
t : LTSeries (Submodule R M)
t' : RelSeries {(a, b) | a ⋖ b}
i : Fin (t.length + 1) ↪ Fin (t'.length + 1)
hi : t'.toFun ∘ ⇑i = t.toFun
ht₁ : t'.head = ⊥
ht₂ : t'.last = ⊤
this : Fin s.length ≃ Fin t'.length
⊢ ↑t.length ≤ ↑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
⊢ length R M ≠ ⊤ ↔ IsFiniteLength R M

Tactic:
by
  refine ⟨fun h ↦ ?_, fun H ↦ ?_⟩
  · rw [length_ne_top_iff_finiteDimensionalOrder] at h
    rw [isFiniteLength_iff_isNoetherian_isArtinian, isNoetherian_iff, isArtinian_iff]
    let R : SetRel (Submodule R M) (Submodule R M) :=
      {(N₁, N₂) : Submodule R M × Submodule R M | N₁ < N₂}
    change R.inv.IsWellFounded ∧ R.IsWellFounded
    exact ⟨.of_finiteDimensional R.inv, .of_finiteDimensional R⟩
  · obtain ⟨s, hs₁, hs₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp H
    rw [← length_compositionSeries s hs₁ hs₂]
    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
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
⊢ FiniteDimensionalOrder (Submodule R M)

Tactic:
by
  rw [Module.finiteDimensionalOrder_submodule_iff, isFiniteLength_iff_isNoetherian_isArtinian]
  tauto

Goal state after:
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
⊢ (fun x1 x2 ↦ x2 < x1) ↪r DvdNotUnit

Tactic:
have : ∀ I : { J : Ideal R // J.FG }, ∃ x : R, (I : Ideal R) = Ideal.span {x} :=
      fun ⟨I, hI⟩ => (IsBezout.isPrincipal_of_FG I hI).1

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
this : ∀ (I : { J // J.FG }), ∃ x, ↑I = Ideal.span {x}
⊢ (fun x1 x2 ↦ x2 < x1) ↪r DvdNotUnit
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case h_option
R : Type u_1
inst✝ : Ring R
⊢ ∀ (α : Type u_5) [inst : Fintype α],
    (∀ (M : α → Type u_6) [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)],
        length R ((i : α) → M i) = ∑ i, length R (M i)) →
      ∀ (M : Option α → Type u_6) [inst_1 : (i : Option α) → AddCommGroup (M i)]
        [inst_2 : (i : Option α) → Module R (M i)], length R ((i : Option α) → M i) = ∑ i, length R (M i)

Tactic:
· intro ι _ IH M _ _
    rw [(LinearEquiv.piOptionEquivProd _).length_eq, Module.length_prod, IH, add_comm,
      Fintype.sum_option, add_comm]

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

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

Tactic:
· rw [h]
      exact hy

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

Goal state before:
pp: case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R

Tactic:
rintro Q ⟨hQ1, hQ2⟩

Goal state after:
case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
Q : Ideal R
hQ1 : Q ≠ ⊥
hQ2 : Q.IsPrime
⊢ Q = maximalIdeal R
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 𝒪 : 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 : 𝒪
h0 : ¬a = 0
this : (algebraMap 𝒪 K) a ≠ 0
ha : x * (algebraMap 𝒪 K) a = 1
⊢ x * (algebraMap 𝒪 K) ↑(1, ⟨a, ⋯⟩).2 = (algebraMap 𝒪 K) (1, ⟨a, ⋯⟩).1

Tactic:
simpa using ha

Goal state after:
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
f : (R ⧸ j)[X]
hf : f ∈ ⊥.jacobson
⊢ f ∈ ⊥

Tactic:
have r1 : (X : (R ⧸ j)[X]) ≠ 0 := ne_of_apply_ne (coeff · 1) <| by simp

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
f : (R ⧸ j)[X]
hf : f ∈ ⊥.jacobson
r1 : X ≠ 0
⊢ f ∈ ⊥
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
⊢ IsUnit (1 + -x * y)

Tactic:
let f : ℕ → R := fun n => ∑ i ∈ range n, (x * y) ^ i

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
⊢ IsUnit (1 + -x * y)
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
⊢ (addVal R) ↑u = 0

Tactic:
addVal_def (u : R) u hϖ 0

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
⊢ ↑0 = 0

R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
⊢ ↑u = ↑u * ϖ ^ 0
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
hx : 0 < v x
⊢ v.restrict a ≠ 0

Tactic:
simpa using ha

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

Goal state before:
pp: case inl
K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : Kˣ
hx : v ↑x < 1
⊢ ∃ x, x ≠ 0 ∧ v x < 1

Tactic:
use x
    simp [hx]

Goal state after: