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 : ℤ
φ₁ φ₂ : F ⟶ G
z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
⊢ φ₁.f p =
    (((dNext p) fun i j ↦ if hij : i + -1 = j then (↑z).v i j hij else 0) +
        (prevD p) fun i j ↦ if hij : i + -1 = j then (↑z).v i j hij else 0) +
      φ₂.f p

Tactic:
by
        have eq := Cochain.congr_v z.2 p p (add_zero p)
        have h₁ : (ComplexShape.up ℤ).Rel (p - 1) p := by simp
        have h₂ : (ComplexShape.up ℤ).Rel p (p + 1) := by simp
        simp only [δ_neg_one_cochain, Cochain.ofHom_v, ComplexShape.up_Rel, Cochain.add_v,
          Homotopy.nullHomotopicMap'_f h₁ h₂] at eq
        rw [dNext_eq _ h₂, prevD_eq _ h₁, eq, dif_pos, dif_pos]

Goal state after:
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 : ℤ
φ₁ φ₂ : F ⟶ G
z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p q : ℤ
hpq : p + -1 = q
⊢ (↑((fun ho ↦ ⟨ofHomotopy ho, ⋯⟩)
            ((fun z ↦ { hom := fun i j ↦ if hij : i + -1 = j then (↑z).v i j hij else 0, zero := ⋯, comm := ⋯ }) z))).v
      p q hpq =
    (↑z).v p q hpq

Tactic:
dsimp [Cochain.ofHomotopy]

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 : ℤ
φ₁ φ₂ : F ⟶ G
z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p q : ℤ
hpq : p + -1 = q
⊢ (if hij : p + -1 = q then (↑z).v p q hij else 0) = (↑z).v p q hpq
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ inrX K j ≫
      (Homotopy.nullHomotopicMap' fun i j hij ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ biprod.snd.f i ≫ inlX K i j hij).f
        j =
    inrX K j ≫ ((π K).f j ≫ (ι₀ K).f j - 𝟙 (homotopyCofiber.X (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
simp only [Homotopy.nullHomotopicMap'_f hij hjk, homotopyCofiber_d, assoc, comp_add,
      homotopyCofiber.inrX_d_assoc, homotopyCofiber.inrX_sndX_assoc, comp_sub,
      inrX_π_assoc, comp_id, ← Hom.comm_assoc, homotopyCofiber.inlX_d _ _ _ _ _ hjk,
      comp_neg, add_neg_cancel_left]

Goal state after:
case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    (biprod.desc (𝟙 K) (𝟙 K)).f j ≫ (ι₀ K).f j - inrX K j
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
X✝ Y✝ Z✝ : HomologicalComplex V c
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ homotopyEquivalences V c f → homotopyEquivalences V c g → homotopyEquivalences V c (f ≫ g)

Tactic:
rintro ⟨f, rfl⟩ ⟨g, rfl⟩

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
X✝ Y✝ Z✝ : HomologicalComplex V c
f : HomotopyEquiv X✝ Y✝
g : HomotopyEquiv Y✝ Z✝
⊢ homotopyEquivalences V c (f.hom ≫ g.hom)
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i : ι
X✝ Y✝ Z✝ : HomologicalComplex V c
x✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ homotopyEquivalences V c x✝ → homotopyEquivalences V c (x✝ ≫ g) → homotopyEquivalences V c g

Tactic:
by
    rintro ⟨f, rfl⟩ ⟨e, he⟩
    refine (f.symm.trans e).homotopyEquivalences_hom.of_homotopy ?_
    simp only [HomotopyEquiv.trans_hom, HomotopyEquiv.symm_hom, he, ← Category.assoc]
    exact f.homotopyInvHomId.compRightId g

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

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
h : ¬p'' = p'
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''

Tactic:
rw [single_v_eq_zero _ _ _ _ _ h, single_v_eq_zero, comp_zero, smul_zero]
        lia

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝³ : DecidableRel c.Rel
inst✝² : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝¹ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
D : Type u_3
inst✝ : Category.{v_2, u_3} D
H : HomologicalComplex C c ⥤ D
hH : (homotopyEquivalences C c).IsInvertedBy H
⊢ H.map (ι₀ K) = H.map (ι₁ K)

Tactic:
have : IsIso (H.map (cylinder.π K)) := hH _ ⟨homotopyEquiv K hc, rfl⟩
  simp only [← cancel_mono (H.map (cylinder.π K)), ← H.map_comp, ι₀_π, H.map_id, ι₁_π]

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

Goal state before:
pp: ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
⊢ (MorphismProperty.isomorphisms (HomotopyCategory V c)).inverseImage (quotient V c) = homotopyEquivalences V c

Tactic:
ext K L f

Goal state after:
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
K L : HomologicalComplex V c
f : K ⟶ L
⊢ (MorphismProperty.isomorphisms (HomotopyCategory V c)).inverseImage (quotient V c) f ↔ homotopyEquivalences V c f
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

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
K L M : CochainComplex C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p + n = p'
⊢ p' = q + a

Tactic:
← hp',

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
K L M : CochainComplex C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p + n = p'
⊢ p + n = q + a
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' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
⊢ δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'

Tactic:
by
  by_cases hnm : n + 1 = m
  · have hnm' : n' + 1 = m' := by lia
    ext p q hpq
    dsimp
    rw [(δ n m γ).leftShift_v a m' hm' p q hpq (p + a) (by lia),
      δ_v n m hnm _ (p + a) q (by lia) (p + n') (p + 1 + a) (by lia) (by lia),
      δ_v n' m' hnm' _ p q hpq (p + n') (p + 1) (by lia) rfl,
      γ.leftShift_v a n' hn' p (p + n') rfl (p + a) (by lia),
      γ.leftShift_v a n' hn' (p + 1) q (by lia) (p + 1 + a) (by lia)]
    simp only [shiftFunctor_obj_X, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl,
      Iso.refl_hom, id_comp, Linear.units_smul_comp, shiftFunctor_obj_d',
      Linear.comp_units_smul, smul_add, smul_smul]
    congr 2
    · rw [← hnm', add_comm n', mul_add, mul_one]
      simp only [Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul]
    · simp only [← Int.negOnePow_add, ← hn', ← hm', ← hnm]
      congr 1
      linarith
  · have hnm' : ¬ n' + 1 = m' := fun _ => hnm (by lia)
    rw [δ_shape _ _ hnm', δ_shape _ _ hnm, leftShift_zero, smul_zero]

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
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
⊢ ∃ a, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃

Tactic:
obtain ⟨a, ⟨ha₁, ha₂⟩⟩ := complete_distinguished_triangle_morphism _ _
    (rot_of_distTriang _ hT₁) (rot_of_distTriang _ hT₂) b c comm
  refine ⟨(shiftFunctor C (1 : ℤ)).preimage a, ⟨?_, ?_⟩⟩
  · apply (shiftFunctor C (1 : ℤ)).map_injective
    dsimp at ha₂
    rw [neg_comp, comp_neg, neg_inj] at ha₂
    simpa only [Functor.map_comp, Functor.map_preimage] using! ha₂
  · simpa only [Functor.map_preimage] using! ha₁

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
p : ℤ
⊢ (Cochain.ofHom ((triangle φ).mor₃ ≫ (rotateHomotopyEquiv φ).hom)).v p p ⋯ =
    (δ (-1) 0 (-(snd φ).comp (inl (inr φ)) ⋯) + Cochain.ofHom (inr (inr φ))).v p p ⋯

Tactic:
dsimp [rotateHomotopyEquiv]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
p : ℤ
⊢ (Cochain.ofHom
          ((triangle φ).mor₃ ≫
            lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 triangle._proof_3)
              (-(inl φ).leftShift 1 0 rotateHomotopyEquiv._proof_9) ⋯)).v
      p p ⋯ =
    (δ (-1) 0 (-(snd φ).comp (inl (inr φ)) ⋯)).v p p ⋯ + (Cochain.ofHom (inr (inr φ))).v p p ⋯
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
K L : CochainComplex C ℤ
φ : K ⟶ L
p : ℤ
⊢ ((rotateHomotopyEquiv φ).hom ≫ (triangle (inr φ)).mor₃).f p =
    (-(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ).f p

Tactic:
dsimp [rotateHomotopyEquiv]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p : ℤ
⊢ (lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 triangle._proof_3)
            (-(inl φ).leftShift 1 0 rotateHomotopyEquiv._proof_9) ⋯).f
        p ≫
      (triangle (inr φ)).mor₃.f p =
    -φ.f (p + 1)
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
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this✝¹ : IsIso φ.hom₁
this✝ : IsIso φ.hom₂
this : IsIso φ.hom₃
⊢ ∃ e', e'.hom.hom₁ = Arrow.Hom.left e.hom ∧ e'.hom.hom₂ = Arrow.Hom.right e.hom

Tactic:
have : IsIso φ := by
    apply Triangle.isIso_of_isIsos
    all_goals infer_instance

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
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this✝² : IsIso φ.hom₁
this✝¹ : IsIso φ.hom₂
this✝ : IsIso φ.hom₃
this : IsIso φ
⊢ ∃ e', e'.hom.hom₁ = Arrow.Hom.left e.hom ∧ e'.hom.hom₂ = Arrow.Hom.right e.hom
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V : Type u
C : Type u₁
inst✝¹ : Quiver V
inst✝ : Category.{v₁, u₁} C
G : V ⥤q C
⊢ (fun F ↦ Paths.of V ⋙q F.toPrefunctor) ((fun G ↦ Cat.freeMap G ⋙ pathComposition C) G) = G

Tactic:
by
    dsimp
    rw [← Functor.toPrefunctor_comp, ← Prefunctor.comp_assoc,
      pathsOf_freeMap_toPrefunctor, Prefunctor.comp_assoc,
      pathsOf_pathComposition_toPrefunctor, Prefunctor.comp_id]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction X Y
hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
Y' : C
t₁ : φ₀.Y' ⟶ Y'
t₂ : φ.Y' ⟶ Y'
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ neg' W (φ₀.map L ⋯) ≫ L.map φ₀.s ≫ L.map t₁ = φ.neg.map L ⋯ ≫ L.map (φ₀.s ≫ t₁)

Tactic:
rw [hφ₀, hst, LeftFraction.map_comp_map_s_assoc, L.map_comp,
    LeftFraction.map_comp_map_s_assoc, ← L.map_comp, ← L.map_comp,
    neg_comp, neg_comp, hft]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
⊢ AddCommGroup (L.obj X ⟶ L.obj Y)

Tactic:
letI : Zero (L.obj X ⟶ L.obj Y) := ⟨L.map 0⟩

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
this : Zero (L.obj X ⟶ L.obj Y) := { zero := L.map 0 }
⊢ AddCommGroup (L.obj X ⟶ L.obj Y)
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝¹ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
a : α
⊢ (P.strictLimitsClosureIter J κ.ord).isoClosure.limitsOfShape (J a) ≤
    ((P.strictLimitsClosureIter J κ.ord).strictLimitsClosureStep J).isoClosure

Tactic:
rw [limitsOfShape_isoClosure, ← isoClosure_strictLimitsOfShape,
        strictLimitsClosureStep]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝¹ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
a : α
⊢ ((P.strictLimitsClosureIter J κ.ord).strictLimitsOfShape (J a)).isoClosure ≤
    (P.strictLimitsClosureIter J κ.ord ⊔ ⨆ a, (P.strictLimitsClosureIter J κ.ord).strictLimitsOfShape (J a)).isoClosure
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasTerminal C
P Q : ObjectProperty C
inst✝¹ : Q.IsClosedUnderBinaryProducts
inst✝ : Q.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
h : P ≤ Q
this : Q.IsClosedUnderIsomorphisms := IsClosedUnderBinaryProducts.closedUnderIsomorphisms Q
⊢ P.binaryProductsClosure ≤ Q

Tactic:
exact limitsClosure_le h

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ homMk (ofHom W f) ≫ homMk (ofInv s hs) = homMk { Y' := Y', f := f, s := s, hs := hs }

Tactic:
homMk_comp_homMk (ofHom W f) (ofInv s hs) (ofHom W (𝟙 _)) (by simp)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ homMk ((ofHom W f).comp₀ (ofInv s hs) (ofHom W (𝟙 (ofHom W f).Y'))) = homMk { Y' := Y', f := f, s := s, hs := hs }
Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : HasShift C ℤ
inst✝⁶ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁵ : HasZeroObject C
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : Abelian A
inst✝ : F.PreservesZeroMorphisms
hF : ∀ (T : Triangle C) (hT : T ∈ distinguishedTriangles), ∃ T' e, ((shortComplexOfDistTriangle T' ⋯).map F).Exact
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ ((shortComplexOfDistTriangle T hT).map F).Exact

Tactic:
obtain ⟨T', e, h'⟩ := hF T hT

Goal state after:
C : Type u_1
A : Type u_3
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : HasShift C ℤ
inst✝⁶ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁵ : HasZeroObject C
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : Abelian A
inst✝ : F.PreservesZeroMorphisms
hF : ∀ (T : Triangle C) (hT : T ∈ distinguishedTriangles), ∃ T' e, ((shortComplexOfDistTriangle T' ⋯).map F).Exact
T : Triangle C
hT : T ∈ distinguishedTriangles
T' : Triangle C
e : T ≅ T'
h' : ((shortComplexOfDistTriangle T' ⋯).map F).Exact
⊢ ((shortComplexOfDistTriangle T hT).map F).Exact
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT✝ : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
hT : ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)
⊢ ∃ T' e, ((Pretriangulated.shortComplexOfDistTriangle T' ⋯).map (homologyFunctor C (ComplexShape.up ℤ) n)).Exact

Tactic:
obtain ⟨S, σ, ⟨e⟩⟩ := hT

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
⊢ ∃ T' e, ((Pretriangulated.shortComplexOfDistTriangle T' ⋯).map (homologyFunctor C (ComplexShape.up ℤ) n)).Exact
Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
X Y : C
f : X ⟶ (shiftFunctor C n).obj Y
a a' : M
h : n + a = a'
⊢ ((F.shift a).map (L.map f) ≫ (F.shift a).map ((commShiftIso L n).hom.app Y)) ≫
      (F.shiftIso n a a' h).hom.app (L.obj Y) =
    (e' a).hom.app X ≫ ((G.shift a).map f ≫ (G.shiftIso n a a' h).hom.app Y) ≫ (e' a').inv.app Y

Tactic:
induced_shiftIso_hom_app_obj,

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
X Y : C
f : X ⟶ (shiftFunctor C n).obj Y
a a' : M
h : n + a = a'
⊢ ((F.shift a).map (L.map f) ≫ (F.shift a).map ((commShiftIso L n).hom.app Y)) ≫
      (F.shift a).map ((commShiftIso L n).inv.app Y) ≫
        (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y =
    (e' a).hom.app X ≫ ((G.shift a).map f ≫ (G.shiftIso n a a' h).hom.app Y) ≫ (e' a').inv.app Y
Module: Mathlib.CategoryTheory.Localization.Composition

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝¹ : L₁.IsLocalization W₁
inst✝ : L₂.IsLocalization W₂
W₃ : MorphismProperty C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := { functor := E₂.functor, map := ⋯ }
this : Φ.IsLocalizedEquivalence
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans
    (Trans.trans
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (compUniqFunctor L₁ W₁.Q W₁).symm (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight (CatCommSq.iso Φ.functor L₂ W₂'.Q (Φ.localizedFunctor L₂ W₂'.Q)) E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)
⊢ (fun x ↦ x.map E₂.functor) (W₃.map L₁) ≤ W₃.map W₁.Q

Tactic:
by simpa only [W₃.map_map]
      using le_of_eq (W₃.map_eq_of_iso (compUniqFunctor L₁ W₁.Q W₁))

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ quasiIso C (ComplexShape.up ℤ) = (subcategoryAcyclic C).trW

Tactic:
ext K L f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
K L : HomotopyCategory C (ComplexShape.up ℤ)
f : K ⟶ L
⊢ quasiIso C (ComplexShape.up ℤ) f ↔ (subcategoryAcyclic C).trW f
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n i i' : ℤ
hi : n + i = i'
⊢ n + (up ℤ).prev i = (up ℤ).prev i'

Tactic:
simp only [prev]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n i i' : ℤ
hi : n + i = i'
⊢ n + (i - 1) = i' - 1
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.IsStableUnderShift ℤ
n : ℤ
⊢ P.trW.inverseImage (shiftFunctor C n) = P.trW

Tactic:
ext K L f

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
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.IsStableUnderShift ℤ
n : ℤ
K L : C
f : K ⟶ L
⊢ P.trW.inverseImage (shiftFunctor C n) f ↔ P.trW f