mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).inv.app P.complex ≫
      (F.mapHomotopyCategory (ComplexShape.down ℕ)).map (P.iso.inv ≫ (projectiveResolutions C).map f) =
    (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).inv.app Q.complex ≫
        (F.mapHomotopyCategory (ComplexShape.down ℕ)).map Q.iso.inv

Tactic:
iso_inv_naturality f P Q φ comm,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).inv.app P.complex ≫
      (F.mapHomotopyCategory (ComplexShape.down ℕ)).map
        ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ ≫ Q.iso.inv) =
    (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).inv.app Q.complex ≫
        (F.mapHomotopyCategory (ComplexShape.down ℕ)).map Q.iso.inv
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Projective X
⊢ IsZero ((ProjectiveResolution.self X).complex.X (n + 1))

Tactic:
by apply isZero_zero

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, 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₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.sc₁ f g fg h n₀ n₁ hn₁).Exact

Tactic:
subst h
  exact (X.exact₁' n₀ n₁ hn₁ (mk₂ f g)).exact 0

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝²⁵ : AddMonoid I
C : Type u_1
inst✝²⁴ : Category.{v_1, u_1} C
inst✝²³ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝²² : X₁.HasTensor X₂
inst✝²¹ : X₂.HasTensor X₃
inst✝²⁰ : X₃.HasTensor X₄
inst✝¹⁹ : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹⁸ : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹⁷ : (tensorObj X₂ X₃).HasTensor X₄
inst✝¹⁶ : X₂.HasTensor (tensorObj X₃ X₄)
inst✝¹⁵ : (tensorObj (tensorObj X₁ X₂) X₃).HasTensor X₄
inst✝¹⁴ : (tensorObj X₁ (tensorObj X₂ X₃)).HasTensor X₄
inst✝¹³ : X₁.HasTensor (tensorObj (tensorObj X₂ X₃) X₄)
inst✝¹² : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
inst✝¹¹ : (tensorObj X₁ X₂).HasTensor (tensorObj X₃ X₄)
inst✝¹⁰ : X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝⁹ : X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝⁸ : X₁.HasGoodTensor₁₂Tensor (tensorObj X₂ X₃) X₄
inst✝⁷ : X₁.HasGoodTensorTensor₂₃ (tensorObj X₂ X₃) X₄
inst✝⁶ : X₂.HasGoodTensor₁₂Tensor X₃ X₄
inst✝⁵ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
inst✝⁴ : (tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄
inst✝³ : (tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄
inst✝² : X₁.HasGoodTensor₁₂Tensor X₂ (tensorObj X₃ X₄)
inst✝¹ : X₁.HasGoodTensorTensor₂₃ X₂ (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor₄ObjExt X₂ X₃ X₄
j i₁ i₂ i₃ i₄ : I
h : i₁ + i₂ + i₃ + i₄ = j
⊢ i₁ + (i₂ + i₃) + i₄ = j

Tactic:
by simp only [← add_assoc, h]

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

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₁ i₂ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂

Tactic:
rw [← cancel_epi (X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles (𝟙 i₁) f₂ f₂ (by simp) n₁),
    X.toCycles_πE_d_assoc (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) f₁ (by simp) _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_EIsoH_hom .., πE_EIsoH_hom_assoc .., cyclesIsoH_inv_hom_id ..,
    comp_id, cyclesIsoH_inv_hom_id_assoc ..]

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₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ X.cycles f₁ f₂₃ n₁
hx₂ : x₂ ≫ X.iCycles f₁ f₂₃ n₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃) = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
obtain ⟨A₁, π₁, _, x₁, hx₁⟩ :=
    (X.kernelSequenceE_exact f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂).exact_up_to_refinements
      (x₂ ≫ X.iCycles f₁ f₂₃ n₁) (by cat_disch)

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₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ X.cycles f₁ f₂₃ n₁
hx₂ : x₂ ≫ X.iCycles f₁ f₂₃ n₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃) = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
x₁ : A₁ ⟶ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ ⋯ ⋯).X₁
hx₁ : π₁ ≫ x₂ ≫ X.iCycles f₁ f₂₃ n₁ = x₁ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ ⋯ ⋯).f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: case neg
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' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : ¬(c r).Rel pq' pq''
⊢ ((if hpq : (c r).Rel pq pq' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯).inv
      else 0) ≫
      if hpq : (c r).Rel pq' pq'' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq' - 1) (data.deg pq')
            (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₀ r pq' ⋯) (data.i₁ pq') ⋯ ⋯ ⋯ ⋯
              (data.deg pq') (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯).inv
      else 0) =
    0

Tactic:
rw [dif_neg hpq', comp_zero]

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₀
r : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
⊢ data.i₂ pq'' = data.i₀ r pq' ⋯

Tactic:
by rw [data.hc₀₂ r pq' pq'' hpq']

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

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

Tactic:
rw [mul_comm (a * a) (a * b), IsCommJordan.lmul_comm_rmul_rmul,
      mul_comm b (a * a)]

Goal state after:
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
J : LieIdeal R L'
⊢ map f I ≤ J ↔ I ≤ comap f J

Tactic:
rw [map_le]
  exact Set.image_subset_iff

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : f.ker = ⊥
⊢ ↑(comap f (map f N)) = ↑N

Tactic:
exact (N : Set M).preimage_image_eq (f.ker_eq_bot.mp hf)

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

Goal state before:
pp: case mpr
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
s : Set M
N : LieSubmodule R L M
⊢ s ⊆ ↑N → lieSpan R L s ≤ N

Tactic:
intro hs m hm; rw [mem_lieSpan] at hm; exact hm _ hs

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

Goal state before:
pp: case h.right
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' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅↑x, ↑⟨n, hn⟩⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
⊢ ∃ z ∈ ⁅I, N'⁆, ⁅↑x, ↑⟨n₁, hn₁⟩⁆ + z = m

Tactic:
use ⁅(x : L), (⟨n₂, hn₂⟩ : N')⁆

Goal state after:
case h
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' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅↑x, ↑⟨n, hn⟩⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
⊢ ⁅↑x, ↑⟨n₂, hn₂⟩⁆ ∈ ⁅I, N'⁆ ∧ ⁅↑x, ↑⟨n₁, hn₁⟩⁆ + ⁅↑x, ↑⟨n₂, hn₂⟩⁆ = m
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₂ : LieSubmodule R L M
⊢ comap N.incl N₂ = ⊥ ↔ N ⊓ N₂ = ⊥

Tactic:
simp only [← toSubmodule_inj, toSubmodule_comap, incl_coe, bot_toSubmodule,
    inf_toSubmodule]
  rw [← Submodule.disjoint_iff_comap_eq_bot, disjoint_iff]

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:
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 pos
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
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim = -∑ x, pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x

Tactic:
eq_neg_iff_add_eq_zero

Goal state after:
case pos
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
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim + ∑ x, pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x = 0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case neg
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✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) (∑ i ∈ Finset.range pb.dim, (f %ₘ minpoly A pb.gen).coeff i • pb.gen ^ i) =
    ∑ i ∈ Finset.range pb.dim, (f %ₘ minpoly A pb.gen).coeff i • y ^ i

Tactic:
map_sum

Goal state after:
case neg
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✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
⊢ ∑ x ∈ Finset.range pb.dim, ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((f %ₘ minpoly A pb.gen).coeff x • pb.gen ^ x) =
    ∑ i ∈ Finset.range pb.dim, (f %ₘ minpoly A pb.gen).coeff i • y ^ i
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ (R ⧸ I)
⊢ ∀ (n : σ),
    (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
        p →
      (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p * X n)) =
        p * X n

Tactic:
i

Goal state after:
case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ (R ⧸ I)
i : σ
⊢ (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
        (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
      p →
    (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
        (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p * X i)) =
      p * X i
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ R
⊢ ∀ (n : σ),
    eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
          ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
        (Ideal.Quotient.mk (Ideal.map C I)) p →
      eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
          ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) (p * X n))) =
        (Ideal.Quotient.mk (Ideal.map C I)) (p * X n)

Tactic:
i

Goal state after:
case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ R
i : σ
⊢ eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
        (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
        ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
      (Ideal.Quotient.mk (Ideal.map C I)) p →
    eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
        (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
        ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          ((Ideal.Quotient.mk (Ideal.map C I)) (p * X i))) =
      (Ideal.Quotient.mk (Ideal.map C I)) (p * X i)
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
hu : IsUnit x
⊢ x ^ n ∣ x

Tactic:
exact (hu.pow n).dvd

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

Goal state before:
pp: case pos.inl
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h✝ : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : emultiplicity a x ≤ 1
⊢ Multiset.count a (normalizedFactors x) ≤ 1

Tactic:
rw [← normalize_normalized_factor _ hmem]

Goal state after:
case pos.inl
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h✝ : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : emultiplicity a x ≤ 1
⊢ Multiset.count (normalize a) (normalizedFactors x) ≤ 1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : derivative f = 0
hp : p > 0
this : IsLocalHom (expand F p)
⊢ ¬f.Separable

Tactic:
separable_iff_derivative_ne_zero hf,

Goal state after:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : derivative f = 0
hp : p > 0
this : IsLocalHom (expand F p)
⊢ ¬derivative f ≠ 0
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_2
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
⊢ ¬Irreducible ((expand R p) f)

Tactic:
rw [polynomial_expand_eq]

Goal state after:
R : Type u_2
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
⊢ ¬Irreducible (map (↑(frobeniusEquiv R p).symm) f ^ p)
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
inst✝¹ : IsDomain R
inst✝ : Free R M
f : M →ₗ[R] M
hf : LinearMap.det f = 0
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : Fin (finrank R M) → R
hv_ne_zero : v ≠ 0
hv_zero : (toMatrix b b) f *ᵥ v = 0
⊢ f (b.equivFun.symm v) = 0

Tactic:
← b.equivFun.injective.eq_iff

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Free R M
f : M →ₗ[R] M
hf : LinearMap.det f = 0
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : Fin (finrank R M) → R
hv_ne_zero : v ≠ 0
hv_zero : (toMatrix b b) f *ᵥ v = 0
⊢ b.equivFun (f (b.equivFun.symm v)) = b.equivFun 0
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : (map (algebraMap F K) p).Splits
⊢ (map (algebraMap F K) p).roots.card = p.natDegree

Tactic:
← hsplit.natDegree_eq_card_roots,

Goal state after:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : (map (algebraMap F K) p).Splits
⊢ (map (algebraMap F K) p).natDegree = p.natDegree
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ f.Separable

Tactic:
separable_iff_derivative_ne_zero hf,

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : CommRing R
f g✝ : R[X]
inst✝ : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
g : R[X]
H : g ∈ span {f}
y : R[X]
hy : g = f * y
⊢ (eval₂RingHom i x) f * (eval₂RingHom i x) y = 0

Tactic:
coe_eval₂RingHom,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : CommRing R
f g✝ : R[X]
inst✝ : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
g : R[X]
H : g ∈ span {f}
y : R[X]
hy : g = f * y
⊢ eval₂ i x f * eval₂ i x y = 0
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:
i

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 : ι), v i = v j → i ≠ j → (MultilinearMap.mk' (fun v ↦ (e.toMatrix v).det) ⋯ ⋯).toFun v = 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: 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
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
⊢ (e.toMatrix (⇑f ∘ v)).det = ((LinearMap.toMatrix e e) f * e.toMatrix v).det

Tactic:
e.toMatrix_eq_toMatrix_constr (f ∘ v),

Goal state after:
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
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
⊢ ((LinearMap.toMatrix e e) ((e.constr ℕ) (⇑f ∘ v))).det = ((LinearMap.toMatrix e e) f * e.toMatrix v).det
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case neg
K : Type u_5
inst✝ : Field K
f : K[X]
hf : ¬f = 0
⊢ PowerBasis.dim ?neg✝ = f.natDegree

pp: case neg
K : Type u_5
inst✝ : Field K
f : K[X]
hf : ¬f = 0
⊢ PowerBasis K (K[X] ⧸ span {f})

Tactic:
exact AdjoinRoot.powerBasis_dim hf

Goal state after:
Module: Mathlib.LinearAlgebra.JordanChevalley

Goal state before:
pp: case refine_3
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
P : K[X]
k✝ : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k✝
ff : ↥K[f] := ⟨f, ⋯⟩
P' : K[X] := derivative P
nil' : IsNilpotent ((aeval ff) P)
sep' : IsUnit ((aeval ff) P')
s : End K V
mem : s ∈ K[f]
hss : (aeval ⟨s, mem⟩) P = 0
k : ℕ
hk : (ff - ⟨s, mem⟩) ^ k = 0
⊢ s.IsSemisimple

Tactic:
replace hss : aeval s P = 0 := by rwa [Subtype.ext_iff, coe_aeval_mk_apply] at hss
    exact isSemisimple_of_squarefree_aeval_eq_zero sep.squarefree hss

Goal state after:
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case refine_2
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 :
  eval (r₁ + (r₂ - r₁)) (map (algebraMap R S) P) =
    eval r₁ (map (algebraMap R S) P) + eval r₁ (derivative (map (algebraMap R S) P)) * (r₂ - r₁) + u * (r₂ - r₁) ^ 2
this : IsUnit ((aeval r₁) (derivative P))
⊢ IsNilpotent (u * (r₂ - x - (r₁ - x)))

Tactic:
exact (Commute.all _ _).isNilpotent_mul_left <| (Commute.all _ _).isNilpotent_sub hr₂ hr₁

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : LinearOrder R
x y : R
⊢ Associated |y| x ↔ Associated x y

Tactic:
associated_abs_left_iff,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : LinearOrder R
x y : R
⊢ Associated y x ↔ Associated x y
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ idealizer I = normalizer I

Tactic:
ext x; exact forall_congr' fun y ↦ by simp only [← lie_skew x y, neg_mem_iff]

Goal state after: