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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (if i₀ = i₀ then 𝟙 ((double f hi₀₁).X i₀) ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ 𝟙 (K.X i₀)
    else if hk₁ : i₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) =
    (doubleXIso₀ f hi₀₁).hom ≫ φ₀

Tactic:
if_pos rfl,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ 𝟙 ((double f hi₀₁).X i₀) ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ 𝟙 (K.X i₀) = (doubleXIso₀ f hi₀₁).hom ≫ φ₀
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (if i₁ = i₁ then 𝟙 ((double f hi₀₁).X i₁) ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ 𝟙 (K.X i₁) else 0) =
    (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁

Tactic:
if_pos rfl,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ 𝟙 ((double f hi₀₁).X i₁) ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ 𝟙 (K.X i₁) = (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁
Module: Mathlib.Algebra.Homology.ExactSequenceFour

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this✝¹ : HasZeroObject C
this✝ : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
this : Mono h.g'
⊢ Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = (S.sc hS k ⋯).g

Tactic:
cokerToKer'_fac

Goal state after:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this✝¹ : HasZeroObject C
this✝ : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
this : Mono h.g'
⊢ S.map' (k + 1) (k + 2) ⋯ ⋯ = (S.sc hS k ⋯).g
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
L : CochainComplex C ℤ
g : L ⟶ K
⊢ L.d p' p ≫ g.f p ≫ f = 0

Tactic:
simp [← g.comm_assoc, hf]

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} E
inst✝ : IsIdempotentComplete D
⊢ (functorExtension C D).IsEquivalence

Tactic:
rw [← karoubiUniversal_functor_eq]

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} E
inst✝ : IsIdempotentComplete D
⊢ (karoubiUniversal C D).functor.IsEquivalence
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ (toKaroubi C).map f.f
h₂ : (toKaroubi C ⋙ F).map f.f ≫ τ.app Y.X = τ.app X.X ≫ (toKaroubi C ⋙ G).map f.f
h₃ : X.decompId_p ≫ f = (toKaroubi C).map f.f ≫ Y.decompId_p
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f

Tactic:
dsimp at h₂

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ (toKaroubi C).map f.f
h₂ : F.map ((toKaroubi C).map f.f) ≫ τ.app Y.X = τ.app X.X ≫ G.map ((toKaroubi C).map f.f)
h₃ : X.decompId_p ≫ f = (toKaroubi C).map f.f ≫ Y.decompId_p
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
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
fg : i ⟶ k
h : f ≫ g = fg
n : ℤ
⊢ (X.cokernelSequenceCycles f g fg h n).Exact

Tactic:
apply ShortComplex.exact_of_g_is_cokernel

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
fg : i ⟶ k
h : f ≫ g = fg
n : ℤ
⊢ IsColimit (CokernelCofork.ofπ (X.cokernelSequenceCycles f g fg h n).g ⋯)
Module: Mathlib.CategoryTheory.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
sq₁ sq₂ : Square C
e₁ : sq₁.X₁ ≅ sq₂.X₁
e₂ : sq₁.X₂ ≅ sq₂.X₂
e₃ : sq₁.X₃ ≅ sq₂.X₃
e₄ : sq₁.X₄ ≅ sq₂.X₄
comm₁₂ : sq₁.f₁₂ ≫ e₂.hom = e₁.hom ≫ sq₂.f₁₂
comm₁₃ : sq₁.f₁₃ ≫ e₃.hom = e₁.hom ≫ sq₂.f₁₃
comm₂₄ : sq₁.f₂₄ ≫ e₄.hom = e₂.hom ≫ sq₂.f₂₄
comm₃₄ : sq₁.f₃₄ ≫ e₄.hom = e₃.hom ≫ sq₂.f₃₄
⊢ sq₂.f₁₃ ≫ e₃.inv = e₁.inv ≫ sq₁.f₁₃

Tactic:
by simp only [← cancel_mono e₃.hom, assoc, Iso.inv_hom_id,
                      comp_id, comm₁₃, Iso.inv_hom_id_assoc]

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
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq pq'
n : ℤ
hn : n = data.deg pq + 1
i₀' i₀ : ι
hi₀' : i₀' = data.i₀ r' pq ⋯
hi₀ : i₀ = data.i₀ r pq ⋯
⊢ IsZero ((X.H n).obj (mk₁ (homOfLE ⋯)))

Tactic:
by
  subst hi₀' hi₀
  exact HasSpectralSequence.isZero_H_obj_mk₁_i₀_le r r' pq hpq n hn

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₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.cyclesIsoH f n₀ n₁ hn₁).inv = X.toCycles (𝟙 i₀) f f ⋯ n₀

Tactic:
rw [← cancel_mono (X.iCycles (𝟙 _) f n₀), toCycles_i]

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₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.cyclesIsoH f n₀ n₁ hn₁).inv ≫ X.iCycles (𝟙 i₀) f n₀ = (X.H n₀).map (twoδ₁Toδ₀ (𝟙 i₀) f f ⋯)
Module: Mathlib.Order.Filter.EventuallyConst

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
inst✝ : One β
s : Set α
c : β
⊢ EventuallyConst (s.mulIndicator fun x ↦ c) l ↔ c = 1 ∨ EventuallyConst s l

