mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: 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
Y : C
⊢ P.trW.isLocal Y ↔ P.rightOrthogonal Y

Tactic:
refine ⟨fun hY X f hX ↦ ?_, fun hY X₁ X₂ f ⟨X₃, g, h, hT, hX₃⟩ ↦ ⟨?_, fun α ↦ ?_⟩⟩

Goal state after:
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
Y : C
hY : P.trW.isLocal Y
X : C
f : X ⟶ Y
hX : P X
⊢ f = 0

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
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
x✝ : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hT : Triangle.mk f g h ∈ distinguishedTriangles
hX₃ : P X₃
⊢ Function.Injective fun g ↦ f ≫ g

case refine_3
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
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
x✝ : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hT : Triangle.mk f g h ∈ distinguishedTriangles
hX₃ : P X₃
α : X₁ ⟶ Y
⊢ ∃ a, (fun g ↦ f ≫ g) a = α
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: case refine_2.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₃
Y₁ : C
f : Y₁ ⟶ Y₂
g : Y₃ ⟶ (shiftFunctor C 1).obj Y₁
hT : Triangle.mk f h g ∈ distinguishedTriangles
hY₁ : P Y₁
α : X ⟶ Y₃
⊢ ∃ a, (fun f ↦ f ≫ h) a = α

Tactic:
obtain ⟨β, rfl⟩ := Triangle.coyoneda_exact₂ _ (rot_of_distTriang _ hT)
        α (hX _ (P.le_shift _ _ hY₁))
      exact ⟨β, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (K.extendXIso e ⋯).hom ≫ (dNext i) h.hom ≫ (L.extendXIso e ⋯).inv = (dNext (e.f i)) (extend.hom e h.hom)

Tactic:
rw [dNext_eq_zero _ _ hi]
          by_cases hi' : c'.Rel (e.f i) (c'.next (e.f i))
          · simp [dNext_eq _ hi', K.extend_d_from_eq_zero _ _ _ _ rfl hi]
          · simp [dNext_eq_zero _ _ hi']

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

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 Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst✝¹ : t.IsLE X n₀
inst✝ : t.IsGE Y n₁
⊢ f = 0

Tactic:
have := t.isLE_shift X n₀ n₀ 0 (add_zero n₀)

Goal state after:
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst✝¹ : t.IsLE X n₀
inst✝ : t.IsGE Y n₁
this : t.IsLE ((shiftFunctor C n₀).obj X) 0
⊢ f = 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

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
n : ℤ
X : C
i : ℤ
h✝ : t.IsGE X i
⊢ t.plus.shift n X

Tactic:
exact ⟨i - n, t.isGE_shift _ i _ _ (by omega)⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (fun X ↦ ∃ K x, K.IsStrictlyLE 0) ≤ fun X ↦ ∃ K x, K.IsStrictlyLE 1

Tactic:
by
    rintro X ⟨K, e, _⟩
    exact ⟨K, e, K.isStrictlyLE_of_le 0 1 (by lia)⟩

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
f : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
⊢ ∃ α, δ m n α = ↑z

Tactic:
refine ⟨n.negOnePow • Cochain.rightUnshift f m (by lia), ?_⟩

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
⊢ δ m n (n.negOnePow • f.rightUnshift m ⋯) = ↑z
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
inst✝ : IsCofibrant X
f g : X ⟶ Y
⊢ mk f = mk g ↔ LeftHomotopyRel f g

Tactic:
by
  rw [← (LeftHomotopyRel.equivalence X Y).eqvGen_iff]
  exact Quot.eq

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
⊢ (quotient C).Full

Tactic:
dsimp [quotient]

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
⊢ ((plus C).lift (CochainComplex.Plus.ι C ⋙ HomotopyCategory.quotient C (ComplexShape.up ℤ)) ⋯).Full
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated

Goal state before:
pp: case refine_2
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
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
⊢ w₁₃ ≫ (shiftFunctor Cᵒᵖ 1).map u₁₂ = o.m₁.op ≫ w₂₃

Tactic:
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

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
n : ℤ
⊢ (t.truncLE n).Additive

Tactic:
dsimp only [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
n : ℤ
⊢ (t.truncLT (n + 1)).Additive
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:
refine ⟨fun _ _ ↦ inferInstance, fun _ ↦ ?_⟩
  have : IsIso (ι.map f) := by rwa [DerivedCategory.isIso_iff]
  exact isIso_of_fully_faithful ι _

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
⊢ epiWithInjectiveKernel g ↔
    ∃ I,
      ∃ (_ : Injective I),
        ∃ f, ∃ (w : f ≫ g = 0), Nonempty { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w }.Splitting

Tactic:
constructor
  · rintro ⟨_, _⟩
    let S := ShortComplex.mk (kernel.ι g) g (by simp)
    exact ⟨_, inferInstance, _, S.zero,
      ⟨ShortComplex.Splitting.ofExactOfRetraction S
        (S.exact_of_f_is_kernel (kernelIsKernel g)) (Injective.factorThru (𝟙 _) (kernel.ι g))
        (by simp [S]) inferInstance⟩⟩
  · rintro ⟨I, _, f, w, ⟨σ⟩⟩
    have : IsSplitEpi g := ⟨σ.s, σ.s_g⟩
    let e : I ≅ kernel g :=
      IsLimit.conePointUniqueUpToIso σ.shortExact.fIsKernel (limit.isLimit _)
    exact ⟨inferInstance, Injective.of_iso e inferInstance⟩

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
⊢ ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful

Tactic:
let := Localization.preadditive L₂ B.trW

Goal state after:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
this✝ : Preadditive D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
this : Preadditive D₂ := Localization.preadditive L₂ B.trW
⊢ ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful
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
⊢ (I K).IsStrictlyGE n

Tactic:
rw [isStrictlyGE_iff]
  intro i hi
  exact Injective.isZero_under _ (K.isZero_of_isStrictlyGE n i hi)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
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
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr) ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.f +
      { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.g ≫
        σ₂.s ≫ σ₁.s =
    𝟙 { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.X₂

Tactic:
by
            dsimp
            have h := g₁ ≫= σ₂.id =≫ σ₁.s
            simp only [add_comp, assoc, comp_add, id_comp] at h
            rw [← σ₁.id, ← h]
            simp only [comp_add, add_comp, assoc, BinaryBicone.inl_fst_assoc,
              BinaryBicone.inr_fst_assoc, zero_comp, comp_zero, add_zero,
              BinaryBicone.inl_snd_assoc, BinaryBicone.inr_snd_assoc, zero_add]
            abel

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: case zero.succ.succ.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ 0) (hjk : 0 ≤ k),
    map f 0 k ⋯ = map f 0 0 hij ≫ map f 0 k hjk
hij : 0 ≤ 0 + 1
hjk : 0 + 1 ≤ 0 + 1
⊢ map f 0 (0 + 1) ⋯ = map f 0 (0 + 1) hij ≫ 𝟙 (X (0 + 1))

Tactic:
comp_id

Goal state after:
case zero.succ.succ.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ 0) (hjk : 0 ≤ k),
    map f 0 k ⋯ = map f 0 0 hij ≫ map f 0 k hjk
hij : 0 ≤ 0 + 1
hjk : 0 + 1 ≤ 0 + 1
⊢ map f 0 (0 + 1) ⋯ = map f 0 (0 + 1) hij
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

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

Tactic:
by_cases h : a ≤ b + 1
  · exact t.isLE_truncLT_obj ..
  · have := (t.isLE_iff_isIso_truncLTι_app (a - 1) a (by lia) X).1 (t.isLE_of_le _ b _ (by lia))
    exact t.isLE_of_iso (show X ≅ _ from (asIso ((t.truncLTι a).app X)).symm) _

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 q : ℤ
hq : q < n
⊢ QuasiIsoAt (π f n) q

Tactic:
have := mono_homologyMap_π f n q (by lia)
  have := epi_homologyMap_π f n q hq
  rw [quasiIsoAt_iff_isIso_homologyMap]
  apply Balanced.isIso_of_mono_of_epi

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

Goal state before:
pp: case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
⊢ IsIso α

Tactic:
have : ∀ (X₂ : D₂), IsIso (α.app X₂) := fun X₂ => by
      have := Φ.essSurj_of_hasLeftResolutions L₂
      rw [← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)]
      apply hα

Goal state after:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
this : ∀ (X₂ : D₂), IsIso (α.app X₂)
⊢ IsIso α
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

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

Tactic:
rw [← hasPointwiseLeftKanExtensionAt_iff_of_equivalence W.Q L F
    (Localization.uniq W.Q L W) (Localization.compUniqFunctor W.Q L W) (W.Q.obj X) (L.obj X)
    ((Localization.compUniqFunctor W.Q L W).app X)]
  exact ⟨fun h ↦ h.hasColimit', fun h ↦ ⟨h⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: case refine_1
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
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  (e.hom.app X₂ ≫ G.map φ) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk φ)
eq : F.map f ≫ s.ι.app (CostructuredArrow.mk φ) = s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)) ≫ 𝟙 s.pt
⊢ (e.hom.app X₁ ≫ G.map (L.map f ≫ φ)) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk (L.map f ≫ φ))

Tactic:
comp_id

Goal state after:
case refine_1
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
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  (e.hom.app X₂ ≫ G.map φ) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk φ)
eq : F.map f ≫ s.ι.app (CostructuredArrow.mk φ) = s.ι.app (CostructuredArrow.mk (L.map f ≫ φ))
⊢ (e.hom.app X₁ ≫ G.map (L.map f ≫ φ)) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk (L.map f ≫ φ))
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φ :
  (e.hom.app X₁ ≫ G.map φ) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk φ)
this : IsIso (F.map w)
eq :
  F.map w ≫ s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)) =
    s.ι.app (CostructuredArrow.mk φ) ≫ 𝟙 s.pt
⊢ (e.hom.app X₂ ≫ G.map ((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:
comp_id

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φ :
  (e.hom.app X₁ ≫ G.map φ) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk φ)
this : IsIso (F.map w)
eq :
  F.map w ≫ s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)) = s.ι.app (CostructuredArrow.mk φ)
⊢ (e.hom.app X₂ ≫ G.map ((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.Algebra.Homology.Embedding.StupidTrunc

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
i' : ι'
hi' : e.f i = i'
⊢ (K.restriction e).X i = K.X i'

Tactic:
by subst hi'; rfl

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
⊢ F.map X.d ≫
      ((shiftFunctor C 1 ⋙ F).map X.d ≫ η.app ((shiftFunctor C 1).obj X.obj)) ≫ (shiftFunctor D 1).map (η.app X.obj) =
    0

Tactic:
Functor.comp_map

Goal state after:
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
⊢ F.map X.d ≫
      (F.map ((shiftFunctor C 1).map X.d) ≫ η.app ((shiftFunctor C 1).obj X.obj)) ≫
        (shiftFunctor D 1).map (η.app X.obj) =
    0
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₁ i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi₀₁ : c.Rel i i₁
hj : j = i₁
⊢ ((if hk : i = i ∧ j = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) ≫
      if hk : j = i ∧ k = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) =
    0

Tactic:
subst hj
        nth_rw 2 [dif_neg (by tauto)]
        rw [comp_zero]

Goal state after:
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₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ 𝟙 (K.X i₀) = (doubleXIso₀ f hi₀₁).hom ≫ φ₀

Tactic:
comp_id

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ = (doubleXIso₀ f hi₀₁).hom ≫ φ₀