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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
⊢ (γ.rightShift a n' hn').leftShift a n hn' = (a * n + a * (a - 1) / 2).negOnePow • γ.shift a

Tactic:
by
  ext p q hpq
  simp only [leftShift_v _ a n hn' p q hpq (p + a) (by lia),
    rightShift_v _ a n' hn' (p + a) q (by lia) (q + a) (by lia), units_smul_v, shift_v']
  dsimp
  rw [id_comp, comp_id]

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

Goal state before:
pp: case refine_1
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✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).mor₁ ≫
      (Iso.refl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).obj₂).hom =
    (Iso.refl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).obj₁).hom ≫
      (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₁

Tactic:
dsimp
    simp only [comp_id, id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝ : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
ha'' : ∀ (j : J), ∃ g, (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun j ↦ (T j).obj₃) j = g ≫ (T j).mor₂
b : (j : J) → A ⟶ (T j).obj₂ := fun j ↦ ⋯.choose
hb : ∀ (j : J), (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun j ↦ (T j).obj₃) j = b j ≫ (T j).mor₂
j : J
⊢ (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun j ↦ (T j).obj₃) j =
    (Pi.lift b ≫ (productTriangle T).mor₂) ≫ Pi.π (fun j ↦ (T j).obj₃) j

Tactic:
rw [hb]

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝ : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
ha'' : ∀ (j : J), ∃ g, (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun j ↦ (T j).obj₃) j = g ≫ (T j).mor₂
b : (j : J) → A ⟶ (T j).obj₂ := fun j ↦ ⋯.choose
hb : ∀ (j : J), (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun j ↦ (T j).obj₃) j = b j ≫ (T j).mor₂
j : J
⊢ b j ≫ (T j).mor₂ = (Pi.lift b ≫ (productTriangle T).mor₂) ≫ Pi.π (fun j ↦ (T j).obj₃) j
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ }.Exact

Tactic:
by_cases h : c.Rel i (c.next i)

Goal state after:
case pos
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : c.Rel i (c.next i)
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ }.Exact

case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ }.Exact
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : V
f : X ⟶ Y
X' Y' : V
hX : X = X'
hY : Y = Y'
X'' Y'' : W
hX' : e X' = X''
hY' : e Y' = Y''
⊢ Quiver.homOfEq ((he X' Y') (Quiver.homOfEq f hX hY)) hX' hY' = Quiver.homOfEq ((he X Y) f) ⋯ ⋯

Tactic:
subst hX hY hX' hY'
  rfl

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ (S.X₁.liftCycles x₁ k hk ⋯ ≫ HomologicalComplex.cyclesMap S.f j) ≫ S.X₂.iCycles j =
    ((x₂ ≫ S.X₂.pOpcycles i) ≫ S.X₂.opcyclesToCycles i j) ≫ S.X₂.iCycles j

Tactic:
HomologicalComplex.liftCycles_comp_cyclesMap,

Goal state after:
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ S.X₂.liftCycles (x₁ ≫ S.f.f j) k hk ⋯ ≫ S.X₂.iCycles j =
    ((x₂ ≫ S.X₂.pOpcycles i) ≫ S.X₂.opcyclesToCycles i j) ≫ S.X₂.iCycles j
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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ G₁ = G₂

Tactic:
refine Functor.ext ?_ ?_
    · rintro ⟨⟨X⟩⟩
      apply Functor.congr_obj h
    · rintro ⟨⟨X⟩⟩ ⟨⟨Y⟩⟩ ⟨f⟩
      apply Functor.congr_hom h'

Goal state after:
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 : D ⥤ E
⊢ (W.Q ⋙ Construction.lift L ⋯) ⋙ F = L ⋙ F

Tactic:
rw [Construction.fac]

Goal state after:
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
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
⊢ AreEqualizedByLocalization W f g ↔ L.map f = L.map g

Tactic:
by
  dsimp [AreEqualizedByLocalization]
  constructor
  · intro h
    let e := Localization.compUniqFunctor W.Q L W
    rw [← NatIso.naturality_1 e f, ← NatIso.naturality_1 e g]
    dsimp
    rw [h]
  · intro h
    let e := Localization.compUniqFunctor L W.Q W
    rw [← NatIso.naturality_1 e f, ← NatIso.naturality_1 e g]
    dsimp
    rw [h]

Goal state after:
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
W : MorphismProperty C
X Y : C
f g : X ⟶ Y
h : AreEqualizedByLocalization W f g
F : C ⥤ D
hF : W.IsInvertedBy F
⊢ F.map f = F.map g

Tactic:
by
  simp [← NatIso.naturality_1 (Localization.fac F hF W.Q), h.map_eq W.Q]

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

Goal state before:
pp: 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₄} D₁
inst✝⁴ : Category.{v₅, u₅} D₂
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✝¹ : CatCommSq Φ.functor L₁ L₂ G
inst✝ : G.IsEquivalence
⊢ G.IsEquivalence

Tactic:
exact inferInstance

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝² : Φ.functor.IsEquivalence
inst✝¹ : Φ.IsInduced
inst✝ : W₂.RespectsIso
⊢ Φ.IsLocalizedEquivalence

Tactic:
refine IsLocalizedEquivalence.of_equivalence _ (fun X Y f hf ↦ ?_)
  let e :
      Arrow.mk (Φ.functor.map (Φ.functor.preimage
        ((Φ.functor.objObjPreimageIso X).hom ≫ f ≫ (Φ.functor.objObjPreimageIso Y).inv))) ≅
      Arrow.mk f :=
    Arrow.isoMk (Φ.functor.objObjPreimageIso X) (Φ.functor.objObjPreimageIso Y)
  simp only [← Φ.inverseImage_eq]
  exact ⟨_, _, _, (W₂.arrow_mk_iso_iff e).2 hf, ⟨e⟩⟩

Goal state after:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : ¬IsMax j
⊢ SuccOrder.limitRecOn (Order.succ j) (motive := fun x ↦ I → I) (fun x x_1 ↦ id) (fun x x_1 g ↦ φ ∘ g)
      (fun y x h ↦ ⨆ x, h ↑x ⋯) i₀ =
    φ
      (SuccOrder.limitRecOn j (motive := fun x ↦ I → I) (fun x x_1 ↦ id) (fun x x_1 g ↦ φ ∘ g) (fun y x h ↦ ⨆ x, h ↑x ⋯)
        i₀)

Tactic:
SuccOrder.limitRecOn_succ_of_not_isMax _ _ _ hj

Goal state after:
I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : ¬IsMax j
⊢ (φ ∘ SuccOrder.limitRecOn j (motive := fun x ↦ I → I) (fun x x_1 ↦ id) (fun x x_1 g ↦ φ ∘ g) fun y x h ↦ ⨆ x, h ↑x ⋯)
      i₀ =
    φ
      (SuccOrder.limitRecOn j (motive := fun x ↦ I → I) (fun x x_1 ↦ id) (fun x x_1 g ↦ φ ∘ g) (fun y x h ↦ ⨆ x, h ↑x ⋯)
        i₀)
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
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X : C
⊢ (ofHom W (𝟙 X)).map F hF = 𝟙 (F.obj X)

Tactic:
map_ofHom,

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
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X : C
⊢ F.map (𝟙 X) = 𝟙 (F.obj X)
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
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
a b c : M
h : b + a = c
ha : a = 0
hb : b = 0
⊢ b + 0 = 0

Tactic:
hb,

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
a b c : M
h : b + a = c
ha : a = 0
hb : b = 0
⊢ 0 + 0 = 0
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case succ
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 : ObjectProperty C
inst✝ : IsTriangulated C
n : ℕ
h : P.extensionProductIter (n + 1) = (P.extensionProductIter n).extensionProduct P
⊢ (P.extensionProduct (P.extensionProductIter n)).extensionProduct P =
    ((P.extensionProductIter n).extensionProduct P).extensionProduct P

Tactic:
← extensionProductIter_succ,

Goal state after:
case succ
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 : ObjectProperty C
inst✝ : IsTriangulated C
n : ℕ
h : P.extensionProductIter (n + 1) = (P.extensionProductIter n).extensionProduct P
⊢ (P.extensionProductIter (n + 1)).extensionProduct P =
    ((P.extensionProductIter n).extensionProduct P).extensionProduct P
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : HomologicalComplex.quasiIso C c f
⊢ IsIso (Q.map f)

Tactic:
exact Localization.inverts Q (HomologicalComplex.quasiIso C c) _ h

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : CochainComplex C ℤ
φ : K ⟶ L
n i j : ℤ
h : n + i = j
⊢ QuasiIsoAt ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).map φ) i ↔ QuasiIsoAt φ j

Tactic:
simp only [quasiIsoAt_iff_isIso_homologyMap]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : CochainComplex C ℤ
φ : K ⟶ L
n i j : ℤ
h : n + i = j
⊢ IsIso (homologyMap ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).map φ) i) ↔ IsIso (homologyMap φ j)
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✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
⊢ ∀ (T₁ T₂ : Triangle C),
    T₁ ∈ distinguishedTriangles →
      T₂ ∈ distinguishedTriangles →
        ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂),
          P.trW a →
            P.trW b →
              T₁.mor₁ ≫ b = a ≫ T₂.mor₁ →
                ∃ c, ∃ (_ : P.trW c), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃

Tactic:
rintro T₁ T₃ mem₁ mem₃ a b ⟨Z₅, g₅, h₅, mem₅, mem₅'⟩ ⟨Z₄, g₄, h₄, mem₄, mem₄'⟩ comm
  obtain ⟨Z₂, g₂, h₂, mem₂⟩ := distinguished_cocone_triangle (T₁.mor₁ ≫ b)
  have H := someOctahedron rfl mem₁ mem₄ mem₂
  have H' := someOctahedron comm.symm mem₅ mem₃ mem₂
  let φ : T₁ ⟶ T₃ := H.triangleMorphism₁ ≫ H'.triangleMorphism₂
  exact ⟨φ.hom₃, P.trW.comp_mem _ _ (trW.mk P H.mem mem₄') (trW.mk' P H'.mem mem₅'),
    by simpa [φ] using φ.comm₂, by simpa [φ] using φ.comm₃⟩

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

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

Tactic:
by_cases hj : ∃ j, e.f j = j'

Goal state after:
case pos
ι : 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' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ∃ j, e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

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✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ¬∃ j, e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
j' k' : ι'
⊢ (((single C c i).obj X).extend e).d j' k' = 0

Tactic:
by_cases hj : ∃ j, e.f j = j'

Goal state after:
case pos
ι : 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
inst✝ : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
j' k' : ι'
hj : ∃ j, e.f j = j'
⊢ (((single C c i).obj X).extend e).d j' k' = 0

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✝¹ : HasZeroMorphisms C
inst✝ : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
j' k' : ι'
hj : ¬∃ j, e.f j = j'
⊢ (((single C c i).obj X).extend e).d j' k' = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
⊢ (mkHomToSingle ((((single C c i).obj X).extendXIso e h).hom ≫ (singleObjXSelf c i X).hom) ⋯ ≫
          mkHomFromSingle ((singleObjXSelf c i X).inv ≫ (((single C c i).obj X).extendXIso e h).inv) ⋯).f
      j' =
    (𝟙 (((single C c i).obj X).extend e)).f j'

Tactic:
by_cases hj : ∃ j, e.f j = j'

Goal state after:
case pos
ι : 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
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
hj : ∃ j, e.f j = j'
⊢ (mkHomToSingle ((((single C c i).obj X).extendXIso e h).hom ≫ (singleObjXSelf c i X).hom) ⋯ ≫
          mkHomFromSingle ((singleObjXSelf c i X).inv ≫ (((single C c i).obj X).extendXIso e h).inv) ⋯).f
      j' =
    (𝟙 (((single C c i).obj X).extend e)).f j'

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✝² : HasZeroMorphisms C
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
hj : ¬∃ j, e.f j = j'
⊢ (mkHomToSingle ((((single C c i).obj X).extendXIso e h).hom ≫ (singleObjXSelf c i X).hom) ⋯ ≫
          mkHomFromSingle ((singleObjXSelf c i X).inv ≫ (((single C c i).obj X).extendXIso e h).inv) ⋯).f
      j' =
    (𝟙 (((single C c i).obj X).extend e)).f j'
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L L' : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
β : L ⟶ L'
⊢ e.homRestrict (ψ ≫ extendMap β e) = e.homRestrict ψ ≫ β

Tactic:
by
  ext i
  simp [homRestrict_f _ _ rfl, extendMap_f β e rfl]

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 L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝³ : K.HasHomology j
inst✝² : L.HasHomology j
inst✝¹ : (K.extend e).HasHomology j'
inst✝ : (L.extend e).HasHomology j'
⊢ QuasiIsoAt (extendMap φ e) j' ↔ QuasiIsoAt φ j

Tactic:
simp only [quasiIsoAt_iff_isIso_homologyMap]

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 L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝³ : K.HasHomology j
inst✝² : L.HasHomology j
inst✝¹ : (K.extend e).HasHomology j'
inst✝ : (L.extend e).HasHomology j'
⊢ IsIso (homologyMap (extendMap φ e) j') ↔ IsIso (homologyMap φ j)
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

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 L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncGE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : K.IsStrictlySupported e
i : ι
hi₁ : c'.Rel (c'.prev (e.f i)) (e.f i)
hi₂ : ∀ (i_1 : ι), ¬c'.Rel (e.f i_1) (e.f i)
j : ι
hj : e.f j = c'.prev (e.f i)
⊢ c'.Rel (e.f j) (e.f i)

Tactic:
by simpa only [hj] using hi₁

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

Goal state before:
pp: case right.inl
ι : 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₁ : ι₁
⊢ ∃ a, fromSum e₁ e₂ a = e₁.f i₁

Tactic:
exact ⟨Sum.inl i₁, rfl⟩

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

Goal state before:
pp: ι : 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₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i : ι₁ ⊕ ι₂
i₁ : ι₁
h : Sum.inl i₁ = i
⊢ ac.desc' x₁ x₂ i = (desc.aux X (e₁.f i₁) (ac.equiv i) ⋯) (x₁ i₁)

Tactic:
by subst h; 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
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ { X₁ := (K.shortComplexTruncLE e).X₁.homology i', X₂ := (K.shortComplexTruncLE e).X₂.homology i',
        X₃ := (K.shortComplexTruncLE e).X₃.homology i', f := homologyMap (K.shortComplexTruncLE e).f i',
        g := homologyMap (K.shortComplexTruncLE e).g i', zero := ⋯ }.f =
    0

Tactic:
by apply ((K.truncLE e).exactAt_of_isSupported e i' hi').isZero_homology.eq_of_src

Goal state after: