mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
⊢ P.complex.d 1 0 ≫ P.π.f 0 = 0

Tactic:
← P.π.comm 1 0,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
⊢ P.π.f 1 ≫ ((single₀ C).obj Z).d 1 0 = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ (lift f P Q ≫ Q.π).f 0 = (P.π ≫ (ChainComplex.single₀ C).map f).f 0

Tactic:
simp [lift, liftFZero, liftFOne]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: case mp
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
p'' : ℤ
hp'' : p + 1 = p''
⊢ (∃ β, δ (n - 1) n β = ↑(toSingleMk f h p' hp' hf)) → ∃ g, K.d p p'' ≫ g = f

Tactic:
rintro ⟨α, hα⟩
    obtain ⟨g, hg⟩ := Cochain.toSingleMk_surjective α p'' (by lia)
    refine ⟨n.negOnePow • g, ?_⟩
    rw [← hg, toSingleMk_coe, Cochain.δ_toSingleMk _ _ _ _ h] at hα
    exact (Cochain.toSingleEquiv h).symm.injective (by simpa)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝ : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp✝ : ∀ (j : J), p (0, j) = j
Y✝ Y' : GradedObject J D
φ : Y✝ ⟶ Y'
hp : ∀ (j : J), p (0, j) = j
Y : GradedObject J D
j : J
a : I × J
ha✝ : p a = j
ha : a.1 = 0
⊢ Y a.2 = Y j

Tactic:
by aesop

Goal state after:
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 : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.fromLeftDerivedZero.app X =
    (P.isoLeftDerivedObj F 0).hom ≫
      (ChainComplex.isoHomologyι₀ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)).hom ≫
        P.fromLeftDerivedZero' F

Tactic:
by
  dsimp [Functor.fromLeftDerivedZero, isoLeftDerivedObj]
  have h₁ := ProjectiveResolution.fromLeftDerivedZero'_naturality
    (𝟙 X) P (projectiveResolution X) (lift (𝟙 X) _ _) (by simp) F
  have h₂ : (P.isoLeftDerivedToHomotopyCategoryObj F).inv =
    (F.mapHomologicalComplex _ ⋙ HomotopyCategory.quotient _ _).map (lift (𝟙 X) _ _) :=
      id_comp _
  simp only [Functor.map_id, comp_id] at h₁
  rw [assoc, ← cancel_epi ((HomotopyCategory.homologyFunctor _ _ 0).map
      (P.isoLeftDerivedToHomotopyCategoryObj F).inv), ← Functor.map_comp_assoc,
      Iso.inv_hom_id, Functor.map_id, id_comp, ← h₁, h₂,
      ← HomologicalComplex.homologyι_naturality_assoc]
  erw [← NatTrans.naturality_assoc]
  rfl

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

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝ : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp✝ : ∀ (j : J), p (j, 0) = j
X✝ X' : GradedObject J D
φ : X✝ ⟶ X'
hp : ∀ (j : J), p (j, 0) = j
X : GradedObject J D
j : J
a : J × I
ha✝ : p a = j
ha : a.2 = 0
⊢ X a.1 = X j

Tactic:
by aesop

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

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝ : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
⊢ ∀ (j_1 : ↑(p ⁻¹' {j})),
    Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) j_1 ≫
        e.inv.app (X j) ≫ (F.obj (X j)).map (singleObjApplyIso 0 Y).inv ≫ s.inj ⟨(j, 0), ⋯⟩ =
      s.inj j_1

Tactic:
rintro ⟨⟨j', i⟩, h⟩

Goal state after:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝ : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
j' : J
i : I
h : (j', i) ∈ p ⁻¹' {j}
⊢ Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j', i), h⟩ ≫
      e.inv.app (X j) ≫ (F.obj (X j)).map (singleObjApplyIso 0 Y).inv ≫ s.inj ⟨(j, 0), ⋯⟩ =
    s.inj ⟨(j', i), h⟩
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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f₁ (f₂ ≫ f₃) n₀ n₁ ⋯ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) =
    X.toCycles f₂ f₃ (f₂ ≫ f₃) ⋯ n₀ ≫ X.iCycles f₂ f₃ n₀ ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁

Tactic:
toCycles_i_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₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f₁ (f₂ ≫ f₃) n₀ n₁ ⋯ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) =
    (X.H n₀).map (twoδ₁Toδ₀ f₂ f₃ (f₂ ≫ f₃) ⋯) ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁
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₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
⊢ hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯) ≫ cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯) =
    0

Tactic:
by rw [this]; simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{?u.4, u_1} C
inst✝ : Abelian C
κ : Type u_2
c : ℤ → ComplexShape κ
r₀ : ℤ
X✝ Y✝ Z✝ : SpectralSequence C c r₀
f : X✝.Hom Y✝
g : Y✝.Hom Z✝
r r' : ℤ
hrr' : κ
pq : r + 1 = r'
hr : r₀ ≤ r
⊢ HomologicalComplex.homologyMap (f.hom r ⋯ ≫ g.hom r ⋯) hrr' ≫ (Z✝.iso r r' hrr' ⋯ ⋯).hom =
    (X✝.iso r r' hrr' ⋯ ⋯).hom ≫ (f.hom r' ⋯ ≫ g.hom r' ⋯).f hrr'

Tactic:
by
        simp [HomologicalComplex.homologyMap_comp, assoc, g.comm r r', f.comm_assoc r r']

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₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hp : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) := ⋯.gIsCokernel
this : hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯) = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
⊢ kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯) ≫
      hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯) =
    0

Tactic:
by rw [this]; simp

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
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
⊢ WithBotTop.coe 0 < coreE₂HomologicalNat.i₃ r (p, q) ⋯

Tactic:
simp only [coreE₂HomologicalNat_i₃, WithBotTop.coe_lt_coe]

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
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
⊢ 0 < -↑q + r - 1
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 r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' pq'' : κ
hpq' : (c r).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : ¬(c r).Rel pq' pq''
⊢ (kfSc X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂ i₃ hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).Exact

Tactic:
· rw [ShortComplex.exact_iff_epi _ ((page X data r hr).shape _ _ h)]
    have := isIso_mapFourδ₁Toδ₀' X data r r' hrr' hr pq' pq'' hpq'
      i₀' i₀ i₁ i₂ i₃ hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' h
    dsimp
    infer_instance

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 : L
m : M
⊢ ⁅-x, m⁆ - -⁅x, m⁆ = 0

Tactic:
sub_neg_eq_add,

Goal state after:
L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅-x, m⁆ + ⁅x, m⁆ = 0
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 : L
m : M
⊢ ⁅x, -m⁆ - -⁅x, m⁆ = 0

Tactic:
sub_neg_eq_add,

Goal state after:
L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅x, -m⁆ + ⁅x, m⁆ = 0
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: case pos
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 r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯ ≅
    X.dCokernelSequence (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯)
      (have this := homOfLE ⋯;
      this)
      (homOfLE ⋯ ≫ homOfLE ⋯) ⋯ (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯

Tactic:
refine ShortComplex.isoMk
      (pageXIso X data _ hr _ _ _ _ _
        (by rw [hi₂, data.hc₀₂ r _ _ h]) (by rw [hi₃, data.hc₁₃ r _ _ h])
        (by rw [hi₃', data.i₃_next r r' _ _ h]) rfl _ _ _ (by have := data.hc r _ _ h; lia))
      (pageXIso X data _ hr _ _ _ _ _ hi₀ hi₁ hi₂ hi₃ _ _ _ hn₁') (Iso.refl _) ?_ (by simp)

Goal state after:
case pos
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 r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ (pageXIso X data r hr pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯).hom ≫
      (X.dCokernelSequence (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯)
          (have this := homOfLE ⋯;
          this)
          (homOfLE ⋯ ≫ homOfLE ⋯) ⋯ (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯).f =
    (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).f ≫
      (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this✝¹ : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
this✝ : I x = N
this : Ideal.span {x} = N
⊢ False

Tactic:
refine (this ▸ ne) ((Submodule.fg_span <| Set.finite_singleton x).eq_bot_of_le_jacobson_smul ?_)

Goal state after:
case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this✝¹ : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
this✝ : I x = N
this : Ideal.span {x} = N
⊢ R ∙ x ≤ Ring.jacobson R • (R ∙ x)
Module: Mathlib.Algebra.Jordan.Basic

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

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

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
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x : L
hx : x ∈ K
hx' : x ∈ lieSpan R L (range (Subtype.val ∘ f))
this : x ∈ map K.incl (lieSpan R (↥K) (range f))
⊢ ⟨x, hx⟩ ∈ lieSpan R (↥K) (range f)

Tactic:
by aesop

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

Goal state before:
pp: case refine_3
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 : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
m₁ m₂ : M
hx✝ : m₁ ∈ Submodule.span R s
hy✝ : m₂ ∈ Submodule.span R s
hm₁ : ⁅y, m₁⁆ ∈ Submodule.span R s
hm₂ : ⁅y, m₂⁆ ∈ Submodule.span R s
⊢ ⁅y, m₁⁆ + ⁅y, m₂⁆ ∈ Submodule.span R s

Tactic:
exact Submodule.add_mem _ hm₁ hm₂

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

Goal state before:
pp: case refine_3
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
ι : Sort u_1
N : ι → LieSubmodule R L M
motive : (x : M) → x ∈ ⨆ i, N i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), motive x hx → motive y hy → motive (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, N i
x y : M
w✝¹ : x ∈ ⨆ i, N i
Cx : motive x w✝¹
w✝ : y ∈ ⨆ i, N i
Cy : motive y w✝
⊢ ∃ (hx : x + y ∈ ⨆ i, N i), motive (x + y) hx

Tactic:
exact ⟨_, add _ _ _ _ Cx Cy⟩

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
p : A[X]
monic : p.Monic
hp0 : (Polynomial.aeval x) p = 0
n : ℕ
hpn : p.degree = ↑n
ind : LinearIndependent A fun i ↦ x ^ ↑i
q : A[X]
lt✝ : q.degree < p.degree
ne : ¬q = 0
hq : (Polynomial.aeval x) (∑ i ∈ Finset.range n, (monomial i) (q.coeff i)) = 0
i : ℕ
lt : i < n
⊢ ∑ i, q.coeff ↑i • x ^ ↑i = 0

Tactic:
by simpa [Finset.sum_range, Algebra.smul_def] using hq

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
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ⊓ ⁅J, N⁆

Tactic:
by
  rw [le_inf_iff]; constructor <;>
  apply mono_lie_left <;> [exact inf_le_left; exact inf_le_right]

Goal state after:
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
⊢ (algebraMap A B) (q.coeff 0) ≠ 0

Tactic:
map_ne_zero_iff _ hf,

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
⊢ q.coeff 0 ≠ 0
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I.incl.idealRange ⊓ I₁, I.incl.idealRange ⊓ I₂⁆

Tactic:
rw [comap_bracket_eq]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = ⁅comap I.incl I₁, comap I.incl I₂⁆ ⊔ I.incl.ker

R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
⊢ I.incl.IsIdealMorphism
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
⊢ Injective (rootsOfMinPolyPiType F E K)

Tactic:
intro f g h
  -- needs explicit coercion on the RHS
  suffices (f : E →ₗ[F] K) = (g : E →ₗ[F] K) by rwa [DFunLike.ext'_iff] at this ⊢
  rw [funext_iff] at h
  exact LinearMap.ext_on (Module.finBasis F E).span_eq fun e he =>
    Subtype.ext_iff.mp (h ⟨e, he⟩)

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

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : (Polynomial.aeval σ.toLinearMap) q = 0
⊢ orderOf σ ≤ q.natDegree

Tactic:
← not_lt

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : (Polynomial.aeval σ.toLinearMap) q = 0
⊢ ¬q.natDegree < orderOf σ
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr
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 b =
    Submodule.Quotient.mk ((algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩)) + Submodule.Quotient.mk 0

Tactic:
← H

Goal state after:
case inr
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
      ((pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x) =
    Submodule.Quotient.mk ((algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩)) + Submodule.Quotient.mk 0
Module: Mathlib.LinearAlgebra.Matrix.Dual

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : CommSemiring K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
u : V₁ →ₗ[K] V₂
⊢ (toMatrix B₂.dualBasis B₁.dualBasis) (Dual.transpose u) = ((toMatrix B₁ B₂) u)ᵀ

Tactic:
by
  ext i j
  simp only [LinearMap.toMatrix_apply, Module.Dual.transpose_apply, B₁.dualBasis_repr,
    B₂.dualBasis_apply, Matrix.transpose_apply, LinearMap.comp_apply]

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
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ (∑ i, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i).degree < ↑pb.dim

Tactic:
apply degree_sum_fin_lt

Goal state after:
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ ((toMatrix b b) ((lmul R S) s)).det = ((leftMulMatrix b) s).det

Tactic:
← toMatrix_lmul_eq

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ ((toMatrix b b) ((lmul R S) s)).det = ((toMatrix b b) (mulLeft R s)).det
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
hd₀ : d ≠ 0
⊢ False

Tactic:
obtain ⟨p, irr, dvd⟩ := WfDvdMonoid.exists_irreducible_factor hdu hd₀

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
hd₀ : d ≠ 0
p : R
irr : Irreducible p
dvd : p ∣ d
⊢ False
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case mp
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
⊢ Multiset.count a (normalizedFactors x) ≤ 1

Tactic:
by_cases hmem : a ∈ normalizedFactors x

Goal state after:
case pos
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
⊢ Multiset.count a (normalizedFactors x) ≤ 1

case neg
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
⊢ Multiset.count a (normalizedFactors x) ≤ 1