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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ biprod.fst.f i ≫ biprod.inl.f i + biprod.snd.f i ≫ biprod.inr.f i = 𝟙 ((K ⊞ L).X i)

Tactic:
by
  simp [← comp_f, ← add_f_apply]

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

Goal state before:
pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : ¬c.Rel i j
⊢ inrX φ i ≫ 0 = G.d i j ≫ inrX φ j

Tactic:
G.shape _ _ hij,

Goal state after:
case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : ¬c.Rel i j
⊢ inrX φ i ≫ 0 = 0 ≫ inrX φ j
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n₀ n₁ n₂ : ℤ
z : Cochain F G n₀
h₁₂ : n₁ + 1 = n₂
h₀₁ : ¬n₀ + 1 = n₁
⊢ δ n₁ n₂ 0 = 0

Tactic:
δ_zero

Goal state after:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n₀ n₁ n₂ : ℤ
z : Cochain F G n₀
h₁₂ : n₁ + 1 = n₂
h₀₁ : ¬n₀ + 1 = n₁
⊢ 0 = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ (↑(fst φ)).v p q hpq ≫ (inl φ).v q p ⋯ + (snd φ).v p p ⋯ ≫ (inr φ).f p = 𝟙 ((mappingCone φ).X p)

Tactic:
by
  simpa only [Cochain.add_v, Cochain.comp_zero_cochain_v, Cochain.ofHom_v, id_f,
    Cochain.comp_v _ _ (add_neg_cancel 1) p q p hpq (by lia)]
    using Cochain.congr_v (id φ) p p (add_zero p)

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 : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
x : ↑s.1
⊢ (ConcreteCategory.hom s.ι) x ∈ cocycle K L n

Tactic:
by
          rw [mem_iff _ _ hm]
          exact ConcreteCategory.congr_hom s.condition x

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]

Goal state after:
case neg.hp'
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'
⊢ p'' + 1 ≠ p
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⟩
    exact h.homologyMap_eq i

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝²⁵ : Category.{v_1, u_1} C₁
inst✝²⁴ : Category.{v_2, u_2} C₂
inst✝²³ : Category.{v_3, u_3} C₃
inst✝²² : Category.{v_4, u_4} D₁
inst✝²¹ : Category.{v_5, u_5} D₂
inst✝²⁰ : Category.{v_6, u_6} D₃
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₁₃ : C₁ ⥤ C₃
α : F₁₃ ⟶ F₁₂ ⋙ F₂₃
G₁₂ : D₁ ⥤ D₂
G₂₃ : D₂ ⥤ D₃
G₁₃ : D₁ ⥤ D₃
β : G₁₂ ⋙ G₂₃ ⟶ G₁₃
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂
e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃
e₁₃ : F₁₃ ⋙ L₃ ⟶ L₁ ⋙ G₁₃
A : Type u_7
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : HasShift C₁ A
inst✝¹⁷ : HasShift C₂ A
inst✝¹⁶ : HasShift C₃ A
inst✝¹⁵ : HasShift D₁ A
inst✝¹⁴ : HasShift D₂ A
inst✝¹³ : HasShift D₃ A
inst✝¹² : F₁₂.CommShift A
inst✝¹¹ : F₂₃.CommShift A
inst✝¹⁰ : F₁₃.CommShift A
inst✝⁹ : CommShift α A
inst✝⁸ : G₁₂.CommShift A
inst✝⁷ : G₂₃.CommShift A
inst✝⁶ : G₁₃.CommShift A
inst✝⁵ : CommShift β A
inst✝⁴ : L₁.CommShift A
inst✝³ : L₂.CommShift A
inst✝² : L₃.CommShift A
inst✝¹ : CommShift e₁₂ A
inst✝ : CommShift e₂₃ A
h₁₃ :
  e₁₃ =
    Functor.whiskerRight α L₃ ≫
      (F₁₂.associator F₂₃ L₃).hom ≫
        F₁₂.whiskerLeft e₂₃ ≫
          (F₁₂.associator L₂ G₂₃).inv ≫ Functor.whiskerRight e₁₂ G₂₃ ≫ (L₁.associator G₁₂ G₂₃).hom ≫ L₁.whiskerLeft β
⊢ CommShift e₁₃ A

Tactic:
subst h₁₃

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝²⁵ : Category.{v_1, u_1} C₁
inst✝²⁴ : Category.{v_2, u_2} C₂
inst✝²³ : Category.{v_3, u_3} C₃
inst✝²² : Category.{v_4, u_4} D₁
inst✝²¹ : Category.{v_5, u_5} D₂
inst✝²⁰ : Category.{v_6, u_6} D₃
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₁₃ : C₁ ⥤ C₃
α : F₁₃ ⟶ F₁₂ ⋙ F₂₃
G₁₂ : D₁ ⥤ D₂
G₂₃ : D₂ ⥤ D₃
G₁₃ : D₁ ⥤ D₃
β : G₁₂ ⋙ G₂₃ ⟶ G₁₃
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂
e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃
A : Type u_7
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : HasShift C₁ A
inst✝¹⁷ : HasShift C₂ A
inst✝¹⁶ : HasShift C₃ A
inst✝¹⁵ : HasShift D₁ A
inst✝¹⁴ : HasShift D₂ A
inst✝¹³ : HasShift D₃ A
inst✝¹² : F₁₂.CommShift A
inst✝¹¹ : F₂₃.CommShift A
inst✝¹⁰ : F₁₃.CommShift A
inst✝⁹ : CommShift α A
inst✝⁸ : G₁₂.CommShift A
inst✝⁷ : G₂₃.CommShift A
inst✝⁶ : G₁₃.CommShift A
inst✝⁵ : CommShift β A
inst✝⁴ : L₁.CommShift A
inst✝³ : L₂.CommShift A
inst✝² : L₃.CommShift A
inst✝¹ : CommShift e₁₂ A
inst✝ : CommShift e₂₃ A
⊢ CommShift
    (Functor.whiskerRight α L₃ ≫
      (F₁₂.associator F₂₃ L₃).hom ≫
        F₁₂.whiskerLeft e₂₃ ≫
          (F₁₂.associator L₂ G₂₃).inv ≫ Functor.whiskerRight e₁₂ G₂₃ ≫ (L₁.associator G₁₂ G₂₃).hom ≫ L₁.whiskerLeft β)
    A
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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ IsZero T.obj₂ ↔ T.mor₁ = 0 ∧ T.mor₂ = 0

Tactic:
by
  constructor
  · intro h
    exact ⟨h.eq_of_tgt _ _, h.eq_of_src _ _⟩
  · intro ⟨h₁, h₂⟩
    obtain ⟨f, hf⟩ := coyoneda_exact₂ T hT (𝟙 _) (by rw [h₂, comp_zero])
    rw [IsZero.iff_id_eq_zero, hf, h₁, comp_zero]

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

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

Tactic:
by
  suffices ∀ (X₁ X₃ : C), IsIso (prodComparison F X₁ X₃) by
    have := fun (X₁ X₃ : C) ↦ PreservesLimitPair.of_iso_prod_comparison F X₁ X₃
    exact ⟨fun {K} ↦ preservesLimit_of_iso_diagram F (diagramIsoPair K).symm⟩
  intro X₁ X₃
  let φ : F.mapTriangle.obj (binaryProductTriangle X₁ X₃) ⟶
      binaryProductTriangle (F.obj X₁) (F.obj X₃) :=
    { hom₁ := 𝟙 _
      hom₂ := prodComparison F X₁ X₃
      hom₃ := 𝟙 _
      comm₁ := by
        dsimp
        ext
        · simp only [assoc, prodComparison_fst, prod.comp_lift, comp_id, comp_zero,
            limit.lift_π, BinaryFan.mk_pt, BinaryFan.π_app_left, BinaryFan.mk_fst,
            ← F.map_comp, F.map_id]
        · simp only [assoc, prodComparison_snd, prod.comp_lift, comp_id, comp_zero,
            limit.lift_π, BinaryFan.mk_pt, BinaryFan.π_app_right, BinaryFan.mk_snd,
            ← F.map_comp, F.map_zero]
      comm₂ := by simp
      comm₃ := by simp }
  exact isIso₂_of_isIso₁₃ φ (F.map_distinguished _ (binaryProductTriangle_distinguished X₁ X₃))
    (binaryProductTriangle_distinguished _ _)
    (by dsimp [φ]; infer_instance) (by dsimp [φ]; infer_instance)

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✝² : HasZeroMorphisms C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ K.opcyclesToCycles i j ≫ K.homologyπ j = 0

Tactic:
by
  simp only [← cancel_epi (K.pOpcycles i),
    pOpcycles_opcyclesToCycles_assoc, toCycles_comp_homologyπ, comp_zero]

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

Goal state before:
pp: case nil
V : Type u₁
inst✝ : Quiver V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ (of V).obj u) (q : u ⟶ v), P p → P (p ≫ (of V).map q)
b✝ : Paths V
⊢ P Quiver.Path.nil

Tactic:
| nil =>

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

Goal state before:
pp: case zero.nil
V : Type u₁
inst✝ : Quiver V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : (of V).obj v ⟶ b) (q : u ⟶ v), P p → P ((of V).map q ≫ p)
h : Quiver.Path.nil.length = 0
⊢ P Quiver.Path.nil

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.6
inst✝ : Category.{v_1, ?u.6} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
⊢ Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ Quiver.Path.nil) =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) Quiver.Path.nil

Tactic:
| nil =>

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

Goal state before:
pp: case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
⊢ Φ.map Quiver.Path.nil =
    𝟙 (Φ.obj X) ≫ Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp ↦ ihp ≫ Φ.map f.toPath) Quiver.Path.nil ≫ 𝟙 (Φ.obj X)

Tactic:
| nil =>

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

Goal state before:
pp: case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
X Y : Paths V
⊢ F.map Quiver.Path.nil = eqToHom ⋯ ≫ G.map Quiver.Path.nil ≫ eqToHom ⋯

Tactic:
| nil =>

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

Goal state before:
pp: case refine_1.nil
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
h : W.paths (p.comp Path.nil)
⊢ W.paths p

Tactic:
| nil =>

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
h : W.paths (p.comp q)
⊢ W.paths p

pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
h : W.paths (p.comp q)
⊢ W.paths q

pp: case refine_3
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
x✝ : W.paths p ∧ W.paths q
hp : W.paths p
hq : W.paths q
⊢ W.paths (p.comp q)

Tactic:
· induction q with
    | nil => simpa using h
    | cons q' f h' =>
      rw [Path.comp_cons] at h
      exact h' h.1

Goal state after:
case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
h : W.paths (p.comp q)
⊢ W.paths q

case refine_3
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
x✝ : W.paths p ∧ W.paths q
hp : W.paths p
hq : W.paths q
⊢ W.paths (p.comp q)
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: case refine_2.nil
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
h : W.paths (p.comp Path.nil)
⊢ W.paths Path.nil

Tactic:
| nil =>

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

Goal state before:
pp: case nil
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Path X Y
⊢ composePath (f.comp Path.nil) = composePath f ≫ composePath Path.nil

Tactic:
| nil =>

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

Goal state before:
pp: case refine_3.nil
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
hp : W.paths p
x✝ : W.paths p ∧ W.paths Path.nil
hq : W.paths Path.nil
⊢ W.paths (p.comp Path.nil)

Tactic:
| nil =>

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
X Y : C
f : X ⟶ Y
⊢ composePath (G.map f).toPath = G.map f

Tactic:
composePath_toPath

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
X Y : C
f : X ⟶ Y
⊢ G.map f = G.map f
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case mpr.nil
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂ : Paths (LocQuiver W)
⊢ P (G.map Quiver.Path.nil)

Tactic:
| nil =>

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
f₁ f₂ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
⊢ α.add.map L ⋯ = α.symm.add.map L ⋯

Tactic:
α.symm_add

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 : C
f₁ f₂ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
⊢ α.add.map L ⋯ = α.add.map L ⋯
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
f₁ f₂ f₃ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₃ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
h₃ : f₃ = α.thd.map L ⋯
⊢ { Y' := α.Y', f := α.f + α.f', f' := α.f'', s := α.s, hs := ⋯ }.add.map L ⋯ = add' W f₁ (α.forgetFst.add.map L ⋯)

Tactic:
add'_eq W _ _ (LeftFraction₂.mk α.f (α.f' + α.f'') α.s α.hs) h₁ rfl

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 : C
f₁ f₂ f₃ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₃ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
h₃ : f₃ = α.thd.map L ⋯
⊢ { Y' := α.Y', f := α.f + α.f', f' := α.f'', s := α.s, hs := ⋯ }.add.map L ⋯ =
    { Y' := α.Y', f := α.f, f' := α.f' + α.f'', s := α.s, hs := ⋯ }.add.map L ⋯
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT (α i) κ
⊢ HasCardinalLT ((i : ι) × α i) κ

Tactic:
have : Fact (Cardinal.lift.{max u v} κ).IsRegular := ⟨Cardinal.IsRegular.lift Fact.out⟩

Goal state after:
ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT (α i) κ
this : Fact (Cardinal.lift.{max u v, w} κ).IsRegular
⊢ HasCardinalLT ((i : ι) × α i) κ
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) κ
hκ : κ.IsRegular
⊢ (P.strictLimitsClosureIter J κ.ord).strictLimitsClosureStep J = P.strictLimitsClosureIter J κ.ord

Tactic:
have (a : α) := (h a).small

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) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
⊢ (P.strictLimitsClosureIter J κ.ord).strictLimitsClosureStep J = P.strictLimitsClosureIter J κ.ord
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) κ
inst✝⁴ : ObjectProperty.EssentiallySmall.{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)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P.limitsClosure J)

Tactic:
by
  obtain ⟨Q, hQ, hQ₁, hQ₂⟩ := EssentiallySmall.exists_small_le.{w} P
  have : ObjectProperty.EssentiallySmall.{w} (Q.isoClosure.limitsClosure J) := by
    rw [limitsClosure_isoClosure,
      ← Q.isoClosure_strictLimitsClosureIter_eq_limitsClosure J κ h]
    infer_instance
  exact .of_le (limitsClosure_monotone J hQ₂)

Goal state after:
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
X Y : C
φ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{v_3, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
e : L₁ ⋙ (Localization.uniq L₁ L₂ W).functor ≅ L₂ := Localization.compUniqFunctor L₁ L₂ W
⊢ (Localization.uniq L₁ L₂ W).functor.map (φ.map L₁ ⋯) ≫
      (L₁ ⋙ (Localization.uniq L₁ L₂ W).functor).map φ.s ≫ e.hom.app φ.Y' =
    (Localization.compUniqFunctor L₁ L₂ W).hom.app X ≫ L₂.map φ.f

Tactic:
simpa [← Functor.map_comp_assoc, map_comp_map_s] using e.hom.naturality φ.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 : ObjectProperty C
i✝ : C
⊢ ⊥.extensionProduct P i✝ ≤ ⊥ i✝

Tactic:
⟨_, _, _, _, _, _, h, _⟩

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 : ObjectProperty C
i✝ w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ i✝
w✝¹ : i✝ ⟶ w✝³
w✝ : w✝³ ⟶ (shiftFunctor C 1).obj w✝⁴
left✝ : Triangle.mk w✝² w✝¹ w✝ ∈ distinguishedTriangles
h : ⊥ w✝⁴
right✝ : P w✝³
⊢ ⊥ 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 : ObjectProperty C
X' X Y : C
e : X' ⟶ X
he : IsIso e
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
mem' : P Z
⊢ P.trW (e ≫ f)

Tactic:
refine ⟨Z, g, h ≫ inv e⟦(1 : ℤ)⟧', isomorphic_distinguished _ mem _ ?_, mem'⟩

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
X' X Y : C
e : X' ⟶ X
he : IsIso e
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
mem' : P Z
⊢ Triangle.mk (e ≫ f) g (h ≫ (shiftFunctor C 1).map (inv e)) ≅ Triangle.mk f g h
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✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
⊢ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f) → quasiIso C c ((quotient C c).map f)

Tactic:
· rintro ⟨K', L', g, h, ⟨e⟩⟩
    rw [← quotient_map_mem_quasiIso_iff] at h
    exact ((quasiIso C c).arrow_mk_iso_iff e).1 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 : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
j' : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j'
⊢ (f ≫ (K.shiftFunctorObjXIso n i (i + n) ⋯).hom) ≫ K.d (i + n) j' = 0

Tactic:
obtain rfl : j' = j + n := by lia

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
⊢ (f ≫ (K.shiftFunctorObjXIso n i (i + n) ⋯).hom) ≫ K.d (i + n) (j + n) = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n a a' : ℤ
ha' : n + a = a'
X Y : C
f : X ⟶ Y
⊢ (single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map f ≫
      (Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯).hom =
    (Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯).hom ≫ (single C (ComplexShape.up ℤ) a).map f

Tactic:
obtain rfl : a' = a + n := by lia
      ext
      simp [single]

Goal state after: