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

Goal state before:
pp: case neg
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₁
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi : ¬i = i₀
⊢ ((if hk : i = i₀ ∧ j = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) ≫
      if hk : j = i₀ ∧ k = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) =
    0

Tactic:
rw [dif_neg (by tauto), zero_comp]

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

Goal state before:
pp: case a
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 : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (φ.app x✝.X).f = (φ.app x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map f.f).f ≫ (F.map x✝.p).f

pp: case a
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 : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (φ.app x✝.X).f = (φ.app x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (φ.app x✝.X).f

Tactic:
rw [h']

Goal state after:
case a
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 : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (φ.app x✝.X).f = (φ.app x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map f.f).f

case a
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 : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (φ.app x✝.X).f = (φ.app x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (φ.app x✝.X).f
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: case a.a
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 H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f ≫ (F.map P.p).f

pp: case a.a
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 H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (φ.app P.X).f

pp: case a
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 H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (φ'.app P.X).f

Tactic:
rw [h']

Goal state after:
case a.a
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 H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f

case a.a
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 H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (φ.app P.X).f

case a
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 H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (φ'.app P.X).f
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 n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
p'' : ℤ
hp'' : p + 1 = p''
g : K.X p'' ⟶ X
hf : K.d p' p ≫ K.d p p'' ≫ g = 0
⊢ δ (n - 1) n (n.negOnePow • Cochain.toSingleMk g ⋯) = ↑(toSingleMk (K.d p p'' ≫ g) h p' hp' hf)

Tactic:
by simp [Cochain.δ_toSingleMk _ _ _ _ h, smul_smul]

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
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
⊢ (NatTrans.leftDerivedToHomotopyCategory α).app X =
    (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) ≫
        (P.isoLeftDerivedToHomotopyCategoryObj G).inv

Tactic:
rw [← cancel_mono (P.isoLeftDerivedToHomotopyCategoryObj G).hom, assoc, assoc,
      Iso.inv_hom_id, comp_id]

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
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
⊢ (NatTrans.leftDerivedToHomotopyCategory α).app X ≫ (P.isoLeftDerivedToHomotopyCategoryObj G).hom =
    (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ (a • φ₁).τ₂ = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + (a • φ₂).τ₂

Tactic:
dsimp
    rw [h.comm₂]
    simp only [smul_add, Linear.comp_smul, Linear.smul_comp]

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
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ i₁ + (i₂ + i₃) = j

Tactic:
← add_assoc,

Goal state after:
I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ i₁ + i₂ + i₃ = j
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
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₂₃ : I
h' : i₂ + i₃ = i₂₃
⊢ i₁ + (i₂ + i₃) = j

Tactic:
← add_assoc,

Goal state after:
I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₂₃ : I
h' : i₂ + i₃ = i₂₃
⊢ i₁ + i₂ + i₃ = j
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 (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
⊢ i₁ + (i₂ + i₃ + i₄) = i₁ + i₂ + i₃ + i₄

Tactic:
← add_assoc,

Goal state after:
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 (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
⊢ i₁ + (i₂ + i₃) + i₄ = i₁ + i₂ + i₃ + i₄
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 (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
i₂₃₄ : I
hi : i₂ + i₃ + i₄ = i₂₃₄
⊢ i₁ + (i₂ + i₃ + i₄) = j

Tactic:
← add_assoc,

Goal state after:
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 (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
i₂₃₄ : I
hi : i₂ + i₃ + i₄ = i₂₃₄
⊢ i₁ + (i₂ + i₃) + i₄ = j
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 (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
i₂₃₄ : I
hi : i₂ + i₃ + i₄ = i₂₃₄
⊢ i₁ + (i₂ + i₃) + i₄ = j

Tactic:
← add_assoc,

Goal state after:
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 (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
i₂₃₄ : I
hi : i₂ + i₃ + i₄ = i₂₃₄
⊢ i₁ + i₂ + i₃ + i₄ = j
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:
← add_assoc,

Goal state after:
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
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ⇑f
h : ¬Surjective ⇑f
⊢ ¬IsArtinian R M

Tactic:
rw [IsArtinian, WellFoundedLT, isWellFounded_iff]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ⇑f
h : ¬Surjective ⇑f
⊢ ¬WellFounded fun x1 x2 ↦ x1 < x2
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⁆

Tactic:
rw [← sub_eq_zero, sub_neg_eq_add, ← add_lie]
  simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n * (x * y - 1) = 0
⊢ ∃ b, x * b = 1

Tactic:
mul_eq_zero,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n = 0 ∨ x * y - 1 = 0
⊢ ∃ b, x * b = 1
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
S : Set (LieSubalgebra R L)
⊢ ↑(sInf S) = ⋂ s ∈ S, ↑s

Tactic:
by
  rw [← coe_toSubmodule, sInf_toSubmodule, Submodule.coe_sInf]
  ext x
  simp

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'
⊢ (↑f).ker = ⊥ ↔ Function.Injective ⇑f

Tactic:
LinearMap.ker_eq_bot,

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'
⊢ Function.Injective ⇑↑f ↔ Function.Injective ⇑f
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
S : Set (LieSubmodule R L M)
⊢ ↑(sInf S) = ⨅ N ∈ S, ↑N

Tactic:
by
  rw [sInf_toSubmodule, ← Set.image, sInf_image]

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 : LieIdeal R L
inst✝ : LieModule R L M
⊢ ↑⁅I, N⁆ = Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Tactic:
by
  rw [lieIdeal_oper_eq_linear_span]
  congr
  ext m
  constructor
  · rintro ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩
    exact ⟨x, hx, n, hn, rfl⟩
  · rintro ⟨x, hx, n, hn, rfl⟩
    exact ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩

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' : LieSubmodule R L M
S : Set (LieSubmodule R L M)
x : L
m : M
s : Finset (Submodule R M)
hs : ↑s ⊆ {x | ∃ p ∈ S, ↑p = x}
hsm : m ∈ ⨆ i ∈ s, i
⊢ ⁅x, m⁆ ∈ sSup {x | ∃ p ∈ S, ↑p = x}

Tactic:
induction s using Finset.induction_on generalizing m with

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

Goal state before:
pp: case refine_2.mem.smul
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
t : R
u : L
hx✝ : u ∈ lieSpan R L s
hu : ⁅⟨w, ⋯⟩, ⟨u, hx✝⟩⁆ = 0
⊢ ⁅⟨w, ⋯⟩, ⟨t • u, ⋯⟩⁆ = 0

Tactic:
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu

Goal state after:
case refine_2.mem.smul
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
t : R
u : L
hx✝ : u ∈ lieSpan R L s
hu : ⁅w, u⁆ = 0
⊢ ⁅⟨w, ⋯⟩, ⟨t • u, ⋯⟩⁆ = 0
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: case refine_2.smul
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x y : L
hy : y ∈ lieSpan R L s
t : R
u : L
hx✝ : u ∈ lieSpan R L s
hu : ⁅⟨u, hx✝⟩, ⟨y, hy⟩⁆ = 0
⊢ ⁅⟨t • u, ⋯⟩, ⟨y, hy⟩⁆ = 0

Tactic:
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu

Goal state after:
case refine_2.smul
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x y : L
hy : y ∈ lieSpan R L s
t : R
u : L
hx✝ : u ∈ lieSpan R L s
hu : ⁅u, y⁆ = 0
⊢ ⁅⟨t • u, ⋯⟩, ⟨y, hy⟩⁆ = 0
Module: Mathlib.Algebra.Lie.Submodule

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

Tactic:
LinearMap.ker_eq_bot,

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ Function.Injective ⇑↑f ↔ Function.Injective ⇑f
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
⊢ x ∈ (algebraMap A B).range

Tactic:
have h : IsIntegral A x := by
    by_contra h
    rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx
    exact ne_of_lt (show ⊥ < ↑1 from WithBot.bot_lt_coe 1) hx
  have key := minpoly.aeval A x
  rw [eq_X_add_C_of_degree_eq_one hx, (minpoly.monic h).leadingCoeff, C_1, one_mul, aeval_add,
    aeval_C, aeval_X, ← eq_neg_iff_add_eq_zero, ← map_neg] at key
  exact ⟨-(minpoly A x).coeff 0, key.symm⟩

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pnz : p ≠ 0
hp : (Polynomial.aeval x) p = 0
⊢ (Polynomial.aeval x) (p * C p.leadingCoeff⁻¹) = 0

Tactic:
by simp [hp]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ (Polynomial.aeval x) (minpoly A x - p) = 0

Tactic:
by simp [hp]

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
⊢ ⁅comap f J₁, comap f J₂⁆ ≤ comap f ⁅J₁, J₂⁆

Tactic:
rw [← map_le_iff_le_comap]
  exact le_trans (map_bracket_le f) (LieSubmodule.mono_lie map_comap_le map_comap_le)

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

Goal state before:
pp: case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
⊢ ¬IsIntegral A (x + (algebraMap A B) a)

Tactic:
refine fun h ↦ hx ?_

Goal state after:
case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
h : IsIntegral A (x + (algebraMap A B) a)
⊢ IsIntegral A x
Module: Mathlib.RingTheory.Polynomial.Ideal

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

Tactic:
rcases dvd_iff_isRoot.mpr h with ⟨p, hp⟩
    rcases @X_sub_C_dvd_sub_C_eval _ b _ P with ⟨q, hq⟩
    exact ⟨C p, q, by rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]⟩

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.degree < ↑d
hy : y = (aeval x) f
hf : f = 0
⊢ f.natDegree < d

Tactic:
simp only [hf, natDegree_zero, Polynomial.degree_zero] at h ⊢

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = (aeval x) f
hf : f = 0
h : ⊥ < ↑d
⊢ 0 < d
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
hf : f = 0
⊢ f.degree < ↑d

Tactic:
simp only [hf, natDegree_zero, Polynomial.degree_zero] at h ⊢

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = (aeval x) f
hf : f = 0
h : 0 < d
⊢ ⊥ < ↑d
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
r : R
⊢ (C r).Separable ↔ IsUnit r

Tactic:
rw [separable_def, derivative_C, isCoprime_zero_right, isUnit_C]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
⊢ f.Separable

Tactic:
obtain ⟨e, hb⟩ := hb.exists_left_inv

Goal state after:
R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb✝ : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
e : R
hb : e * b = 1
⊢ f.Separable
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb✝ : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
e : R
hb : e * b = 1
hderiv : derivative f = C b
⊢ -C b * f + (f * C b + C e * C b) = 1

Tactic:
← add_assoc,

Goal state after:
R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb✝ : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
e : R
hb : e * b = 1
hderiv : derivative f = C b
⊢ -C b * f + f * C b + C e * C b = 1
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι : Type u_7
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
⊢ LinearMap.det 0 = 0

Tactic:
by
  have := Classical.decEq ι
  cases nonempty_fintype ι
  rw [← det_toMatrix b, map_zero, det_zero]

Goal state after: