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

Goal state before:
pp: C : Type u_1
inst✝²⁰ : Category.{v_1, u_1} C
inst✝¹⁹ : HasZeroObject C
inst✝¹⁸ : HasShift C ℤ
inst✝¹⁷ : Preadditive C
inst✝¹⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁵ : Pretriangulated C
D : Type u_2
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Preadditive D
inst✝¹² : HasZeroObject D
inst✝¹¹ : HasShift D ℤ
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁹ : Pretriangulated D
E : Type u_3
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : HasShift E ℤ
P : ObjectProperty C
inst✝⁶ : P.IsTriangulated
F : E ⥤ C
hF : ∀ (X : E), P (F.obj X)
inst✝⁵ : Preadditive E
inst✝⁴ : F.CommShift ℤ
inst✝³ : HasZeroObject E
inst✝² : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝¹ : Pretriangulated E
inst✝ : F.IsTriangulated
⊢ (P.lift F hF).IsTriangulated

Tactic:
by
  rw [Functor.isTriangulated_iff_comp_right (P.liftCompιIso F hF)]
  infer_instance

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
hjk' : ¬c.Rel j k
⊢ j = k

Tactic:
by
      simpa only [c.next_eq_self j (by simpa only [hjk] using hjk')] using hjk

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

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 : HomologicalComplex C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
⊢ e.f k = c'.next (e.f j)

Tactic:
c'.next_eq' (e.rel hjk)

Goal state after:
ι : 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 : HomologicalComplex C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
⊢ e.f k = e.f k
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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 : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : c.Rel j k
⊢ e.f k = c'.next (e.f j)

Tactic:
c'.next_eq' (e.rel hjk)

Goal state after:
ι : 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 : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : c.Rel j k
⊢ e.f k = e.f k
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ ((K.restriction e).sc' i j k).HasHomology

Tactic:
subst hi hk; assumption

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

Goal state before:
pp: case e_a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.sc j').pOpcycles ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv =
    (K.restrictionXIso e hj').inv ≫ ((K.restriction e).sc j).pOpcycles

Tactic:
apply pOpcycles_restrictionOpcyclesIso_inv

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
hi : ∃ i, e.f i = c'.prev j'
⊢ Epi φ.τ₁

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✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
hi : ¬∃ i, e.f i = c'.prev j'
⊢ Epi φ.τ₁

Tactic:
· obtain ⟨i, hi⟩ := hi
        dsimp [φ, πTruncGE]
        rw [e.epi_liftExtend_f_iff _ _ hi]
        infer_instance

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
hi : ¬∃ i, e.f i = c'.prev j'
⊢ Epi φ.τ₁
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
a✝ : K.IsSupported e
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ QuasiIsoAt (K.πTruncGE e) i'

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✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
a✝ : K.IsSupported e
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ QuasiIsoAt (K.πTruncGE e) i'

Tactic:
· obtain ⟨i, rfl⟩ := hi'
      infer_instance

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
a✝ : K.IsSupported e
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ QuasiIsoAt (K.πTruncGE e) i'
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncLE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryLE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncLE' e).HasHomology j
this : (K.op.restriction e.op).HasHomology j
⊢ QuasiIsoAt (K.op.restrictionToTruncGE' e.op) j

Tactic:
exact truncGE'.quasiIsoAt_restrictionToTruncGE' K.op e.op j (by simpa)

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

Goal state before:
pp: case inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ : ι₂
hi : ∀ (i₂_1 : ι₂), e₂.f i₂_1 ≠ e₂.f i₂
⊢ ∃ i₁, e₂.f i₂ = e₁.f i₁

Tactic:
· exfalso
    exact hi i₂ rfl

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

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✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
⊢ Mono (K.shortComplexTruncLE e).f

Tactic:
dsimp [shortComplexTruncLE]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
⊢ Mono (K.ιTruncLE e)
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

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✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
⊢ Epi (K.shortComplexTruncLE e).g

Tactic:
dsimp [shortComplexTruncLE]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
⊢ Epi (cokernel.π (K.ιTruncLE e))
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

Goal state before:
pp: case pos.hf
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ homologyMap (K.ιTruncLE e) (e.f i) ≫
      { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
          X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
          g := ⋯.δ (e.f i) j' hj', zero := ⋯ }.f =
    0

Tactic:
dsimp [shortComplexTruncLE]

Goal state after:
case pos.hf
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ homologyMap (K.ιTruncLE e) (e.f i) ≫ homologyMap (cokernel.π (K.ιTruncLE e)) (e.f i) = 0
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
⊢ K.IsGE n

Tactic:
refine IsSupported.mk (fun i hi ↦ ?_)

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i
⊢ ExactAt K i
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
⊢ K.IsLE n

Tactic:
refine IsSupported.mk (fun i hi ↦ ?_)

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i
⊢ ExactAt K i
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyGE q
i : ℤ
hi : autoParam (i < p) isStrictlyGE_iff._auto_1
⊢ IsZero (K.X i)

Tactic:
exact K.isZero_of_isStrictlyGE q _

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : CochainComplex C ℤ
f : Q.obj X ⟶ Q.obj Y
X' : HomologicalComplex C (ComplexShape.up ℤ)
s : X' ⟶ X
hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s)
g : X' ⟶ Y
hφ :
  f =
    { X' := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X',
          s := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s, hs := hs,
          f := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map g }.map
      Qh ⋯
⊢ ∃ X' s, ∃ (x : IsIso (Q.map s)), ∃ g, f = inv (Q.map s) ≫ Q.map g

Tactic:
rw [← isIso_Qh_map_iff] at hs

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : CochainComplex C ℤ
f : Q.obj X ⟶ Q.obj Y
X' : HomologicalComplex C (ComplexShape.up ℤ)
s : X' ⟶ X
hs✝ : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s)
hs : IsIso (Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s))
g : X' ⟶ Y
hφ :
  f =
    { X' := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X',
          s := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s, hs := hs✝,
          f := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map g }.map
      Qh ⋯
⊢ ∃ X' s, ∃ (x : IsIso (Q.map s)), ∃ g, f = inv (Q.map s) ≫ Q.map g
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : CochainComplex C ℤ
f : Q.obj X ⟶ Q.obj Y
X' : HomologicalComplex C (ComplexShape.up ℤ)
s : Y ⟶ X'
hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s)
g : X ⟶ X'
hφ :
  f =
    { Y' := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X',
          f := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map g,
          s := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s, hs := hs }.map
      Qh ⋯
⊢ ∃ Y' g s, ∃ (x : IsIso (Q.map s)), f = Q.map g ≫ inv (Q.map s)

Tactic:
rw [← isIso_Qh_map_iff] at hs

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : CochainComplex C ℤ
f : Q.obj X ⟶ Q.obj Y
X' : HomologicalComplex C (ComplexShape.up ℤ)
s : Y ⟶ X'
hs✝ : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s)
hs : IsIso (Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s))
g : X ⟶ X'
hφ :
  f =
    { Y' := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X',
          f := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map g,
          s := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s, hs := hs✝ }.map
      Qh ⋯
⊢ ∃ Y' g s, ∃ (x : IsIso (Q.map s)), f = Q.map g ≫ inv (Q.map s)
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C₁ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁶ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
D₁ : Type u₃
inst✝⁵ : Category.{v₃, u₃} D₁
D₂ : Type u₄
inst✝⁴ : Category.{v₄, u₄} D₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝² : L₂.IsLocalization W₂
X✝ Y : C₁
inst✝¹ : HasSmallLocalizedHom W₁ X✝ Y
inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X✝) (Φ.functor.obj Y)
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
g : W₁.Q.obj X✝ ⟶ W₁.Q.obj Y
G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
β : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso Φ.functor W₁.Q W₂.Q G'
E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor
α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor
α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
γ : G' ⋙ E₂ ≅ E₁ ⋙ G :=
  liftNatIso W₁.Q W₁ (W₁.Q ⋙ G' ⋙ E₂) (W₁.Q ⋙ E₁ ⋙ G) (G' ⋙ E₂) (E₁ ⋙ G)
    ((W₁.Q.associator G' E₂).symm ≪≫
      Functor.isoWhiskerRight β.symm E₂ ≪≫
        Φ.functor.associator W₂.Q E₂ ≪≫
          Φ.functor.isoWhiskerLeft α₂ ≪≫ e ≪≫ Functor.isoWhiskerRight α₁.symm G ≪≫ W₁.Q.associator E₁ G)
X : C₁
⊢ γ.hom.app (W₁.Q.obj X) = E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor.obj X) ≫ e.hom.app X ≫ G.map (α₁.inv.app X)

Tactic:
simp [γ, id_comp, comp_id]

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

Goal state before:
pp: C₁ : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁹ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁸ : HasSmallLocalizedHom W₁ X Y
inst✝⁷ : HasSmallLocalizedHom W₁ Y Z
inst✝⁶ : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst✝⁵ : HasSmallLocalizedHom W₂ X' X'
inst✝⁴ : HasSmallLocalizedHom W₂ Y' Y'
inst✝³ : HasSmallLocalizedHom W₂ Z' Z'
inst✝² : HasSmallLocalizedHom W₂ X' Y'
inst✝¹ : HasSmallLocalizedHom W₂ Y' Z'
inst✝ : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor.obj X ≅ X'
eY : Φ.functor.obj Y ≅ Y'
eZ : Φ.functor.obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
this✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Y'
this✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) Z'
this : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)
⊢ Φ.smallHomMap' eX eZ (f.comp g) = (Φ.smallHomMap' eX eY f).comp (Φ.smallHomMap' eY eZ g)

Tactic:
have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm (Iso.refl Z')

Goal state after:
C₁ : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁹ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁸ : HasSmallLocalizedHom W₁ X Y
inst✝⁷ : HasSmallLocalizedHom W₁ Y Z
inst✝⁶ : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst✝⁵ : HasSmallLocalizedHom W₂ X' X'
inst✝⁴ : HasSmallLocalizedHom W₂ Y' Y'
inst✝³ : HasSmallLocalizedHom W₂ Z' Z'
inst✝² : HasSmallLocalizedHom W₂ X' Y'
inst✝¹ : HasSmallLocalizedHom W₂ Y' Z'
inst✝ : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor.obj X ≅ X'
eY : Φ.functor.obj Y ≅ Y'
eZ : Φ.functor.obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this✝³ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
this✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Y'
this✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) Z'
this✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)
this : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Z'
⊢ Φ.smallHomMap' eX eZ (f.comp g) = (Φ.smallHomMap' eX eY f).comp (Φ.smallHomMap' eY eZ g)
Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom

Goal state before:
pp: C₁ : Type u₁
inst✝¹⁹ : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst✝¹⁸ : Category.{v₂, u₂} C₂
D₁ : Type u₁'
inst✝¹⁷ : Category.{v₁', u₁'} D₁
D₂ : Type u₂'
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₂
M : Type w'
inst✝¹³ : AddMonoid M
inst✝¹² : HasShift C₁ M
inst✝¹¹ : HasShift C₂ M
inst✝¹⁰ : HasShift D₁ M
inst✝⁹ : HasShift D₂ M
inst✝⁸ : L₁.CommShift M
inst✝⁷ : L₂.CommShift M
inst✝⁶ : Φ.functor.CommShift M
X₁ Y₁ : C₁
X₂ Y₂ : C₂
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst✝² : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor.obj X₁ ≅ X₂
eY : Φ.functor.obj Y₁ ≅ Y₂
G : D₁ ⥤ D₂
inst✝¹ : G.CommShift M
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
inst✝ : NatTrans.CommShift e.hom M
m : M
f : SmallShiftedHom W₁ X₁ Y₁ m
⊢ (SmallShiftedHom.equiv W₂ L₂) (Φ.smallShiftedHomMap eX eY f) =
    (ShiftedHom.mk₀ 0 ⋯ (L₂.map eX.inv ≫ e.hom.app X₁)).comp
      ((((SmallShiftedHom.equiv W₁ L₁) f).map G).comp (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Y₁ ≫ L₂.map eY.hom)) ⋯) ⋯

Tactic:
by
  have := hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀.{w''} W₂ M X₂ X₂
  apply ((L₂.commShiftIso m).app Y₂).homToEquiv.symm.injective
  simp only [Functor.comp_obj, SmallShiftedHom.equiv_apply, Iso.app_hom,
    Iso.homToEquiv_symm_apply, Iso.app_inv, assoc, Iso.hom_inv_id_app, comp_id]
  refine (Φ.equiv_smallHomMap' L₁ L₂ _ _ G e f).trans ?_
  simp only [Functor.comp_obj, NatTrans.app_shift,
    Functor.commShiftIso_comp_hom_app, Functor.commShiftIso_comp_inv_app, assoc,
    Iso.trans_hom, Iso.app_hom, Functor.mapIso_hom, Functor.map_comp, ShiftedHom.map,
    ShiftedHom.comp_mk₀, ShiftedHom.mk₀_comp,
    Functor.commShiftIso_inv_naturality]
  nth_rw 2 [← Functor.map_comp_assoc]
  simp

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mpr.inr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
⊢ ∀
    (a_1 b_1 :
      (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
        (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))),
    a_1 = b_1

Tactic:
intro x y

Goal state after:
case mpr.inr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
x y :
  (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
    (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))
⊢ x = y
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_1.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ {
      X₁ :=
        (mk₂ ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨0, ⋯⟩,
      X₂ :=
        (mk₂ ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨1, ⋯⟩,
      X₃ :=
        (mk₂ ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨2, ⋯⟩,
      f :=
        (mk₂ ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
          0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
      g :=
        (mk₂ ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
          1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
      zero := ⋯ }.Exact

Tactic:
rw [ShortComplex.exact_iff_mono _ (by simp)]
      infer_instance

Goal state after: