mathlib-initiative/mathlib-tactics huggingface dataset:
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
L : C ⥤ D
W✝ : MorphismProperty C
inst✝ : L.IsLocalization W✝
W : MorphismProperty Cᵒᵖ
h : W.HasLeftCalculusOfFractions
X Y : C
φ : W.unop.LeftFraction X Y
⊢ ∃ ψ, ψ.s ≫ φ.f = ψ.f ≫ φ.s

Tactic:
obtain ⟨ψ, eq⟩ := h.exists_leftFraction φ.op

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✝
W : MorphismProperty Cᵒᵖ
h : W.HasLeftCalculusOfFractions
X Y : C
φ : W.unop.LeftFraction X Y
ψ : W.LeftFraction (Opposite.op Y) (Opposite.op X)
eq : φ.op.f ≫ ψ.s = φ.op.s ≫ ψ.f
⊢ ∃ ψ, ψ.s ≫ φ.f = ψ.f ≫ φ.s
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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ ∃ φ, f = φ.map L ⋯

Tactic:
obtain ⟨φ, eq⟩ := Localization.exists_leftFraction L.op W.op f.op

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.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map L.op ⋯
⊢ ∃ φ, f = φ.map L ⋯
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.IsTriangulatedClosed₁
Y Z : C
b : Y ⟶ Z
hY : P Y
hZ : P Z
X : C
a : X ⟶ Y
c : Z ⟶ (shiftFunctor C 1).obj X
h : Triangle.mk a b c ∈ distinguishedTriangles
⊢ ∃ X, ∃ (_ : P X), ∃ a c, Triangle.mk a b c ∈ distinguishedTriangles

Tactic:
obtain ⟨X', hX', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₁' _ h hY hZ

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
inst✝ : P.IsTriangulatedClosed₁
Y Z : C
b : Y ⟶ Z
hY : P Y
hZ : P Z
X : C
a : X ⟶ Y
c : Z ⟶ (shiftFunctor C 1).obj X
h : Triangle.mk a b c ∈ distinguishedTriangles
X' : C
hX' : P X'
e : (Triangle.mk a b c).obj₁ ≅ X'
⊢ ∃ X, ∃ (_ : P X), ∃ a c, Triangle.mk a b c ∈ distinguishedTriangles
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝³ x✝² x✝¹ x✝ : C
f : x✝³ ⟶ x✝²
g : x✝¹ ⟶ x✝
h : RetractArrow f g
hg : Mono g
Z✝ : C
α β : Z✝ ⟶ x✝³
w : α ≫ f = β ≫ f
⊢ α ≫ f ≫ Arrow.Hom.right h.i = β ≫ f ≫ Arrow.Hom.right h.i

Tactic:
reassoc_of% w

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x✝³ x✝² x✝¹ x✝ : C
f : x✝³ ⟶ x✝²
g : x✝¹ ⟶ x✝
h : RetractArrow f g
hg : Mono g
Z✝ : C
α β : Z✝ ⟶ x✝³
w : α ≫ f = β ≫ f
⊢ β ≫ f ≫ Arrow.Hom.right h.i = β ≫ f ≫ Arrow.Hom.right h.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
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
hP : ∀ T ∈ distinguishedTriangles, P T.obj₂ → P T.obj₃ → P T.obj₁
⊢ ∀ T ∈ distinguishedTriangles, P T.obj₂ → P T.obj₃ → P.isoClosure T.obj₁

Tactic:
by simpa only [isoClosure_eq_self] using hP

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.IsClosedUnderIsomorphisms
hP : ∀ T ∈ distinguishedTriangles, P T.obj₁ → P T.obj₃ → P T.obj₂
⊢ ∀ T ∈ distinguishedTriangles, P T.obj₁ → P T.obj₃ → P.isoClosure T.obj₂

Tactic:
by simpa only [isoClosure_eq_self] using hP

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.IsClosedUnderIsomorphisms
hP : ∀ T ∈ distinguishedTriangles, P T.obj₁ → P T.obj₂ → P T.obj₃
⊢ ∀ T ∈ distinguishedTriangles, P T.obj₁ → P T.obj₂ → P.isoClosure T.obj₃

Tactic:
by simpa only [isoClosure_eq_self] using hP

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

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
X Y : C
a : M
f : ShiftedHom X Y a
F G : C ⥤ D
τ : F ⟶ G
inst✝² : F.CommShift M
inst✝¹ : G.CommShift M
inst✝ : NatTrans.CommShift τ M
⊢ F.map f ≫ (Functor.commShiftIso F a).hom.app Y ≫ (shiftFunctor D a).map (τ.app Y) =
    F.map f ≫ τ.app ((shiftFunctor C a).obj Y) ≫ (Functor.commShiftIso G a).hom.app Y

Tactic:
τ.shift_app_comm a

Goal state after:
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
X Y : C
a : M
f : ShiftedHom X Y a
F G : C ⥤ D
τ : F ⟶ G
inst✝² : F.CommShift M
inst✝¹ : G.CommShift M
inst✝ : NatTrans.CommShift τ M
⊢ F.map f ≫ τ.app ((shiftFunctor C a).obj Y) ≫ (Functor.commShiftIso G a).hom.app Y =
    F.map f ≫ τ.app ((shiftFunctor C a).obj Y) ≫ (Functor.commShiftIso G a).hom.app Y
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case zero
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
⊢ P.extensionProductIter (0 + 1) = (P.extensionProductIter 0).extensionProduct P

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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 Q R : ObjectProperty C
inst✝ : P.Nonempty
⊢ (P.extensionProductIter 0).Nonempty

Tactic:
| zero =>

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

Goal state before:
pp: case zero
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
n n' : ℕ
h : n = n' + 1
⊢ P.extensionProductIter (n + 0) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
m m' : ℕ
h : m = m' + 1
⊢ P.extensionProductIter (0 + m) = (P.extensionProductIter 0).extensionProduct (P.extensionProductIter m')

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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
⊢ P.extensionProductIter 0 ≤ Q.extensionProductIter 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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 Q R : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
⊢ (P.extensionProductIter 0).IsStableUnderShift ℤ

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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
inst✝ : Q.IsTriangulatedClosed₂
h : P ≤ Q
⊢ P.extensionProductIter 0 ≤ Q.isoClosure

Tactic:
| zero =>

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 M K' L' : HomologicalComplex C c
inst✝ : CategoryWithHomology C
X✝ Y✝ Z✝ : HomologicalComplex C c
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
hf : quasiIso C c x✝¹
hg : quasiIso C c x✝
⊢ quasiIso C c (x✝¹ ≫ x✝)

Tactic:
rw [mem_quasiIso_iff] at hf hg ⊢
    infer_instance

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

Goal state before:
pp: case zero
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
⊢ P.retractClosure.extensionProductIter 0 ≤ (P.extensionProductIter 0).retractClosure

Tactic:
| zero =>

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
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

Tactic:
refine Triangle.isoMk _ _ (asIso e) (Iso.refl _) (Iso.refl _) (by simp) (by simp) ?_

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))).mor₃ ≫ (shiftFunctor C 1).map (asIso e).hom =
    (Iso.refl (Triangle.mk (e ≫ f) g (h ≫ (shiftFunctor C 1).map (inv e))).obj₃).hom ≫ (Triangle.mk f g h).mor₃
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 L : HomologicalComplex V c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt ((opFunctor V c).map φ.op) i ↔ QuasiIsoAt φ i

Tactic:
by
  simp only [quasiIsoAt_iff]
  exact ShortComplex.quasiIso_opMap_iff ((shortComplexFunctor V c i).map φ)

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 : 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'
⊢ (K.extendXIso e hi'').hom ≫ K.d i j ≫ (K.extendXIso e hj').inv = f'' ≫ Fork.ι cone ≫ (K.extendXIso e hj').inv

Tactic:
hf'',

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 : 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'
⊢ (K.extendXIso e hi'').hom ≫ K.d i j ≫ (K.extendXIso e hj').inv = (K.extend e).d i' j'
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 : 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
h₁ : f' = 0
⊢ f'' ≫ Fork.ι cone ≫ (K.extendXIso e hj').inv = (0 ≫ Fork.ι cone) ≫ (K.extendXIso e hj').inv

Tactic:
hf'',

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 : 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
h₁ : f' = 0
⊢ (K.extend e).d i' j' = (0 ≫ Fork.ι cone) ≫ (K.extendXIso e hj').inv
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 : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : c.Rel j k
hk'' : e.f k = k'
⊢ (K.extendXIso e hj').hom ≫ K.d j k ≫ (K.extendXIso e hk'').inv = (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f''

Tactic:
hf'',

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 : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : c.Rel j k
hk'' : e.f k = k'
⊢ (K.extendXIso e hj').hom ≫ K.d j k ≫ (K.extendXIso e hk'').inv = (K.extend e).d j' k'
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.restrictionXIso e hi').hom ≫ K.d i' j' ≫ (K.restrictionXIso e hj').inv ≫ (K.restriction e).pOpcycles j =
    (K.restrictionXIso e hi').hom ≫ 0

Tactic:
← restriction_d_eq_assoc,

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
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.restriction e).d i j ≫ (K.restriction e).pOpcycles j = (K.restrictionXIso e hi').hom ≫ 0
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 : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : ¬c.Rel j k
h₁ : f' = 0
⊢ (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ 0

Tactic:
hf'',

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 : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : ¬c.Rel j k
h₁ : f' = 0
⊢ (K.extend e).d j' k' = (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ 0
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 : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ IsZero ((K.extend e).homology j') ↔ IsZero (K.homology j)

Tactic:
exact (K.extendHomologyIso e hj').isZero_iff

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

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i : ι₁ ⊕ ι₂
i₁ : ι₁
h : Sum.inl i₁ = i
⊢ e₁.f i₁ = ac.equiv i

Tactic:
subst h; simp

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

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i : ι₁ ⊕ ι₂
i₂ : ι₂
h : Sum.inr i₂ = i
⊢ e₂.f i₂ = ac.equiv i

Tactic:
subst h; simp

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

Goal state before:
pp: case pos.hf
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ homologyMap (K.ιTruncLE e) (e.f i) ≫ homologyMap (cokernel.π (K.ιTruncLE e)) (e.f i) = 0

Tactic:
rw [← homologyMap_comp, cokernel.condition, homologyMap_zero]

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

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ : ι₁
h : e₁.BoundaryLE i₁
⊢ ∃ i₂, ac.Boundary i₁ i₂

Tactic:
obtain ⟨h₁, h₂⟩ := h
  obtain ⟨i₂, hi₂⟩ := ac.exists_i₂ (c.next (e₁.f i₁))
    (fun i₁' hi₁' => h₂ i₁' (by simpa only [← hi₁'] using! h₁))
  exact ⟨i₂, by simpa only [hi₂] using! h₁⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X X' : C
f : X ⟶ X'
hf : W f
Y : C
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X' Y

Tactic:
by
  simp only [hasSmallLocalizedHom_iff W W.Q]
  exact small_congr (Iso.homCongr (Localization.isoOfHom W.Q W f hf) (Iso.refl _))

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ f =
    Q.map (inv (X.ιTruncLE b) ≫ CochainComplex.truncLEMap g b) ≫
      inv (Q.map (inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b))

Tactic:
simp only [Functor.map_comp, Functor.map_inv, IsIso.inv_comp, IsIso.inv_inv, assoc, fac,
      ← cancel_mono (Q.map s), IsIso.inv_hom_id, comp_id]
    rw [← Functor.map_comp, ← CochainComplex.ιTruncLE_naturality s b,
      Functor.map_comp, IsIso.inv_hom_id_assoc,
      ← Functor.map_comp, CochainComplex.ιTruncLE_naturality g b,
      Functor.map_comp, IsIso.inv_hom_id_assoc]

Goal state after: