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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
l : s.pt ⟶ (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt
hl : l ≫ Fork.ι (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯) = s.ι
⊢ l = AddCommGrpCat.ofHom { toFun := fun x ↦ ⟨(ConcreteCategory.hom s.ι) x, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

Tactic:
ext : 3

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
l : s.pt ⟶ (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt
hl : l ≫ Fork.ι (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯) = s.ι
x✝ : ↑s.pt
⊢ (AddCommGrpCat.Hom.hom l) x✝ =
    (AddCommGrpCat.Hom.hom
        (AddCommGrpCat.ofHom { toFun := fun x ↦ ⟨(ConcreteCategory.hom s.ι) x, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }))
      x✝
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: case h_map
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
⊢ ∀ (X Y : Quotient r) (f : X ⟶ Y), Φ.map f ≍ (lift r (functor r ⋙ Φ) H).map f

Tactic:
rintro _ _ f
    dsimp [lift, Functor]
    refine Quot.inductionOn f fun _ ↦ ?_
    simp only [heq_eq_eq]
    congr

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
ι : Type u_2
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : Preadditive V
c : ComplexShape ι
inst✝ : CategoryWithHomology V
i : ι
⊢ ∀ (x y : HomologicalComplex V c) (f₁ f₂ : x ⟶ y),
    homotopic V c f₁ f₂ →
      (HomologicalComplex.homologyFunctor V c i).map f₁ = (HomologicalComplex.homologyFunctor V c i).map f₂

Tactic:
rintro K L f g ⟨h⟩

Goal state after:
R : Type u_1
inst✝³ : Semiring R
ι : Type u_2
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : Preadditive V
c : ComplexShape ι
inst✝ : CategoryWithHomology V
i : ι
K L : HomologicalComplex V c
f g : K ⟶ L
h : Homotopy f g
⊢ (HomologicalComplex.homologyFunctor V c i).map f = (HomologicalComplex.homologyFunctor V c i).map g
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).inv.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
by
  subst h
  rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_inv_app_f]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ (XIsoOfEq K ⋯).hom ≫ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) b a (a + b) ⋯).hom.app K).f p =
    (XIsoOfEq K ⋯).hom

Tactic:
shiftFunctorAdd'_hom_app_f'

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ (XIsoOfEq K ⋯).hom ≫ (XIsoOfEq K ⋯).hom = (XIsoOfEq K ⋯).hom
Module: Mathlib.CategoryTheory.Shift.CommShift

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
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
x✝ : C
⊢ (isoZero' F A 0 ⋯).hom.app x✝ = (isoZero F A).hom.app x✝

Tactic:
simp [isoZero', shiftFunctorZero']

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

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : ¬n + 1 = m
hnm' : ¬n' + 1 = m'
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

Tactic:
δ_shape _ _ hnm',

Goal state after:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : ¬n + 1 = m
hnm' : ¬n' + 1 = m'
⊢ 0 = a.negOnePow • (δ n m γ).rightShift a m' hm'
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
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₁
s : Fan T
m : s.pt ⟶ (fan T).pt
hm : ∀ (j : J), m ≫ (fan T).proj j = s.proj j
⊢ m.hom₁ = (lift T s.proj).hom₁

pp: case h₂
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
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₁
s : Fan T
m : s.pt ⟶ (fan T).pt
hm : ∀ (j : J), m ≫ (fan T).proj j = s.proj j
⊢ m.hom₂ = (lift T s.proj).hom₂

pp: case h₃
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
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₁
s : Fan T
m : s.pt ⟶ (fan T).pt
hm : ∀ (j : J), m ≫ (fan T).proj j = s.proj j
⊢ m.hom₃ = (lift T s.proj).hom₃

Tactic:
all_goals
      exact Pi.hom_ext _ _ (fun j => (by simp [← hm]))

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
J : Type u_1
T : J → Triangle C
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₁
inst✝ : HasZeroMorphisms C
h : ∀ (j : J), (T j).mor₃ ≫ (shiftFunctor C 1).map (T j).mor₁ = 0
this : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₂
j : J
⊢ ((Limits.Pi.map fun j ↦ (T j).mor₃) ≫
        inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) ≫
          (shiftFunctor C 1).map (Pi.lift fun j ↦ Pi.π (fun j ↦ (T j).obj₁) j ≫ (T j).mor₁) ≫
            piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₂) ≫
      Pi.π (fun b ↦ (shiftFunctor C 1).obj (T b).obj₂) j =
    0 ≫ Pi.π (fun b ↦ (shiftFunctor C 1).obj (T b).obj₂) j

Tactic:
simp [h j]

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

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : ¬n + 1 = m
hnm' : ¬n' + 1 = m'
⊢ δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'

Tactic:
δ_shape _ _ hnm',

Goal state after:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : ¬n + 1 = m
hnm' : ¬n' + 1 = m'
⊢ 0 = a.negOnePow • (δ n m γ).leftShift a m' hm'
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
T : Triangle C
⊢ ((shiftFunctor C n).obj T).mor₃ ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₁).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₃).hom ≫ ((shiftFunctor C a ⋙ shiftFunctor C b).obj T).mor₃

Tactic:
subst h
        dsimp
        rw [Linear.units_smul_comp, Linear.comp_units_smul, Functor.map_units_smul,
          Linear.units_smul_comp, Linear.comp_units_smul, smul_smul, assoc, Functor.map_comp, assoc,
          ← dsimp% (CategoryTheory.shiftFunctorAdd' C a b (a + b) rfl).hom.naturality_assoc]
        simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Int.negOnePow_add,
          shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app, add_comm a]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
⊢ ∃ c,
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = c ≫ T₂.mor₃

Tactic:
let γ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
⊢ ∃ c,
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = c ≫ T₂.mor₃
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.Exact
inst✝³ : Epi S.g
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Epi (S.map (eval C c i)).g
hj : IsColimit (CokernelCofork.ofπ (S.map (eval C c i)).g ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : opcyclesMap S.f i ≫ k = 0
⊢ S.f.f i ≫ S.X₂.pOpcycles i ≫ k = 0

Tactic:
rw [← p_opcyclesMap_assoc, hk, comp_zero]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction₂ X Y
h : LeftFraction₂Rel z₁ z₂
⊢ LeftFractionRel z₁.fst z₂.fst

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, _, ht⟩ := h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction₂ X Y
Z : C
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
w✝ : z₁.f' ≫ t₁ = z₂.f' ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ LeftFractionRel z₁.fst z₂.fst
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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

Tactic:
dsimp at fac₁ fac₂ fac₁' fac₂' fac₃ ⊢

Goal state after:
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
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' ⟶ U
t₂ : b₂.Y' ⟶ U
hst : b₁.s ≫ t₁ = b₂.s ≫ t₂
hft : b₁.f ≫ t₁ = b₂.f ≫ t₂
ht : W (b₁.s ≫ t₁)
z₁ : W.LeftFraction a.Y' b₁.Y'
fac₁ : b₁.f ≫ z₁.s = a.s ≫ z₁.f
z₂ : W.LeftFraction a.Y' b₂.Y'
fac₂ : b₂.f ≫ z₂.s = a.s ≫ z₂.f
w₁ : W.LeftFraction z₁.Y' U
fac₁' : t₁ ≫ w₁.s = z₁.s ≫ w₁.f
w₂ : W.LeftFraction z₂.Y' U
fac₂' : t₂ ≫ w₂.s = z₂.s ≫ w₂.f
u : W.LeftFraction w₁.Y' w₂.Y'
fac₃ : w₂.s ≫ u.s = w₁.s ≫ u.f
⊢ a.comp b₁ = a.comp b₂
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case isMin
C : Type u
inst✝¹⁰ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁹ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝⁸ : LinearOrder β
inst✝⁷ : OrderBot β
inst✝⁶ : SuccOrder β
inst✝⁵ : WellFoundedLT β
inst✝⁴ : ObjectProperty.Small.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β}, b ≤ c → ∀ [Small.{w, w'} ↑(Set.Iio c)], Small.{w, w'} ↑(Set.Iio b)
hb : IsMin ⊥
hb₀ : Small.{w, w'} ↑(Set.Iio ⊥)
⊢ ObjectProperty.Small.{w, v, u} (P.strictLimitsClosureIter J ⊥)

Tactic:
simp only [transfiniteIterate_bot]

Goal state after:
case isMin
C : Type u
inst✝¹⁰ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁹ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝⁸ : LinearOrder β
inst✝⁷ : OrderBot β
inst✝⁶ : SuccOrder β
inst✝⁵ : WellFoundedLT β
inst✝⁴ : ObjectProperty.Small.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β}, b ≤ c → ∀ [Small.{w, w'} ↑(Set.Iio c)], Small.{w, w'} ↑(Set.Iio b)
hb : IsMin ⊥
hb₀ : Small.{w, w'} ↑(Set.Iio ⊥)
⊢ ObjectProperty.Small.{w, v, u} P
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case mp
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 R : ObjectProperty C✝
inst✝ : IsTriangulated C✝
X Y✝ C : C✝
f : Y✝ ⟶ X
g : X ⟶ C
h : C ⟶ (shiftFunctor C✝ 1).obj Y✝
hT : Triangle.mk f g h ∈ distinguishedTriangles
A B : C✝
f' : A ⟶ Y✝
g' : Y✝ ⟶ B
h' : B ⟶ (shiftFunctor C✝ 1).obj A
hT' : Triangle.mk f' g' h' ∈ distinguishedTriangles
hP : P A
hQ : Q B
hR : R C
Y : C✝
g'' : X ⟶ Y
h'' : Y ⟶ (shiftFunctor C✝ 1).obj A
hT'' : Triangle.mk (f' ≫ f) g'' h'' ∈ distinguishedTriangles
⊢ P.extensionProduct (Q.extensionProduct R) X

Tactic:
let o := someOctahedron rfl hT' hT hT''

Goal state after:
case mp
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 R : ObjectProperty C✝
inst✝ : IsTriangulated C✝
X Y✝ C : C✝
f : Y✝ ⟶ X
g : X ⟶ C
h : C ⟶ (shiftFunctor C✝ 1).obj Y✝
hT : Triangle.mk f g h ∈ distinguishedTriangles
A B : C✝
f' : A ⟶ Y✝
g' : Y✝ ⟶ B
h' : B ⟶ (shiftFunctor C✝ 1).obj A
hT' : Triangle.mk f' g' h' ∈ distinguishedTriangles
hP : P A
hQ : Q B
hR : R C
Y : C✝
g'' : X ⟶ Y
h'' : Y ⟶ (shiftFunctor C✝ 1).obj A
hT'' : Triangle.mk (f' ≫ f) g'' h'' ∈ distinguishedTriangles
o : Octahedron ⋯ hT' hT hT'' := someOctahedron ⋯ hT' hT hT''
⊢ P.extensionProduct (Q.extensionProduct R) X
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₁ P₂ Q : ObjectProperty C
inst✝¹ : Q.IsTriangulatedClosed₂
inst✝ : Q.IsClosedUnderIsomorphisms
h₁ : P₁ ≤ Q
h₂ : P₂ ≤ Q
i✝ w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ i✝
w✝¹ : i✝ ⟶ w✝³
w✝ : w✝³ ⟶ (shiftFunctor C 1).obj w✝⁴
hT : Triangle.mk w✝² w✝¹ w✝ ∈ distinguishedTriangles
hY : P₁ w✝⁴
hZ : P₂ w✝³
⊢ Q i✝

Tactic:
exact ext_of_isTriangulatedClosed₂ Q _ hT (h₁ _ hY) (h₂ _ hZ)

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
⊢ (P.retractClosure.extensionProduct Q.retractClosure).retractClosure = (P.extensionProduct Q).retractClosure

Tactic:
apply le_antisymm
  · rw [retractClosure_le_iff]
    exact extensionProduct_retractClosure_retractClosure_le P Q
  · apply monotone_retractClosure
    grw [monotone_extensionProduct_right _ (le_retractClosure Q),
      monotone_extensionProduct_left _ (le_retractClosure P)]

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

Goal state before:
pp: case mp
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hK : IsZero (K.sc i).homology
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f)) → IsZero (L.sc i).homology

Tactic:
intro h
    exact IsZero.of_iso hK (@asIso _ _ _ _ _ h).symm

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

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L K' L' : HomologicalComplex C c
φ : K ⟶ L
φ' : K' ⟶ L'
e : Arrow.mk φ ≅ Arrow.mk φ'
inst✝³ : ∀ (i : ι), K.HasHomology i
inst✝² : ∀ (i : ι), L.HasHomology i
inst✝¹ : ∀ (i : ι), K'.HasHomology i
inst✝ : ∀ (i : ι), L'.HasHomology i
⊢ QuasiIso φ ↔ QuasiIso φ'

Tactic:
simp [← quasiIso_iff_comp_left (show K' ⟶ K from e.inv.left) φ,
    ← quasiIso_iff_comp_right φ' (show L' ⟶ L from e.inv.right)]

Goal state after:
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 Q : ObjectProperty C
hPQ : P ≤ Q
n : ℕ
h : P.extensionProductIter n ≤ Q.extensionProductIter n
⊢ Q.extensionProduct (P.extensionProductIter n) ≤ Q.extensionProduct (Q.extensionProductIter n)

Tactic:
monotone_extensionProduct_right _ h

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 Q : ObjectProperty C
hPQ : P ≤ Q
n : ℕ
h : P.extensionProductIter n ≤ Q.extensionProductIter n
⊢ Q.extensionProduct (Q.extensionProductIter n) ≤ Q.extensionProduct (Q.extensionProductIter n)
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: case mp
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 : IsIso (Q.map f)
⊢ ∀ (i : ι), QuasiIsoAt f i

Tactic:
intro i

Goal state after:
case mp
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 : IsIso (Q.map f)
i : ι
⊢ QuasiIsoAt f i
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
hf : HomologicalComplex.quasiIso C c f
⊢ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f)

Tactic:
exact MorphismProperty.map_mem_map _ _ _ hf

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 : ObjectProperty C
inst✝¹ : P.ContainsZero
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ P.trW f

Tactic:
refine (P.trW.arrow_mk_iso_iff ?_).1 (MorphismProperty.id_mem _ X)
  exact Arrow.isoMk (Iso.refl _) (asIso f)

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ i, c.Rel i j
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
⊢ (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)

Tactic:
apply Functor.IsLocalization.mk'
  all_goals apply c.strictUniversalPropertyFixedTargetQuotient hc

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
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
X Y : C
φ : P.trW.RightFraction X Y
Z : C
f : X ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj φ.X'
H : Triangle.mk φ.s f g ∈ distinguishedTriangles
mem : P Z
Y' : C
s' : Y ⟶ Y'
f' : Y' ⟶ Z
mem' : Triangle.mk s' f' (g ≫ (shiftFunctor C 1).map φ.f) ∈ distinguishedTriangles
b : (Triangle.mk φ.s f g).obj₂ ⟶ (Triangle.mk s' f' (g ≫ (shiftFunctor C 1).map φ.f)).obj₂
hb₁ : (Triangle.mk φ.s f g).mor₁ ≫ b = φ.f ≫ (Triangle.mk s' f' (g ≫ (shiftFunctor C 1).map φ.f)).mor₁
right✝ : (Triangle.mk φ.s f g).mor₂ ≫ 𝟙 Z = b ≫ (Triangle.mk s' f' (g ≫ (shiftFunctor C 1).map φ.f)).mor₂
⊢ ∃ ψ, φ.f ≫ ψ.s = φ.s ≫ ψ.f

Tactic:
exact ⟨MorphismProperty.LeftFraction.mk b s' ⟨_, _, _, mem', mem⟩, hb₁.symm⟩

Goal state after:
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₃
⊢ δ 0 1 (descCochain g 0 (Cochain.ofHom (inr (f ≫ g))) ⋯) +
      (↑(descCocycle g (Cochain.ofHom (inr f)) 0 ⋯ ⋯)).comp (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) ⋯ =
    0

Tactic:
by
      ext p _ rfl
      dsimp [mappingConeCompTriangle, map]
      simp [ext_from_iff _ _ _ rfl, inl_v_d_assoc _ (p + 1) p (p + 2) (by lia) (by lia)]

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✝ Y✝ : HomologicalComplex V c.symm
f : X✝ ⟶ Y✝
i j : ι
x✝ : c.Rel i j
⊢ (f.f i).op ≫ X✝.opSymm.d i j = Y✝.opSymm.d i j ≫ (f.f j).op

Tactic:
simp only [opSymm_d, ← op_comp, f.comm]

Goal state after: