mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Predicate

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
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{v_3, u_3} E
hW : W ≤ MorphismProperty.isomorphisms C
F : C ⥤ E
hF : W.IsInvertedBy F
⊢ 𝟭 C ⋙ F = F

Tactic:
cases F
    rfl

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

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
X : C
⊢ app τ (W.Q.obj X) = τ.app X

Tactic:
by
  simp only [app, eqToHom_refl, comp_id, id_comp]
  rfl

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

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
this : MorphismProperty.naturalityProperty (NatTransExtension.app τ) = ⊤
X : W.Localization
⊢ ∀ ⦃Y : W.Localization⦄ (f : X ⟶ Y), F₁.map f ≫ NatTransExtension.app τ Y = NatTransExtension.app τ X ≫ F₂.map f

Tactic:
Y

Goal state after:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
this : MorphismProperty.naturalityProperty (NatTransExtension.app τ) = ⊤
X Y : W.Localization
⊢ ∀ (f : X ⟶ Y), F₁.map f ≫ NatTransExtension.app τ Y = NatTransExtension.app τ X ≫ F₂.map f
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), MorphismProperty.naturalityProperty (NatTransExtension.app τ) (W.Q.map f)

Tactic:
Y

Goal state after:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
X Y : C
⊢ ∀ (f : X ⟶ Y), MorphismProperty.naturalityProperty (NatTransExtension.app τ) (W.Q.map f)
Module: Mathlib.CategoryTheory.Localization.Predicate

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
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
F₁ F₂ F₃ : C ⥤ E
F₁' F₂' F₃' : D ⥤ E
h₁ : Lifting L W F₁ F₁'
h₂ : Lifting L W F₂ F₂'
h₃ : Lifting L W F₃ F₃'
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
X : C
⊢ (liftNatTrans L W F₁ F₂ F₁' F₂' τ ≫ liftNatTrans L W F₂ F₃ F₂' F₃' τ').app (L.obj X) =
    (liftNatTrans L W F₁ F₃ F₁' F₃' (τ ≫ τ')).app (L.obj X)

Tactic:
simp only [NatTrans.comp_app, liftNatTrans_app, assoc, Iso.inv_hom_id_app_assoc]

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁹ : Category.{v₁, u₁} C₁
inst✝⁸ : Category.{v₂, u₂} C₂
inst✝⁷ : Category.{v₃, u₃} C₃
inst✝⁶ : Category.{v₄, u₄} D₁
inst✝⁵ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝⁴ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝³ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝² : Φ.functor.IsEquivalence
inst✝¹ : Φ.IsInduced
inst✝ : W₂.RespectsIso
X : C₂
⊢ ∀ ⦃Y : C₂⦄ (f : X ⟶ Y), W₂ f → (W₂.inverseImage Φ.functor).inverseImage Φ.functor.inv f

Tactic:
Y

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁹ : Category.{v₁, u₁} C₁
inst✝⁸ : Category.{v₂, u₂} C₂
inst✝⁷ : Category.{v₃, u₃} C₃
inst✝⁶ : Category.{v₄, u₄} D₁
inst✝⁵ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝⁴ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝³ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝² : Φ.functor.IsEquivalence
inst✝¹ : Φ.IsInduced
inst✝ : W₂.RespectsIso
X Y : C₂
⊢ ∀ (f : X ⟶ Y), W₂ f → (W₂.inverseImage Φ.functor).inverseImage Φ.functor.inv f
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
φ : W.RightFraction₂ X Y
inst✝ : W.HasLeftCalculusOfFractions
ψ₁ : W.LeftFraction X Y
hψ₁ : φ.f ≫ ψ₁.s = φ.s ≫ ψ₁.f
ψ₂ : W.LeftFraction X Y
hψ₂ : φ.f' ≫ ψ₂.s = φ.s ≫ ψ₂.f
α : W.LeftFraction ψ₁.Y' ψ₂.Y'
hα : ψ₂.s ≫ α.s = ψ₁.s ≫ α.f
⊢ φ.f ≫ { Y' := α.Y', f := ψ₁.f ≫ α.f, f' := ψ₂.f ≫ α.s, s := ψ₂.s ≫ α.s, hs := ⋯ }.s =
    φ.s ≫ { Y' := α.Y', f := ψ₁.f ≫ α.f, f' := ψ₂.f ≫ α.s, s := ψ₂.s ≫ α.s, hs := ⋯ }.f

Tactic:
dsimp
    rw [hα, reassoc_of% hψ₁]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a b : A
X : C
⊢ (commShiftOfLocalization.iso L W F F' (a + b)).hom.app (L.obj X) =
    (CommShift.isoAdd (commShiftOfLocalization.iso L W F F' a) (commShiftOfLocalization.iso L W F F' b)).hom.app
      (L.obj X)

Tactic:
simp only [commShiftOfLocalization.iso_hom_app, comp_obj, commShiftIso_add,
      CommShift.isoAdd_inv_app, map_comp, CommShift.isoAdd_hom_app, Category.assoc]

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a b : A
X : C
⊢ F'.map ((shiftFunctorAdd D a b).hom.app (L.obj X)) ≫
      F'.map ((shiftFunctor D b).map ((commShiftIso L a).inv.app X)) ≫
        F'.map ((commShiftIso L b).inv.app ((shiftFunctor C a).obj X)) ≫
          F'.map (L.map ((shiftFunctorAdd C a b).inv.app X)) ≫
            (Lifting.iso L W F F').hom.app ((shiftFunctor C (a + b)).obj X) ≫
              F.map ((shiftFunctorAdd C a b).hom.app X) ≫
                (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
                  (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
                    (shiftFunctorAdd E a b).inv.app (F.obj X) ≫
                      (shiftFunctor E (a + b)).map ((Lifting.iso L W F F').inv.app X) =
    F'.map ((shiftFunctorAdd D a b).hom.app (L.obj X)) ≫
      (commShiftOfLocalization.iso L W F F' b).hom.app ((shiftFunctor D a).obj (L.obj X)) ≫
        (shiftFunctor E b).map (F'.map ((commShiftIso L a).inv.app X)) ≫
          (shiftFunctor E b).map ((Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X)) ≫
            (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
              (shiftFunctor E b).map ((shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)) ≫
                (shiftFunctorAdd E a b).inv.app (F'.obj (L.obj X))
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : { X' := Y, s := a₁.s, hs := ⋯, f := b.f }.f ≫ z₁.s = { X' := Y, s := a₁.s, hs := ⋯, f := b.f }.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : { X' := Y, s := a₂.s, hs := ⋯, f := b.f }.f ≫ z₂.s = { X' := Y, s := a₂.s, hs := ⋯, f := b.f }.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
fac₁' :
  { X' := Y, s := a₁.s ≫ t₁, hs := ht, f := b.f ≫ z₁.s }.f ≫ w₁.s =
    { X' := Y, s := a₁.s ≫ t₁, hs := ht, f := b.f ≫ z₁.s }.s ≫ w₁.f
⊢ W (a₂.s ≫ t₂)

Tactic:
rw [← hst]

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
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : { X' := Y, s := a₁.s, hs := ⋯, f := b.f }.f ≫ z₁.s = { X' := Y, s := a₁.s, hs := ⋯, f := b.f }.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : { X' := Y, s := a₂.s, hs := ⋯, f := b.f }.f ≫ z₂.s = { X' := Y, s := a₂.s, hs := ⋯, f := b.f }.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
fac₁' :
  { X' := Y, s := a₁.s ≫ t₁, hs := ht, f := b.f ≫ z₁.s }.f ≫ w₁.s =
    { X' := Y, s := a₁.s ≫ t₁, hs := ht, f := b.f ≫ z₁.s }.s ≫ w₁.f
⊢ W (a₁.s ≫ t₁)
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: case succ.inr
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k' : J
hk' : ¬IsMax k'
hkk' : Order.succ k' ≤ k' → (fun j ↦ transfiniteIterate φ j i₀) (Order.succ k') ≤ (fun j ↦ transfiniteIterate φ j i₀) k'
hkj : Order.succ k' ≤ Order.succ k'
⊢ (fun j ↦ transfiniteIterate φ j i₀) (Order.succ k') ≤ (fun j ↦ transfiniteIterate φ j i₀) (Order.succ k')

Tactic:
· rfl

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: case mpr
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
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
X : C
⊢ ∀ ⦃Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g

Tactic:
Y

Goal state after:
case mpr
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
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
X Y : C
⊢ ∀ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: case isSuccLimit.inr
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k : J
hk' : Order.IsSuccLimit k
a✝ : ∀ b < k, k ≤ b → (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) b
hkj : k ≤ k
⊢ (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) k

Tactic:
· rfl

Goal state after:
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
c : M
h : 0 + 0 = c
⊢ c = 0

Tactic:
rw [← h, zero_add]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P f → P.retracts f

Tactic:
Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
⊢ ∀ (f : X ⟶ Y), P f → P.retracts f
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P.retracts f → P f

Tactic:
Y

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f
X Y : C
⊢ ∀ (f : X ⟶ Y), P.retracts f → P f
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
X Y : C
a : M
f : ShiftedHom X Y a
F G : C ⥤ D
e : F ≅ G
inst✝² : F.CommShift M
inst✝¹ : G.CommShift M
inst✝ : NatTrans.CommShift e.hom M
⊢ (mk₀ 0 ⋯ (e.inv.app X)).comp ((f.map F).comp (mk₀ 0 ⋯ (e.hom.app Y)) ⋯) ⋯ = f.map G

Tactic:
simp [map_naturality]

Goal state after:
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
P Q : ObjectProperty C
X A B : C
f₁ : A ⟶ X
f₂ : X ⟶ B
f₃ : B ⟶ (shiftFunctor C 1).obj A
hT : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
A' : C
hP : P A'
a₁ : A ⟶ A'
b₁ : A' ⟶ A
h₁ : a₁ ≫ b₁ = 𝟙 A
B' : C
hQ : Q B'
a₃ : B ⟶ B'
b₃ : B' ⟶ B
h₃ : a₃ ≫ b₃ = 𝟙 B
X' : C
g₁ : A' ⟶ X'
g₂ : X' ⟶ B'
hT' : Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁) ∈ distinguishedTriangles
a₂ : X ⟶ X'
ha₁₂ : (Triangle.mk f₁ f₂ f₃).mor₁ ≫ a₂ = a₁ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₁
ha₂₃ : (Triangle.mk f₁ f₂ f₃).mor₂ ≫ a₃ = a₂ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₂
b₂ : X' ⟶ X
hb₁₂ : (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₁ ≫ b₂ = b₁ ≫ (Triangle.mk f₁ f₂ f₃).mor₁
hb₂₃ : (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₂ ≫ b₃ = b₂ ≫ (Triangle.mk f₁ f₂ f₃).mor₂
⊢ (P.extensionProduct Q).retractClosure X

Tactic:
dsimp at ha₁₂ ha₂₃ hb₁₂ hb₂₃

Goal state after:
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
P Q : ObjectProperty C
X A B : C
f₁ : A ⟶ X
f₂ : X ⟶ B
f₃ : B ⟶ (shiftFunctor C 1).obj A
hT : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
A' : C
hP : P A'
a₁ : A ⟶ A'
b₁ : A' ⟶ A
h₁ : a₁ ≫ b₁ = 𝟙 A
B' : C
hQ : Q B'
a₃ : B ⟶ B'
b₃ : B' ⟶ B
h₃ : a₃ ≫ b₃ = 𝟙 B
X' : C
g₁ : A' ⟶ X'
g₂ : X' ⟶ B'
hT' : Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁) ∈ distinguishedTriangles
a₂ : X ⟶ X'
ha₁₂ : f₁ ≫ a₂ = a₁ ≫ g₁
ha₂₃ : f₂ ≫ a₃ = a₂ ≫ g₂
b₂ : X' ⟶ X
hb₁₂ : g₁ ≫ b₂ = b₁ ≫ f₁
hb₂₃ : g₂ ≫ b₃ = b₂ ≫ f₂
⊢ (P.extensionProduct Q).retractClosure X
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
a : ℤ
K : CochainComplex C ℤ
⊢ (shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K =
    (shortComplexFunctor C (up ℤ) a).map ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)

Tactic:
ext <;> simp [one_smul, shiftFunctorZero_hom_app_f]

Goal state after:
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
P Q : ObjectProperty C
h : P ≤ Q
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P.trW f → Q.trW f

Tactic:
Y

Goal state after:
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
P Q : ObjectProperty C
h : P ≤ Q
X Y : C
⊢ ∀ (f : X ⟶ Y), P.trW f → Q.trW f
Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : i = a
⊢ ((single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj X).X i =
    ((single C (ComplexShape.up ℤ) a).obj X).X i

Tactic:
subst h

Goal state after:
case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n : ℤ
X : C
i : ℤ
ha' : n + i = i + n
⊢ ((single C (ComplexShape.up ℤ) (i + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj X).X i =
    ((single C (ComplexShape.up ℤ) i).obj X).X i
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 P' : ObjectProperty C
inst✝² : P.IsTriangulatedClosed₂
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P'.IsTriangulatedClosed₂
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : (P ⊓ P') T.obj₁
h₃ : (P ⊓ P') T.obj₃
X₂ : C
h₂ : P' X₂
e : T.obj₂ ≅ X₂
⊢ (P ⊓ P').isoClosure T.obj₂

Tactic:
exact ⟨X₂, ⟨P.prop_of_iso e (P.ext_of_isTriangulatedClosed₂ T hT h₁.1 h₃.1), h₂⟩, ⟨e⟩⟩

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
n m : ℤ
α : Cochain K M m
β : Cochain L M n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
p q : ℤ
hpq : p + n = q
⊢ (δ m n ((-m + 1).negOnePow • (mappingCone.descCochain φ α β h).leftShift (-1) m ⋯)).v p q hpq =
    ((Cochain.ofHom (-((mappingCone.fst φ).leftShift (-1) 0 fst._proof_1).homOf)).comp
            (δ m n α + m.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯ +
          ((mappingCone.snd φ).leftShift (-1) (-1) snd._proof_1).comp (δ n n' β) ⋯).v
      p q hpq

Tactic:
subst h

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
m : ℤ
α : Cochain K M m
n' p q : ℤ
β : Cochain L M (m + 1)
hn' : m + 1 + 1 = n'
hpq : p + (m + 1) = q
⊢ (δ m (m + 1) ((-m + 1).negOnePow • (mappingCone.descCochain φ α β ⋯).leftShift (-1) m ⋯)).v p q hpq =
    ((Cochain.ofHom (-((mappingCone.fst φ).leftShift (-1) 0 fst._proof_1).homOf)).comp
            (δ m (m + 1) α + m.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯ +
          ((mappingCone.snd φ).leftShift (-1) (-1) snd._proof_1).comp (δ (m + 1) n' β) ⋯).v
      p q hpq
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst✝² : AddCommSemigroup A
inst✝¹ : IsRightCancelAdd A
inst✝ : One A
a b : A
⊢ (embeddingDown'Add a b).IsRelIff

Tactic:
dsimp [embeddingDown'Add]; infer_instance

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ g.op ≫ f.op = 0

Tactic:
by rw [← op_comp, w, op_zero]

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

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : (HomologicalComplex V c)ᵒᵖ
⊢ ∀ {Y : (HomologicalComplex V c)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (HomologicalComplex V c)ᵒᵖ).map f ≫
        (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop Y).op.unopSymm.X x)) ⋯).op.hom =
      (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯).op.hom ≫
        (opFunctor V c ⋙ opInverse V c).map f

Tactic:
Y

Goal state after:
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X Y : (HomologicalComplex V c)ᵒᵖ
⊢ ∀ (f : X ⟶ Y),
    (𝟭 (HomologicalComplex V c)ᵒᵖ).map f ≫
        (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop Y).op.unopSymm.X x)) ⋯).op.hom =
      (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯).op.hom ≫
        (opFunctor V c ⋙ opInverse V c).map f
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
⊢ ∀ {Y : (HomologicalComplex Vᵒᵖ c)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (HomologicalComplex Vᵒᵖ c)ᵒᵖ).map f ≫
        (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop Y).op.unopSymm.X x)) ⋯).op.hom =
      (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯).op.hom ≫
        (unopFunctor V c ⋙ unopInverse V c).map f

Tactic:
Y

Goal state after:
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X Y : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
⊢ ∀ (f : X ⟶ Y),
    (𝟭 (HomologicalComplex Vᵒᵖ c)ᵒᵖ).map f ≫
        (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop Y).op.unopSymm.X x)) ⋯).op.hom =
      (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯).op.hom ≫
        (unopFunctor V c ⋙ unopInverse V c).map f
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ (mappingConeCompTriangleh f g).mor₂ ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (mappingConeCompTriangle f g).mor₁)

Tactic:
by
  rw [← cancel_mono (HomotopyCategory.isoOfHomotopyEquiv
      (mappingConeCompHomotopyEquiv f g)).inv, assoc]
  dsimp [mappingConeCompTriangleh]
  rw [← Functor.map_comp, ← Functor.map_comp, ← Functor.map_comp,
    mappingConeCompHomotopyEquiv_hom_inv_id, comp_id,
    mappingConeCompHomotopyEquiv_comm₁ f g,
    mappingConeCompTriangle_mor₂]

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

Goal state before:
pp: case inl
ι : 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✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
hi' : e.r i' = none
⊢ extend.d K (e.r i') (e.r j') = 0

pp: case inr
ι : 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✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
⊢ extend.d K (e.r i') (e.r j') = 0

Tactic:
· rw [extend.d_none_eq_zero K _ _ hi']

Goal state after:
case inr
ι : 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✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
⊢ extend.d K (e.r i') (e.r j') = 0
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryLE j
inst✝ : e.IsTruncGE
⊢ False

Tactic:
obtain ⟨k, hk⟩ := e.mem_next hj.1
  exact hj.2 k (by simpa only [hk] using hj.1)

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

Goal state before:
pp: case mp.zero
p : ℤ
h : (embeddingUpIntGE p).BoundaryGE 0
⊢ 0 = 0

pp: case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
⊢ n + 1 = 0

Tactic:
· rfl

Goal state after:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
⊢ n + 1 = 0
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mp.zero
p : ℤ
h : (embeddingUpIntLE p).BoundaryLE 0
⊢ 0 = 0

pp: case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntLE p).BoundaryLE (n + 1)
⊢ n + 1 = 0

Tactic:
· rfl

Goal state after:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntLE p).BoundaryLE (n + 1)
⊢ n + 1 = 0