mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
this✝ : Preadditive D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
this : Preadditive D₂ := Localization.preadditive L₂ B.trW
⊢ ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful

Tactic:
have := Localization.functor_additive L₁ (B.inverseImage A.ι).trW

Goal state after:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
this✝¹ : Preadditive D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
this✝ : Preadditive D₂ := Localization.preadditive L₂ B.trW
this : L₁.Additive
⊢ ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences C)
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ L.map f ≫ L.map (iResolutionObj x✝) = L.map (iResolutionObj x✝¹) ≫ (resolution ⋙ toLocalization L).map f

Tactic:
by
    simpa only [Functor.map_comp] using! L.congr_map (HoCat.resolutionMap_fac f).symm

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

Goal state before:
pp: case mp
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ IsIso α → ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))

pp: case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ (∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))) → IsIso α

Tactic:
· intros
    infer_instance

Goal state after:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ (∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))) → IsIso α
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: case mp
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ IsIso α → ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))

pp: case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ (∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))) → IsIso α

Tactic:
· intros
    infer_instance

Goal state after:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ (∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))) → IsIso α
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
i : ℤ
hi : i ≤ n₀ + ↑q₁
this : ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂), i ≤ n₀ + ↑q₁ → q₁ + 1 = q₂ → IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
k : ℕ
hk : q₁ + k = q₂
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)

Tactic:
induction k generalizing q₁ q₂ with
    | zero =>
      obtain rfl : q₁ = q₂ := by simpa using hk
      simp only [homOfLE_refl, op_id, CategoryTheory.Functor.map_id,
        ObjectProperty.FullSubcategory.id_hom, Factorisation.id_h, id_f]
      infer_instance
    | succ k h =>
      rw [← homOfLE_comp (show q₁ ≤ q₁ + k by lia) (show q₁ + k ≤ q₂ by lia),
        op_comp, Functor.map_comp]
      exact IsIso.comp_isIso' (this _ (by lia) (by lia)) (h _ (by lia) rfl)

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : C₃ ⥤ D₃
E : C₂ ≌ C₃
E' : D₂ ≌ D₃
w' : E.functor ⋙ V₃ ≅ V₂ ⋙ E'.functor
T₁₂ : C₁ ⥤ C₃
B₁₂ : D₁ ⥤ D₃
eT : T₁ ⋙ E.functor ≅ T₁₂
eB : B₁ ⋙ E'.functor ≅ B₁₂
⊢ (w.hComp' w'.hom eT eB).GuitartExact ↔ w.GuitartExact

Tactic:
rw [← hComp_iff_of_equivalences w E E' w', TwoSquare.hComp', whiskerHorizontal_iff]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Abelian C
inst✝⁴ : Category.{v_2, u_2} H
inst✝³ : EnoughInjectives C
F : Plus C ⥤ H
inst✝² : HasDerivedCategory C
F' : DerivedCategory.Plus C ⥤ H
α : F ⟶ DerivedCategory.Plus.Qh ⋙ F'
inst✝¹ : F'.IsRightDerivedFunctor α (quasiIso C)
K : Plus C
inst✝ : ∀ (n : ℤ), Injective (K.obj.as.X n)
this : ∀ (Y : Plus (InjectiveObject C)), IsIso (α.app ((InjectiveObject.ι C).mapHomotopyCategoryPlus.obj Y))
Y : Plus (InjectiveObject C)
e : (InjectiveObject.ι C).mapHomotopyCategoryPlus.obj Y ≅ K
⊢ IsIso (α.app K)

Tactic:
rw [← NatTrans.isIso_app_iff_of_iso α e]

Goal state after:
C : Type u_1
H : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Abelian C
inst✝⁴ : Category.{v_2, u_2} H
inst✝³ : EnoughInjectives C
F : Plus C ⥤ H
inst✝² : HasDerivedCategory C
F' : DerivedCategory.Plus C ⥤ H
α : F ⟶ DerivedCategory.Plus.Qh ⋙ F'
inst✝¹ : F'.IsRightDerivedFunctor α (quasiIso C)
K : Plus C
inst✝ : ∀ (n : ℤ), Injective (K.obj.as.X n)
this : ∀ (Y : Plus (InjectiveObject C)), IsIso (α.app ((InjectiveObject.ι C).mapHomotopyCategoryPlus.obj Y))
Y : Plus (InjectiveObject C)
e : (InjectiveObject.ι C).mapHomotopyCategoryPlus.obj Y ≅ K
⊢ IsIso (α.app ((InjectiveObject.ι C).mapHomotopyCategoryPlus.obj Y))
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₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : k = i₀
⊢ (double f hi₀₁).X k = (double f hi₀₁).X i₀

Tactic:
hk₀

Goal state after:
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₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : k = i₀
⊢ (double f hi₀₁).X i₀ = (double f hi₀₁).X i₀
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₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : k = i₀
⊢ K.X i₀ = K.X k

Tactic:
hk₀

Goal state after:
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₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : k = i₀
⊢ K.X i₀ = K.X i₀
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
α : Cochain K ((singleFunctor C q).obj X) n
⊢ (fun f ↦ toSingleMk f h) ((fun α ↦ α.v p q h ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).hom) α) = α

Tactic:
ext p' q' hpq'
    by_cases hq : q' = q
    · aesop
    · exact (HomologicalComplex.isZero_single_obj_X _ _ _ _ hq).eq_of_tgt _ _

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X 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
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (F.leftDerivedToHomotopyCategory.map f) ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (Q.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) ≫
      HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) n

Tactic:
rw [assoc, ← Functor.map_comp_assoc,
    ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality f P Q φ comm F,
    Functor.map_comp, assoc]

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
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
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map φ) ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
        HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) n
Module: Mathlib.CategoryTheory.GradedObject.Unitor

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

Tactic:
rw [mapBifunctorRightUnitorCofan_inj]

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 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₁
⊢ f₁ ≫ f₂₃ = f₁ ≫ f₂ ≫ f₃

Tactic:
rw [h₂₃]

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
inst✝⁸ : DecidableEq I
inst✝⁷ : HasInitial C
inst✝⁶ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁵ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
X₁ X₃ : GradedObject I C
inst✝⁴ : X₁.HasTensor X₃
inst✝³ : (tensorObj X₁ tensorUnit).HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj tensorUnit X₃)
inst✝¹ : X₁.HasGoodTensor₁₂Tensor tensorUnit X₃
inst✝ : X₁.HasGoodTensorTensor₂₃ tensorUnit X₃
⊢ (associator X₁ tensorUnit X₃).hom ≫ tensorHom (𝟙 X₁) (leftUnitor X₃).hom = tensorHom (rightUnitor X₁).hom (𝟙 X₃)

Tactic:
convert!
    mapBifunctor_triangle (curriedAssociatorNatIso C) (𝟙_ C) (rightUnitorNatIso C)
      (leftUnitorNatIso C) (triangleIndexData I) X₁ X₃ (by simp)
  all_goals assumption

Goal state after:
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₃
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂ f₃
n₀ n₁ n₂ n₃ : ℤ
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hα₃ : α.app 3 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 3)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
this : X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ ⋯ ⋯ ≫ X.ιE f₁' f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ = X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯
⊢ Mono (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ hn₁ hn₂)

Tactic:
exact mono_of_mono_fac this

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

Goal state before:
pp: case h₁
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
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₁ =
    (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)).τ₁

pp: case h₂
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
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₂ =
    (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)).τ₂

pp: case h₃
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
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₃ =
    (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)).τ₃

Tactic:
all_goals dsimp; convert! (X.H _).map_id _; cat_disch

Goal state after:
Module: Mathlib.Order.Filter.EventuallyConst

Goal state before:
pp: case refine_2.base
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
⊢ f n = f n

Tactic:
| base =>

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 M
hs : s = ↑N
⊢ 0 ∈ s

Tactic:
by simp [hs]

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

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
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
⊢ ⇑(maxTrivLinearMapEquivLieModuleHom f) = ⇑↑f

Tactic:
by ext; rfl

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
⊢ 1 = p.leadingCoeff

Tactic:
pmonic.leadingCoeff

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]
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
⊢ 1 = 1
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - C a) * p
q : R[X][X]
hq : P - C (eval b P) = (X - C b) * q
⊢ C (X - C a) * C p + (X - C b) * q = C ((X - C a) * p) + (X - C b) * q

Tactic:
C_mul

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - C a) * p
q : R[X][X]
hq : P - C (eval b P) = (X - C b) * q
⊢ C (X - C a) * C p + (X - C b) * q = C (X - C a) * C p + (X - C b) * q
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (-⁅L b, L (a * a)⁆ + -⁅L a, L (b * b)⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (⁅L (a * a), L c⁆ + ⁅L (c * c), L a⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (⁅L (b * b), L c⁆ + ⁅L (c * c), L b⁆)) =
    0

Tactic:
← lie_skew (L (c * c))

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (-⁅L b, L (a * a)⁆ + -⁅L a, L (b * b)⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (⁅L (a * a), L c⁆ + -⁅L a, L (c * c)⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (⁅L (b * b), L c⁆ + ⁅L (c * c), L b⁆)) =
    0
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (-⁅L b, L (a * a)⁆ + -⁅L a, L (b * b)⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (-⁅L c, L (a * a)⁆ + -⁅L a, L (c * c)⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (-⁅L c, L (b * b)⁆ + ⁅L (c * c), L b⁆)) =
    0

Tactic:
← lie_skew (L (c * c))

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (-⁅L b, L (a * a)⁆ + -⁅L a, L (b * b)⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (-⁅L c, L (a * a)⁆ + -⁅L a, L (c * c)⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (-⁅L c, L (b * b)⁆ + -⁅L b, L (c * c)⁆)) =
    0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝³ : Ring S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ pb.minpolyGen.degree = ↑pb.dim

Tactic:
unfold minpolyGen
  rw [degree_sub_eq_left_of_degree_lt] <;> rw [degree_X_pow]
  apply degree_sum_fin_lt

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
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
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim = ∑ x, -pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x

Tactic:
neg_smul,

Goal state after:
case pos
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
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim = ∑ x, -(pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x)
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case mk.refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f : R[X]
n : ℕ
a : R
⊢ (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
      ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
        (Quot.mk (⇑(Submodule.quotientRel (map C I))) ((monomial n) a))) =
    Quot.mk (⇑(Submodule.quotientRel (map C I))) ((monomial n) a)

Tactic:
simp only [← smul_X_eq_monomial, ← C_mul' a (X ^ n), Quotient.lift_mk,
        Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk,
        coe_eval₂RingHom, map_pow, eval₂_C, RingHom.coe_comp, map_mul, eval₂_X,
        Function.comp_apply]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (g * f).Separable
⊢ g.Separable

Tactic:
exact h.of_mul_left

Goal state after:
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
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f

Tactic:
by
  classical
    by_cases H : ∃ s : Finset M, Nonempty (Basis s A M)
    · rcases H with ⟨s, ⟨b⟩⟩
      rw [← det_toMatrix b f, ← det_toMatrix (b.map e), toMatrix_comp (b.map e) b (b.map e),
        toMatrix_comp (b.map e) b b, ← Matrix.mul_assoc, Matrix.det_conj_of_mul_eq_one]
      · rw [← toMatrix_comp, LinearEquiv.comp_coe, e.symm_trans_self, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
      · rw [← toMatrix_comp, LinearEquiv.comp_coe, e.self_trans_symm, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
    · have H' : ¬∃ t : Finset N, Nonempty (Basis t A N) := by
        contrapose H
        rcases H with ⟨s, ⟨b⟩⟩
        exact ⟨_, ⟨(b.map e.symm).reindexFinsetRange⟩⟩
      simp only [coe_det, H, H', MonoidHom.one_apply, dif_neg, not_false_eq_true]

Goal state after: