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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝³³ : Category.{v_1, u_1} C₁
inst✝³² : Category.{v_2, u_2} C₂
inst✝³¹ : Category.{v_3, u_5} C₃
inst✝³⁰ : Category.{v_4, u_6} C₄
inst✝²⁹ : Category.{v_5, u_3} C₁₂
inst✝²⁸ : Category.{v_6, u_4} C₂₃
inst✝²⁷ : HasZeroMorphisms C₁
inst✝²⁶ : HasZeroMorphisms C₂
inst✝²⁵ : HasZeroMorphisms C₃
inst✝²⁴ : Preadditive C₁₂
inst✝²³ : Preadditive C₂₃
inst✝²² : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝²¹ : F₁₂.PreservesZeroMorphisms
inst✝²⁰ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝¹⁹ : G.Additive
inst✝¹⁸ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
inst✝¹⁷ : G₂₃.PreservesZeroMorphisms
inst✝¹⁶ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁵ : F.PreservesZeroMorphisms
inst✝¹⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝¹³ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝¹² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹¹ : TotalComplexShape c₁₂ c₃ c₄
inst✝¹⁰ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁹ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁸ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝⁷ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝⁶ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝⁵ : DecidableEq ι₁₂
inst✝⁴ : DecidableEq ι₂₃
inst✝³ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
inst✝² : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝¹ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
⊢ (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom ≫ mapBifunctor₂₃.D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' =
    mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' ≫ (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom

Tactic:
ext i₁ i₂ i₃ h
  rw [mapBifunctor₁₂.ι_D₂_assoc, ι_mapBifunctorAssociatorX_hom_assoc, mapBifunctor₂₃.ι_D₂]
  by_cases h₁ : c₂.Rel i₂ (c₂.next i₂)
  · have := NatTrans.naturality_app (associator.hom.app (K₁.X i₁)) (K₃.X i₃) (K₂.d i₂ (c₂.next i₂))
    dsimp at this
    rw [mapBifunctor₁₂.d₂_eq _ _ _ _ _ _ _ _ h₁, mapBifunctor₂₃.d₂_eq _ _ _ _ _ _ _ _ _ h₁,
      Linear.units_smul_comp, assoc, ιOrZero_mapBifunctorAssociatorX_hom,
      reassoc_of% this, Linear.comp_units_smul,
      ComplexShape.associative_ε₂_ε₁ c₁ c₂ c₃ c₁₂ c₂₃ c₄]
  · rw [mapBifunctor₁₂.d₂_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₁,
      mapBifunctor₂₃.d₂_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₁, comp_zero, zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced

Goal state before:
pp: C : Type u_1
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasShift C ℤ
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
P✝ : ObjectProperty C
t✝ : TStructure C
inst✝⁶ : P✝.IsTriangulated
h : P✝.HasInducedTStructure t✝
P P' : ObjectProperty C
inst✝⁵ : P.IsTriangulated
inst✝⁴ : P'.IsTriangulated
t : TStructure C
inst✝³ : P.HasInducedTStructure t
inst✝² : P'.HasInducedTStructure t
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P'.IsClosedUnderIsomorphisms
⊢ ∀ (X : C), (P ⊓ P') X → ∀ (n : ℤ), (P ⊓ P') ((t.truncLE n).obj X) ∧ (P ⊓ P') ((t.truncGE n).obj X)

Tactic:
rintro X ⟨hX, hX'⟩ n

Goal state after:
C : Type u_1
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasShift C ℤ
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
P✝ : ObjectProperty C
t✝ : TStructure C
inst✝⁶ : P✝.IsTriangulated
h : P✝.HasInducedTStructure t✝
P P' : ObjectProperty C
inst✝⁵ : P.IsTriangulated
inst✝⁴ : P'.IsTriangulated
t : TStructure C
inst✝³ : P.HasInducedTStructure t
inst✝² : P'.HasInducedTStructure t
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
⊢ (P ⊓ P') ((t.truncLE n).obj X) ∧ (P ⊓ P') ((t.truncGE n).obj X)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X : C
a b : ℤ
hn : a ≤ b + 1
⊢ t.IsLE ((t.truncLT a).obj X) b

Tactic:
have : t.IsLE ((t.truncLT a).obj X) (a - 1) := by dsimp [truncLT]; infer_instance
  exact t.isLE_of_le _ (a - 1) _ (by lia)

Goal state after:
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
this✝ : L₁.Additive
this : L₂.Additive
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
X₁ X₂ : A.FullSubcategory
f : X₁ ⟶ X₂
X₃ : C
s : X₂.obj ⟶ X₃
hs : B.trW s
fac : f.hom ≫ s = 0 ≫ s
X₄ : C
t : X₂.obj ⟶ X₄
a : X₃ ⟶ X₄
hX₄ : A X₄
ht : (A ⊓ B).trW t
fac' : s ≫ a = t
⊢ L₁.map f = 0

Tactic:
let t' : X₂ ⟶ ⟨X₄, hX₄⟩ := A.homMk t

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
this : L₂.Additive
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
X₁ X₂ : A.FullSubcategory
f : X₁ ⟶ X₂
X₃ : C
s : X₂.obj ⟶ X₃
hs : B.trW s
fac : f.hom ≫ s = 0 ≫ s
X₄ : C
t : X₂.obj ⟶ X₄
a : X₃ ⟶ X₄
hX₄ : A X₄
ht : (A ⊓ B).trW t
fac' : s ≫ a = t
t' : X₂ ⟶ { obj := X₄, property := hX₄ } := homMk t
⊢ L₁.map f = 0
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
⊢ ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), epiWithInjectiveKernel g → epiWithInjectiveKernel f

Tactic:
rintro X' Y' X Y f' f r ⟨_, hf⟩
    have : Epi f' :=
      (MorphismProperty.epimorphisms C).of_retract r (.infer_property _)
    let r' : Retract (kernel f') (kernel f) :=
      { i := kernel.map _ _ r.i.left r.i.right (Arrow.w r.i).symm
        r := kernel.map _ _ r.r.left r.r.right (Arrow.w r.r).symm
        retract := by ext; simp }
    exact ⟨inferInstance, r'.injective⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
hX : ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0
⊢ 𝟙 ((t.truncLT n₁).obj X) ≫ (t.truncLTι n₁).app X = 0 ≫ (t.truncLTι n₁).app X

Tactic:
simpa using hX _ _ (by rw [← h]; infer_instance)

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : ℤ
X : C
⊢ IsIso ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)))

Tactic:
rw [← t.isLE_iff_isIso_truncLTι_app (b - 1) b (by lia)]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : ℤ
X : C
⊢ t.IsLE ((t.truncGE a).obj ((t.truncLT b).obj X)) (b - 1)
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
⊢ Function.Injective fun f ↦ f.postcomp g

Tactic:
intro f₀ f₁ h
    obtain ⟨f₀, rfl⟩ := f₀.mk_surjective
    obtain ⟨f₁, rfl⟩ := f₁.mk_surjective
    simp only [postcomp_mk, mk_eq_mk_iff] at h
    obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_cylinder
    have sq : CommSq (coprod.desc f₀ f₁) P.i g h.h := { }
    rw [mk_eq_mk_iff]
    exact ⟨P,
      ⟨{h := sq.lift
        h₀ := by
          have := coprod.inl ≫= sq.fac_left
          rwa [P.inl_i_assoc, coprod.inl_desc] at this
        h₁ := by
          have := coprod.inr ≫= sq.fac_left
          rwa [P.inr_i_assoc, coprod.inr_desc] at this }⟩⟩

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

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₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : C₂ ⥤ C₃
R₂ : D₂ ⥤ D₃
H₃ : C₃ ⥤ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
inst✝¹ : w.GuitartExact
inst✝ : w'.GuitartExact
L₁₂ : C₁ ⥤ C₃
R₁₂ : D₁ ⥤ D₃
eL : L₁ ⋙ L₂ ≅ L₁₂
eR : R₁ ⋙ R₂ ≅ R₁₂
⊢ (w.vComp' w' eL eR).GuitartExact

Tactic:
dsimp only [TwoSquare.vComp']
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : Φ.HasRightResolutions
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
this✝ :
  Φ.IsRightDerivabilityStructure ↔
    TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom
e' : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
E₁ : W₁.Localization ≌ D₁ := uniq W₁.Q L₁ W₁
E₂ : W₂.Localization ≌ D₂ := uniq W₂.Q L₂ W₂
e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
e'' : (Φ.functor ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
  Φ.functor.associator W₂.Q E₂.functor ≪≫ Φ.functor.isoWhiskerLeft e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F
e''' : Φ.localizedFunctor W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F :=
  liftNatIso W₁.Q W₁ ((Φ.functor ⋙ W₂.Q) ⋙ E₂.functor) ((W₁.Q ⋙ E₁.functor) ⋙ F)
    (Φ.localizedFunctor W₁.Q W₂.Q ⋙ E₂.functor) (E₁.functor ⋙ F) e''
this : TwoSquare.vComp' e'.hom e'''.hom e₁ e₂ = e.hom
⊢ TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom ↔
    TwoSquare.GuitartExact e.hom

Tactic:
← TwoSquare.GuitartExact.vComp'_iff_of_equivalences e'.hom E₁ E₂ e''' e₁ e₂,

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : Φ.HasRightResolutions
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
this✝ :
  Φ.IsRightDerivabilityStructure ↔
    TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom
e' : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
E₁ : W₁.Localization ≌ D₁ := uniq W₁.Q L₁ W₁
E₂ : W₂.Localization ≌ D₂ := uniq W₂.Q L₂ W₂
e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
e'' : (Φ.functor ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
  Φ.functor.associator W₂.Q E₂.functor ≪≫ Φ.functor.isoWhiskerLeft e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F
e''' : Φ.localizedFunctor W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F :=
  liftNatIso W₁.Q W₁ ((Φ.functor ⋙ W₂.Q) ⋙ E₂.functor) ((W₁.Q ⋙ E₁.functor) ⋙ F)
    (Φ.localizedFunctor W₁.Q W₂.Q ⋙ E₂.functor) (E₁.functor ⋙ F) e''
this : TwoSquare.vComp' e'.hom e'''.hom e₁ e₂ = e.hom
⊢ (TwoSquare.vComp' e'.hom e'''.hom e₁ e₂).GuitartExact ↔ TwoSquare.GuitartExact e.hom
Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_5, u_2} H
RF RF' : D ⥤ H
F F' : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
⊢ α ≫ L.whiskerLeft (RF.rightDerivedNatTrans RF' α α' W τ) = τ ≫ α'

Tactic:
dsimp only [rightDerivedNatTrans]

Goal state after:
C : Type u_1
D : Type u_3
H : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_5, u_2} H
RF RF' : D ⥤ H
F F' : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
⊢ α ≫ L.whiskerLeft (RF.rightDerivedDesc α W RF' (τ ≫ α')) = τ ≫ α'
Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_5, u_2} H
RF RF' : D ⥤ H
F F' : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
X : C
⊢ α.app X ≫ (RF.rightDerivedNatTrans RF' α α' W τ).app (L.obj X) = τ.app X ≫ α'.app X

Tactic:
dsimp only [rightDerivedNatTrans]

Goal state after:
C : Type u_1
D : Type u_3
H : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_5, u_2} H
RF RF' : D ⥤ H
F F' : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
X : C
⊢ α.app X ≫ (RF.rightDerivedDesc α W RF' (τ ≫ α')).app (L.obj X) = τ.app X ≫ α'.app X
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
X : C
inst✝ : F.HasPointwiseRightDerivedFunctorAt W X
⊢ L.HasPointwiseLeftKanExtensionAt F (L.obj X)

Tactic:
← hasPointwiseRightDerivedFunctorAt_iff F L W

Goal state after:
C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
X : C
inst✝ : F.HasPointwiseRightDerivedFunctorAt W X
⊢ F.HasPointwiseRightDerivedFunctorAt W X
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} H
D₂ : Type u₄
inst✝³ : Category.{v₄, u₄} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
h : Φ.Derives F
inst✝² : Φ.IsRightDerivabilityStructure
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
RF : D₂ ⥤ H
α : F ⟶ L₂ ⋙ RF
X₁ : C₁
inst✝ : RF.IsRightDerivedFunctor α W₂
G : W₁.Localization ⥤ H := Localization.lift (Φ.functor ⋙ F) h W₁.Q
eG : W₁.Q ⋙ G ≅ Φ.functor ⋙ F := Localization.Lifting.iso W₁.Q W₁ (Φ.functor ⋙ F) G
this✝ : G.IsRightDerivedFunctor eG.inv W₁
this : (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁
⊢ IsIso (α.app (Φ.functor.obj X₁))

Tactic:
rw [← Φ.isIso_iff_of_isRightDerivabilityStructure W₁.Q L₂ F G eG.inv RF α]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} H
D₂ : Type u₄
inst✝³ : Category.{v₄, u₄} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
h : Φ.Derives F
inst✝² : Φ.IsRightDerivabilityStructure
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
RF : D₂ ⥤ H
α : F ⟶ L₂ ⋙ RF
X₁ : C₁
inst✝ : RF.IsRightDerivedFunctor α W₂
G : W₁.Localization ⥤ H := Localization.lift (Φ.functor ⋙ F) h W₁.Q
eG : W₁.Q ⋙ G ≅ Φ.functor ⋙ F := Localization.Lifting.iso W₁.Q W₁ (Φ.functor ⋙ F) G
this✝ : G.IsRightDerivedFunctor eG.inv W₁
this : (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁
⊢ IsIso (eG.inv.app X₁)
Module: Mathlib.Algebra.Homology.Embedding.StupidTrunc

Goal state before:
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✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝¹ : e.IsRelIff
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
hi'' : ¬∃ i, e.f i = i'
⊢ IsZero ((K.stupidTrunc e).X i')

Tactic:
· apply isZero_stupidTrunc_X
      simpa using hi''

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

Goal state before:
pp: case pos
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₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
h₁ : k₀ = i₁
⊢ (if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0

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₁
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₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
h₁ : ¬k₀ = i₁
⊢ (if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0

Tactic:
· subst h₁
        dsimp
        rw [if_pos rfl, comp_id, id_comp, assoc, hφ k₁ hk, comp_zero,
          double_d_eq_zero₀ _ _ _ _ h.symm, zero_comp]

Goal state after:
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₁
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₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
h₁ : ¬k₀ = i₁
⊢ (if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0
Module: Mathlib.Algebra.Homology.Functor

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
i j : ι
h : ¬c.Rel i j
this : (C.d i j).app = NatTrans.app 0
⊢ (C.d i j).app t = 0

Tactic:
funext_iff

Goal state after:
T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
i j : ι
h : ¬c.Rel i j
this : ∀ (x : T), (C.d i j).app x = NatTrans.app 0 x
⊢ (C.d i j).app t = 0
Module: Mathlib.Algebra.Homology.Functor

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
i j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
this : (C.d i j ≫ C.d j k).app = NatTrans.app 0
⊢ (C.d i j).app t ≫ (C.d j k).app t = 0

Tactic:
funext_iff

Goal state after:
T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
i j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
this : ∀ (x : T), (C.d i j ≫ C.d j k).app x = NatTrans.app 0 x
⊢ (C.d i j).app t ≫ (C.d j k).app t = 0
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 : C ⥤ Karoubi D
⊢ FunctorExtension₁.map (𝟙 F) = 𝟙 (FunctorExtension₁.obj F)

Tactic:
by
    ext P
    exact comp_p (F.map P.p)

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Reduced

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
inst✝² : Preadditive C
inst✝¹ : Preadditive A
inst✝ : ι.Additive
X : A
⊢ Epi ((karoubi.π Λ).app ((toKaroubi A).obj X))

Tactic:
by
  rw [karoubi.π_app_toKaroubi_obj]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
⊢ { X₁ := syzygies f, X₂ := X, X₃ := Y, f := d f, g := f, zero := ⋯ }.Exact

Tactic:
let α : ShortComplex.mk (d f) f (by simp) ⟶ ShortComplex.mk (kernel.ι f) f (by simp) :=
    { τ₁ := Projective.π _
      τ₂ := 𝟙 _
      τ₃ := 𝟙 _ }
  rw [ShortComplex.exact_iff_of_epi_of_isIso_of_mono α]
  apply ShortComplex.exact_of_f_is_kernel
  apply kernelIsKernel

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
J : Ideal R
k : ℕᵒᵖ
⊢ J ≤ ((idealPowersDiagram J).obj k).radical

Tactic:
change _ ≤ (J ^ unop k).radical

Goal state after:
R : Type u
inst✝ : CommRing R
J : Ideal R
k : ℕᵒᵖ
⊢ J ≤ (J ^ unop k).radical