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
hI : IsAtom I
⊢ (Φ.restrict (LieIdeal.toLieSubalgebra K L I).toSubmodule).Nondegenerate

Tactic:
rw [LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal hΦ_refl]

Goal state after:
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 : IsAtom I
⊢ IsCompl (LieIdeal.toLieSubalgebra K L I).toSubmodule (Φ.orthogonal (LieIdeal.toLieSubalgebra K L I).toSubmodule)
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 : IsAtom I
⊢ (Φ.restrict (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule).Nondegenerate

Tactic:
rw [LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal hΦ_refl]

Goal state after:
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 : IsAtom I
⊢ IsCompl (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule
    (Φ.orthogonal (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule)
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
this : W ⊓ B.orthogonal W = ⊥
⊢ finrank K V ≤ finrank K ↥(W ⊔ B.orthogonal W) + 0

Tactic:
← finrank_bot K V,

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
this : W ⊓ B.orthogonal W = ⊥
⊢ finrank K V ≤ finrank K ↥(W ⊔ B.orthogonal W) + finrank K ↥⊥
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
⊢ (∀ (I : LieIdeal R L), IsSolvable ↥I → I = ⊥) ↔ ∀ (I : LieIdeal R L), IsLieAbelian ↥I → I = ⊥

Tactic:
constructor <;> intro h₁ I h₂

Goal state after:
case mp
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsSolvable ↥I → I = ⊥
I : LieIdeal R L
h₂ : IsLieAbelian ↥I
⊢ I = ⊥

case mpr
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian ↥I → I = ⊥
I : LieIdeal R L
h₂ : IsSolvable ↥I
⊢ I = ⊥
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 = ⊥
this : W ⊔ B.orthogonal W = ⊤
⊢ W = ⊤

Tactic:
rwa [b₃, sup_bot_eq] at this

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

Goal state before:
pp: case neg
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ Classical.choose ⋯ ∣ f

Tactic:
exact (Classical.choose_spec <| WfDvdMonoid.exists_irreducible_factor hf1 hf2).2

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

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) *
      map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠
    0
⊢ Algebra.adjoin K
      ↑((X -
                map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
                  (C (AdjoinRoot.root f.factor))).roots +
            (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
                f.removeFactor).roots).toFinset =
    ⊤

Tactic:
map_C,

Goal state after:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) *
      map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠
    0
⊢ Algebra.adjoin K
      ↑((X -
                C
                  ((algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
                    (AdjoinRoot.root f.factor))).roots +
            (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
                f.removeFactor).roots).toFinset =
    ⊤
Module: Mathlib.LinearAlgebra.PID

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ p
hf' : ∀ x ∈ p, f x ∈ p
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN) (f.restrict hf')
B : Matrix ι ι R := (toMatrix snf.bM snf.bM) f
i : ι
hi : B i i ≠ 0
⊢ i ∈ Set.range ⇑snf.f

Tactic:
contrapose hi; exact snf.repr_eq_zero_of_notMem_range ⟨_, (hf _)⟩ hi

Goal state after:
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 : ℕ
⊢ (map (↑(toSplittingField s)) (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f) -
          ∏ x, (X - map (↑(toSplittingField s)) (C (MvPolynomial.X ⟨f, x⟩)))).coeff
      n =
    0

Tactic:
map_C,

Goal state after:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map (↑(toSplittingField s)) (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f) -
          ∏ x, (X - C (↑(toSplittingField s) (MvPolynomial.X ⟨f, x⟩)))).coeff
      n =
    0
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: case hL
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : LieAlgebra K L
inst✝² : IsKilling R L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
h₁ : IsAtom I
h₂ : IsLieAbelian ↥I
⊢ False

Tactic:
exact h₁.1 <| IsKilling.ideal_eq_bot_of_isLieAbelian I

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

Goal state before:
pp: case mem.inl
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
H : LieSubalgebra R L
α χ : ↥H → R
p : ℤ
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hq : genWeightSpace M ((k + 1) • α + χ) = ⊥
hk : k ∈ Ioo p (k + 1)
hz : z ∈ genWeightSpace M (↑⟨k, hk⟩ • α + χ)
⊢ genWeightSpace M ((k + 1) • α + χ) ≤ ⨆ k_1 ∈ Ioo p (k + 1), genWeightSpace M (k_1 • α + χ)

Tactic:
simp only [hq, bot_le]

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

Goal state before:
pp: case hx
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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ ⁅e, f⁆ - ((killingForm K L) e) f • ↑α' ∈ H

Tactic:
refine sub_mem ?_ (H.smul_mem _ α'.property)

Goal state after:
case hx
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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ ⁅e, f⁆ ∈ H
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α : ¬α.IsZero
⊢ IsCompl Weight.ker ↑(corootSpace ⇑α)

Tactic:
apply Module.Dual.isCompl_ker_of_disjoint_of_ne_bot (by simp_all)
      (disjoint_ker_weight_corootSpace α)

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
⊢ (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule ≠ ⊥
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 j : ι
e : ↥H.toSubmodule ≃ₗ[R] ↥(Submodule.span R (range b.h)) :=
  LinearEquiv.ofEq H.toSubmodule (Submodule.span R (range b.h)) ⋯
f : ι → R := fun k ↦ b.A i k • ((Basis.span ⋯).repr (e (b.h' j))) k
⊢ ∑ k, f k = ↑(b.A i j)

Tactic:
have : f = fun k ↦ if j = k then (b.A i k : R) else 0 := by
    have : (Basis.span b.linInd).repr (e <| b.h' j) = .single j 1 := Basis.span_repr_eq_single _ _
    ext k
    simp [f, this, Finsupp.single_apply]

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 j : ι
e : ↥H.toSubmodule ≃ₗ[R] ↥(Submodule.span R (range b.h)) :=
  LinearEquiv.ofEq H.toSubmodule (Submodule.span R (range b.h)) ⋯
f : ι → R := fun k ↦ b.A i k • ((Basis.span ⋯).repr (e (b.h' j))) k
this : f = fun k ↦ if j = k then ↑(b.A i k) else 0
⊢ ∑ k, f k = ↑(b.A i 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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x : L
i : ι
y : L
hy : y ∈ H
⊢ (((LieModule.toEnd R L L) y - (∑ x, ↑(Pi.single i 1 x) * (b.baseSupp x) ⟨y, hy⟩) • 1) ^ 1) (b.e i) = 0

Tactic:
simp [Pi.single_apply]

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

Goal state before:
pp: case h
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
χ : ↑s
i : ↥H
⊢ ↑((fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) ⟨Exists.choose ⋯, ⋯⟩) i = ↑χ i

Tactic:
simpa using congr_fun χ.property.choose_spec.2.symm i

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

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

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

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

Goal state before:
pp: case refine_1.refine_3
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 (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ c₃ • ⁅e, f⁆ ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α

Tactic:
suffices ∃ y ∈ corootSpace α, H.subtype y = c₃ • h' from
        mem_sup_right <| by simpa [ht.lie_e_f, -Subtype.exists]

Goal state after:
case refine_1.refine_3
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 (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ ∃ y ∈ corootSpace ⇑α, H.subtype y = c₃ • 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 k : ι
hij : P.reflectionPerm i = P.reflectionPerm j
⊢ P.pairing i k • P.coroot i = P.pairing j k • P.coroot j

Tactic:
by
  have h : P.coreflection i (P.coroot k) = P.coreflection j (P.coroot k) := by
    simp only [← coroot_reflectionPerm, hij]
  simpa only [coreflection_apply_coroot, sub_right_inj] using 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 ι
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
hUV : Disjoint sU sV
⊢ iSupIndep ![rootSpace H 0, U, V]

Tactic:
have key := LieModule.iSupIndep_genWeightSpace R H L

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
hUV : Disjoint sU sV
key : iSupIndep fun χ ↦ LieModule.genWeightSpace L χ
⊢ iSupIndep ![rootSpace H 0, U, V]
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
i : Fin s.length
ih : IsFiniteLength R ↥(s.toFun i.castSucc)
cov : (s.toFun i.castSucc, s.toFun i.succ) ∈ {(x, y) | JordanHolderLattice.IsMaximal x y} := s.step i
this✝ : IsSimpleModule R (↥(s.toFun i.succ) ⧸ Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc))
this : ↥(Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc)) ≃ₗ[R] ↥(s.toFun i.castSucc)
⊢ IsFiniteLength R ↥(s.toFun i.succ)

Tactic:
exact .of_simple_quotient (this.symm.isFiniteLength ih)

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 : IsNoetherian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M,
      ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE

Tactic:
tfae_have 3 → 5 := fun _ ↦ ⟨s, WellFoundedLT.finite_of_sSupIndep hs.1, hs⟩

Goal state after:
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 : IsNoetherian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_3_to_5 : IsArtinian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M,
      ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE
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) ↔ FiniteDimensionalOrder (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 inl
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
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ Quotient.mk'' ((algebraMap A K) xa / (algebraMap A K) ya + (algebraMap A K) xb / (algebraMap A K) yb) ≤
    max (Quotient.mk'' ((algebraMap A K) xa / (algebraMap A K) ya))
      (Quotient.mk'' ((algebraMap A K) xb / (algebraMap A K) yb))

pp: case 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
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ Quotient.mk'' ((algebraMap A K) xa / (algebraMap A K) ya + (algebraMap A K) xb / (algebraMap A K) yb) ≤
    max (Quotient.mk'' ((algebraMap A K) xa / (algebraMap A K) ya))
      (Quotient.mk'' ((algebraMap A K) xb / (algebraMap A K) yb))

Tactic:
· apply le_trans _ (le_max_left _ _)
      use c + 1
      rw [Algebra.smul_def]
      field_simp
      simp only [← map_mul, ← map_add]
      congr 1; linear_combination h

Goal state after:
case 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
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ Quotient.mk'' ((algebraMap A K) xa / (algebraMap A K) ya + (algebraMap A K) xb / (algebraMap A K) yb) ≤
    max (Quotient.mk'' ((algebraMap A K) xa / (algebraMap A K) ya))
      (Quotient.mk'' ((algebraMap A K) xb / (algebraMap A K) yb))
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case inr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : ValuationRing R
x y : R
h : Ideal.span {y} ≤ Ideal.span {x}
⊢ Submodule.IsPrincipal (max (Ideal.span {x}) (Ideal.span {y}))

Tactic:
sup_eq_left.mpr h

Goal state after:
case inr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : ValuationRing R
x y : R
h : Ideal.span {y} ≤ Ideal.span {x}
⊢ Submodule.IsPrincipal (Ideal.span {x})
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
y : R
inst✝² : Algebra R S
inst✝¹ : Away y S
inst✝ : IsJacobsonRing R
I : Ideal R
hI : I.IsMaximal
hy : y ∉ I
⊢ (Ideal.map (algebraMap R S) I).IsMaximal

Tactic:
rw [isMaximal_iff_isMaximal_disjoint S y, under_map_of_isPrime_disjoint (powers y) S hI.isPrime]
  · exact ⟨hI, hy⟩
  · rwa [disjoint_powers_iff_notMem_of_isPrime]

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

Goal state before:
pp: case coe
R✝ : Type u
inst✝⁵ : CommRing R✝
inst✝⁴ : IsDomain R✝
inst✝³ : IsDiscreteValuationRing R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
k : ℕ
⊢ OrderDual.toDual ((addVal R) (generator (ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) ↑k))) = OrderDual.toDual ↑k

Tactic:
obtain ⟨ϖ, hϖ⟩ := exists_irreducible R
      rw [OrderDual.toDual_inj, ENat.recTopCoe_natCast, hϖ.maximalIdeal_eq,
        span_singleton_pow, ← hϖ.addVal_pow k, addVal_eq_iff_associated]
      exact associated_generator_span_self (ϖ ^ k)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
h' : ∀ a ∈ maximalIdeal R, a = 0
⊢ False

Tactic:
apply ne_bot

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
h' : ∀ a ∈ maximalIdeal R, a = 0
⊢ maximalIdeal R = ⊥