mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ r r' : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ WithBotTop.coe (↑pq.2 + r - 1) ≤ WithBotTop.coe (↑pq.2 + r' - 1)

Tactic:
by simp; lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
⊢ ∀ (r r' : ℤ) (pq pq' : ℤ × Fin l),
    (ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq pq' →
      ∀ (hrr' : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_41)
        (hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_43), ⟨(↑↑pq.2 - (r' - 2)).toNat, ⋯⟩ = pq'.2.castSucc

Tactic:
by
    rintro r r' ⟨a, ⟨a', _⟩⟩ ⟨b, ⟨b', _⟩⟩ ⟨h₁, h₂⟩ hrr' hr
    ext
    dsimp
    lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
⊢ WithBotTop.coe (-↑pq.2 - r + 2) ≤ WithBotTop.coe (-↑pq.2)

Tactic:
by simp; lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
⊢ WithBotTop.coe (-↑pq.2 + 1) ≤ WithBotTop.coe (-↑pq.2 + r - 1)

Tactic:
by simp; lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq pq' : ℕ × ℕ
hpq : (ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq pq'
hr : 2 ≤ r
⊢ -↑pq.1 - ↑pq.2 + 1 = -↑pq'.1 - ↑pq'.2

Tactic:
simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq
    lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ r r' : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ WithBotTop.coe (-↑pq.2 - r' + 2) ≤ WithBotTop.coe (-↑pq.2 - r + 2)

Tactic:
by simp; lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ r r' : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ WithBotTop.coe (-↑pq.2 + r - 1) ≤ WithBotTop.coe (-↑pq.2 + r' - 1)

Tactic:
by simp; lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
n : ℤ
k : ℕ
hr : 2 ≤ 2 + ↑k
p : ℤ
t : ℕ
hq : k + 1 + t < l
hn : n = (coreE₂CohomologicalFin l).deg (p, ⟨k + 1 + t, hq⟩) + 1
this : k < k + 1 + t
hpq : ∀ (a : ℤ) (b : Fin l), p + (2 + ↑k) = a → ¬↑(k + 1 + t) + (1 - (2 + ↑k)) = ↑↑b
⊢ ↑(k + 1 + t) + (1 - (2 + ↑k)) = ↑↑⟨t, ⋯⟩

Tactic:
by simp; lia

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

Goal state before:
pp: L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x y : L
m : M
⊢ ⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆

Tactic:
by rw [leibniz_lie, add_sub_cancel_right]

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
⊢ range PrimeSpectrum.asIdeal = range MaximalSpectrum.asIdeal

Tactic:
simp only [PrimeSpectrum.range_asIdeal, MaximalSpectrum.range_asIdeal,
    isPrime_iff_isMaximal]

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : q < 0
⊢ coreE₂Cohomological.i₂ (p, q) ≤ WithBotTop.coe 0

Tactic:
by simp; lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : p < 0
⊢ WithBotTop.coe (coreE₂Cohomological.deg (p, q)) < coreE₂Cohomological.i₁ (p, q)

Tactic:
by simp; lia

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (x y z : ↥L'), ⟨⁅↑x, ↑(y + z)⁆, ⋯⟩ = ⟨⁅↑x, ↑y⁆, ⋯⟩ + ⟨⁅↑x, ↑z⁆, ⋯⟩

Tactic:
by
    intros
    apply SetCoe.ext
    apply lie_add

Goal state after:
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
x y : M
hx : x ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0}
hy : y ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0}
z : L
⊢ ⁅z, x + y⁆ = 0

Tactic:
rw [lie_add, hx, hy, add_zero]

Goal state after:
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ LieSubmodule.map f ⊤ = f.range

Tactic:
ext; simp [LieSubmodule.mem_map]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : IsReduced B
n : ℕ
p : A[X]
dvd : (Polynomial.aeval x) (p ^ n) = 0
⊢ (Polynomial.aeval x) p = 0

Tactic:
map_pow

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : IsReduced B
n : ℕ
p : A[X]
dvd : (Polynomial.aeval x) p ^ n = 0
⊢ (Polynomial.aeval x) p = 0
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_3
K : Type u_4
R : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : Ring R
inst✝³ : Algebra A K
inst✝² : Algebra A R
inst✝¹ : Algebra K R
inst✝ : IsScalarTower A K R
x : R
⊢ minpoly K x ∣ map (algebraMap A K) (minpoly A x)

Tactic:
by
  refine minpoly.dvd K x ?_
  rw [aeval_map_algebraMap, minpoly.aeval]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case h
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : Ring L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ algebraMap R L = (algebraMap S L).comp (algebraMap R S)

Tactic:
← IsScalarTower.algebraMap_eq

Goal state after:
case h
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : Ring L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ algebraMap R L = algebraMap R L
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
hdvd : DvdNotUnit a (minpoly A x)
⊢ (Polynomial.aeval x) a ≠ 0

Tactic:
refine fun ha => (min A x hamonic ha).not_gt (degree_lt_degree ?_)
  obtain ⟨_, c, hu, he⟩ := hdvd
  have hcm := hamonic.of_mul_monic_left (he.subst <| monic hx)
  rw [he, hamonic.natDegree_mul hcm]
  -- TODO: port Nat.lt_add_of_zero_lt_left from lean3 core
  apply lt_add_of_pos_right
  refine (lt_of_not_ge fun h => hu ?_)
  rw [eq_C_of_natDegree_le_zero h, ← Nat.eq_zero_of_le_zero h, ← leadingCoeff, hcm.leadingCoeff,
    C_1]
  exact isUnit_one

Goal state after:
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: A : Type u_3
inst✝ : CommRing A
I : Ideal A
ι : Type u_6
s : Finset ι
x y : ι → A
hxy : ∀ i ∈ s, x i ≡ y i [SMOD I]
⊢ ∏ i ∈ s, x i ≡ ∏ i ∈ s, y i [SMOD I]

Tactic:
by
  induction s using Finset.cons_induction with
  | empty => simp [SModEq.rfl]
  | cons i s _ ih =>
    grw [Finset.prod_cons, Finset.prod_cons, hxy i (Finset.mem_cons_self i s),
      ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
⊢ (∃ f, f.degree < ↑d ∧ y = (aeval x) f) → ∃ f, f.natDegree < d ∧ y = (aeval x) f

Tactic:
rintro ⟨f, h, hy⟩

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.degree < ↑d
hy : y = (aeval x) f
⊢ ∃ f, f.natDegree < d ∧ y = (aeval x) f
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.degree < ↑d
hy : y = (aeval x) f
⊢ f.natDegree < d

Tactic:
by_cases hf : f = 0

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.degree < ↑d
hy : y = (aeval x) f
hf : f = 0
⊢ f.natDegree < d

case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.degree < ↑d
hy : y = (aeval x) f
hf : ¬f = 0
⊢ f.natDegree < d
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
⊢ (∃ f, f.natDegree < d ∧ y = (aeval x) f) → ∃ f, f.degree < ↑d ∧ y = (aeval x) f

Tactic:
rintro ⟨f, h, hy⟩

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
⊢ ∃ f, f.degree < ↑d ∧ y = (aeval x) f
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
⊢ f.degree < ↑d

Tactic:
by_cases hf : f = 0

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
hf : f = 0
⊢ f.degree < ↑d

case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
hf : ¬f = 0
⊢ f.degree < ↑d
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inl
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Subsingleton A
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) 0 = (aeval y) 0

Tactic:
map_zero,

Goal state after:
case inl
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Subsingleton A
⊢ 0 = (aeval y) 0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
K : Type u_6
inst✝² : Field K
S' : Type u_7
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
pb : PowerBasis R S
e : S ≃ₐ[R] S'
i : Fin pb.dim
⊢ e (pb.gen ^ ↑i) = e pb.gen ^ ↑i

Tactic:
map_pow

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
K : Type u_6
inst✝² : Field K
S' : Type u_7
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
pb : PowerBasis R S
e : S ≃ₐ[R] S'
i : Fin pb.dim
⊢ e pb.gen ^ ↑i = e pb.gen ^ ↑i
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
hn : n ≠ 1
H : Irreducible (X ^ n - C 0)
⊢ False

Tactic:
map_zero,

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
hn : n ≠ 1
H : Irreducible (X ^ n - 0)
⊢ False
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
hn : 0 < n
H : Irreducible (X ^ n - C 0)
this : n = 1
⊢ root (X - C 0) = 0

Tactic:
map_zero,

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
hn : 0 < n
H : Irreducible (X ^ n - C 0)
this : n = 1
⊢ root (X - 0) = 0
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: n : ℤ
⊢ (∀ (x : ℤ), x.natAbs * x.natAbs ∣ n.natAbs → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x

Tactic:
← natAbs_mul,

Goal state after:
n : ℤ
⊢ (∀ (x : ℤ), (x * x).natAbs ∣ n.natAbs → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case intro
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι : Type u_7
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
this : DecidableEq ι
val✝ : Fintype ι
⊢ ((toMatrix b b) 0).det = 0

Tactic:
map_zero,

Goal state after:
case intro
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι : Type u_7
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
this : DecidableEq ι
val✝ : Fintype ι
⊢ det 0 = 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset N
b : Basis (↥s) A N
⊢ ∃ s, Nonempty (Basis (↥s) A M)

Tactic:
exact ⟨_, ⟨(b.map e.symm).reindexFinsetRange⟩⟩

Goal state after:
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : 𝕜[X]
a : A
⊢ p ∈ annIdeal 𝕜 a ↔ annIdealGenerator 𝕜 a ∣ p

Tactic:
← Ideal.mem_span_singleton,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : 𝕜[X]
a : A
⊢ p ∈ annIdeal 𝕜 a ↔ p ∈ Ideal.span {annIdealGenerator 𝕜 a}
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Ideal.span {p} = annIdeal 𝕜 a
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p

Tactic:
rw [← span_singleton_annIdealGenerator, Ideal.span_singleton_eq_span_singleton] at p_gen

Goal state after:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_3
E' : Type u_4
inst✝³ : Field E
inst✝² : Field E'
inst✝¹ : Algebra F E
inst✝ : Algebra F E'
f : E →ₐ[F] E'
x : E
h : IsSeparable F (f x)
⊢ IsSeparable F x

Tactic:
let _ : Algebra E E' := RingHom.toAlgebra f.toRingHom

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
E' : Type u_4
inst✝³ : Field E
inst✝² : Field E'
inst✝¹ : Algebra F E
inst✝ : Algebra F E'
f : E →ₐ[F] E'
x : E
h : IsSeparable F (f x)
x✝ : Algebra E E' := f.toAlgebra
⊢ IsSeparable F x
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → ι → R
⊢ (basisFun R ι).det v = (of v).det

Tactic:
rw [Pi.basisFun_det]

Goal state after:
R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → ι → R
⊢ detRowAlternating v = (of v).det
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: K : Type u_5
inst✝ : Field K
f : K[X]
⊢ finrank K (K[X] ⧸ span {f}) = f.natDegree

Tactic:
by_cases hf : f = 0

Goal state after:
case pos
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f = 0
⊢ finrank K (K[X] ⧸ span {f}) = f.natDegree

case neg
K : Type u_5
inst✝ : Field K
f : K[X]
hf : ¬f = 0
⊢ finrank K (K[X] ⧸ span {f}) = f.natDegree
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case pos
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f = 0
⊢ finrank K (K[X] ⧸ span {f}) = f.natDegree

Tactic:
hf,

Goal state after:
case pos
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f = 0
⊢ finrank K (K[X] ⧸ span {0}) = natDegree 0
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : X ^ n ∈ annihilator R[X] (AEval R M f)
⊢ X ∈ annihilator R[X] (AEval R M f)

Tactic:
exact hs.annihilator_isRadical _ _ ⟨n, h0⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 | ∃ i, ∃ (_ : i ≤ k), (f ^ i) x = x_1}
hp₁ : p ∈ f.invtSubmodule
⊢ Module.Finite R ↥p

Tactic:
let g : ℕ → M := fun i ↦ (f ^ i) x

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 | ∃ i, ∃ (_ : i ≤ k), (f ^ i) x = x_1}
hp₁ : p ∈ f.invtSubmodule
g : ℕ → M := fun i ↦ (f ^ i) x
⊢ Module.Finite R ↥p
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
⊢ ↑(j ! * (i - j)!) ≠ 0

Tactic:
by positivity

Goal state after:
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
r₁ r₂ : S
x✝¹ : IsNilpotent (r₁ - x) ∧ (aeval r₁) P = 0
x✝ : IsNilpotent (r₂ - x) ∧ (aeval r₂) P = 0
hr₁ : IsNilpotent (r₁ - x)
hr₁' : (aeval r₁) P = 0
hr₂ : IsNilpotent (r₂ - x)
hr₂' : (aeval r₂) P = 0
u : S
hu : 0 = (aeval r₁) (derivative P) * (r₂ - r₁) + u * (r₂ - r₁) * (r₂ - r₁)
this : IsUnit ((aeval r₁) (derivative P) + u * (r₂ - r₁))
⊢ r₁ = r₂

Tactic:
← add_mul,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
r₁ r₂ : S
x✝¹ : IsNilpotent (r₁ - x) ∧ (aeval r₁) P = 0
x✝ : IsNilpotent (r₂ - x) ∧ (aeval r₂) P = 0
hr₁ : IsNilpotent (r₁ - x)
hr₁' : (aeval r₁) P = 0
hr₂ : IsNilpotent (r₂ - x)
hr₂' : (aeval r₂) P = 0
u : S
hu : 0 = ((aeval r₁) (derivative P) + u * (r₂ - r₁)) * (r₂ - r₁)
this : IsUnit ((aeval r₁) (derivative P) + u * (r₂ - r₁))
⊢ r₁ = r₂
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst✝¹⁷ : LieRing L
inst✝¹⁶ : LieAlgebra R L
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : LieRingModule L M
inst✝¹² : LieModule R L M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : LieRingModule L N
inst✝⁸ : LieModule R L N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ hasBracketAux x ∘ₗ hasBracketAux y = hasBracketAux ⁅x, y⁆ + hasBracketAux y ∘ₗ hasBracketAux x

Tactic:
ext m n

Goal state after:
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst✝¹⁷ : LieRing L
inst✝¹⁶ : LieAlgebra R L
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : LieRingModule L M
inst✝¹² : LieModule R L M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : LieRingModule L N
inst✝⁸ : LieModule R L N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
m : M
n : N
⊢ ((AlgebraTensorModule.curry (hasBracketAux x ∘ₗ hasBracketAux y)) m) n =
    ((AlgebraTensorModule.curry (hasBracketAux ⁅x, y⁆ + hasBracketAux y ∘ₗ hasBracketAux x)) m) n
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst✝¹⁷ : LieRing L
inst✝¹⁶ : LieAlgebra R L
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : LieRingModule L M
inst✝¹² : LieModule R L M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : LieRingModule L N
inst✝⁸ : LieModule R L N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x : L
f : M →ₗ[R] N →ₗ[R] P
⊢ (↑(lift.equiv (RingHom.id R) M N P)).toFun ⁅x, f⁆ = ⁅x, (↑(lift.equiv (RingHom.id R) M N P)).toFun f⁆

Tactic:
ext m n

Goal state after:
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst✝¹⁷ : LieRing L
inst✝¹⁶ : LieAlgebra R L
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : LieRingModule L M
inst✝¹² : LieModule R L M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : LieRingModule L N
inst✝⁸ : LieModule R L N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x : L
f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
⊢ ((AlgebraTensorModule.curry ((↑(lift.equiv (RingHom.id R) M N P)).toFun ⁅x, f⁆)) m) n =
    ((AlgebraTensorModule.curry ⁅x, (↑(lift.equiv (RingHom.id R) M N P)).toFun f⁆) m) n
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
ha : IsNilpotent a
a✝ : Nontrivial A
x✝¹ : ℕ
x✝ : x✝¹ ∈ range (nilpotencyClass a - 1)
⊢ x✝¹ + 1 ≠ 0

Tactic:
by positivity

Goal state after:
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x y : L
hy : y ∈ {x | ∀ (m : M), ⁅x, m⁆ ∈ N}
m : M
⊢ ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆ ∈ N

Tactic:
exact sub_mem (N.lie_mem (hy m)) (hy ⁅x, m⁆)

Goal state after: