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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
j' : ι'
i : ι
hj' : ∃ j, e.f j = j'
⊢ (h.ofExtend.extend e).hom (e.f i) j' = h.hom (e.f i) j'

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
j' : ι'
i : ι
hj' : ¬∃ j, e.f j = j'
⊢ (h.ofExtend.extend e).hom (e.f i) j' = h.hom (e.f i) j'

Tactic:
· obtain ⟨j, rfl⟩ := hj'
      simp [extend_hom_eq _ e rfl rfl, ofExtend_hom]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
j' : ι'
i : ι
hj' : ¬∃ j, e.f j = j'
⊢ (h.ofExtend.extend e).hom (e.f i) j' = h.hom (e.f i) j'
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K : CochainComplex C ℤ
n : ℤ
⊢ (Q.obj K).IsLE n ↔ K.IsLE n

Tactic:
have eq := fun i ↦ ((homologyFunctorFactors C i).app K).isZero_iff
  simp only [Functor.comp_obj, HomologicalComplex.homologyFunctor_obj] at eq
  simp only [isLE_iff, CochainComplex.isLE_iff,
    HomologicalComplex.exactAt_iff_isZero_homology, eq]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : (cofibrations C).IsStableUnderRetracts
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (trivialCofibrations C).IsStableUnderRetracts

Tactic:
dsimp [trivialCofibrations]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Localization.OfQuotient

Goal state before:
pp: case h_map.mk
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
r : HomRel C
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Quotient r ⥤ E
h : functor r ⋙ F₁ = functor r ⋙ F₂
X Y : C
f✝ : { as := X } ⟶ { as := Y }
f : { as := X }.as ⟶ { as := Y }.as
⊢ F₁.map (Quot.mk (HomRel.CompClosure r) f) = eqToHom ⋯ ≫ F₂.map (Quot.mk (HomRel.CompClosure r) f) ≫ eqToHom ⋯

Tactic:
exact Functor.congr_hom h f

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
A : Type u_3
inst✝¹ : Category.{v_3, u_3} A
inst✝ : Abelian A
K : Plus C
⊢ (quotient C).essImage K

Tactic:
by
    obtain ⟨L, rfl⟩ := quotient_obj_surjective K
    exact ⟨L, ⟨Iso.refl _⟩⟩

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

Goal state before:
pp: case hY
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
hL : IsZero L
n : ℤ
⊢ IsZero (L.X n)

Tactic:
exact (HomologicalComplex.eval _ _ n).map_isZero hL

Goal state after:
Module: Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant

Goal state before:
pp: C : Type u_1
J : Type u_2
ι : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} J
c : ComplexShape ι
inst✝³ : IsCofiltered J
inst✝² : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝¹ : ∀ (j : ι), HasLimit (F ⋙ eval C c j)
cF : Cone F
hcF : IsLimit cF
inst✝ : CategoryWithHomology C
q₀ q₁ q₂ : ι
h₀ : c.prev q₁ = q₀
h₂ : c.next q₁ = q₂
j : J
hq₀ : (F ⋙ eval C c q₀).IsEventuallyConstantTo j
hq₁ : (F ⋙ eval C c q₁).IsEventuallyConstantTo j
hq₂ : (F ⋙ eval C c q₂).IsEventuallyConstantTo j
φ : (shortComplexFunctor' C c q₀ q₁ q₂).obj (((Functor.const J).obj cF.pt).obj j) ⟶
  (shortComplexFunctor' C c q₀ q₁ q₂).obj (F.obj j) :=
  (shortComplexFunctor' C c q₀ q₁ q₂).map (cF.π.app j)
this✝¹ : IsIso φ.τ₁
this✝ : IsIso φ.τ₂
this : IsIso φ.τ₃
⊢ ShortComplex.QuasiIso ((shortComplexFunctor' C c q₀ q₁ q₂).map (cF.π.app j))

Tactic:
apply ShortComplex.quasiIso_of_epi_of_isIso_of_mono

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Quotient

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
W : MorphismProperty C
homRel : HomRel C
inst✝² : HomRel.IsStableUnderPrecomp homRel
inst✝¹ : HomRel.IsStableUnderPostcomp homRel
inst✝ : W.HasQuotient homRel
⊢ W = (W.quotient homRel).inverseImage (Quotient.functor homRel)

Tactic:
by
  ext
  exact (quotient_iff _ _ _).symm

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
⊢ (cokernel f).IsGE n

Tactic:
rw [isGE_iff]
  intro i hi
  rw [exactAt_iff_isZero_homology]
  refine ((shortExact f).homology_exact₃ i (i + 1) (by simp)).isZero_X₂ ?_ ?_
  · have := hf i hi
    rw [← ((shortExact f).homology_exact₂ i).epi_f_iff]
    infer_instance
  · rw [← ((shortExact f).homology_exact₁ i (i + 1) (by simp)).mono_g_iff]
    by_cases hi' : i + 1 < n
    · have := hf (i + 1) (by lia)
      infer_instance
    · obtain rfl : n = i + 1 := by lia
      infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.StructuredArrowRightwards g
φ : f₁ ⟶ f₂
⊢ (CostructuredArrow.mk (StructuredArrow.homMk (StructuredArrow.right f₁).hom ⋯)).left.hom ≫
      T.map (StructuredArrow.Hom.right φ).left =
    (CostructuredArrow.mk (StructuredArrow.homMk (StructuredArrow.right f₂).hom ⋯)).left.hom

Tactic:
by dsimp; rw [← StructuredArrow.w φ]; rfl

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.embeddingUpIntGE 0).f (n - 1) = m - 1

Tactic:
have := NeZero.ne n

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
this : n ≠ 0
⊢ (ComplexShape.embeddingUpIntGE 0).f (n - 1) = m - 1
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n - 1) = m + 1

Tactic:
have := NeZero.ne n

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
this : n ≠ 0
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n - 1) = m + 1
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
n : ℕ
⊢ P.complex.d n (n + 1) ≫ P.complex.d (n + 1) (n + 2) = 0

Tactic:
by
  simp

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} ι
inst✝¹ : Abelian C
X : SpectralObject C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
⊢ IsZero ((X.H n).obj (mk₁ f))

Tactic:
by
  let φ := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) (by simp) ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀)
  have : IsIso φ := by
    rw [isIso_iff₁]
    constructor <;> dsimp [φ] <;> infer_instance
  rw [IsZero.iff_id_eq_zero]
  rw [← cancel_mono ((X.H n).map φ), Category.id_comp, zero_comp,
    ← X.zero₂ f (inv f) (𝟙 _) (by simp), ← Functor.map_comp]

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

Goal state before:
pp: case h₁
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₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Epi (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯).τ₁

pp: case h₂
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₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ IsIso (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯).τ₂

pp: case h₃
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₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Mono (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯).τ₃

Tactic:
· exact (X.exact₂ f₃ f₄ f₃₄ h₃₄ _).epi_f h

Goal state after:
case h₂
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₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ IsIso (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯).τ₂

case h₃
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₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Mono (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ 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₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)

Tactic:
apply ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono'
  · dsimp
    convert! (inferInstance : Epi ((X.H n₀).map (𝟙 _)))
    cat_disch
  · dsimp
    convert! (inferInstance : IsIso ((X.H n₁).map (𝟙 _)))
    cat_disch
  · exact (X.exact₂ f₂ f₃ f₂₃ h₂₃ n₂).mono_g h

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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₂₃)
hx₂ : x₂ ≫ biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯) = 0
⊢ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁ ≫ X.δ f₁ f₂₃ n₁ n₂ ⋯ = 0

Tactic:
X.liftOpcycles_fromOpcycles_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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₂₃)
hx₂ : x₂ ≫ biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯) = 0
⊢ x₂ ≫ X.δ f₁ f₂₃ n₁ n₂ ⋯ = 0
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x y✝ z✝ : L
m n : M
y z : L
⊢ { toFun := fun m ↦ ⁅y + z, m⁆, map_zero' := ⋯, map_add' := ⋯ } =
    { toFun := fun m ↦ ⁅y, m⁆, map_zero' := ⋯, map_add' := ⋯ } +
      { toFun := fun m ↦ ⁅z, m⁆, map_zero' := ⋯, map_add' := ⋯ }

Tactic:
by ext n; exact add_lie y z n

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m✝ n : M
x : L
f : M →ₗ[R] N
t : R
m : M
⊢ ⁅x, f (t • m)⁆ - f ⁅x, t • m⁆ = (RingHom.id R) t • (⁅x, f m⁆ - f ⁅x, m⁆)

Tactic:
simp only [smul_sub, map_smul, lie_smul, RingHom.id_apply]

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

Goal state before:
pp: 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
⊢ Jac ^ Nat.zero * N = N

Tactic:
by rw [Jac.pow_zero, N.one_mul]

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

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
x y : L
z : M
⊢ (φ x) ⁅y, z⁆ = ⁅((ad R L) x) y, z⁆ + ⁅y, (φ x) z⁆

Tactic:
by
  simp

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
s : Set L
⊢ Submodule.span R s ≤ (lieSpan R L s).toSubmodule

Tactic:
Submodule.span_le,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
⊢ s ⊆ ↑(lieSpan R L s).toSubmodule
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 M
hs : s = ↑N
⊢ 0 ∈ s

Tactic:
simp [hs]

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'
x : L
⊢ f x ∈ f.idealRange

Tactic:
by
  rw [idealRange_eq_map]
  exact LieIdeal.mem_map (LieSubmodule.mem_top x)

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

Goal state before:
pp: case refine_1
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
i : ι
x : M
hx : x ∈ N i
⊢ ∃ (hx : x ∈ ⨆ i, N i), motive x hx

Tactic:
exact ⟨_, mem _ _ hx⟩

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
⊢ (∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0) → ∀ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, m = 0

Tactic:
rintro h - ⟨⟨x, hx⟩, ⟨⟨n, hn⟩, rfl⟩⟩

Goal state after:
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
h : ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ = 0
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]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = r.leadingCoeff
⊢ r.natDegree ≤ 0

Tactic:
have hr0 : r ≠ 0 := by
      rintro rfl
      exact ne_zero hx (mul_zero p ▸ hr)

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = r.leadingCoeff
hr0 : r ≠ 0
⊢ r.natDegree ≤ 0
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]
⊢ minpoly A x ∣ p ↔ p ∈ A[X] ∙ minpoly A x

Tactic:
Submodule.mem_span_singleton,

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
⊢ minpoly A x ∣ p ↔ ∃ a, a • minpoly A x = p
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₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
hf₁ : f.ker = ⊥
hf₂ : N₂ ≤ f.range
⊢ comap f ⁅I, map f (comap f N₂)⁆ = ⁅I, comap f N₂⁆

Tactic:
rw [← map_bracket_eq, comap_map_eq _ f hf₁]

Goal state after:
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
S : Type u_2
inst✝³ : Ring S
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module S M
U : Submodule R M
V : Submodule S M
h : U.toAddSubgroup ≤ V.toAddSubgroup
x y : M
hxy : x ≡ y [SMOD U]
⊢ x ≡ y [SMOD V]

Tactic:
simp only [SModEq, Submodule.Quotient.eq] at hxy ⊢
  exact h hxy

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ RingHom.ker constantCoeff = Ideal.span {X}

Tactic:
refine le_antisymm (fun p hp ↦ ?_) (by simp [Ideal.span_le])
  simp only [RingHom.mem_ker, constantCoeff_apply, ← Polynomial.X_dvd_iff] at hp
  rwa [Ideal.mem_span_singleton]

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

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

Tactic:
simp [hp, hb']

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

Goal state before:

Tactic:
0 = ⁅L (a + b + c), L ((a + b + c) * (a + b + c))⁆ := by
      rw [(commute_lmul_lmul_sq (a + b + c)).lie_eq]
    _ = _ := by rw [aux0, aux1, aux2, aux3, nsmul_add, nsmul_add]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

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

Tactic:
pb.basis_eq_pow

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

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
⊢ (pb.map e).minpolyGen = pb.minpolyGen

Tactic:
by
  simp

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:
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.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
⊢ Squarefree x ↔ ∀ (p : R), Irreducible p → ¬p * p ∣ x

Tactic:
by
  refine ⟨fun h p hp hp' ↦ hp.not_isUnit (h p hp'), fun h d hd ↦ by_contra fun hdu ↦ ?_⟩
  have hd₀ : d ≠ 0 := ne_zero_of_dvd_ne_zero (ne_zero_of_dvd_ne_zero hx₀ hd) (dvd_mul_left d d)
  obtain ⟨p, irr, dvd⟩ := WfDvdMonoid.exists_irreducible_factor hdu hd₀
  exact h p irr ((mul_dvd_mul dvd dvd).trans hd)

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case prime
K : Type u_1
inst✝¹ : Field K
inst✝ : PerfectField K
p : ℕ
y : K
hp : Nat.Prime p
hchar✝ : CharP K p
⊢ ¬∀ (x : K), ¬(frobenius K p) x = y

Tactic:
apply mt (X_pow_sub_C_irreducible_of_prime hp)

Goal state after:
case prime
K : Type u_1
inst✝¹ : Field K
inst✝ : PerfectField K
p : ℕ
y : K
hp : Nat.Prime p
hchar✝ : CharP K p
⊢ ¬Irreducible (X ^ p - C y)
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case e_a.e_p
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
r x✝ : R
⊢ r ^ p ^ n = x✝ ↔ r = (iterateFrobeniusEquiv R p n).symm x✝

Tactic:
exact (iterateFrobeniusEquiv R p n).eq_symm_apply.symm

Goal state after: