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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ c₁.ε₁ c₂ c (i₁, i₂) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d₂ c i₁ i₂ j =
    -(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j

Tactic:
rw [HomologicalComplex₂.d₂_eq _ _ _ hi₂ _ hj', HomologicalComplex₂.d₂_eq _ _ _ hi₂ _
        (by rw [← c.next_eq' (ComplexShape.rel_π₂ c₁ c i₁' hi₂), hj]),
    Linear.comp_units_smul, Linear.comp_units_smul, Linear.units_smul_comp, assoc,
    ιMapBifunctor_hom₁ _ _ _ _ _ _ _ _ _ _ (c₁.prev_eq' hi₁),
    ιMapBifunctorOrZero_eq _ _ _ _ _ _ _ hj',
    Linear.comp_units_smul, smul_smul, smul_smul,
    Functor.mapBifunctorHomologicalComplex_obj_obj_X_d,
    Functor.mapBifunctorHomologicalComplex_obj_obj_X_d,
    NatTrans.naturality_assoc, ComplexShape.ε₁_ε₂ c hi₁ hi₂, neg_mul, Units.neg_smul, neg_inj,
    smul_left_cancel_iff, ← Functor.map_comp_assoc, ← Functor.map_comp_assoc, f₂.comm]

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

Goal state before:
pp: case pos
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : ¬c₁.Rel (c₁.prev i₁) i₁
h₄ : c₂.Rel i₂ (c₂.next i₂)
⊢ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁ i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j = 0

Tactic:
by_cases h₅ : c.Rel j (c.next j)
        · rw [HomologicalComplex₂.d₂_eq _ _ _ h₄ _ (by rw [← ComplexShape.next_π₂ c₁ c i₁ h₄, h]),
            Linear.units_smul_comp, assoc, Functor.mapBifunctorHomologicalComplex_obj_obj_X_d,
            ιMapBifunctor_hom₁ _ _ _ _ _ _ _ _ _ _ rfl, h₁.zero _ _ h₃,
            Functor.map_zero, zero_app, zero_comp, smul_zero, comp_zero, smul_zero]
        · rw [zero₁ _ _ _ _ _ _ h₅, comp_zero]

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

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      ((shiftFunctor₂ C y).obj K).D₁ (up ℤ) n₀ n₁ ≫
        ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₁' ⋯) =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (y.negOnePow •
        (((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₀' ⋯) ≫
          K.D₁ (up ℤ) n₀' n₁')

Tactic:
rw [ι_D₁_assoc, Linear.comp_units_smul, ι_totalDesc_assoc, Linear.units_smul_comp,
      ι_D₁, smul_smul, ((shiftFunctor₂ C y).obj K).d₁_eq _ rfl _ _ (by dsimp; lia),
      K.d₁_eq _ rfl _ _ (by dsimp; lia)]

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (((up ℤ).ε₁ (up ℤ) (up ℤ) (p, q) •
        (((shiftFunctor₂ C y).obj K).d p (p + 1)).f q ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₁' ⋯) =
    (y.negOnePow * (p * y).negOnePow) •
      (up ℤ).ε₁ (up ℤ) (up ℤ) (p, q + y) • (K.d p (p + 1)).f (q + y) ≫ K.ιTotal (up ℤ) (p + 1) (q + y) n₁' ⋯
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' : ℤ
hb' : b' = b + y
n' : ℤ
hn' : n' = n + y
⊢ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h ≫ (K.totalShift₂Iso y).hom.f n =
    (a * y).negOnePow •
      (K.shiftFunctor₂XXIso a b y b' hb').hom ≫
        K.ιTotal (up ℤ) a b' n' ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n n' hn').inv

Tactic:
subst hb' hn'
  dsimp [totalShift₂Iso, totalShift₂XIso]
  simp only [ι_totalDesc, comp_id, id_comp]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
hφ : Cochain.ofHom φ = (↑z).rightShift n 0 ⋯
h : Homotopy φ 0
⊢ ∃ α, δ m n α = ↑z

Tactic:
obtain ⟨f, hf⟩ := Cochain.equivHomotopy _ _ h

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
hφ : Cochain.ofHom φ = (↑z).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f + Cochain.ofHom 0
⊢ ∃ α, δ m n α = ↑z
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasCoproduct A
inst✝ : Limits.HasCoproduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.llp (f j)
X Y : C
⊢ ∀ (g : X ⟶ Y), T g → HasLiftingProperty (Limits.Sigma.map f) g

Tactic:
p

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasCoproduct A
inst✝ : Limits.HasCoproduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.llp (f j)
X Y : C
p : X ⟶ Y
⊢ T p → HasLiftingProperty (Limits.Sigma.map f) p
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasProduct A
inst✝ : Limits.HasProduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.rlp (f j)
X Y : C
⊢ ∀ (g : X ⟶ Y), T g → HasLiftingProperty g (Limits.Pi.map f)

Tactic:
p

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasProduct A
inst✝ : Limits.HasProduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.rlp (f j)
X Y : C
p : X ⟶ Y
⊢ T p → HasLiftingProperty p (Limits.Pi.map f)
Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
A : C
inst✝⁷ : CategoryWithWeakEquivalences C
P : Cylinder A
inst✝⁶ : HasBinaryCoproduct A A
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : HasInitial C
inst✝³ : (cofibrations C).IsStableUnderComposition
inst✝² : (cofibrations C).IsStableUnderCobaseChange
inst✝¹ : IsCofibrant A
inst✝ : P.IsGood
⊢ Cofibration P.i₀

Tactic:
by
  rw [← P.inl_i]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : Cofibration i
hp : Fibration p ∧ WeakEquivalence p
this : Fibration p
⊢ HasLiftingProperty i p

Tactic:
have := hp.2

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : Cofibration i
hp : Fibration p ∧ WeakEquivalence p
this✝ : Fibration p
this : WeakEquivalence p
⊢ HasLiftingProperty i p
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
P : Cylinder X
f g : X ⟶ Y
h : P.LeftHomotopy f g
⊢ ∃ P', P'.IsGood ∧ Nonempty (P'.LeftHomotopy f g)

Tactic:
let d := MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.i

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
P : Cylinder X
f g : X ⟶ Y
h : P.LeftHomotopy f g
d : (cofibrations C).MapFactorizationData (trivialFibrations C) P.i :=
  (cofibrations C).factorizationData (trivialFibrations C) P.i
⊢ ∃ P', P'.IsGood ∧ Nonempty (P'.LeftHomotopy f g)
Module: Mathlib.CategoryTheory.Localization.OfQuotient

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
L : C ⥤ D
inst✝¹ : L.EssSurj
inst✝ : L.Full
W : MorphismProperty C
hW : W.IsInvertedBy L
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.π
F : Quotient L.homRel ⥤ D := Quotient.lift L.homRel L ⋯
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
hf : W f
⊢ IsIso ((Quotient.functor L.homRel).map f)

Tactic:
by
    have : IsIso (F.map ((Quotient.functor L.homRel).map f)) := hW _ hf
    apply isIso_of_reflects_iso _ F

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
K : Plus C
⊢ (quotient C).essImage K

Tactic:
obtain ⟨L, rfl⟩ := quotient_obj_surjective K

Goal state after:
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
L : CochainComplex.Plus C
⊢ (quotient C).essImage ((quotient C).obj L)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
⊢ ∀ {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : u₁₂ ≫ u₂₃ = u₁₃)
    {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁}
    (h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : X₃ ⟶ Z₂₃}
    {w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂} (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles)
    {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁}
    (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles),
    Nonempty (Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
intro X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ u₁₂ u₂₃ u₁₃ comm v₁₂ w₁₂ h₁₂ v₂₃ w₂₃ h₂₃ v₁₃ w₁₃ h₁₃
    let o := Triangulated.someOctahedron' (by aesop) ((mem_distTriang_op_iff _).mp h₂₃)
      ((mem_distTriang_op_iff _).mp h₁₂) ((mem_distTriang_op_iff _).mp h₁₃)
    refine ⟨o.m₃.op, o.m₁.op, congr($(o.comm₄).op), ?_, congr($(o.comm₁).op), ?_, ?_⟩
    · have eq₃ := congr($(o.comm₃).op)
      dsimp at eq₃
      rw [← Category.assoc, ← op_comp, ← Functor.map_comp,
        NatIso.cancel_natIso_inv_right (opShiftFunctorEquivalence C _).unitIso] at eq₃
      exact congr($(Functor.map_injective _ congr($(eq₃).unop)).op)
    · have eq₂ := congr($(o.comm₂).op)
      dsimp at eq₂
      rw [← Category.assoc, ← op_comp, ← Functor.map_comp, Category.assoc,
        ← opShiftFunctorEquivalence_unitIso_inv_naturality, ← Category.assoc,
        NatIso.cancel_natIso_inv_right (opShiftFunctorEquivalence C _).unitIso, ← op_comp,
        ← Functor.map_comp] at eq₂
      exact congr($(Functor.map_injective _ congr($(eq₂).unop)).op).symm
    · have := op_distinguished _ o.mem
      dsimp at this
      convert! this using 2
      rw [Category.assoc, Functor.map_comp, Functor.map_comp,
        ← opShiftFunctorEquivalence_counitIso_hom_app_shift,
        ← opShiftFunctorEquivalence_counitIso_inv_naturality_assoc, Iso.inv_hom_id_app_assoc]

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
a : ℤ
⊢ (t.truncLEIsoTruncLT a (a + 1) ⋯).inv ≫ t.truncLEι a = t.truncLTι (a + 1)

Tactic:
dsimp [truncLEIsoTruncLT, truncLEι, truncLE]

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
t : TStructure C
a : ℤ
⊢ 𝟙 (t.truncLT (a + 1)) ≫ t.truncLTι (a + 1) = t.truncLTι (a + 1)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case mp
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 : ℤ
X : C
h : t.IsGE X n
e : (contractibleTriangle X).invRotate ≅ (t.triangleLTGE n).obj X
he : e.hom.hom₂ = (Iso.refl X).hom
⊢ IsIso ((t.truncGEπ n).app X)

Tactic:
dsimp at he

Goal state after:
case mp
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 : ℤ
X : C
h : t.IsGE X n
e : (contractibleTriangle X).invRotate ≅ (t.triangleLTGE n).obj X
he : e.hom.hom₂ = 𝟙 X
⊢ IsIso ((t.truncGEπ n).app X)
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 ℤ
⊢ degreewiseEpiWithInjectiveKernel (p K L)

Tactic:
intro n

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K L : CochainComplex C ℤ
n : ℤ
⊢ epiWithInjectiveKernel ((p K L).f n)
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: case mp
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₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this✝ : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ := (CatCommSq.vInvEquiv H₂ eL eR H₃) inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ L₁.isoWhiskerLeft eL.unitIso.symm ≪≫ L₁.rightUnitor
⊢ w.GuitartExact

Tactic:
let β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
      Functor.associator _ _ _ ≪≫ Functor.isoWhiskerLeft R₁ eR.unitIso.symm ≪≫ R₁.rightUnitor

Goal state after:
case mp
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₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this✝ : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ := (CatCommSq.vInvEquiv H₂ eL eR H₃) inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ L₁.isoWhiskerLeft eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ R₁.isoWhiskerLeft eR.unitIso.symm ≪≫ R₁.rightUnitor
⊢ w.GuitartExact
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case inr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝² : EnoughInjectives C
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
hq : n ≤ n
this✝ : Mono (homologyMap (π f n) n)
this : Mono (homologyMap (mappingCocone.triangle (α f n)).mor₁ n)
⊢ QuasiIsoAt (ι f n) n

Tactic:
have h₁ := (exact_homologyShortComplex f n).fIsKernel

Goal state after:
case inr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝² : EnoughInjectives C
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
hq : n ≤ n
this✝ : Mono (homologyMap (π f n) n)
this : Mono (homologyMap (mappingCocone.triangle (α f n)).mor₁ n)
h₁ : IsLimit (KernelFork.ofι (homologyShortComplex f n).f ⋯)
⊢ QuasiIsoAt (ι f n) n
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₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
b : L.obj X₁ ⟶ X₃
φ : CostructuredArrow.mk g ⟶ (w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)
⊢ ∃ X₁_1 a b_1, ∃ (comm : R.map a ≫ w.app X₁_1 ≫ B.map b_1 = g), StructuredArrow.mk φ = mk w g X₁_1 a b_1 comm

Tactic:
obtain ⟨a, ha, rfl⟩ := CostructuredArrow.homMk_surjective φ

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
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
b : L.obj X₁ ⟶ X₃
a : (CostructuredArrow.mk g).left ⟶ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).left
ha : R.map a ≫ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).hom = (CostructuredArrow.mk g).hom
⊢ ∃ X₁_1 a_1 b_1,
    ∃ (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b_1 = g),
      StructuredArrow.mk (CostructuredArrow.homMk a ha) = mk w g X₁_1 a_1 b_1 comm
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
K : Plus (InjectiveObject C)
⊢ ∀ (n : ℤ), Injective (((InjectiveObject.ι C).mapCochainComplexPlus.obj K).obj.X n)

Tactic:
intro n

Goal state after:
C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
K : Plus (InjectiveObject C)
n : ℤ
⊢ Injective (((InjectiveObject.ι C).mapCochainComplexPlus.obj K).obj.X n)
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
⊢ (localizerMorphism C).IsRightDerivabilityStructure

Tactic:
LocalizerMorphism.isRightDerivabilityStructure_iff_of_equivalences
    (T := localizerMorphism C) (B := FibrantObject.localizerMorphism (Plus C))
    (R := .id _) (L := fibrantObjectLocalizerMorphism C) (Iso.refl _)

Goal state after:
C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
⊢ (FibrantObject.localizerMorphism (Plus C)).IsRightDerivabilityStructure
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K L : Plus (InjectiveObject C)
f : K ⟶ L
hf : IsIso f
⊢ ∀ (n : ℤ),
    IsIso
      ((homologyFunctor C (ComplexShape.up ℤ) n).map ((ι C).map ((InjectiveObject.ι C).mapHomotopyCategoryPlus.map f)))

Tactic:
intro n

Goal state after:
C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K L : Plus (InjectiveObject C)
f : K ⟶ L
hf : IsIso f
n : ℤ
⊢ IsIso
    ((homologyFunctor C (ComplexShape.up ℤ) n).map ((ι C).map ((InjectiveObject.ι C).mapHomotopyCategoryPlus.map f)))
Module: Mathlib.CategoryTheory.DifferentialObject

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

Tactic:
shiftComm_hom_comp

Goal state after:
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ (CategoryTheory.shiftFunctor C n).map X✝.d ≫
      (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C 1).map f.f) ≫ (shiftComm Y✝.obj 1 n).hom =
    (CategoryTheory.shiftFunctor C n).map f.f ≫
      (CategoryTheory.shiftFunctor C n).map Y✝.d ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ¬∃ k, c.Rel j k
⊢ (eval C c j ⋙ coyoneda.obj (op X)).CorepresentableBy ((single C c j).obj X)

Tactic:
apply evalCompCoyonedaCorepresentableBySingle
    obtain _ | _ := c.exists_distinct_prev_or j <;> tauto

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
G : Karoubi C ⥤ Karoubi D
⊢ { app := fun P ↦ { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ } ≫
      { app := fun P ↦ { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ } =
    𝟙 (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G)

Tactic:
ext P
          simpa only [hom_ext_iff, G.map_comp, G.map_id] using! G.congr_map P.decomp_p.symm

Goal state after: