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

Goal state before:
pp: case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
by_cases h₃ : c₁.Rel i₁ (c₁.next i₁)

Goal state after:
case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = -K.d₁ c₁₂ i₁ i₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂''

Tactic:
by_cases h₃ : c₁.Rel i₁ (c₁.next i₁)

Goal state after:
case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = -K.d₁ c₁₂ i₁ i₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂''

case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = -K.d₁ c₁₂ i₁ i₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂''
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: case pos.h
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₃ : c₁.Rel (c₁.prev i₁) i₁
h₄ : c₁.π c₂ c (c₁.prev i₁, i₂) = j'
⊢ False

Tactic:
apply h

Goal state after:
case pos.h
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₃ : c₁.Rel (c₁.prev i₁) i₁
h₄ : c₁.π c₂ c (c₁.prev i₁, i₂) = j'
⊢ c.Rel j' j
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ (f ≫ biprod.inl - g ≫ biprod.inr) ≫ s.π = 0

Tactic:
convert! s.condition <;> cat_disch

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

Goal state before:
pp: case h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
m : sq.cokernelCofork.pt ⟶ s.pt
hm : Cofork.π sq.cokernelCofork ≫ m = s.π
⊢ (PushoutCocone.mk inl inr ⋯).inl ≫ m =
    (PushoutCocone.mk inl inr ⋯).inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯

pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
m : sq.cokernelCofork.pt ⟶ s.pt
hm : Cofork.π sq.cokernelCofork ≫ m = s.π
⊢ (PushoutCocone.mk inl inr ⋯).inr ≫ m =
    (PushoutCocone.mk inl inr ⋯).inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯

Tactic:
· replace hm := biprod.inl ≫= hm
          dsimp at hm ⊢
          simp only [biprod.inl_desc_assoc] at hm
          rw [hm]
          symm
          apply PushoutCocone.IsColimit.inl_desc h

Goal state after:
case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
m : sq.cokernelCofork.pt ⟶ s.pt
hm : Cofork.π sq.cokernelCofork ≫ m = s.π
⊢ (PushoutCocone.mk inl inr ⋯).inr ≫ m =
    (PushoutCocone.mk inl inr ⋯).inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy f g
p q : ℤ
⊢ ((fun h ↦ homotopyUnop h) ((fun h ↦ homotopyOp h) h)).hom p q = h.hom p q

Tactic:
simp [homotopyUnop_hom_eq _ p q (-p) (-q),
      homotopyOp_hom_eq _ (-q) (-p) q p]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (biprod.desc f (-g)) 0
⊢ s.ι ≫ (biprod.fst ≫ f - biprod.snd ≫ g) = 0

Tactic:
convert! s.condition <;> cat_disch

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

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✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i' j' : ι'
hij' : ¬c'.Rel j' i'
hi' : ∃ i, e.f i = i'
⊢ extend.hom e h.hom i' j' = 0

Tactic:
obtain ⟨i, rfl⟩ := hi'

Goal state after:
case pos
ι : 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✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
j' : ι'
i : ι
hij' : ¬c'.Rel j' (e.f i)
⊢ extend.hom e h.hom (e.f i) j' = 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: case neg
ι : 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✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i' j' : ι'
hij' : ¬c'.Rel j' i'
hi' : ¬∃ i, e.f i = i'
⊢ extend.hom e h.hom i' j' = 0

Tactic:
· exact extend.hom_eq_zero₁ _ _ _ _ (by tauto)

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

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✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap f e).f i' = (dNext i') (extend.hom e h.hom) + (prevD i') (extend.hom e h.hom) + (extendMap g e).f i'

Tactic:
obtain ⟨i, rfl⟩ := hi'

Goal state after:
case pos
ι : 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✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (extendMap f e).f (e.f i) =
    (dNext (e.f i)) (extend.hom e h.hom) + (prevD (e.f i)) (extend.hom e h.hom) + (extendMap g e).f (e.f i)
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

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✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i j : ι
hij : ¬c.Rel j i
⊢ (K.extendXIso e ⋯).inv ≫ h.hom (e.f i) (e.f j) ≫ (L.extendXIso e ⋯).hom = 0

Tactic:
h.zero _ _ (by rwa [e.rel_iff]),

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✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i j : ι
hij : ¬c.Rel j i
⊢ (K.extendXIso e ⋯).inv ≫ 0 ≫ (L.extendXIso e ⋯).hom = 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

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✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i' j' : ι'
hi' : ∃ i, e.f i = i'
⊢ (h.ofExtend.extend e).hom i' j' = h.hom i' j'

Tactic:
obtain ⟨i, rfl⟩ := hi'

Goal state after:
case pos
ι : 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✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
j' : ι'
i : ι
⊢ (h.ofExtend.extend e).hom (e.f i) j' = h.hom (e.f i) j'
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
⊢ (s ≫ u) ≫ g' = f ≫ t ≫ v

Tactic:
rw [← Category.assoc, ← h.w, Category.assoc, Category.assoc, sq.w]

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ s ≫ u = f ≫ ⋯.lift

Tactic:
CommSq.fac_left

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ s ≫ u = s ≫ u
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ sq.HasLift

Tactic:
exact ⟨h.desc u (CommSq.mk w).lift (by rw [CommSq.fac_left]), h.inl_desc ..,
      h.hom_ext (by rw [h.inl_desc_assoc, sq.w]) (by rw [h.inr_desc_assoc, CommSq.fac_right])⟩

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ f' ≫ ⋯.lift = u ≫ s

Tactic:
CommSq.fac_left

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ u ≫ s = u ≫ s
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f₀ f₁ f₂ : X ⟶ Y
inst✝ : IsFibrant Y
h'✝ : RightHomotopyRel f₁ f₂
P : PathObject Y
h : P.RightHomotopy f₀ f₁
P' : PathObject Y
left✝ : P'.IsGood
h' : P'.RightHomotopy f₁ f₂
⊢ RightHomotopyRel f₀ f₂

Tactic:
exact (h.trans h').rightHomotopyRel

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
L : CochainComplex C ℤ
h : CochainComplex.plus C L
hL : (quotient C (ComplexShape.up ℤ)).obj L = (quotient C (ComplexShape.up ℤ)).obj L
⊢ CochainComplex.plus C L

Tactic:
exact h

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

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✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
n : ℤ
X : C
⊢ plus C ((singleFunctor C n).obj X)

Tactic:
← quotient_obj_singleFunctors_obj,

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✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
n : ℤ
X : C
⊢ plus C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj ((CochainComplex.singleFunctor C n).obj X))
Module: Mathlib.Algebra.Homology.DerivedCategory.Plus

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K : CochainComplex C ℤ
hK : HomologicalComplex.Acyclic K
L : CochainComplex C ℤ
n : ℤ
hn : L.IsStrictlyGE n
φ : K ⟶ L
⊢ HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj (K.truncGE n))

Tactic:
rw [HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic]

Goal state after:
case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K : CochainComplex C ℤ
hK : HomologicalComplex.Acyclic K
L : CochainComplex C ℤ
n : ℤ
hn : L.IsStrictlyGE n
φ : K ⟶ L
⊢ HomologicalComplex.Acyclic (K.truncGE n)
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
this : L₁.EssSurj
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
X₁ X₂ : A.FullSubcategory
φ : F.obj (L₁.obj X₁) ⟶ F.obj (L₁.obj X₂)
⊢ φ = e.inv.app X₁ ≫ (e.hom.app X₁ ≫ φ ≫ e.inv.app X₂) ≫ e.hom.app X₂

Tactic:
simp [dsimp% e.inv_hom_id_app_assoc, dsimp% e.inv_hom_id_app]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ : ℤ
X : C
x✝ : t.IsLE X n₀
e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X
he : e.hom.hom₂ = (Iso.refl X).hom
⊢ e.inv.hom₂ = 𝟙 X

Tactic:
← cancel_mono e.hom.hom₂,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ : ℤ
X : C
x✝ : t.IsLE X n₀
e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X
he : e.hom.hom₂ = (Iso.refl X).hom
⊢ e.inv.hom₂ ≫ e.hom.hom₂ = 𝟙 X ≫ e.hom.hom₂
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
X Y : C
p : X ⟶ Y
hp :
  ∃ I,
    ∃ (_ : Injective I),
      ∃ f, ∃ (w : f ≫ p = 0), Nonempty { X₁ := I, X₂ := X, X₃ := Y, f := f, g := p, zero := w }.Splitting
A B : C
i : A ⟶ B
inst✝ : Mono i
⊢ (MorphismProperty.monomorphisms C).rlp p

Tactic:
obtain ⟨I, _, s, hs, ⟨σ⟩⟩ := hp

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
X Y : C
p : X ⟶ Y
A B : C
i : A ⟶ B
inst✝ : Mono i
I : C
w✝ : Injective I
s : I ⟶ X
hs : s ≫ p = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs }.Splitting
⊢ (MorphismProperty.monomorphisms C).rlp p
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ (t.truncLT a).map ((t.truncLTι b).app X) ≫ (t.natTransTruncLTOfLE a b h).app X =
    (t.truncLTι a).app ((t.truncLT b).obj X)

Tactic:
exact t.to_truncLT_obj_ext (by simp)

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
W : MorphismProperty C
homRel : HomRel C
inst✝² : HomRel.IsStableUnderPrecomp homRel
inst✝¹ : HomRel.IsStableUnderPostcomp homRel
inst✝ : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
x✝ : W.quotient homRel ((Quotient.functor homRel).map f)
f' : ((Quotient.functor homRel).1 X).as ⟶ ((Quotient.functor homRel).1 Y).as
hf' : W f'
h : Relation.EqvGen homRel f f'
⊢ W f

Tactic:
HasQuotient.iff_of_eqvGen W h

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
W : MorphismProperty C
homRel : HomRel C
inst✝² : HomRel.IsStableUnderPrecomp homRel
inst✝¹ : HomRel.IsStableUnderPostcomp homRel
inst✝ : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
x✝ : W.quotient homRel ((Quotient.functor homRel).map f)
f' : ((Quotient.functor homRel).1 X).as ⟶ ((Quotient.functor homRel).1 Y).as
hf' : W f'
h : Relation.EqvGen homRel f f'
⊢ W f'
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsFibrant Z
f : X ⟶ Y
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h✝ : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
P : PathObject Z
left✝ : P.IsGood
h : P.RightHomotopy (f ≫ f₀) (f ≫ f₁)
sq : CommSq h.h f P.p (prod.lift f₀ f₁)
this : (sq.lift ≫ P.p) ≫ prod.fst = prod.lift f₀ f₁ ≫ prod.fst
⊢ sq.lift ≫ P.p₀ = f₀

Tactic:
rwa [Category.assoc, P.p_fst, prod.lift_fst] at this

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ (homRel C).FactorsThroughLocalization (weakEquivalences (FibrantObject C))

Tactic:
rintro X Y f g h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : FibrantObject C
f g : X ⟶ Y
h : homRel C f g
⊢ AreEqualizedByLocalization (weakEquivalences (FibrantObject C)) f g
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
x✝¹ x✝ : FibrantObject C
f : x✝¹ ⟶ x✝
⊢ f ≫ { hom := iResolutionObj (ι.obj x✝) } = { hom := iResolutionObj (ι.obj x✝¹) } ≫ homMk (resolutionMap (ι.map f))

Tactic:
ext : 1

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
x✝¹ x✝ : FibrantObject C
f : x✝¹ ⟶ x✝
⊢ (f ≫ { hom := iResolutionObj (ι.obj x✝) }).hom =
    ({ hom := iResolutionObj (ι.obj x✝¹) } ≫ homMk (resolutionMap (ι.map f))).hom
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : Mono f
T : ShortComplex C :=
  { X₁ := homology K n, X₂ := homology L n, X₃ := homology (cokernel f) n, f := homologyMap f n,
    g := homologyMap (cokernel.π f) n, zero := ⋯ }
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ Mono (homologyMap ((cokernel f).πTruncGE n) n ≫ homologyMap (p f n) n) ∧ IsIso (𝟙 T.X₂) ∧ Epi (𝟙 T.X₁)

Tactic:
exact ⟨inferInstance, inferInstance, inferInstance⟩

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
inst✝⁴ : Category.{v_3, u_3} D₁
inst✝³ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝² : R.functor.EssSurj
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : T.HasLeftResolutions
⊢ B.HasLeftResolutions

Tactic:
by
  intro Y₂
  obtain ⟨X₂, ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := R.functor) Y₂
  let ρ : T.LeftResolution X₂ := Classical.arbitrary _
  exact ⟨{
    X₁ := L.functor.obj ρ.X₁
    w := iso.inv.app _ ≫ R.functor.map ρ.w ≫ e.hom
    hw := (W₂'.arrow_mk_iso_iff (Arrow.isoMk (iso.app _) e)).1 (R.map _ ρ.hw) }⟩

Goal state after: