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

Goal state before:
pp: V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
i j : α
h : i ≠ j + 1
⊢ of.d X d i j = 0

Tactic:
simp [of.d, dif_neg h]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ Subsingleton Ω[S⁄R]

Tactic:
suffices (⊤ : Submodule S Ω[S⁄R]) ≤ ⊥ from
    (subsingleton_iff_forall_eq 0).mpr fun y ↦ this trivial

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ ⊤ ≤ ⊥
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
i j : α
h : i + 1 ≠ j
⊢ of.d X d i j = 0

Tactic:
simp [of.d, dif_neg h]

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i : A
⊢ shiftFunctorComm C i i = Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i)

Tactic:
rw [shiftFunctorComm_eq C i i (i + i) rfl, Iso.symm_self_id]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
K L : ChainComplex C ℕ
φ : K ⟶ L
inst✝¹ : HomologicalComplex.HasHomology K 0
inst✝ : HomologicalComplex.HasHomology L 0
⊢ K.isoHomologyι₀.inv ≫ HomologicalComplex.homologyMap φ 0 = HomologicalComplex.opcyclesMap φ 0 ≫ L.isoHomologyι₀.inv

Tactic:
by
  simp only [assoc, ← cancel_mono (L.homologyι 0),
    HomologicalComplex.homologyι_naturality, HomologicalComplex.isoHomologyι_inv_hom_id_assoc,
    HomologicalComplex.isoHomologyι_inv_hom_id, comp_id]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E₁ : Type u_3
E₂ : Type u_4
inst✝¹ : Category.{v_3, u_3} E₁
inst✝ : Category.{v_4, u_4} E₂
F₁ : C₁ ⥤ E₁
F₂ : C₂ ⥤ E₂
h₁ : W₁.IsInvertedBy F₁
h₂ : W₂.IsInvertedBy F₂
x✝¹ x✝ : C₁ × C₂
f : x✝¹ ⟶ x✝
hf : W₁.prod W₂ f
⊢ IsIso ((F₁.prod F₂).map f)

Tactic:
isIso_prod_iff

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E₁ : Type u_3
E₂ : Type u_4
inst✝¹ : Category.{v_3, u_3} E₁
inst✝ : Category.{v_4, u_4} E₂
F₁ : C₁ ⥤ E₁
F₂ : C₂ ⥤ E₂
h₁ : W₁.IsInvertedBy F₁
h₂ : W₂.IsInvertedBy F₂
x✝¹ x✝ : C₁ × C₂
f : x✝¹ ⟶ x✝
hf : W₁.prod W₂ f
⊢ IsIso ((F₁.prod F₂).map f).1 ∧ IsIso ((F₁.prod F₂).map f).2
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z₁ z₂ : Cochain F G 0
h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯
⊢ z₁ = z₂

Tactic:
ext
  grind

Goal state after:
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✝ : ι
f g : C ⟶ D
h : Homotopy f g
i : ι
⊢ g.f i = (dNext i) (-h.hom) + (prevD i) (-h.hom) + f.f i

Tactic:
map_neg,

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✝ : ι
f g : C ⟶ D
h : Homotopy f g
i : ι
⊢ g.f i = -(dNext i) h.hom + (prevD i) (-h.hom) + f.f i
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✝ : ι
f g : C ⟶ D
h : Homotopy f g
i : ι
⊢ g.f i = -(dNext i) h.hom + (prevD i) (-h.hom) + f.f i

Tactic:
map_neg,

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✝ : ι
f g : C ⟶ D
h : Homotopy f g
i : ι
⊢ g.f i = -(dNext i) h.hom + -(prevD i) h.hom + f.f i
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

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

Tactic:
ext p q hpq
  simp only [comp_v _ _ h p _ q rfl (by lia), zero_v, zero_comp]

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

Goal state before:
pp: case mpr
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
K : HomologicalComplex C c
x y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
⊢ (x.fst = y.fst ∧ ∀ (i j : ι), c.Rel j i → x.snd.hom i j = y.snd.hom i j) → x = y

Tactic:
obtain ⟨x₁, x₂⟩ := x

Goal state after:
case mpr
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
K : HomologicalComplex C c
y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
⊢ (⟨x₁, x₂⟩.fst = y.fst ∧ ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = y.snd.hom i j) → ⟨x₁, x₂⟩ = y
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
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''

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:
· subst h
        obtain rfl : p = p'' + 1 := by lia
        simp

Goal state after:
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''
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
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
X : C
this :
  F.map ((shiftFunctor C a).map ((shiftFunctorZero C A).inv.app X)) ≫ e.hom.app ((shiftFunctor C 0).obj X) =
    e.hom.app X ≫ (shiftFunctor D a).map (F.map ((shiftFunctorZero C A).inv.app X))
⊢ (isoAdd' ⋯ (isoZero F A) e).hom.app X = e.hom.app X

Tactic:
simp [shiftFunctorAdd'_zero_add_hom_app,
    shiftFunctorAdd'_zero_add_inv_app, ← map_comp,
    reassoc_of% this]

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
G : C ⥤ D
inst✝ : G.Additive
⊢ (G.mapHomologicalComplex (ComplexShape.up ℤ)).map (triangle φ).mor₃ ≫
      (Functor.commShiftIso (G.mapHomologicalComplex (ComplexShape.up ℤ)) 1).hom.app K =
    (mapHomologicalComplexIso φ G).hom ≫ (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃

Tactic:
by
  ext n
  dsimp [mapHomologicalComplexIso]
  rw [mapHomologicalComplexXIso_eq φ G n (n + 1) rfl, mapHomologicalComplexXIso'_hom]
  simp only [Functor.mapHomologicalComplex_obj_X, add_comp, assoc, inl_v_triangle_mor₃_f,
    shiftFunctor_obj_X, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv,
    comp_neg, comp_id, inr_f_triangle_mor₃_f, comp_zero, add_zero]
  dsimp [triangle]
  rw [Cochain.rightShift_v _ 1 0 (by lia) n n (by lia) (n + 1) (by lia)]
  simp only [shiftFunctor_obj_X, Cochain.neg_v, shiftFunctorObjXIso,
    HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv, comp_id, Functor.map_neg]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
p : ℤ
this : Mono (S.map (eval C (ComplexShape.up ℤ) (p + 2))).f
⊢ (δ 1 2 (Cochain.mk fun p q x ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)).v p (p + 2) ⋯ = Cochain.v 0 p (p + 2) ⋯

Tactic:
have r_f := fun n => (σ n).r_f

Goal state after:
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
p : ℤ
this : Mono (S.map (eval C (ComplexShape.up ℤ) (p + 2))).f
r_f :
  ∀ (n : ℤ),
    (σ n).r ≫ (S.map (eval C (ComplexShape.up ℤ) n)).f =
      𝟙 (S.map (eval C (ComplexShape.up ℤ) n)).X₂ - (S.map (eval C (ComplexShape.up ℤ) n)).g ≫ (σ n).s
⊢ (δ 1 2 (Cochain.mk fun p q x ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)).v p (p + 2) ⋯ = Cochain.v 0 p (p + 2) ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
p : ℤ
this : Mono (S.map (eval C (ComplexShape.up ℤ) (p + 2))).f
r_f :
  ∀ (n : ℤ),
    (σ n).r ≫ (S.map (eval C (ComplexShape.up ℤ) n)).f =
      𝟙 (S.map (eval C (ComplexShape.up ℤ) n)).X₂ - (S.map (eval C (ComplexShape.up ℤ) n)).g ≫ (σ n).s
⊢ (δ 1 2 (Cochain.mk fun p q x ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)).v p (p + 2) ⋯ = Cochain.v 0 p (p + 2) ⋯

Tactic:
have s_g := fun n => (σ n).s_g

Goal state after:
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
p : ℤ
this : Mono (S.map (eval C (ComplexShape.up ℤ) (p + 2))).f
r_f :
  ∀ (n : ℤ),
    (σ n).r ≫ (S.map (eval C (ComplexShape.up ℤ) n)).f =
      𝟙 (S.map (eval C (ComplexShape.up ℤ) n)).X₂ - (S.map (eval C (ComplexShape.up ℤ) n)).g ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ (S.map (eval C (ComplexShape.up ℤ) n)).g = 𝟙 (S.map (eval C (ComplexShape.up ℤ) n)).X₃
⊢ (δ 1 2 (Cochain.mk fun p q x ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)).v p (p + 2) ⋯ = Cochain.v 0 p (p + 2) ⋯
Module: Mathlib.CategoryTheory.PathCategory.Basic

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

Tactic:
intro a b
  revert a
  exact induction_fixed_target (P := fun f ↦ P f) id (fun _ _ ↦ comp _ _)

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

Goal state before:
pp: case refine_3.cons
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
b✝ c✝ : C
q : Path Y b✝
q' : b✝ ⟶ c✝
h : W.paths p ∧ W.paths q → W.paths q → W.paths (p.comp q)
x✝ : W.paths p ∧ W.paths (q.cons q')
hq : W.paths (q.cons q')
⊢ W.paths (p.comp (q.cons q'))

Tactic:
| cons q q' h =>

Goal state after:
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''
⊢ e X' = X''

Tactic:
hX'

Goal state after:
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''
⊢ X'' = X''
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s) ≫ u = (t₁ ≫ α.f) ≫ u
⊢ ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u

Tactic:
← reassoc_of% hst,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s) ≫ u = (t₁ ≫ α.f) ≫ u
⊢ φ.s ≫ t₁ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case of_isoClosure
C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝² : (a : α) → Category.{v', u'} (J a)
Q : ObjectProperty C
inst✝¹ : Q.IsClosedUnderIsomorphisms
inst✝ : ∀ (a : α), Q.IsClosedUnderLimitsOfShape (J a)
h : P ≤ Q
X X✝ Y✝ : C
e : X✝ ≅ Y✝
hX : P.limitsClosure J X✝
hX' : Q X✝
⊢ Q Y✝

Tactic:
exact Q.prop_of_iso e hX'

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure

Goal state before:
pp: case of_isoClosure
C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝² : (a : α) → Category.{v', u'} (J a)
Q : ObjectProperty C
inst✝¹ : Q.IsClosedUnderIsomorphisms
inst✝ : ∀ (a : α), Q.IsClosedUnderColimitsOfShape (J a)
h : P ≤ Q
X X✝ Y✝ : C
e : X✝ ≅ Y✝
hX : P.colimitsClosure J X✝
hX' : Q X✝
⊢ Q Y✝

Tactic:
exact Q.prop_of_iso e hX'

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : P.IsClosedUnderIsomorphisms
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : HasShift C G
| P

Tactic:
rw [← P.shift_zero G]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : P.IsClosedUnderIsomorphisms
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : HasShift C G
| P.shift 0
Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Goal state before:
pp: case mp
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.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h✝ : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h✝ ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h✝) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h✝) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
h : ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
n : ℤ
⊢ IsIso ((F.shift n).map f)

Tactic:
obtain ⟨m, rfl⟩ : ∃ (m : ℤ), n = m + 1 := ⟨n - 1, by simp⟩

Goal state after:
case mp
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.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h✝ : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h✝ ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h✝) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h✝) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
h : ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
m : ℤ
⊢ IsIso ((F.shift (m + 1)).map 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
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : (up ℤ).next i = j
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj' : (up ℤ).next i' = j'
⊢ (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) ≫ K.d i' j' = 0

Tactic:
simp only [next] at hj hj'

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
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj : i + 1 = j
hj' : i' + 1 = j'
⊢ (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) ≫ K.d i' j' = 0
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₃
inst✝ : HasZeroObject C
⊢ ((quotient C (ComplexShape.up ℤ)).map
          ((mappingCone.triangle g).mor₃ ≫
            (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (mappingCone.inr f)) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone f)) ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (𝟙 ((quotient C (ComplexShape.up ℤ)).obj (mappingCone f))) =
    (quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom ≫
      (quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯)).mor₃ ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone f)

Tactic:
rw [CategoryTheory.Functor.map_id, comp_id, ← Functor.map_comp_assoc]

Goal state after:
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₃
inst✝ : HasZeroObject C
⊢ (quotient C (ComplexShape.up ℤ)).map
        ((mappingCone.triangle g).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (mappingCone.inr f)) ≫
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone f) =
    (quotient C (ComplexShape.up ℤ)).map
        ((mappingConeCompHomotopyEquiv f g).hom ≫ (mappingCone.triangle (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯)).mor₃) ≫
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone f)
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j

Tactic:
by
  by_cases hij : c.Rel j i
  · obtain rfl := c.prev_eq' hij
    exact (K.sc i).opcyclesOpIso_hom_toCycles_op
  · rw [K.toCycles_eq_zero hij, K.op.fromOpcycles_eq_zero hij, op_zero, comp_zero]

Goal state after:
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
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')

Tactic:
by_cases hi' : ∃ i, e.f i = i'
  · obtain ⟨i, hi⟩ := hi'
    simp [extendMap_f _ e hi]
  · apply (K.isZero_extend_X e i' (fun i hi => hi' ⟨i, hi⟩)).eq_of_src

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

Goal state before:
pp: case pos
ι : 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 : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ i, e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ 0 = K.d i' (e.f j) ≫ 𝟙 (K.X (e.f j)) ≫ φ.f j ≫ (L.extendXIso e ⋯).inv

Tactic:
rw [id_comp, reassoc_of% (hφ j (e.boundaryGE hij'
          (by simpa using hi')) i' hij'), zero_comp]

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

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✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ (K.extendXIso e hj').inv = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : c.Rel i j
hi'' : e.f i = i'
this : (K.extendXIso e hi'').hom ≫ f' = f''
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0

Tactic:
rw [← cancel_epi (K.extendXIso e hi'').hom, comp_zero, ← this, assoc]

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

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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ K.d i' j' ≫ (K.restrictionXIso e hj').inv ≫ (K.restriction e).pOpcycles j = 0

Tactic:
by
      rw [← cancel_epi (K.restrictionXIso e hi').hom, ← restriction_d_eq_assoc,
        comp_zero, d_pOpcycles]

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 M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
⊢ (K.extend e).d i' j' ≫ (K.extendXIso e hj').hom ≫ h.p = 0

Tactic:
rw [← d_comp_eq_zero_iff K e hj' hi hi']

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 M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
⊢ K.d i j ≫ h.p = 0