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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasLimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).LimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ 𝟙 (K.X i) = 0

Tactic:
exact (isLimitOfPreserves (HomologicalComplex.eval _ _ i) p.isLimit).hom_ext
      (fun j ↦ (isZero_of_isStrictlyGE (p.diag.obj j) n i).eq_of_tgt _ _)

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
X : C
hX : P.trW.isColocal X
Y : C
f : X ⟶ Y
hY : P Y
⊢ f = 0

pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
hh : P.trW h
⊢ Function.Bijective fun f ↦ f ≫ h

Tactic:
· exact (hX _ (trW.mk P (contractible_distinguished₂ Y) (P.le_shift _ _ hY))).injective (by simp)

Goal state after:
case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
hh : P.trW h
⊢ Function.Bijective fun f ↦ f ≫ h
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
h₁ : Cofibration f₁
h₂ : Cofibration f₂
inst✝¹ : HasBinaryCoproduct X₁ X₂
inst✝ : HasBinaryCoproduct Y₁ Y₂
⊢ Cofibration (coprod.map f₁ f₂)

Tactic:
rw [cofibration_iff] at h₁ h₂ ⊢

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
h₁ : cofibrations C f₁
h₂ : cofibrations C f₂
inst✝¹ : HasBinaryCoproduct X₁ X₂
inst✝ : HasBinaryCoproduct Y₁ Y₂
⊢ cofibrations C (coprod.map f₁ f₂)
Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
A : C
inst✝⁴ : CategoryWithWeakEquivalences C
P : PathObject A
inst✝³ : HasBinaryProducts C
inst✝² : CategoryWithFibrations C
inst✝¹ : P.IsGood
inst✝ : (fibrations C).RespectsIso
⊢ Fibration P.symm.p

Tactic:
have hp : fibrations C P.p := by rw [← fibration_iff]; infer_instance

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
A : C
inst✝⁴ : CategoryWithWeakEquivalences C
P : PathObject A
inst✝³ : HasBinaryProducts C
inst✝² : CategoryWithFibrations C
inst✝¹ : P.IsGood
inst✝ : (fibrations C).RespectsIso
hp : fibrations C P.p
⊢ Fibration P.symm.p
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: case e_a
C₁ : Type u_1
C₂ : Type u_2
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_6, u_4} C₂₃
inst✝¹⁸ : HasZeroMorphisms C₁
inst✝¹⁷ : HasZeroMorphisms C₂
inst✝¹⁶ : HasZeroMorphisms C₃
inst✝¹⁵ : Preadditive C₂₃
inst✝¹⁴ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : 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₃ G₂₃ c₂₃
inst✝³ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝² : DecidableEq ι₂₃
inst✝¹ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₂₃ : ι₂₃ := c₂.π c₃ c₂₃ (i₂, i₃)
h₁ : c₂₃.Rel i₂₃ (c₂₃.next i₂₃)
h₂ : ¬c₁.π c₂₃ c₄ (i₁, c₂₃.next i₂₃) = j'
⊢ 0 = d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'

Tactic:
· by_cases h₃ : c₃.Rel i₃ (c₃.next i₃)
          · rw [d₃_eq _ _ _ _ _ _ _ _ _ _ h₃, ιOrZero_eq_zero, comp_zero, smul_zero]
            intro h₄
            apply h₂
            rw [← h₄]
            dsimp [ComplexShape.r]
            rw [ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄, ComplexShape.next_π₂ c₂ c₂₃ i₂ h₃]
          · rw [d₃_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₃]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : Plus C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (n : ℤ), IsIso ((homologyFunctor C n).map f)

Tactic:
by
  refine ⟨fun _ _ ↦ inferInstance, fun _ ↦ ?_⟩
  have : IsIso (ι.map f) := by rwa [DerivedCategory.isIso_iff]
  exact isIso_of_fully_faithful ι _

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
inst✝³ : Preadditive D₁
inst✝² : Preadditive D₂
inst✝¹ : L₁.Additive
inst✝ : L₂.Additive
⊢ ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Additive

Tactic:
let F := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
  rw [Localization.functor_additive_iff L₁ (B.inverseImage A.ι).trW]
  let e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso
    (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
  exact Functor.additive_of_iso e

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₂
hf : F.map (L₁.map f) = 0
⊢ L₂.map f.hom = L₂.map 0

Tactic:
simp [← dsimp% NatIso.naturality_2 e f, hf]

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.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝⁵ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝⁴ : L₂.IsLocalization B.trW
inst✝³ : Preadditive D₁
inst✝² : Preadditive D₂
inst✝¹ : L₁.Additive
inst✝ : L₂.Additive
⊢ ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Additive

Tactic:
let F := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
  rw [Localization.functor_additive_iff L₁ (B.inverseImage A.ι).trW]
  let e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso
    (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
  exact Functor.additive_of_iso e

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₁ : ℤ
⊢ degreewiseEpiWithInjectiveKernel (π K L n₁)

Tactic:
by
  intro q
  rw [Abelian.epiWithInjectiveKernel_iff]
  exact ⟨(S K n₁).X q, inferInstance, (biprod.inl : _ ⟶ mid K L n₁).f q, by simp,
    ⟨{ r := (biprod.fst : mid K L n₁ ⟶ _).f q, s := (biprod.inr : _ ⟶ mid K L n₁).f q }⟩⟩

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

Goal state before:
pp: case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi✝ : i ≤ n₀
hi : i < n₀
φ : (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).obj (mid K L n₁) ⟶
  (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).obj L :=
  (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).map (π K L n₁)
this✝ : IsIso φ.τ₁
this : IsIso φ.τ₂
⊢ ShortComplex.QuasiIso ((shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).map (π K L n₁))

Tactic:
have : IsIso φ.τ₃ := isIso_π_f ..

Goal state after:
case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi✝ : i ≤ n₀
hi : i < n₀
φ : (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).obj (mid K L n₁) ⟶
  (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).obj L :=
  (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).map (π K L n₁)
this✝¹ : IsIso φ.τ₁
this✝ : IsIso φ.τ₂
this : IsIso φ.τ₃
⊢ ShortComplex.QuasiIso ((shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).map (π K L n₁))
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
x✝² x✝¹ : FibrantObject C
x✝ : x✝² ⟶ x✝¹
h : weakEquivalences (FibrantObject C) x✝
⊢ (weakEquivalences (HoCat C)).inverseImage toHoCat x✝

Tactic:
by
    simp only [← weakEquivalence_iff] at h
    simpa only [MorphismProperty.inverseImage_iff, ← weakEquivalence_iff,
      weakEquivalence_toHoCat_map_iff]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n i : ℤ
⊢ { X₁ := (S f n).X (i - 1), X₂ := (mid f n).X i, X₃ := L.X i, f := (↑(mappingCocone.inr (α f n))).v (i - 1) i ⋯,
            g := (π f n).f i, zero := ⋯ }.g ≫
        (mappingCocone.inl (α f n)).v i i ⋯ +
      (mappingCocone.snd (α f n)).v i (i - 1) ⋯ ≫
        { X₁ := (S f n).X (i - 1), X₂ := (mid f n).X i, X₃ := L.X i, f := (↑(mappingCocone.inr (α f n))).v (i - 1) i ⋯,
            g := (π f n).f i, zero := ⋯ }.f =
    𝟙
      { X₁ := (S f n).X (i - 1), X₂ := (mid f n).X i, X₃ := L.X i, f := (↑(mappingCocone.inr (α f n))).v (i - 1) i ⋯,
          g := (π f n).f i, zero := ⋯ }.X₂

Tactic:
by simp [mappingCocone.id_X]

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

Goal state before:
pp: case mp
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
⊢ w.op.GuitartExact → w.GuitartExact

Tactic:
intro
    let w₁ : TwoSquare T (opOp C₁) (opOp C₂) T.op.op := 𝟙 _
    let w₂ : TwoSquare B.op.op (unopUnop C₃) (unopUnop C₄) B := 𝟙 _
    have : w = (w₁ ≫ᵥ w.op.op) ≫ᵥ w₂ := by cat_disch
    rw [this]
    infer_instance

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

Goal state before:
pp: case inr.zero
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)
i : ℤ
this : ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂), i ≤ n₀ + ↑q₁ → q₁ + 1 = q₂ → IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
hi : i ≤ n₀ + ↑q₁
hk : q₁ + 0 = q₂
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)

Tactic:
obtain rfl : q₁ = q₂ := by simpa using hk

Goal state after:
case inr.zero
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)
i : ℤ
this : ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂), i ≤ n₀ + ↑q₁ → q₁ + 1 = q₂ → IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
q₁ : ℕ
hi : i ≤ n₀ + ↑q₁
hq : q₁ ≤ q₁
hk : q₁ + 0 = q₁
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
⊢ (∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial) → w.GuitartExact

Tactic:
rw [guitartExact_iff_isConnected_downwards]
    intros
    infer_instance

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
inst✝² : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝¹ : w.GuitartExact
inst✝ : B.EssSurj
F : C₂ ⥤ D
⊢ (∀ (Y : C₃), L.HasPointwiseLeftKanExtensionAt (T ⋙ F) Y) ↔ ∀ (Y : C₄), R.HasPointwiseLeftKanExtensionAt F Y

Tactic:
simp only [hasPointwiseLeftKanExtensionAt_iff w]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
inst✝² : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝¹ : w.GuitartExact
inst✝ : B.EssSurj
F : C₂ ⥤ D
⊢ (∀ (Y : C₃), R.HasPointwiseLeftKanExtensionAt F (B.obj Y)) ↔ ∀ (Y : C₄), R.HasPointwiseLeftKanExtensionAt F Y
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived

Goal state before:
pp: case mpr
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
⊢ (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁ → F.HasPointwiseRightDerivedFunctor W₂

Tactic:
intro hF X₂

Goal state after:
case mpr
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
hF : (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁
X₂ : C₂
⊢ F.HasPointwiseRightDerivedFunctorAt W₂ X₂
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
⊢ h.map h (𝟙 K) (𝟙 L) ⋯ = 𝟙 h.cochainComplex

Tactic:
ext (m | _ | m)

Goal state after:
case ofNat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m : ℕ
⊢ (h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.ofNat m) = (𝟙 h.cochainComplex).f (Int.ofNat m)

case negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
⊢ (h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.negSucc 0) = (𝟙 h.cochainComplex).f (Int.negSucc 0)

case negSucc.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m : ℕ
⊢ (h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.negSucc (m + 1)) = (𝟙 h.cochainComplex).f (Int.negSucc (m + 1))
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm' = h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯

Tactic:
ext (m | _ | m)

Goal state after:
case ofNat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
m : ℕ
⊢ (h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.ofNat m) =
    (h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.ofNat m)

case negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ (h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.negSucc 0) =
    (h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.negSucc 0)

case negSucc.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
m : ℕ
⊢ (h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.negSucc (m + 1)) =
    (h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.negSucc (m + 1))
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 n : ℤ
α : Cocycle ((singleFunctor C p).obj X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = ↑α
hα : (Cochain.fromSingleMk (f ≫ K.d q q') ⋯).v p q' ⋯ = Cochain.v 0 p q' ⋯
⊢ f ≫ K.d q q' = 0

Tactic:
by simpa using hα

Goal state after:
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 ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : δ n (n + 1) ↑((n + 1).negOnePow • α) = 0
⊢ ∃ f, ∃ (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α

Tactic:
rw [coe_units_smul, δ_units_smul, ← hf, Cochain.δ_toSingleMk _ _ _ p' (by lia),
    smul_smul, Int.units_mul_self, one_smul] at hα

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : Cochain.toSingleMk (K.d p' p ≫ f) ⋯ = 0
⊢ ∃ f, ∃ (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α
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).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 ≫ ((F.map P.p).f ≫ (φ.app P.X).f) ≫ (φ'.app P.X).f

Tactic:
slice_rhs 1 2 => rw [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) ≫ (φ'.app P.X).f
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
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
P : Karoubi C
⊢ ((X.map ((toKaroubi C).map P.p)).f ≫ (φ.app ((toKaroubi C).obj P.X)).f) ≫ (Y.map P.decompId_p).f =
    (X.map P.decompId_p).f ≫ (φ.app P).f

Tactic:
rw [natTrans_eq φ P, P.decomp_p]

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
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
P : Karoubi C
⊢ ((X.map (P.decompId_p ≫ P.decompId_i)).f ≫ (φ.app ((toKaroubi C).obj P.X)).f) ≫ (Y.map P.decompId_p).f =
    (X.map P.decompId_p).f ≫ (X.map P.decompId_i ≫ φ.app { X := P.X, p := 𝟙 P.X, idem := ⋯ } ≫ Y.map P.decompId_p).f
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
inst✝ : IsIdempotentComplete D
⊢ (functorExtension C D).IsEquivalence

Tactic:
by
  rw [← karoubiUniversal_functor_eq]
  infer_instance

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

Tactic:
by
  apply kernel.lift_ι

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₁)
X X' : GradedObject I C
φ : X ⟶ X'
⊢ tensorHom φ (𝟙 tensorUnit) ≫ (rightUnitor X').hom = (rightUnitor X).hom ≫ φ

Tactic:
apply mapBifunctorRightUnitor_naturality

Goal state after: