mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: case neg
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}
hi : ¬i = 0
⊢ 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⟩

Tactic:
· apply IsInitial.hom_ext
        exact mapBifunctorObjObjSingle₀IsInitial _ _ _ _ hi

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.iCycles f g n ≫ (X.H n).map (homMk₁ (α.app 1) (α.app 2) ⋯) =
    (X.H n).map β ≫ (X.H n).map (twoδ₁Toδ₀ f' g' fg' h')

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 : ι
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) ≫ (X.H n).map (homMk₁ (α.app 1) (α.app 2) ⋯) =
    (X.H n).map β ≫ (X.H n).map (twoδ₁Toδ₀ f' g' fg' 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₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.δ (f₁ ≫ f₂) f₃₄ n₁ n₂ hn₂ ≫
      X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.iCycles f₁ f₂ n₂ ≫ (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) =
    X.toCycles f₃ f₄ f₃₄ h₃₄ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫
        X.ιE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.fromOpcycles f₄ f₅ f₄₅ h₄₅ 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₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.δ (f₁ ≫ f₂) f₃₄ n₁ n₂ hn₂ ≫ (X.H n₂).map (twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯) ≫ (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) =
    X.toCycles f₃ f₄ f₃₄ h₃₄ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫
        X.ιE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.fromOpcycles f₄ f₅ f₄₅ h₄₅ n₁ ≫ X.δ f₂₃ f₄₅ n₁ n₂ hn₂
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₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.δ (f₁ ≫ f₂) f₃₄ n₁ n₂ hn₂ ≫ (X.H n₂).map (twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯) ≫ (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) =
    X.toCycles f₃ f₄ f₃₄ h₃₄ n₁ ≫ X.iCycles f₃ f₄ n₁ ≫ X.δ f₂₃ f₄ n₁ n₂ ⋯

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₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.δ (f₁ ≫ f₂) f₃₄ n₁ n₂ hn₂ ≫ (X.H n₂).map (twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯) ≫ (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) =
    (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) ≫ X.δ f₂₃ f₄ n₁ n₂ ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂ ≫
      X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ =
    0

Tactic:
simp [← cancel_mono (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃),
    ← cancel_mono (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₂),
    X.d_ιE_fromOpcycles f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ _ rfl _ rfl n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃, X.map_ιE_assoc
    f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) (𝟙 _) n₀ n₁ n₂ (by cat_disch) hn₁ hn₂]

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₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : 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.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.iCycles f₁ f₂ n₂ ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂

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₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : 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.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ (X.H n₂).map (twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯) ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
A : C
x : A ⟶ (X.H n₁).obj (mk₁ f₂₃)
h : x ≫ (X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃) = 0
hn₂ : n₁ + 1 = n₂
h' : x ≫ X.δ f₁ f₂₃ n₁ n₂ hn₂ = 0
hn₁ : n₀ + 1 = n₁
⊢ X.liftE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ x h hn₂ h' hn₁ ≫ X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁ =
    x

Tactic:
by
  apply (X.kernelSequenceE_exact f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).lift_f

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₁₂
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
f₁₂' : i₀' ⟶ i₂'
h₁₂' : f₁' ≫ f₂' = f₁₂'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁₂ f₃ ⟶ mk₂ f₁₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : β.app 0 = α.app 0
h₁ : β.app 1 = α.app 2
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫
      X.iCycles f₁ f₂ n₁ ≫
        (X.H n₁).map
            (homMk₁ ((homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯).app 1)
              ((homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯).app 2) ⋯) ≫
          X.pOpcycles f₂' f₃' n₁ =
    X.pOpcycles f₁₂ f₃ n₁ ≫
      X.opcyclesMap f₁₂ f₃ f₁₂' f₃' β n₁ ≫ X.opcyclesMap f₁₂' f₃' f₂' f₃' (threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂') n₁

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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
f₁₂' : i₀' ⟶ i₂'
h₁₂' : f₁' ≫ f₂' = f₁₂'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁₂ f₃ ⟶ mk₂ f₁₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : β.app 0 = α.app 0
h₁ : β.app 1 = α.app 2
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₁).map (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) ≫
      (X.H n₁).map
          (homMk₁ ((homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯).app 1) ((homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯).app 2)
            ⋯) ≫
        X.pOpcycles f₂' f₃' n₁ =
    X.pOpcycles f₁₂ f₃ n₁ ≫
      X.opcyclesMap f₁₂ f₃ f₁₂' f₃' β n₁ ≫ X.opcyclesMap f₁₂' f₃' f₂' f₃' (threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂') n₁
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsArtinian R M
inst✝ : IsScalarTower S R M
H : Function.Surjective ⇑(algebraMap S R)
⊢ Function.Injective fun N ↦
    let __AddSubmonoid := N.toAddSubmonoid;
    { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }

pp: case refine_3
R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsArtinian R M
inst✝ : IsScalarTower S R M
H : Function.Surjective ⇑(algebraMap S R)
⊢ ∀ {a b : Submodule S M},
    {
            toFun := fun N ↦
              let __AddSubmonoid := N.toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            inj' := ?refine_2 }
          a ≤
        {
            toFun := fun N ↦
              let __AddSubmonoid := N.toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            inj' := ?refine_2 }
          b ↔
      a ≤ b

Tactic:
· intro N1 N2 h
    rwa [Submodule.ext_iff] at h ⊢

Goal state after:
case refine_3
R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsArtinian R M
inst✝ : IsScalarTower S R M
H : Function.Surjective ⇑(algebraMap S R)
⊢ ∀ {a b : Submodule S M},
    {
            toFun := fun N ↦
              let __AddSubmonoid := N.toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            inj' := ⋯ }
          a ≤
        {
            toFun := fun N ↦
              let __AddSubmonoid := N.toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            inj' := ⋯ }
          b ↔
      a ≤ b
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: L : Type v
inst✝ : LieRing L
x y z : L
⊢ ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + -⁅z, -⁅x, y⁆⁆ = 0

Tactic:
lie_skew y x,

Goal state after:
L : Type v
inst✝ : LieRing L
x y z : L
⊢ ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + -⁅z, ⁅y, x⁆⁆ = 0
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
M : Type w₁
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : LieRingModule L₂ M
f : L₁ →ₗ⁅R⁆ L₂
inst✝¹ : Module R M
inst✝ : LieModule R L₂ M
t : R
x : L₁
m : M
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
simp only [LieRingModule.compLieHom_apply, lie_smul]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : Semiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
H : IsArtinianRing R
⊢ IsArtinianRing S

Tactic:
rw [isArtinianRing_iff] at H ⊢

Goal state after:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : Semiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
H : IsArtinian R R
⊢ IsArtinian S S
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
a : R
ha : a ∈ R⁰
⊢ IsUnit a

Tactic:
rwa [isUnit_iff_isRegular, isRegular_iff_mem_nonZeroDivisors]

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
p : Submodule R M
⊢ (∃ N, ↑N = p) ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p

Tactic:
constructor
  · rintro ⟨N, rfl⟩ _ _; exact N.lie_mem
  · intro h; use { p with lie_mem := @h }

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'✝ N N' : LieSubmodule R L M
x : L
y : M
hy : y ∈ ↑N
z : M
hz : z ∈ ↑N'
⊢ ∃ y_1 ∈ ↑N, ∃ z_1 ∈ ↑N', y_1 + z_1 = ⁅x, y + z⁆

Tactic:
exact ⟨⁅x, y⁆, N.lie_mem hy, ⁅x, z⁆, N'.lie_mem hz, (lie_add _ _ _).symm⟩

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
m : M
x : L
n : ↥N
hx✝ : x ∈ ⊥
hx : x = 0
hn : ⁅↑⟨x, hx✝⟩, ↑n⁆ = m
⊢ ⁅↑⟨x, hx✝⟩, ↑n⁆ ∈ ↑⊥

Tactic:
simp [hx]

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ maxTrivEquiv LieModuleEquiv.refl = LieModuleEquiv.refl

Tactic:
by
  ext; simp only [coe_maxTrivEquiv_apply, LieModuleEquiv.refl_apply]

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

Goal state before:
pp: case hp2
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : (Polynomial.aeval x) p = 0
this : p.leadingCoeff ≠ 0
⊢ (Polynomial.aeval x) (p * C p.leadingCoeff⁻¹) = 0

pp: case hp3
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : (Polynomial.aeval x) p = 0
this : p.leadingCoeff ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).Monic

Tactic:
· rw [aeval_mul, hp2, zero_mul]

Goal state after:
case hp3
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : (Polynomial.aeval x) p = 0
this : p.leadingCoeff ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).Monic
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
h : ↑U ⊆ -x +ᵥ y +ᵥ ↑U
⊢ x - y ∈ U

Tactic:
vadd_vadd,

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
h : ↑U ⊆ (-x + y) +ᵥ ↑U
⊢ x - y ∈ U
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
h : x - y ∈ U
⊢ ↑U ⊆ -x +ᵥ y +ᵥ ↑U

Tactic:
vadd_vadd,

Goal state after:
case refine_2
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
h : x - y ∈ U
⊢ ↑U ⊆ (-x + y) +ᵥ ↑U
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
⊢ RingHom.ker (evalRingHom x) = Ideal.span {X - C x}

Tactic:
by
  ext y
  simp [Ideal.mem_span_singleton, dvd_iff_isRoot, RingHom.mem_ker]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: case mp.add
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)
ha' : ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑a
hb' : ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑b
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑(a + b)

Tactic:
| add a b ha hb ha' hb' =>

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B✝ : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : Algebra A B✝
K : Type u_6
inst✝¹ : Field K
ι : Type u_7
inst✝ : Fintype ι
B : Basis ι R S
x : S
e : ι ≃ Fin (Fintype.card ι)
hx : ∀ (i : ι), B i = x ^ ↑(e i)
i : Fin (Fintype.card ι)
⊢ (B.reindex e) i = x ^ ↑i

Tactic:
simp [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
pb : PowerBasis A S
⊢ ((pb.basis.repr (pb.gen ^ pb.dim)).sum fun i a ↦ a • pb.basis i) =
    ∑ x, (pb.basis.repr (pb.gen ^ pb.dim)) x • pb.gen ^ ↑x

Tactic:
Finsupp.sum_fintype

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
⊢ ∑ i, (pb.basis.repr (pb.gen ^ pb.dim)) i • pb.basis i = ∑ x, (pb.basis.repr (pb.gen ^ pb.dim)) x • pb.gen ^ ↑x

case h
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ ∀ (i : Fin pb.dim), 0 • pb.basis i = 0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
x : S
hx : B.gen ∈ R[x]
⊢ {B.gen} ⊆ ↑R[x]

Tactic:
simp [hx]

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : ¬IsUnit x
⊢ n = 0 ∨ n = 1

Tactic:
by
  contrapose! h'
  replace h' : 2 ≤ n := by lia
  have : x * x ∣ x ^ n := by rw [← sq]; exact pow_dvd_pow x h'
  exact h.squarefree_of_dvd this x (refl _)

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
x y : ι
hfs : ((X - C (f y)) ^ 2 * ∏ x ∈ (s.erase x).erase y, (X - C (f x))).Separable
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False

Tactic:
cases (hfs.of_mul_left.of_pow (not_isUnit_X_sub_C _) two_ne_zero).2

Goal state after:
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
ι' : Type u_7
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
tb : Trunc (Basis ι A M)
b' : Basis ι' A M
f : M →ₗ[A] M
⊢ (detAux tb) f = ((toMatrix b' b') f).det

Tactic:
by
  induction tb using Trunc.induction_on with
  | h b => rw [detAux_def', det_toMatrix_eq_det_toMatrix b b']

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
hn : n ≠ 0
⊢ (expand F (p ^ n)) (derivative f) * (↑(p ^ n) * X ^ (p ^ n - 1)) = 0

Tactic:
Nat.cast_pow,

Goal state after:
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
hn : n ≠ 0
⊢ (expand F (p ^ n)) (derivative f) * (↑p ^ n * X ^ (p ^ n - 1)) = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f p : R[X]
⊢ (mk f) (Polynomial.map (algebraMap R R) p) = (mk f) p

Tactic:
Algebra.algebraMap_self,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f p : R[X]
⊢ (mk f) (Polynomial.map (RingHom.id R) p) = (mk f) p
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:
| inr l =>

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ (quotEquivOfEq ⋯).symm ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) x) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) x

Tactic:
Ideal.quotEquivOfEq_symm

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ (quotEquivOfEq ⋯) ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) x) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) x
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
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this✝ : IsReduced R
this : FiniteDimensional K R
⊢ f.IsSemisimple

Tactic:
have : IsArtinianRing R := .of_finite K R

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
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this✝¹ : IsReduced R
this✝ : FiniteDimensional K R
this : IsArtinianRing R
⊢ f.IsSemisimple
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 g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝¹ : Module.Finite K R
this✝ : Module.Finite R S
this : Module.Finite K S
⊢ a.IsSemisimple

Tactic:
have : IsArtinianRing R := .of_finite K R

Goal state after:
M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝² : Module.Finite K R
this✝¹ : Module.Finite R S
this✝ : Module.Finite K S
this : IsArtinianRing R
⊢ a.IsSemisimple