Tactic:
by
  rcases eq_or_ne c 1 with rfl | hc <;> simp [mulIndicator_const_iff_of_ne, *]

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 ι
n₁ n₂ : ℤ
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
hn₁ : n₁ - 1 + 1 = n₁
h : (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).LeftHomologyData :=
  (X.homologyDataIdId f (n₁ - 1) n₁ n₂ hn₁ hn₂).left
this : h.cyclesIso.inv = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv
⊢ (X.homologyDataIdId f (n₁ - 1) n₁ n₂ ⋯ ⋯).left.homologyIso.inv =
    X.toCycles (𝟙 i) f f ⋯ n₁ ≫ X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂

Tactic:
rw [← cancel_epi h.π, h.π_comp_homologyIso_inv]

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 ι
n₁ n₂ : ℤ
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
hn₁ : n₁ - 1 + 1 = n₁
h : (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).LeftHomologyData :=
  (X.homologyDataIdId f (n₁ - 1) n₁ n₂ hn₁ hn₂).left
this : h.cyclesIso.inv = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv
⊢ h.cyclesIso.inv ≫ (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).homologyπ =
    h.π ≫ X.toCycles (𝟙 i) f f ⋯ n₁ ≫ X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
M₁ M₂ : Submodule R P
inst✝¹ : IsArtinian R ↥M₁
inst✝ : IsArtinian R ↥M₂
⊢ IsArtinian R ↥(M₁ ⊔ M₂)

Tactic:
have := isArtinian_range (M₁.subtype.coprod M₂.subtype)

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
M₁ M₂ : Submodule R P
inst✝¹ : IsArtinian R ↥M₁
inst✝ : IsArtinian R ↥M₂
this : IsArtinian R ↥(M₁.subtype.coprod M₂.subtype).range
⊢ IsArtinian R ↥(M₁ ⊔ M₂)
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ b * a * (a * a) = b * (a * a) * a

Tactic:
← mul_assoc,

Goal state after:
A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ b * a * a * a = b * (a * a) * a
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: 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'
I : LieIdeal R L
x : L'
y : L
hy₂ : ↑f y = x
z₁ : L
hz₁ : z₁ ∈ I
z₂ : L
hz₂ : z₂ ∈ f.ker
hy : z₁ + z₂ = y
⊢ ↑f (z₁ + z₂) ∈ ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)

Tactic:
map_add,

Goal state after:
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'
I : LieIdeal R L
x : L'
y : L
hy₂ : ↑f y = x
z₁ : L
hz₁ : z₁ ∈ I
z₂ : L
hz₂ : z₂ ∈ f.ker
hy : z₁ + z₂ = y
⊢ ↑f z₁ + ↑f z₂ ∈ ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: 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₂
h₁ : Surjective ⇑f
h₂ : IsLieAbelian L₁
x y : L₂
⊢ ⁅x, y⁆ = 0

Tactic:
obtain ⟨u, rfl⟩ := h₁ x
      obtain ⟨v, rfl⟩ := h₁ y
      rw [← LieHom.map_lie, trivial_lie_zero, map_zero]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
f : B →ₐ[A] B'
hf : Injective ⇑f
x : B
⊢ minpoly A (f x) = minpoly A x

Tactic:
minpoly,

Goal state after:
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
f : B →ₐ[A] B'
hf : Injective ⇑f
x : B
⊢ (if hx : IsIntegral A (f x) then ⋯.min (fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B') (f x) x_1 = 0) hx else 0) =
    if hx : IsIntegral A x then ⋯.min (fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx else 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:
rwa [aeval_C, map_ne_zero_iff _ hf, ← C_ne_zero]

Goal state after:
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
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
⊢ a.natDegree < (minpoly A x).natDegree

Tactic:
have hcm := hamonic.of_mul_monic_left (he.subst <| monic hx)

Goal state after:
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
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
⊢ a.natDegree < (minpoly A x).natDegree
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
I : Ideal R
y a✝ b✝ : ↥R[x]
ha✝ : a✝ ∈ Submodule.span (↥R[x]) (⇑(algebraMap R ↥R[x]) '' ↑I)
hb✝ : b✝ ∈ Submodule.span (↥R[x]) (⇑(algebraMap R ↥R[x]) '' ↑I)
a : R[X]
ha : ∀ (i : ℕ), a.coeff i ∈ I
ha' : (aeval x) a = ↑a✝
b : R[X]
hb : ∀ (i : ℕ), b.coeff i ∈ I
hb' : (aeval x) b = ↑b✝
i : ℕ
⊢ (a + b).coeff i ∈ I

Tactic:
simpa using add_mem (ha i) (hb i)

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ ((Algebra.lmul A S) pb.gen) (pb.gen ^ ↑k) =
    ∑ x, (if ↑k + 1 = pb.dim then -pb.minpolyGen.coeff ↑x else if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x

Tactic:
apply (pow_succ' _ _).symm.trans

Goal state after:
case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ pb.gen ^ (↑k + 1) =
    ∑ x, (if ↑k + 1 = pb.dim then -pb.minpolyGen.coeff ↑x else if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ a.support
this : coeff n a ∈ RingHom.ker (Ideal.Quotient.mk I)
⊢ C ((Ideal.Quotient.mk I) (coeff n a)) = 0

Tactic:
RingHom.mem_ker

Goal state after:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ a.support
this : (Ideal.Quotient.mk I) (coeff n a) = 0
⊢ C ((Ideal.Quotient.mk I) (coeff n a)) = 0
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible ((X ^ k - C b) * q)
this : q.degree = 0
hq : m * k = k
⊢ False

Tactic:
exact hm' ((mul_eq_right₀ (mul_ne_zero_iff.mp hn).2).mp hq)

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r → ∀ (x : R), Irreducible x → ¬x * x ∣ r

Tactic:
· rintro (⟨rfl, h⟩ | h)
    · simpa using h
    intro x hx t
    exact hx.not_isUnit (h x t)

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ((expand F (p ^ n)) f).Separable
⊢ IsUnit f ∨ n = 0

Tactic:
rw [or_iff_not_imp_right]
  rintro hn : n ≠ 0
  have hf2 : derivative (expand F (p ^ n) f) = 0 := by
    rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn, zero_mul, mul_zero]
  rw [separable_def, hf2, isCoprime_zero_right, isUnit_iff] at hf
  rcases hf with ⟨r, hr, hrf⟩
  rw [eq_comm, expand_eq_C (pow_pos hp _)] at hrf
  rwa [hrf, isUnit_C]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case neg
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₂ : ι
h : ¬i₂ = j₂
⊢ (b.repr ((f i₂) 0)) i₁ = 0

Tactic:
· simp only [map_zero, Finsupp.coe_zero, Pi.zero_apply]

Goal state after:
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
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
⊢ ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → (MultilinearMap.mk' (fun v ↦ (e.toMatrix v).det) ⋯ ⋯).toFun v = 0

Tactic:
intro v i j h hij

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (MultilinearMap.mk' (fun v ↦ (e.toMatrix v).det) ⋯ ⋯).toFun v = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case h2
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ q ≠ 0

Tactic:
exact q_monic.ne_zero

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
⊢ (-f).IsSemisimple ↔ f.IsSemisimple

Tactic:
by
  simp [isSemisimple_iff, mem_invtSubmodule]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inl.inr
R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
i : m
l : n
⊢ (toMatrix b b) e (Sum.inl i) (Sum.inr l) = fromBlocks A B 0 D (Sum.inl i) (Sum.inr l)

Tactic:
simp [b, LinearMap.toMatrix_apply, Matrix.fromBlocks_apply₁₂, B]

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
⊢ IsRadical (minpoly K f)

Tactic:
isRadical_iff_span_singleton,

Goal state after:
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
⊢ (Ideal.span {minpoly K f}).IsRadical
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inr
R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
v : m ⊕ n
j : n
⊢ (toMatrix b b) e (Sum.inr j) v = fromBlocks A B 0 D (Sum.inr j) v

Tactic:
cases v with
    | inl k =>
      suffices W.mkQ (e (bW k)) = 0 by simp [LinearMap.toMatrix_apply, b, this]
      rw [← LinearMap.mem_ker, Submodule.ker_mkQ]
      exact he (Submodule.coe_mem (bW k))
    | inr l =>
      simp only [LinearMap.toMatrix_apply, sumQuot_repr_inr,
        Matrix.fromBlocks_apply₂₂, b, D]
      rw [← sumQuot_inr bW bQ l, W.mapQ_apply]
      simp

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]},
      p.Monic →
        p.natDegree = m →
          ∃ S x x_1,
            ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq : Polynomial.map (algebraMap R (AdjoinRoot p)) p = (X - C (AdjoinRoot.root p)) * q
hqm : q.Monic
this✝¹ : Free R (AdjoinRoot p)
this✝ : Module.Finite R (AdjoinRoot p)
this : Nontrivial (AdjoinRoot p)
⊢ ∃ S x x_1, ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits

Tactic:
obtain ⟨S, _, _, _, _, _, hS⟩ := IH _
    (by rw [← hn, ← hp.natDegree_map (algebraMap R (AdjoinRoot p)), hq,
      Monic.natDegree_mul (monic_X_sub_C _) hqm]; simp) hqm rfl

Goal state after:
case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]},
      p.Monic →
        p.natDegree = m →
          ∃ S x x_1,
            ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq : Polynomial.map (algebraMap R (AdjoinRoot p)) p = (X - C (AdjoinRoot.root p)) * q
hqm : q.Monic
this✝¹ : Free R (AdjoinRoot p)
this✝ : Module.Finite R (AdjoinRoot p)
this : Nontrivial (AdjoinRoot p)
S : Type u
w✝⁴ : CommRing S
w✝³ : Algebra (AdjoinRoot p) S
w✝² : Module.Finite (AdjoinRoot p) S
w✝¹ : Free (AdjoinRoot p) S
w✝ : Nontrivial S
hS : (Polynomial.map (algebraMap (AdjoinRoot p) S) q).Splits
⊢ ∃ S x x_1, ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits