mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map
      (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S.X₁) =
    F.mapDerivedCategoryFactors.hom.app (CochainComplex.mappingCone S.f) ≫
      Q.map
          ((CochainComplex.mappingCone.mapHomologicalComplexIso S.f F).hom ≫
            CochainComplex.mappingCone.descShortComplex (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ)))) ≫
        triangleOfSESδ ⋯ ≫
          (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
            (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)

Tactic:
Functor.map_comp_assoc,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map
      (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S.X₁) =
    F.mapDerivedCategoryFactors.hom.app (CochainComplex.mappingCone S.f) ≫
      Q.map (CochainComplex.mappingCone.mapHomologicalComplexIso S.f F).hom ≫
        Q.map (CochainComplex.mappingCone.descShortComplex (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ)))) ≫
          triangleOfSESδ ⋯ ≫
            (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
              (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map
      (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S.X₁) =
    F.mapDerivedCategoryFactors.hom.app (CochainComplex.mappingCone S.f) ≫
      Q.map
          ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
            (Functor.commShiftIso (F.mapHomologicalComplex (ComplexShape.up ℤ)) 1).hom.app S.X₁) ≫
        (Functor.commShiftIso Q 1).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj S.X₁) ≫
          (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
            (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)

Tactic:
Functor.map_comp_assoc,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map
      (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S.X₁) =
    F.mapDerivedCategoryFactors.hom.app (CochainComplex.mappingCone S.f) ≫
      Q.map ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle S.f).mor₃) ≫
        Q.map ((Functor.commShiftIso (F.mapHomologicalComplex (ComplexShape.up ℤ)) 1).hom.app S.X₁) ≫
          (Functor.commShiftIso Q 1).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj S.X₁) ≫
            (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
              (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: 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₁
k k' : ι
hk : k = i₀ ∧ k' = i₁ ∧ i₀ ≠ i₁
⊢ X₁ = if k' = i₀ then X₀ else if k' = i₁ then X₁ else 0

Tactic:
rw [if_neg, if_pos hk.2.1]
        aesop

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| η.app X✝.obj ≫ (shiftFunctor D 1).map (F.map f.f)

pp: case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| F.map X✝.d

Tactic:
← Functor.comp_map F (shiftFunctor D (1 : S)),

Goal state after:
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| η.app X✝.obj ≫ (F ⋙ shiftFunctor D 1).map f.f

case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| F.map X✝.d
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: 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
⊢ FunctorExtension₁.map (φ ≫ φ') = FunctorExtension₁.map φ ≫ FunctorExtension₁.map φ'

Tactic:
ext P
    simp only [comp_f, FunctorExtension₁.map_app_f, NatTrans.comp_app, assoc]
    have h := φ.naturality P.p
    have h' := F.congr_map P.idem
    simp only [hom_ext_iff, comp_f, F.map_comp] at h h'
    slice_rhs 2 3 => rw [← h]
    slice_rhs 1 2 => rw [h']
    simp only [assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
n : ℕ
g : P.complex.X n ⟶ Q.complex.X n
g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 1)
w : g' ≫ Q.complex.d (n + 1) n = P.complex.d (n + 1) n ≫ g
⊢ (P.complex.d (n + 2) (n + 1) ≫ g') ≫
      { X₁ := Q.complex.X (n + 2), X₂ := Q.complex.X (n + 1), X₃ := Q.complex.X n, f := Q.complex.d (n + 2) (n + 1),
          g := Q.complex.d (n + 1) n, zero := ⋯ }.g =
    0

Tactic:
simp [w]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
f : P.complex ⟶ Q.complex
n : ℕ
g : P.complex.X n ⟶ Q.complex.X (n + 1)
g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)
w : f.f (n + 1) = P.complex.d (n + 1) n ≫ g + g' ≫ Q.complex.d (n + 2) (n + 1)
⊢ (f.f (n + 2) - P.complex.d (n + 2) (n + 1) ≫ g') ≫
      { X₁ := Q.complex.X (n + 1 + 2), X₂ := Q.complex.X (n + 1 + 1), X₃ := Q.complex.X (n + 1),
          f := Q.complex.d (n + 1 + 2) (n + 1 + 1), g := Q.complex.d (n + 1 + 1) (n + 1), zero := ⋯ }.g =
    0

Tactic:
simp [w]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: case g_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
⊢ (((projectiveResolution X).homotopyEquiv P).inv ≫ lift f (projectiveResolution X) (projectiveResolution Y)) ≫
      (projectiveResolution Y).π =
    P.π ≫ (ChainComplex.single₀ C).map f

pp: case h_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
⊢ (φ ≫ ((projectiveResolution Y).homotopyEquiv Q).inv) ≫ (projectiveResolution Y).π =
    P.π ≫ (ChainComplex.single₀ C).map f

Tactic:
all_goals
    cat_disch

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 : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ P.π.f 0 ≫ ((ChainComplex.single₀ C).map f).f 0 = P.π.f 0 ≫ f

Tactic:
ChainComplex.single₀_map_f_zero

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 : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ P.π.f 0 ≫ f = P.π.f 0 ≫ f
Module: Mathlib.CategoryTheory.Triangulated.SpectralObject

Goal state before:
pp: case e'_2
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
w✝² w✝¹ w✝ : ι'
f : w✝² ⟶ w✝¹
g : w✝¹ ⟶ w✝
this :
  X.ω₁.map (homMk₁ (𝟙 (F.obj w✝¹)) (𝟙 (F.obj w✝)) ⋯) ≫ X.δ'.app (mk₂ (F.map f) (F.map g)) =
    X.δ'.app ((F.mapComposableArrows 2).obj (mk₂ f g)) ≫
      (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (𝟙 (F.obj w✝²)) (𝟙 (F.obj w✝¹)) ⋯))
⊢ X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso f).inv ≫ (isoMk₁ (Iso.refl (F.obj w✝²)) (Iso.refl (F.obj w✝¹)) ⋯).hom) =
    X.ω₁.map (homMk₁ (𝟙 (F.obj w✝²)) (𝟙 (F.obj w✝¹)) ⋯)

Tactic:
congr; cat_disch

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

Goal state before:
pp: I : Type u
inst✝⁵ : AddMonoid I
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝² : X₃.HasTensor X₄
inst✝¹ : X₂.HasTensor (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₂₃₄
⊢ ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h =
    X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ hi ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j ⋯

Tactic:
subst hi
  rfl

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'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
α' : mk₂ f' g' ⟶ mk₂ f'' g''
n : ℤ
⊢ X.cyclesMap f g f' g' α n ≫ X.cyclesMap f' g' f'' g'' α' n = X.cyclesMap f g f'' g'' (α ≫ α') n

Tactic:
rw [← cancel_mono (X.iCycles f'' g'' n), Category.assoc,
    X.cyclesMap_i f' g' f'' g'' α' _ n rfl,
    X.cyclesMap_i_assoc f g f' g' α _ n rfl,
    ← Functor.map_comp]

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'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
α' : mk₂ f' g' ⟶ mk₂ f'' g''
n : ℤ
⊢ X.iCycles f g n ≫ (X.H n).map (homMk₁ (α.app 1) (α.app 2) ⋯ ≫ homMk₁ (α'.app 1) (α'.app 2) ⋯) =
    X.cyclesMap f g f'' g'' (α ≫ α') n ≫ X.iCycles f'' g'' n
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
n : ℕ
⊢ Function.Injective fun x ↦
    match x with
    | ⟨(i₁, i₂, i₃), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩, ⟨i₃, ⋯⟩)

Tactic:
intro _

Goal state after:
I : Type u
inst✝² : AddMonoid I
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
n : ℕ
a₁✝ : ↑{i | i.1 + i.2.1 + i.2.2 = n}
⊢ ∀ ⦃a₂ : ↑{i | i.1 + i.2.1 + i.2.2 = n}⦄,
    (fun x ↦
            match x with
            | ⟨(i₁, i₂, i₃), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩, ⟨i₃, ⋯⟩))
          a₁✝ =
        (fun x ↦
            match x with
            | ⟨(i₁, i₂, i₃), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩, ⟨i₃, ⋯⟩))
          a₂ →
      a₁✝ = a₂
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₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ ∀ ⦃A : C⦄
    (x₂ :
      A ⟶
        { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
            g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.X₂),
    x₂ ≫
          { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
              g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.g =
        0 →
      ∃ A' π,
        ∃ (_ : Epi π),
          ∃ x₁,
            π ≫ x₂ =
              x₁ ≫
                { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁,
                    f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁,
                    zero := ⋯ }.f

Tactic:
intro _

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₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A✝ : C
⊢ ∀
    (x₂ :
      A✝ ⟶
        { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
            g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.X₂),
    x₂ ≫
          { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
              g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.g =
        0 →
      ∃ A' π,
        ∃ (_ : Epi π),
          ∃ x₁,
            π ≫ x₂ =
              x₁ ≫
                { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁,
                    f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁,
                    zero := ⋯ }.f
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: ι : Type u_2
κ : Type u_3
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq' : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
⊢ i₁ ≤ i₂

Tactic:
simpa only [hi₁, hi₂] using data.le₁₂ pq'

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₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).Exact

Tactic:
by
  let φ : X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⟶
      (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂) :=
    { τ₁ := X.pOpcycles f₁ f₂₃ n₁
      τ₂ := 𝟙 _
      τ₃ := 𝟙 _
      comm₁₂ := by
        dsimp
        rw [Category.comp_id, X.p_opcyclesMap _ _ _ _ _ (twoδ₂Toδ₁ f₁ f₂ f₁₂)] }
  rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ]
  exact X.cokernelSequenceOpcyclesE_exact f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂

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

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
⊢ ∀ {α β : Type u_5} (a : α ≃ β),
    (∀ {M : α → Submodule R P} [∀ (i : α), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)) →
      ∀ {M : β → Submodule R P} [∀ (i : β), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)

Tactic:
intro _

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
α✝ : Type u_5
⊢ ∀ {β : Type u_5} (a : α✝ ≃ β),
    (∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)) →
      ∀ {M : β → Submodule R P} [∀ (i : β), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
⊢ ∀ {α : Type u_5} [Fintype α],
    (∀ {M : α → Submodule R P} [∀ (i : α), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)) →
      ∀ {M : Option α → Submodule R P} [∀ (i : Option α), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)

Tactic:
intro _

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
α✝ : Type u_5
⊢ ∀ [Fintype α✝],
    (∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)) →
      ∀ {M : Option α✝ → Submodule R P} [∀ (i : Option α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
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
L' : LieSubalgebra R L
⊢ ∀ (x y z : ↥L'), ⟨⁅↑(x + y), ↑z⁆, ⋯⟩ = ⟨⁅↑x, ↑z⁆, ⋯⟩ + ⟨⁅↑y, ↑z⁆, ⋯⟩

Tactic:
intros
    apply SetCoe.ext
    apply add_lie

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 (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), ↑K ⊆ ↑K' ↔ K ≤ K'
⊢ IsGLB (SetLike.coe '' S) (⋂ s ∈ S, ↑s)

Tactic:
exact isGLB_biInf

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∃ I, LieIdeal.toLieSubalgebra R (↥K') I = ofLe h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

Tactic:
simp only [exists_lieIdeal_coe_eq_iff, coe_bracket, mem_ofLe]
  constructor
  · intro h' x y hx hy; exact h' ⟨x, hx⟩ ⟨y, h hy⟩ hy
  · rintro h' ⟨x, hx⟩ ⟨y, hy⟩ hy'; exact h' x y hx hy'

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

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

Tactic:
by
  unfold map
  gcongr; exact h

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

Goal state before:
pp: case refine_2.lie
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
u v : L
hx✝ : u ∈ lieSpan R L s
hy✝ : v ∈ lieSpan R L s
hu : ⁅⟨u, hx✝⟩, ⟨y, hy⟩⁆ = 0
hv : ⁅⟨v, hy✝⟩, ⟨y, hy⟩⁆ = 0
⊢ ⁅⟨⁅u, v⁆, ⋯⟩, ⟨y, hy⟩⁆ = 0

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

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
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
hne : Nonempty ↑s
this : ↑(⨆ i, ↑i) = ⋃ i ∈ s, ↑i
⊢ ↑(sSup s) = ⋃ N ∈ s, ↑N

Tactic:
rw [← this, SetLike.coe_set_eq, sSup_eq_iSup, iSup_subtype]

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieRing L'
inst✝⁶ : LieAlgebra R L'
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
x : L
m' : M'
h : m' ∈ (Submodule.map ↑f ↑N).carrier
⊢ ⁅x, m'⁆ ∈ (Submodule.map ↑f ↑N).carrier

Tactic:
rcases h with ⟨m, hm, hfm⟩; use ⁅x, m⁆; constructor
      · apply N.lie_mem hm
      · norm_cast at hfm; simp [hfm]

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

Goal state before:
pp: case inl
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 : (minpoly A x).leadingCoeff = (p * r).leadingCoeff
⊢ p = p * r

Tactic:
rw [mul_comm, leadingCoeff_mul_monic hm, (monic hx).leadingCoeff] at hlead

Goal state after:
case inl
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
⊢ p = p * r
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: R : Type u_6
inst✝ : CommRing R
I : Ideal R
x y : R
h : x ≡ y [SMOD I]
f : R[X]
⊢ Polynomial.eval x f ≡ Polynomial.eval y f [SMOD I]

Tactic:
by
  simp_rw [Polynomial.eval_eq_sum, Polynomial.sum]
  gcongr

Goal state after: