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

Goal state before:
pp: case refine_1
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
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
⊢ ⁅x, Φ⁆ = 0

Tactic:
ext y z

Goal state after:
case refine_1
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
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
y z : M
⊢ (⁅x, Φ⁆ y) z = (0 y) z
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
⊢ InjOn (fun χ ↦ genWeightSpace M χ) {χ | genWeightSpace M χ ≠ ⊥}

Tactic:
rintro χ₁ _ χ₂ hχ₂ (hχ₁₂ : genWeightSpace M χ₁ = genWeightSpace M χ₂)
  contrapose! hχ₂
  simpa [hχ₁₂] using disjoint_genWeightSpace R L M hχ₂

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

Goal state before:
pp: case mpr
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
x : V
hx : x ∈ W ⊓ ker B
⊢ x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker

Tactic:
Submodule.mem_map,

Goal state after:
case mpr
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
x : V
hx : x ∈ W ⊓ ker B
⊢ ∃ y ∈ (domRestrict B W).ker, (Submodule.subtype W) y = x
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ ↑↑J
a : L
ha : a ∈ I
b : L
hb : b ∈ sSup ({I' | IsAtom I'} \ {I})
this : ⁅b, ↑y⁆ = 0
⊢ ⁅b, ↑I.incl y⁆ ∈ Submodule.map ↑I.incl ↑J

Tactic:
erw [this]

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ ↑↑J
a : L
ha : a ∈ I
b : L
hb : b ∈ sSup ({I' | IsAtom I'} \ {I})
this : ⁅b, ↑y⁆ = 0
⊢ 0 ∈ Submodule.map ↑I.incl ↑J
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
a : α
⊢ {x ∈ m.toEnumFinset | x.1 = a} = {a} ×ˢ Finset.range (count a m)

Tactic:
by aesop

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

Goal state before:
pp: case smul
ι : 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 : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
t : R
u : L
hx✝ : u ∈ lieSpan R L (range b.e)
hu : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
⊢ ⁅t • u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
smul_lie

Goal state after:
case smul
ι : 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 : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
t : R
u : L
hx✝ : u ∈ lieSpan R L (range b.e)
hu : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
⊢ t • ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
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
x : L
D : LieDerivation R L L
⊢ D ∈ ((killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule).carrier →
    ⁅x, D⁆ ∈ ((killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule).carrier

Tactic:
hD

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : Field R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
hD : D ∈ ((killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule).carrier
⊢ ⁅x, D⁆ ∈ ((killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule).carrier
Module: Mathlib.RingTheory.Finiteness.Nilpotent

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

Tactic:
refine ⟨fun h i ↦ ?_, fun h v ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
A : Matrix ι ι R
h : ∀ (v : ι → R), ∃ n, Aᵀ ^ n *ᵥ v = 0
i : ι
⊢ ∃ n, (A ^ n).row i = 0

case refine_2
R : Type u_1
inst✝² : CommSemiring R
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
A : Matrix ι ι R
h : ∀ (i : ι), ∃ n, (A ^ n).row i = 0
v : ι → R
⊢ ∃ n, Aᵀ ^ n *ᵥ v = 0
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie
ι : 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 yc : L
hyc : yc ∈ H
yl : L
hyl : yl ∈ lieSpan R L (range b.f)
yu : L
hyu : yu ∈ lieSpan R L (range b.e)
hx✝ : yc + yl + yu ∈ lieSpan R L (range b.e ∪ range b.f)
hu : yc + yl + yu ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ H
zl : L
hzl : zl ∈ lieSpan R L (range b.f)
zu : L
hzu : zu ∈ lieSpan R L (range b.e)
hy✝ : zc + zl + zu ∈ lieSpan R L (range b.e ∪ range b.f)
hv : zc + zl + zu ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc + yl + yu, zc + zl + zu⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
simp only [lie_add, add_lie, ← add_assoc]

Goal state after:
case lie
ι : 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 yc : L
hyc : yc ∈ H
yl : L
hyl : yl ∈ lieSpan R L (range b.f)
yu : L
hyu : yu ∈ lieSpan R L (range b.e)
hx✝ : yc + yl + yu ∈ lieSpan R L (range b.e ∪ range b.f)
hu : yc + yl + yu ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ H
zl : L
hzl : zl ∈ lieSpan R L (range b.f)
zu : L
hzu : zu ∈ lieSpan R L (range b.e)
hy✝ : zc + zl + zu ∈ lieSpan R L (range b.e ∪ range b.f)
hv : zc + zl + zu ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ + ⁅yc, zu⁆ + ⁅yl, zu⁆ + ⁅yu, zu⁆ ∈
    H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
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
x : L
⊢ ⁅x, traceForm R L M⁆ = 0

Tactic:
ext y z

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
x y z : L
⊢ (⁅x, traceForm R L M⁆ y) z = (0 y) z
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
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x a b c : L
hbc : φ c = ⁅y, φ b⁆
⊢ ⁅φ b, y⁆ = -φ c

Tactic:
hbc,

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
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x a b c : L
hbc : φ c = ⁅y, φ b⁆
⊢ ⁅φ b, y⁆ = -⁅y, φ b⁆
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: case mem
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
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x a b c : L
hbc : ⁅φ b, y⁆ = -φ c
⊢ (trace R M) (φ a * ⁅φ b, y⁆) = 0

Tactic:
hbc,

Goal state after:
case mem
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
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x a b c : L
hbc : ⁅φ b, y⁆ = -φ c
⊢ (trace R M) (φ a * -φ c) = 0
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
α : Weight K (↥H) L
x : ↥H
this : ((cartanEquivDual H) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x = α x
⊢ 2 •
      ((α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ •
          (traceForm K (↥H) L) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))
        x =
    2 • (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ • α x

Tactic:
LinearMap.smul_apply

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
α : Weight K (↥H) L
x : ↥H
this : ((cartanEquivDual H) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x = α x
⊢ 2 •
      (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ •
        ((traceForm K (↥H) L) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x =
    2 • (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ • α x
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
α : Weight K (↥H) L
⊢ (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) ∈ corootSpace ⇑α

Tactic:
by
  obtain ⟨e : L, he₀ : e ≠ 0, he : ∀ x, ⁅x, e⁆ = α x • e⟩ := exists_forall_lie_eq_smul K H L α
  have heα : e ∈ rootSpace H α := (mem_genWeightSpace L α e).mpr fun x ↦ ⟨1, by simp [← he x]⟩
  obtain ⟨f, hfα, hf⟩ : ∃ f ∈ rootSpace H (-α), killingForm K L e f ≠ 0 := by
    contrapose! he₀
    simpa using mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg K L H heα he₀
  suffices ⁅e, f⁆ = killingForm K L e f • ((cartanEquivDual H).symm α : L) from
    (mem_corootSpace α).mpr <| Submodule.subset_span ⟨(killingForm K L e f)⁻¹ • e,
      Submodule.smul_mem _ _ heα, f, hfα, by simpa [inv_smul_eq_iff₀ hf]⟩
  exact lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux heα hfα he

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
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
    change b.baseSupp i (b.h' j) • _ = _
    simp [b.lie_h_e, Int.cast_smul_eq_zsmul]

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

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

Tactic:
smul_lie

Goal state after:
case smul
ι : 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
t : R
u : L
hu : u ∈ H
hv' : ∀ (hx : u ∈ H), (b.baseSupp i) ⟨u, hx⟩ • b.e i = ⁅u, b.e i⁆
hx : t • u ∈ H
⊢ t • ⁅u, b.e i⁆ = t • ⁅u, b.e i⁆
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.toLinearMap (P.root i - (P.root i + P.root i))) (P.coroot j) = -P.pairing i j

Tactic:
sub_add_cancel_left,

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 : ι
⊢ (P.toLinearMap (-P.root i)) (P.coroot j) = -P.pairing i j
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.coroot j - (P.coroot j + P.coroot j)) = -P.pairing i j

Tactic:
sub_add_cancel_left,

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 : ι
⊢ (P.root' i) (-P.coroot j) = -P.pairing i j
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
have h₁ := congr_arg derivative <| T_eq_X_mul_T_sub_pol_U R n
  simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow,
    T_derivative_eq_U, C_eq_natCast] at h₁
  have h₂ := T_eq_U_sub_X_mul_U R (n + 1)
  linear_combination (norm := (push_cast; ring_nf))
    h₁ + (n + 2) * h₂

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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
this : num A r ∣ p.coeff 0 * ↑(den A r) ^ (p.natDegree - 0)
inst : (a : Prop) → Decidable a
⊢ num A r ∣ p.coeff 0

Tactic:
by_cases hr : num A r = 0

Goal state after:
case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : (aeval r) p = 0
this : num A r ∣ p.coeff 0 * ↑(den A r) ^ (p.natDegree - 0)
inst : (a : Prop) → Decidable a
hr : num A r = 0
⊢ num A r ∣ p.coeff 0

case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : (aeval r) p = 0
this : num A r ∣ p.coeff 0 * ↑(den A r) ^ (p.natDegree - 0)
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
⊢ num A r ∣ p.coeff 0
Module: Mathlib.RingTheory.Polynomial.RationalRoot

Goal state before:
pp: case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : (aeval r) p = 0
this : num A r ∣ p.coeff 0 * ↑(den A r) ^ (p.natDegree - 0)
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
q : A
⊢ q ∣ num A r → q ∣ ↑(den A r) ^ (p.natDegree - 0) → ¬Prime q

Tactic:
dvd_num

Goal state after:
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : (aeval r) p = 0
this : num A r ∣ p.coeff 0 * ↑(den A r) ^ (p.natDegree - 0)
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
q : A
dvd_num : q ∣ num A r
⊢ q ∣ ↑(den A r) ^ (p.natDegree - 0) → ¬Prime q
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
this : (p.compl₁₂ (span L (Set.range ⇑i)).subtype (span L (Set.range ⇑j)).subtype).IsPerfPair
⊢ span L ↑(Submodule.inclusionSpan L j.range).range = ⊤

Tactic:
exact (LinearMap.range j).span_range_inclusionSpan L

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
tfae_3_to_5 : IsArtinian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
x✝ : ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
s : Set (Submodule R M)
fin : s.Finite
left✝ : sSupIndep s
sSup_eq_top : sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ IsNoetherian R M ∧ IsArtinian R M

Tactic:
rw [← isNoetherian_top_iff, ← Submodule.topEquiv.isArtinian_iff,
      ← sSup_eq_top, sSup_eq_iSup, ← iSup_subtype'']

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
x✝ : ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
s : Set (Submodule R M)
fin : s.Finite
left✝ : sSupIndep s
sSup_eq_top : sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ IsNoetherian R ↥(⨆ i, ↑i) ∧ IsArtinian R ↥(⨆ i, ↑i)
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
tfae_3_to_5 : IsArtinian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
x✝ : ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
s : Set (Submodule R M)
fin : s.Finite
left✝ : sSupIndep s
sSup_eq_top : sSup s = ⊤
simple : ∀ (x : ↑s), IsSimpleModule R ↥↑x
this : Finite ↑s
⊢ IsNoetherian R ↥(⨆ i, ↑i) ∧ IsArtinian R ↥(⨆ i, ↑i)

Tactic:
exact ⟨isNoetherian_iSup, isArtinian_iSup⟩

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : FiniteDimensionalOrder (Submodule R M)
⊢ IsFiniteLength R M

Tactic:
isFiniteLength_iff_isNoetherian_isArtinian,

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : FiniteDimensionalOrder (Submodule R M)
⊢ IsNoetherian R M ∧ IsArtinian R M
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
p : Submodule R M
h : p ≠ ⊥
⊢ ↑(Order.coheight p) < Order.krullDim (Submodule R M)

Tactic:
← Order.coheight_bot_eq_krullDim,

Goal state after:
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
p : Submodule R M
h : p ≠ ⊥
⊢ ↑(Order.coheight p) < ↑(Order.coheight ⊥)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x : ValueGroup A K
⊢ ∀ (a b : K), (MulAction.orbitRel Aˣ K) a b → Quotient.mk'' a⁻¹ = Quotient.mk'' b⁻¹

Tactic:
by
        rintro _ a ⟨b, rfl⟩
        apply Quotient.sound'
        use b⁻¹
        dsimp
        rw [Units.smul_def, Units.smul_def, Algebra.smul_def, Algebra.smul_def, mul_inv,
          map_units_inv]

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

Goal state before:
pp: case h
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
e f : A
hf : (algebraMap A K) (f * e) * b = b
hb : ¬b = 0
⊢ 1 = f * e

Tactic:
nth_rw 2 [← one_mul b] at hf

Goal state after:
case h
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
e f : A
hf : (algebraMap A K) (f * e) * b = 1 * b
hb : ¬b = 0
⊢ 1 = f * e
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 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✝ : ValueGroup A K
a : K
ha : ¬Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≤ 0
b✝ : ValueGroup A K
b : K
c✝ : ValueGroup A K
d : A
⊢ d • b = (algebraMap A K) d * b

Tactic:
by simp [Algebra.smul_def]

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

Goal state before:
pp: Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
x : ↥v.integer
hx : x ∈ I
⊢ v.leIdeal (v ↑x) ≤ I

Tactic:
by
  rcases eq_or_ne x 0 with rfl | hx0
  · simp
  intro y hy
  have : v ((y : K) / x) ≤ 1 := by simpa using div_le_one_of_le₀ hy zero_le
  convert! I.smul_mem ⟨_, this⟩ hx using 1
  simp [Subtype.ext_iff, div_mul_cancel₀ _ (ZeroMemClass.coe_eq_zero.not.mpr hx0)]

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ ^ (1 + n + 1))
H : 1 < 1 + n + 1
⊢ Associated p ϖ

Tactic:
rw [pow_succ'] at this

Goal state after:
case inr.inr
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
⊢ Associated p ϖ
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 : 𝒪
ha : x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
h0 : a = 0
⊢ x * (algebraMap 𝒪 K) ↑(0, 1).2 = (algebraMap 𝒪 K) (0, 1).1

Tactic:
simpa [h0, eq_comm] using ha

Goal state after: