mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝³ : R.functor.IsEquivalence
inst✝² : R.IsInduced
inst✝¹ : L.functor.IsEquivalence
inst✝ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
⊢ T.arrow.HasLeftResolutions ↔ B.arrow.HasLeftResolutions

Tactic:
let : CatCommSq T.functor L.functor R.functor B.functor := ⟨iso⟩

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝³ : R.functor.IsEquivalence
inst✝² : R.IsInduced
inst✝¹ : L.functor.IsEquivalence
inst✝ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
this : CatCommSq T.functor L.functor R.functor B.functor := { iso := iso }
⊢ T.arrow.HasLeftResolutions ↔ B.arrow.HasLeftResolutions
Module: Mathlib.CategoryTheory.GuitartExact.Opposite

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
inst✝ : w.GuitartExact
⊢ w.op.GuitartExact

Tactic:
rw [guitartExact_iff_isConnected_rightwards]

Goal state after:
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
inst✝ : w.GuitartExact
⊢ ∀ {X₂ : C₃ᵒᵖ} {X₃ : C₂ᵒᵖ} (g : B.op.obj X₂ ⟶ R.op.obj X₃), IsConnected (w.op.StructuredArrowRightwards g)
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
F : C₁ ⥤ C₂
⊢ (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)).GuitartExact

Tactic:
rw [guitartExact_iff_isConnected_rightwards]

Goal state after:
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
F : C₁ ⥤ C₂
⊢ ∀ {X₂ : C₁} {X₃ : C₂} (g : F.obj X₂ ⟶ (𝟭 C₂).obj X₃),
    IsConnected ((mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)).StructuredArrowRightwards g)
Module: Mathlib.CategoryTheory.GuitartExact.Quotient

Goal state before:
pp: C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₀
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} H₀
inst✝³ : Category.{v_4, u_4} H
T : C₀ ⥤ H₀
L : C₀ ⥤ C
R : H₀ ⥤ H
B : C ⥤ H
inst✝² : T.EssSurj
inst✝¹ : T.Full
inst✝ : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ → ∃ P, T.map P.i₀ = T.map P.i₁ ∧ Nonempty ((P.map L).LeftHomotopy f₀ f₁)
⊢ ∀ {X₂ : H₀} {X₃ : C} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (CostructuredArrowDownwards e.hom g)

Tactic:
intro Y₀ X g

Goal state after:
C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₀
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} H₀
inst✝³ : Category.{v_4, u_4} H
T : C₀ ⥤ H₀
L : C₀ ⥤ C
R : H₀ ⥤ H
B : C ⥤ H
inst✝² : T.EssSurj
inst✝¹ : T.Full
inst✝ : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ → ∃ P, T.map P.i₀ = T.map P.i₁ ∧ Nonempty ((P.map L).LeftHomotopy f₀ f₁)
Y₀ : H₀
X : C
g : R.obj Y₀ ⟶ B.obj X
⊢ IsConnected (CostructuredArrowDownwards e.hom g)
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:
rw [← TwoSquare.GuitartExact.vComp'_iff_of_equivalences e'.hom E₁ E₂ e''' e₁ e₂, this]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
⊢ P g

Tactic:
let X₀ : Paths (LocQuiver W) := ⟨X⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := { obj := X }
⊢ P g
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: case refine_2
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' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ F'
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cocone (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app (CostructuredArrow.mk φ) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk φ)
⊢ ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app
        (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ))

Tactic:
have : IsIso (F.map w) := by
        have := Localization.inverts L W w hw
        rw [← NatIso.naturality_2 e w]
        dsimp
        infer_instance

Goal state after:
case refine_2
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' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ F'
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cocone (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app (CostructuredArrow.mk φ) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk φ)
this : IsIso (F.map w)
⊢ ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app
        (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ))
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D₁
inst✝⁸ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁷ : W₂'.RespectsIso
inst✝⁶ : L.IsLocalizedEquivalence
inst✝⁵ : R.IsLocalizedEquivalence
inst✝⁴ : R.functor.EssSurj
inst✝³ : L.functor.EssSurj
inst✝² : R.functor.Full
inst✝¹ : R.IsInduced
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
x✝ : B.IsLeftDerivabilityStructure
this✝ : T.HasLeftResolutions
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor W₁'.Q W₂'.Q
e' : B.functor ⋙ W₂'.Q ≅ W₁'.Q ⋙ F := CatCommSq.iso B.functor W₁'.Q W₂'.Q F
e : T.functor ⋙ R.functor ⋙ W₂'.Q ≅ (L.functor ⋙ W₁'.Q) ⋙ F :=
  (T.functor.associator R.functor W₂'.Q).symm ≪≫
    Functor.isoWhiskerRight iso W₂'.Q ≪≫
      L.functor.associator B.functor W₂'.Q ≪≫ L.functor.isoWhiskerLeft e' ≪≫ (L.functor.associator W₁'.Q F).symm
he' : TwoSquare.GuitartExact e'.inv
this : TwoSquare.hComp iso.inv e'.inv = e.inv
⊢ T.IsLeftDerivabilityStructure

Tactic:
T.isLeftDerivabilityStructure_iff (L.functor ⋙ W₁'.Q)
    (R.functor ⋙ W₂'.Q) F e,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D₁
inst✝⁸ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁷ : W₂'.RespectsIso
inst✝⁶ : L.IsLocalizedEquivalence
inst✝⁵ : R.IsLocalizedEquivalence
inst✝⁴ : R.functor.EssSurj
inst✝³ : L.functor.EssSurj
inst✝² : R.functor.Full
inst✝¹ : R.IsInduced
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
x✝ : B.IsLeftDerivabilityStructure
this✝ : T.HasLeftResolutions
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor W₁'.Q W₂'.Q
e' : B.functor ⋙ W₂'.Q ≅ W₁'.Q ⋙ F := CatCommSq.iso B.functor W₁'.Q W₂'.Q F
e : T.functor ⋙ R.functor ⋙ W₂'.Q ≅ (L.functor ⋙ W₁'.Q) ⋙ F :=
  (T.functor.associator R.functor W₂'.Q).symm ≪≫
    Functor.isoWhiskerRight iso W₂'.Q ≪≫
      L.functor.associator B.functor W₂'.Q ≪≫ L.functor.isoWhiskerLeft e' ≪≫ (L.functor.associator W₁'.Q F).symm
he' : TwoSquare.GuitartExact e'.inv
this : TwoSquare.hComp iso.inv e'.inv = e.inv
⊢ TwoSquare.GuitartExact e.inv
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case refine_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X : DifferentialObject S C
⊢ ((CategoryTheory.shiftFunctor C (m + n)).map X.d ≫ (shiftFunctorComm C 1 (m + n)).hom.app X.obj) ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj) =
    (CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj ≫
      (CategoryTheory.shiftFunctor C n).map
          ((CategoryTheory.shiftFunctor C m).map X.d ≫ (shiftFunctorComm C 1 m).hom.app X.obj) ≫
        (shiftFunctorComm C 1 n).hom.app ((CategoryTheory.shiftFunctor C m).obj X.obj)

Tactic:
← cancel_epi ((shiftFunctorAdd C m n).inv.app X.obj)

Goal state after:
case refine_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X : DifferentialObject S C
⊢ (CategoryTheory.shiftFunctorAdd C m n).inv.app X.obj ≫
      ((CategoryTheory.shiftFunctor C (m + n)).map X.d ≫ (shiftFunctorComm C 1 (m + n)).hom.app X.obj) ≫
        (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj) =
    (CategoryTheory.shiftFunctorAdd C m n).inv.app X.obj ≫
      (CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj ≫
        (CategoryTheory.shiftFunctor C n).map
            ((CategoryTheory.shiftFunctor C m).map X.d ≫ (shiftFunctorComm C 1 m).hom.app X.obj) ≫
          (shiftFunctorComm C 1 n).hom.app ((CategoryTheory.shiftFunctor C m).obj X.obj)
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₁
X : C
K : HomologicalComplex C c
g : double (𝟙 X) hi₀₁ ⟶ K
⊢ (fun φ₀ ↦ mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) ⋯ ⋯) ((fun g ↦ (doubleXIso₀ (𝟙 X) hi₀₁).inv ≫ g.f i₀) g) = g

Tactic:
by
        ext
        · simp
        · simp [double_d _ _ h]

Goal state after:
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
⊢ (C.d i j).app t = 0

Tactic:
by
        have := C.shape _ _ h
        rw [NatTrans.ext_iff, funext_iff] at this
        exact this t

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso ((twoδ₂Toδ₁ f g fg h).app 0) ∧ IsIso ((twoδ₂Toδ₁ f g fg h).app 1)

Tactic:
constructor <;> dsimp

Goal state after:
case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso (𝟙 i)

case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso g
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso ((twoδ₁Toδ₀ f g fg h).app 0) ∧ IsIso ((twoδ₁Toδ₀ f g fg h).app 1)

Tactic:
constructor <;> dsimp

Goal state after:
case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso f

case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso (𝟙 k)
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 : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
L : CochainComplex C ℤ
g : K ⟶ L
⊢ ↑(fromSingleMk (f ≫ g.f q) h q' hq' ⋯) = ↑((fromSingleMk f h q' hq' hf).postcomp g)

Tactic:
exact (Cochain.fromSingleEquiv h).injective (by simp [Cochain.fromSingleMk_postcomp])

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

Tactic:
simp only [hom_ext_iff, comp_f, F.map_comp] at h h'

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
⊢ (F.map P.p).f ≫ (φ.app P.X).f ≫ (φ'.app P.X).f = (F.map P.p).f ≫ (φ.app P.X).f ≫ (G.map P.p).f ≫ (φ'.app P.X).f
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 : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝ : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
j : J
s : Cofan ((((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).mapObjFun p j)
i : I
j' : J
h : (i, j') ∈ p ⁻¹' {j}
⊢ Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(i, j'), h⟩ ≫
      e.inv.app (Y j) ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫ s.inj ⟨(0, j), ⋯⟩ =
    s.inj ⟨(i, j'), h⟩

Tactic:
by_cases hi : i = 0

Goal state after:
case pos
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 : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝ : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
j : J
s : Cofan ((((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).mapObjFun p j)
i : I
j' : J
h : (i, j') ∈ p ⁻¹' {j}
hi : i = 0
⊢ Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(i, j'), h⟩ ≫
      e.inv.app (Y j) ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫ s.inj ⟨(0, j), ⋯⟩ =
    s.inj ⟨(i, j'), h⟩

case neg
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 : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝ : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
j : J
s : Cofan ((((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).mapObjFun p j)
i : I
j' : J
h : (i, j') ∈ p ⁻¹' {j}
hi : ¬i = 0
⊢ Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(i, j'), h⟩ ≫
      e.inv.app (Y j) ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫ s.inj ⟨(0, j), ⋯⟩ =
    s.inj ⟨(i, j'), h⟩
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 X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
j' : J
i : I
h : (j', i) ∈ p ⁻¹' {j}
⊢ Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j', i), h⟩ ≫
      e.inv.app (X j) ≫ (F.obj (X j)).map (singleObjApplyIso 0 Y).inv ≫ s.inj ⟨(j, 0), ⋯⟩ =
    s.inj ⟨(j', i), h⟩

Tactic:
by_cases hi : i = 0

Goal state after:
case pos
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 X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
j' : J
i : I
h : (j', i) ∈ p ⁻¹' {j}
hi : i = 0
⊢ Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j', i), h⟩ ≫
      e.inv.app (X j) ≫ (F.obj (X j)).map (singleObjApplyIso 0 Y).inv ≫ s.inj ⟨(j, 0), ⋯⟩ =
    s.inj ⟨(j', i), h⟩

case neg
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 X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
j' : J
i : I
h : (j', i) ∈ p ⁻¹' {j}
hi : ¬i = 0
⊢ Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j', i), h⟩ ≫
      e.inv.app (X j) ≫ (F.obj (X j)).map (singleObjApplyIso 0 Y).inv ≫ s.inj ⟨(j, 0), ⋯⟩ =
    s.inj ⟨(j', i), h⟩
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
n : ℤ
h : IsZero ((X.H n).obj (mk₁ f))
⊢ IsZero (X.opcycles f g n)

Tactic:
by
  rw [IsZero.iff_id_eq_zero, ← cancel_epi (X.pOpcycles ..)]
  apply h.eq_of_src

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
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
x : (X.H n₁).obj (mk₁ f) ⟶ A
hx : X.δ f g n₀ n₁ hn₁ ≫ x = 0
⊢ X.δ f g (n₁ - 1) n₁ ⋯ ≫ x = 0

Tactic:
obtain rfl : n₀ = n₁ -1 := by lia
    exact hx

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₁
⊢ (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ (f₂ ≫ f₃) ⋯) ≫ X.δ f₁ (f₂ ≫ f₃) n₀ n₁ hn₁ ≫ X.pOpcycles f₁ f₂ n₁ = 0

Tactic:
X.δ_naturality_assoc f₁ f₂ f₁ (f₂ ≫ f₃) (𝟙 _) (twoδ₂Toδ₁ f₂ f₃ _ rfl) _ _ rfl,

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₁
⊢ X.δ f₁ f₂ n₀ n₁ (CategoryTheory.Abelian.SpectralObject.d._proof_1 n₀ n₁ hn₁) ≫
      (X.H n₁).map (𝟙 (mk₁ f₁)) ≫ X.pOpcycles f₁ f₂ n₁ =
    0
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
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g' = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂

Tactic:
let hp := (X.cokernelSequenceOpcycles_exact f₂ f₃ _ _ hn₁).gIsCokernel
  exact Cofork.IsColimit.hom_ext hp (by simpa using! hp.fac _ .one)

Goal state after: