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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₁ : ℤ
A : C
x : (X.H n₁).obj (mk₁ f) ⟶ A
hn₁ : n₁ - 1 + 1 = n₁
hx : X.δ f g (n₁ - 1) n₁ hn₁ ≫ x = 0
⊢ X.δ f g (n₁ - 1) n₁ ⋯ ≫ x = 0

Tactic:
exact hx

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : β.app 0 = α.app 0
hβ₁ : β.app 1 = α.app 2
⊢ X.toCycles f g fg h n ≫ X.cyclesMap f g f' g' α n = (X.H n).map β ≫ X.toCycles f' g' fg' h' n

Tactic:
rw [← cancel_mono (X.iCycles f' g' n), Category.assoc, Category.assoc, toCycles_i,
    X.cyclesMap_i f g f' g' α (homMk₁ (α.app 1) (α.app 2) (naturality' α 1 2)) n rfl,
    toCycles_i_assoc, ← Functor.map_comp, ← Functor.map_comp]

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : β.app 0 = α.app 0
hβ₁ : β.app 1 = α.app 2
⊢ (X.H n).map (twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) ⋯) = (X.H n).map (β ≫ twoδ₁Toδ₀ f' g' fg' h')
Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n : ℤ
hn : n = data.deg pq
⊢ r₀ ≤ r₀

Tactic:
by rfl

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_hom._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_hom._auto_3
⊢ r₀ ≤ r₀

Tactic:
by rfl

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_inv._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_inv._auto_3
⊢ r₀ ≤ r₀

Tactic:
by rfl

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
A : C
x : (X.H n₁).obj (mk₁ f₁₂) ⟶ A
h : (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ x = 0
hn₁ : n₀ + 1 = n₁
h' : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ x = 0
hn₂ : n₁ + 1 = n₂
⊢ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≫ ⋯.desc x ⋯ = x

Tactic:
rw [← Category.assoc]

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
A : C
x : (X.H n₁).obj (mk₁ f₁₂) ⟶ A
h : (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ x = 0
hn₁ : n₀ + 1 = n₁
h' : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ x = 0
hn₂ : n₁ + 1 = n₂
⊢ (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) ≫ ⋯.desc x ⋯ = x
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 : ℤ × Fin l),
    autoParam (2 ≤ r) SpectralSequenceDataCore._auto_32 →
      autoParam (r ≤ r') SpectralSequenceDataCore._auto_34 →
        Fin.clamp (↑↑pq.2 + (r - 1)).toNat l ≤ Fin.clamp (↑↑pq.2 + (r' - 1)).toNat l

Tactic:
rintro r r' ⟨a, ⟨a', _⟩⟩ hr hrr'
    rw [Fin.mk_le_mk]
    exact Fin.clamp_monotone (by 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))
r r' : ℤ
pq : ℤ × Fin l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq pq'
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq + 1
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ (coreE₂CohomologicalFin l).i₀ r' pq ⋯ = (coreE₂CohomologicalFin l).i₀ r pq ⋯

Tactic:
subst hrr'

Goal state after:
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))
r : ℤ
pq : ℤ × Fin l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq pq'
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq + 1
hr : 2 ≤ r
⊢ (coreE₂CohomologicalFin l).i₀ (r + 1) pq ⋯ = (coreE₂CohomologicalFin l).i₀ r pq ⋯
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))
r r' : ℤ
pq : ℤ × Fin l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' pq
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq - 1
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ (coreE₂CohomologicalFin l).i₃ r pq ⋯ = (coreE₂CohomologicalFin l).i₃ r' pq ⋯

Tactic:
subst hrr'

Goal state after:
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))
r : ℤ
pq : ℤ × Fin l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' pq
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq - 1
hr : 2 ≤ r
⊢ (coreE₂CohomologicalFin l).i₃ r pq ⋯ = (coreE₂CohomologicalFin l).i₃ (r + 1) pq ⋯
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₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
h₀ : i₀ = data.i₀ r pq' ⋯
h₁ : i₁ = data.i₁ pq'
h₂ : i₂ = data.i₀ r pq ⋯
h₃ : i₃ = data.i₁ pq
h₄ : i₄ = data.i₂ pq
h₅ : i₅ = data.i₃ r pq ⋯
n₀ n₁ n₂ n₃ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) pageD_eq._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) pageD_eq._auto_3
hn₃ : autoParam (n₂ + 1 = n₃) pageD_eq._auto_5
⊢ n₂ = data.deg pq'

Tactic:
simpa only [← hn₂, hn₁'] using data.hc r pq pq' hpq

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₀
inst✝ : X.HasSpectralSequence data
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
h₀ : i₀ = data.i₀ r pq' ⋯
h₁ : i₁ = data.i₁ pq'
h₂ : i₂ = data.i₀ r pq ⋯
h₃ : i₃ = data.i₁ pq
h₄ : i₄ = data.i₂ pq
h₅ : i₅ = data.i₃ r pq ⋯
n₀ n₁ n₂ n₃ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequence_page_d_eq._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequence_page_d_eq._auto_3
hn₃ : autoParam (n₂ + 1 = n₃) spectralSequence_page_d_eq._auto_5
⊢ n₂ = data.deg pq'

Tactic:
simpa only [← hn₂, hn₁'] using data.hc r pq pq' hpq

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

Goal state before:
pp: case a
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J : LieIdeal R L'
h : f.IsIdealMorphism
⊢ map f (comap f J) ≤ f.idealRange ⊓ J

Tactic:
rw [le_inf_iff]; exact ⟨f.map_le_idealRange _, map_comap_le⟩

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' x✝² x✝¹ x✝ : LieSubmodule R L M
⊢ ↑x✝² ≤ ↑x✝ → (↑x✝² ⊔ ↑x✝¹) ⊓ ↑x✝ ≤ ↑x✝² ⊔ ↑x✝¹ ⊓ ↑x✝

Tactic:
exact IsModularLattice.sup_inf_le_assoc_of_le _

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑(⁅I, N⁆ ⊔ ⁅J, N⁆)

Tactic:
rintro m ⟨⟨x, hx⟩, n, h⟩

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
⊢ m ∈ ↑(⁅I, N⁆ ⊔ ⁅J, N⁆)
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
hx : (minpoly A x).degree = 1
h : IsIntegral A x
key : (Polynomial.aeval x) X + (Polynomial.aeval x) (C ((minpoly A x).coeff 0)) = 0
⊢ x ∈ (algebraMap A B).range

Tactic:
aeval_C,

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
h : IsIntegral A x
key : (Polynomial.aeval x) X + (algebraMap A B) ((minpoly A x).coeff 0) = 0
⊢ x ∈ (algebraMap A B).range
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
p : A[X]
⊢ (∃ c, p = c * minpoly A x) ↔ ∃ a, a * minpoly A x = p

Tactic:
eq_comm (a := p)

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

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
a : A
hf : Injective ⇑(algebraMap A B)
a✝ : Nontrivial A
⊢ (Polynomial.aeval ((algebraMap A B) a)) X - (Polynomial.aeval ((algebraMap A B) a)) (C a) = 0

Tactic:
aeval_C,

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
a : A
hf : Injective ⇑(algebraMap A B)
a✝ : Nontrivial A
⊢ (Polynomial.aeval ((algebraMap A B) a)) X - (algebraMap A B) a = 0
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
a : A
hf : Injective ⇑(algebraMap A B)
a✝ : Nontrivial A
q : A[X]
hl : q.natDegree = 0
h0 : ¬C (q.coeff 0) = 0
⊢ (Polynomial.aeval ((algebraMap A B) a)) (C (q.coeff 0)) ≠ 0

Tactic:
aeval_C,

Goal state after:
case refine_2
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
a : A
hf : Injective ⇑(algebraMap A B)
a✝ : Nontrivial A
q : A[X]
hl : q.natDegree = 0
h0 : ¬C (q.coeff 0) = 0
⊢ (algebraMap A B) (q.coeff 0) ≠ 0
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁹ : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : Ring S
inst✝⁵ : Ring T
inst✝⁴ : IsDomain S
inst✝³ : IsDomain T
inst✝² : Algebra R S
inst✝¹ : Algebra A T
inst✝ : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp : (algebraMap A T).comp ↑f = (↑g).comp (algebraMap R S)
x : S
⊢ Irreducible (minpoly R x)

Tactic:
exact minpoly.irreducible (Algebra.IsIntegral.isIntegral x)

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✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
y : A
h : (minpoly A x).IsRoot y
key : minpoly A x = X - C y
this : x - (Polynomial.aeval x) (C y) = 0
⊢ (algebraMap A B) y = x

Tactic:
aeval_C,

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
y : A
h : (minpoly A x).IsRoot y
key : minpoly A x = X - C y
this : x - (algebraMap A B) y = 0
⊢ (algebraMap A B) y = x
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : ∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P
⊢ eval a (eval b P) = 0

pp: case mpr
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
⊢ ∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P

Tactic:
· rcases h with ⟨_, _, rfl⟩
    simp

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
⊢ ∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr.e_a
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
H : (pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x = b
⊢ Submodule.Quotient.mk (∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x) = Submodule.Quotient.mk 0

Tactic:
rw [Quotient.mk_zero, Quotient.mk_eq_zero, coe_basis]

Goal state after:
case inr.e_a
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
H : (pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x = b
⊢ ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • (fun i ↦ pb.gen ^ ↑i) x ∈ Ideal.span {pb.gen}
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ (aeval pb.gen) X ^ pb.dim - ∑ x, (aeval pb.gen) (C ((pb.basis.repr (pb.gen ^ pb.dim)) x)) * (aeval pb.gen) X ^ ↑x = 0

Tactic:
aeval_C,

Goal state after:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ (aeval pb.gen) X ^ pb.dim - ∑ x, (algebraMap A S) ((pb.basis.repr (pb.gen ^ pb.dim)) x) * (aeval pb.gen) X ^ ↑x = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ((Quotient.mk I).comp C) y ∈ ((Quotient.mk I).comp C).range
hx : C ⟨((Quotient.mk I).comp C) y, hx'⟩ ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
⊢ C (i y) ∈ map (mapRingHom i) I

Tactic:
exact hx

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: 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
x x' : S
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) (x * x') =
    ((pb.basis.constr A) fun i ↦ y ^ ↑i) x * ((pb.basis.constr A) fun i ↦ y ^ ↑i) x'

Tactic:
by
  obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
  obtain ⟨g, rfl⟩ := pb.exists_eq_aeval' x'
  simp only [← aeval_mul, pb.constr_pow_aeval hy]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : ∃ x, Irreducible x
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r

Tactic:
irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree,

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : ∃ x, Irreducible x
⊢ Squarefree r ↔ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case hMM'
M : Type u_2
inst✝⁶ : AddCommGroup M
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type u_6
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ c.toMatrix ⇑b * b.toMatrix ⇑c = 1

Tactic:
Basis.toMatrix_mul_toMatrix,

Goal state after:
case hMM'
M : Type u_2
inst✝⁶ : AddCommGroup M
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type u_6
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ c.toMatrix ⇑c = 1
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case hM'M
M : Type u_2
inst✝⁶ : AddCommGroup M
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type u_6
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ b.toMatrix ⇑c * c.toMatrix ⇑b = 1

Tactic:
Basis.toMatrix_mul_toMatrix,

Goal state after:
case hM'M
M : Type u_2
inst✝⁶ : AddCommGroup M
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type u_6
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ b.toMatrix ⇑b = 1
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
H : ¬∃ s, Nonempty (Basis (↥s) A M)
⊢ ¬∃ t, Nonempty (Basis (↥t) A N)

Tactic:
contrapose H

Goal state after:
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
H : ∃ t, Nonempty (Basis (↥t) A N)
⊢ ∃ s, Nonempty (Basis (↥s) A M)
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ (toMatrix
        ((Pi.basis fun x ↦ b).reindex
          ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M))))
        ((Pi.basis fun x ↦ b).reindex
          ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))))
      (pi fun i ↦ f i ∘ₗ proj i) (i₁, i₂) (j₁, j₂) =
    blockDiagonal (fun i ↦ (toMatrix b b) (f i)) (i₁, i₂) (j₁, j₂)

Tactic:
simp_rw [LinearMap.toMatrix_apply', Matrix.blockDiagonal_apply, Basis.coe_reindex,
      Function.comp_apply, Basis.repr_reindex_apply, Equiv.symm_trans_apply, Equiv.prodComm_symm,
      Equiv.prodComm_apply, Equiv.sigmaEquivProd_symm_apply, Prod.swap_prod_mk, Pi.basis_apply,
      Pi.basis_repr, LinearMap.pi_apply, LinearMap.coe_comp, Function.comp_apply,
      LinearMap.toMatrix_apply', LinearMap.coe_proj, Function.eval, Pi.single_apply]

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ (b.repr ((f i₂) (if i₂ = j₂ then b j₁ else 0))) i₁ = if i₂ = j₂ then (b.repr ((f i₂) (b j₁))) i₁ else 0
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ ¬↑(f.natDegree - 1) = ⊥

pp: F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ f.natDegree ≠ 0

Tactic:
· rintro ⟨⟩

Goal state after:
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ f.natDegree ≠ 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ eval₂ (of f) (root f) f = 0

Tactic:
rw [← algebraMap_eq, ← aeval_def, aeval_eq, mk_self]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f g : S[X]
hfg : Associated f g
⊢ (algEquivOfAssociated R f g hfg) (root f) = root g

Tactic:
by
  rw [coe_algEquivOfAssociated, algHomOfDvd_root]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case calc_2
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 ∈ R2N, (↑i !)⁻¹ • ∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * ↑(i.choose j) =
    ∑ i ∈ R2N, ∑ j ∈ range (i + 1), ((↑j !)⁻¹ * (↑(i - j)!)⁻¹) • (a ^ j * b ^ (i - j))

Tactic:
simp_rw [smul_sum]

Goal state after:
case calc_2
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)
⊢ ∑ x ∈ R2N, ∑ x_1 ∈ range (x + 1), (↑x !)⁻¹ • (a ^ x_1 * b ^ (x - x_1) * ↑(x.choose x_1)) =
    ∑ i ∈ R2N, ∑ j ∈ range (i + 1), ((↑j !)⁻¹ * (↑(i - j)!)⁻¹) • (a ^ j * b ^ (i - j))
Module: Mathlib.Algebra.Lie.AdjointAction.Derivation

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ (ad R L).ker = LieAlgebra.center R L

Tactic:
ext x
  rw [← LieAlgebra.self_module_ker_eq_center, LieHom.mem_ker, LieModule.mem_ker]
  simp [DFunLike.ext_iff]

Goal state after: