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

Goal state before:
pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ (prevD n) h.hom =
    ((dNext (-n)) fun p q ↦
        (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom).op

Tactic:
refine (prevD_eq _ (j' := n - 1) (by dsimp; lia)).trans ?_

Goal state after:
case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ h.hom n (n - 1) ≫ ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).d (n - 1) n =
    ((dNext (-n)) fun p q ↦
        (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom).op
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
f :
  (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
      ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L)
⊢ ∃ a, toHom a = f

Tactic:
obtain ⟨f, rfl⟩ := Functor.map_surjective _ f
    exact ⟨mk (Cocycle.equivHomShift f), by simp [toHom_mk]⟩

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
L : CochainComplex C ℤ
x✝ : L.IsKInjective
K : HomologicalComplex C (ComplexShape.up ℤ)
f : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L
hK : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
⊢ f = 0

Tactic:
obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective f

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
L : CochainComplex C ℤ
x✝ : L.IsKInjective
K : HomologicalComplex C (ComplexShape.up ℤ)
hK : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
f : K ⟶ L
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f = 0
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
inst✝² : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
inst✝¹ : (weakEquivalences C).IsStableUnderRetracts
inst✝ : (weakEquivalences C).IsStableUnderComposition
x✝ : C
⊢ weakEquivalences C (𝟙 x✝)

Tactic:
rw [← weakEquivalence_iff]
    infer_instance

Goal state after:
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
inst✝² : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
inst✝¹ : (weakEquivalences C).IsStableUnderRetracts
inst✝ : (weakEquivalences C).IsStableUnderComposition
x✝³ x✝² : C
x✝¹ : x✝³ ⟶ x✝²
x✝ : IsIso x✝¹
⊢ weakEquivalences C x✝¹

Tactic:
rw [← weakEquivalence_iff]
    infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder

Goal state before:
pp: case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : Cylinder A
inst✝² : IsCofibrant A
P P' : Cylinder A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : P.I ⨿ A ⟶ (P.trans P').I := ⋯
⊢ coprod.inr ≫ coprod.map P.i₁ (𝟙 A) ≫ ψ = coprod.inr ≫ P'.i ≫ pushout.inr P.i₁ P'.i₀

Tactic:
· simp [ψ]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject

Goal state before:
pp: case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : PathObject A
inst✝² : IsFibrant A
P P' : PathObject A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : (P.trans P').P ⟶ P.P ⨯ A := ⋯
⊢ (ψ ≫ prod.map P.p₁ (𝟙 A)) ≫ prod.snd = (pullback.snd P.p₁ P'.p₀ ≫ P'.p) ≫ prod.snd

Tactic:
· simp [ψ]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : Cylinder X
h : P.LeftHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
⊢ weakEquivalences C P.π

Tactic:
rw [← weakEquivalence_iff]
    infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : PathObject Y
h : P.RightHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
⊢ weakEquivalences C P.ι

Tactic:
rw [← weakEquivalence_iff]
    infer_instance

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
⊢ ∀ ⦃X Y : CochainComplex.Plus C⦄ (f₀ f₁ : X ⟶ Y),
    (quotient C).map f₀ = (quotient C).map f₁ →
      ∃ P x, (homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C) P.π

Tactic:
rintro K L f₀ f₁ hf
    obtain ⟨f₀, rfl⟩ := ObjectProperty.homMk_surjective f₀
    obtain ⟨f₁, rfl⟩ := ObjectProperty.homMk_surjective f₁
    replace hf := homotopyOfEq f₀ f₁ ((HomotopyCategory.Plus.ι _).congr_map hf)
    exact ⟨K.precylinder, Precylinder.LeftHomotopy.fullSubcategoryEquiv.symm
      { h := cylinder.desc _ _ hf }, ⟨cylinder.homotopyEquiv _ (fun n ↦ ⟨n - 1, by simp⟩), rfl⟩⟩

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

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
t : TStructure C
X : C
a b : ℤ
inst✝ : t.IsGE X a
⊢ t.IsGE ((t.truncGT b).obj X) a

Tactic:
dsimp [truncGT]
  infer_instance

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
inst✝² : P.IsTriangulated
t : TStructure C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P.HasInducedTStructure t
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
⊢ t.IsLE (((P.tStructure t).truncLE n₀).obj { obj := T.obj₂, property := h₂ }).obj n₀

Tactic:
rw [← P.tStructure_isLE_iff]

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
inst✝² : P.IsTriangulated
t : TStructure C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P.HasInducedTStructure t
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
⊢ (P.tStructure t).IsLE (((P.tStructure t).truncLE n₀).obj { obj := T.obj₂, property := h₂ }) n₀
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
I : C
w✝ : Injective I
f : I ⟶ X
w : f ≫ g = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w }.Splitting
this : IsSplitEpi g
⊢ epiWithInjectiveKernel g

Tactic:
let e : I ≅ kernel g :=
      IsLimit.conePointUniqueUpToIso σ.shortExact.fIsKernel (limit.isLimit _)

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
I : C
w✝ : Injective I
f : I ⟶ X
w : f ≫ g = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w }.Splitting
this : IsSplitEpi g
e : I ≅ kernel g :=
  ⋯.fIsKernel.conePointUniqueUpToIso
    (limit.isLimit (parallelPair { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w }.g 0))
⊢ epiWithInjectiveKernel g
Module: Mathlib.Algebra.Homology.Factorizations.CM5b

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero
    ((HomologicalComplex.eval C (ComplexShape.up ℤ) i).obj (mappingCone (𝟙 (I K))) ⊞
      (HomologicalComplex.eval C (ComplexShape.up ℤ) i).obj L)

Tactic:
simp only [HomologicalComplex.eval_obj, biprod_isZero_iff, mappingCone.isZero_X_iff, I_X]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ (IsZero (Injective.under (K.X (i + 1))) ∧ IsZero (Injective.under (K.X i))) ∧ IsZero (L.X i)
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✝⁴ : L.functor.EssSurj
inst✝³ : R.functor.Full
inst✝² : R.IsInduced
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : B.HasLeftResolutions
⊢ T.HasLeftResolutions

Tactic:
by
  intro X₂
  let ρ : B.LeftResolution (R.functor.obj X₂) := Classical.arbitrary _
  obtain ⟨X₁, ⟨e⟩⟩ := Functor.EssSurj.mem_essImage L.functor ρ.X₁
  exact ⟨{
    X₁ := X₁
    w := R.functor.preimage (iso.hom.app X₁ ≫ B.functor.map e.hom ≫ ρ.w)
    hw := by
      simp only [← R.inverseImage_eq, MorphismProperty.inverseImage_iff, Functor.map_preimage]
      refine (W₂'.arrow_mk_iso_iff ?_).2 ρ.hw
      exact Arrow.isoMk (iso.app _ ≪≫ B.functor.mapIso e) (Iso.refl _) }⟩

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✝² : R₁.EssSurj
inst✝¹ : w.GuitartExact
inst✝ : (w ≫ᵥ w').GuitartExact
⊢ w'.GuitartExact

Tactic:
rw [guitartExact_iff_initial]
  intro Y₂
  rw [structuredArrowDownwards_initial_iff_of_iso _ (R₁.objObjPreimageIso Y₂).symm]
  have := Functor.initial_of_natIso (structuredArrowDownwardsComp w w' (R₁.objPreimage Y₂)).symm
  exact Functor.initial_of_initial_comp (w.structuredArrowDownwards (R₁.objPreimage Y₂)) _

Goal state after:
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₂ X₂' : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
g' : R.obj X₂' ⟶ B.obj X₃
γ : X₂' ⟶ X₂
hγ : R.map γ ≫ g = g'
A A' : w.CostructuredArrowDownwards g
φ : A ⟶ A'
⊢ (γ ≫ (CostructuredArrow.left A).hom) ≫ T.map (StructuredArrow.Hom.right φ.left) = γ ≫ (CostructuredArrow.left A').hom

Tactic:
rw [assoc, StructuredArrow.w]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
R₀ : (localizerMorphism C).RightResolution X :=
  { X₁ := mk (HoCat.resolutionObj X), w := HoCat.iResolutionObj X, hw := ⋯ }
⊢ IsConnected ((localizerMorphism C).RightResolution X)

Tactic:
have hR₀ (R) : Nonempty (Zigzag R R₀) := by
    have sq : CommSq R.w R₀.w (terminal.from _) (terminal.from _) := ⟨by simp⟩
    exact ⟨Zigzag.of_inv { f := homMk sq.lift }⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
R₀ : (localizerMorphism C).RightResolution X :=
  { X₁ := mk (HoCat.resolutionObj X), w := HoCat.iResolutionObj X, hw := ⋯ }
hR₀ : ∀ (R : (localizerMorphism C).RightResolution X), Nonempty (Zigzag R R₀)
⊢ IsConnected ((localizerMorphism C).RightResolution X)
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived

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₄
D₂ : Type u₅
inst✝⁷ : Category.{v₄, u₄} D₁
inst✝⁶ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
F : C₂ ⥤ H
F₁ : D₁ ⥤ H
α₁ : Φ.functor ⋙ F ⟶ L₁ ⋙ F₁
F₂ : D₂ ⥤ H
α₂ : F ⟶ L₂ ⋙ F₂
inst✝³ : F₁.IsRightDerivedFunctor α₁ W₁
inst✝² : Φ.IsRightDerivabilityStructure
inst✝¹ : (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst✝ : F₂.IsRightDerivedFunctor α₂ W₂
this : F.HasPointwiseRightDerivedFunctor W₂
⊢ IsIso
    (F₁.rightDerivedDesc α₁ W₁ (Φ.localizedFunctor L₁ L₂ ⋙ F₂)
      (Φ.functor.whiskerLeft α₂ ≫
        (Φ.functor.associator L₂ F₂).inv ≫
          whiskerRight (CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom F₂ ≫
            (L₁.associator (Φ.localizedFunctor L₁ L₂) F₂).hom))

Tactic:
rw [← isRightDerivedFunctor_iff_isIso_rightDerivedDesc,
    isRightDerivedFunctor_iff_isLeftKanExtension]

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₄
D₂ : Type u₅
inst✝⁷ : Category.{v₄, u₄} D₁
inst✝⁶ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
F : C₂ ⥤ H
F₁ : D₁ ⥤ H
α₁ : Φ.functor ⋙ F ⟶ L₁ ⋙ F₁
F₂ : D₂ ⥤ H
α₂ : F ⟶ L₂ ⋙ F₂
inst✝³ : F₁.IsRightDerivedFunctor α₁ W₁
inst✝² : Φ.IsRightDerivabilityStructure
inst✝¹ : (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst✝ : F₂.IsRightDerivedFunctor α₂ W₂
this : F.HasPointwiseRightDerivedFunctor W₂
⊢ (Φ.localizedFunctor L₁ L₂ ⋙ F₂).IsLeftKanExtension
    (Φ.functor.whiskerLeft α₂ ≫
      (Φ.functor.associator L₂ F₂).inv ≫
        whiskerRight (CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom F₂ ≫
          (L₁.associator (Φ.localizedFunctor L₁ L₂) F₂).hom)
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✝⁴ : W₂'.RespectsIso
inst✝³ : L.IsInduced
inst✝² : L.functor.IsEquivalence
inst✝¹ : R.IsInduced
inst✝ : R.functor.IsEquivalence
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
x✝ : B.IsLeftDerivabilityStructure
⊢ T.IsLeftDerivabilityStructure

Tactic:
let e : B.functor ⋙ R.inv.functor ≅ L.inv.functor ⋙ T.functor :=
      (leftUnitor _).symm ≪≫
        isoWhiskerRight L.functor.asEquivalence.counitIso.symm _ ≪≫
        associator _ _ _ ≪≫ isoWhiskerLeft _ (associator _ _ _).symm ≪≫
        isoWhiskerLeft _ (isoWhiskerRight iso.symm R.inv.functor) ≪≫
        isoWhiskerLeft _ (associator _ _ _) ≪≫
        isoWhiskerLeft _ (isoWhiskerLeft _ R.functor.asEquivalence.unitIso.symm) ≪≫
        (associator _ _ _).symm ≪≫ rightUnitor _

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✝⁴ : W₂'.RespectsIso
inst✝³ : L.IsInduced
inst✝² : L.functor.IsEquivalence
inst✝¹ : R.IsInduced
inst✝ : R.functor.IsEquivalence
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
x✝ : B.IsLeftDerivabilityStructure
e : B.functor ⋙ R.inv.functor ≅ L.inv.functor ⋙ T.functor :=
  (B.functor ⋙ R.inv.functor).leftUnitor.symm ≪≫
    isoWhiskerRight L.functor.asEquivalence.counitIso.symm (B.functor ⋙ R.inv.functor) ≪≫
      L.functor.asEquivalence.inverse.associator L.functor.asEquivalence.functor (B.functor ⋙ R.inv.functor) ≪≫
        L.functor.asEquivalence.inverse.isoWhiskerLeft
            (L.functor.asEquivalence.functor.associator B.functor R.inv.functor).symm ≪≫
          L.functor.asEquivalence.inverse.isoWhiskerLeft (isoWhiskerRight iso.symm R.inv.functor) ≪≫
            L.functor.asEquivalence.inverse.isoWhiskerLeft (T.functor.associator R.functor R.inv.functor) ≪≫
              L.functor.asEquivalence.inverse.isoWhiskerLeft
                  (T.functor.isoWhiskerLeft R.functor.asEquivalence.unitIso.symm) ≪≫
                (L.functor.asEquivalence.inverse.associator T.functor (𝟭 C₂)).symm ≪≫
                  (L.functor.asEquivalence.inverse ⋙ T.functor).rightUnitor
⊢ T.IsLeftDerivabilityStructure
Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K : CochainComplex C ℤ
x✝ : K.IsKProjective
L : HomologicalComplex C (ComplexShape.up ℤ)
f : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L
hL : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)
⊢ f = 0

Tactic:
obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective f

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K : CochainComplex C ℤ
x✝ : K.IsKProjective
L : HomologicalComplex C (ComplexShape.up ℤ)
hL : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)
f : K ⟶ L
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K : CochainComplex C ℤ
x✝ : K.IsKProjective
L : HomologicalComplex C (ComplexShape.up ℤ)
hL : L.Acyclic
f : K ⟶ L
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f = 0

Tactic:
HomotopyCategory.eq_of_homotopy f 0 (IsKProjective.homotopyZero f hL),

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K : CochainComplex C ℤ
x✝ : K.IsKProjective
L : HomologicalComplex C (ComplexShape.up ℤ)
hL : L.Acyclic
f : K ⟶ L
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map 0 = 0
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m✝ : ℤ
m : ℕ
hnm : Int.negSucc 0 + 1 ≠ Int.ofNat m
⊢ h.d (Int.negSucc 0) (Int.ofNat m) = 0

pp: case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
m n : ℕ
hnm : Int.negSucc (n + 1) + 1 ≠ Int.ofNat m
⊢ h.d (Int.negSucc (n + 1)) (Int.ofNat m) = 0

Tactic:
· obtain _ | m := m
      · simp at hnm
      · rfl

Goal state after:
case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
m n : ℕ
hnm : Int.negSucc (n + 1) + 1 ≠ Int.ofNat m
⊢ h.d (Int.negSucc (n + 1)) (Int.ofNat m) = 0
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: case e_a
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ 𝟙 P = P.decompId_i ≫ P.decompId_p

Tactic:
apply decompId

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 : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
⊢ ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (φ.app P.X).f) ≫ ((obj G).obj P).p = (F.map P.p).f ≫ (φ.app P.X).f

Tactic:
have h := φ.naturality P.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
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : F.map P.p ≫ φ.app P.X = φ.app P.X ≫ G.map P.p
⊢ ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (φ.app P.X).f) ≫ ((obj G).obj P).p = (F.map P.p).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
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
⊢ (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:
have h := φ.naturality P.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
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
⊢ (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