mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x y : X.N
⊢ (∃ f,
      (ConcreteCategory.hom (Y.map f.op))
          (mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯).simplex =
        (mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯).simplex) ↔
    ∃ f, (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex

Tactic:
refine exists_congr (fun f ↦ ?_)

Goal state after:
X Y : SSet
e : X ≅ Y
x y : X.N
f :
  ⦋(mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯).dim⦌ ⟶
    ⦋(mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯).dim⦌
⊢ (ConcreteCategory.hom (Y.map f.op))
        (mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯).simplex =
      (mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯).simplex ↔
    (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
d : ℕ
h✝ : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
hf : ∀ (k : SimplexCategoryᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.app k))
⊢ Finite (Y _⦋i⦌)

Tactic:
exact Finite.of_surjective _ (hf _)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: case mp
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
⊢ s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i)) → s.obj i.castSucc = s.obj i.succ

Tactic:
rintro ⟨s, rfl⟩
    simp [-nerve_obj, nerve.σ_obj]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
hab : a ≤ b
⊢ ![a, b] (Fin.castSucc 0) ≤ ![a, b] (Fin.succ 0)

Tactic:
apply Fin.mk_le_mk.mpr hab

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
f : j ⟶ ⦋m⦌
⊢ (fun x ↦
        match x with
        | ⟨x, hx⟩ => Hom.mk { toFun := fun i ↦ e.symm ⟨(Hom.toOrderHom (objEquiv x)) i, ⋯⟩, monotone' := ⋯ })
      ((fun f ↦
          ⟨objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))),
            ⋯⟩)
        f) =
    f

Tactic:
ext i : 3

Goal state after:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
f : j ⟶ ⦋m⦌
i : Fin (j.len + 1)
⊢ (Hom.toOrderHom
        ((fun x ↦
            match x with
            | ⟨x, hx⟩ => Hom.mk { toFun := fun i ↦ e.symm ⟨(Hom.toOrderHom (objEquiv x)) i, ⋯⟩, monotone' := ⋯ })
          ((fun f ↦
              ⟨objMk
                  ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))),
                ⋯⟩)
            f)))
      i =
    (Hom.toOrderHom f) i
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : ↑j.succ ≤ ↑i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j.succ + l = ↑i
⊢ ∃ l, ↑i = ↑j + 1 + l

Tactic:
exact ⟨l, by grind⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case right.refine_1
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
⊢ objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom) ∈ Δ[n].nonDegenerate m

pp: case right.refine_2
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
⊢ (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom), ?right.refine_1⟩ =
    ⟨S, hS⟩

Tactic:
· rw [mem_nonDegenerate_iff_mono, SimplexCategory.mono_iff_injective]
      intro a b h
      grind [e.injective, dsimp% h]

Goal state after:
case right.refine_2
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
⊢ (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom), ⋯⟩ =
    ⟨S, hS⟩
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case zero
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
⊢ (AlternatingFaceMapComplex.ε.app X ≫
          ((AlternatingFaceMapComplex.obj (drop.obj X)).fromSingle₀Equiv (point.obj X)).symm ed.s').f
      0 =
    (((dNext 0) fun i ↦ Pi.single (i + 1) (-ed.s i)) + (prevD 0) fun i ↦ Pi.single (i + 1) (-ed.s i)) +
      (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))).f 0

Tactic:
Homotopy.prevD_chainComplex,

Goal state after:
case zero
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
⊢ (AlternatingFaceMapComplex.ε.app X ≫
          ((AlternatingFaceMapComplex.obj (drop.obj X)).fromSingle₀Equiv (point.obj X)).symm ed.s').f
      0 =
    ((dNext 0) fun i ↦ Pi.single (i + 1) (-ed.s i)) +
        Pi.single (0 + 1) (-ed.s 0) (0 + 1) ≫ (AlternatingFaceMapComplex.obj (drop.obj X)).d (0 + 1) 0 +
      (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))).f 0
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case succ
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
i : ℕ
⊢ (AlternatingFaceMapComplex.ε.app X ≫
          ((AlternatingFaceMapComplex.obj (drop.obj X)).fromSingle₀Equiv (point.obj X)).symm ed.s').f
      (i + 1) =
    (((dNext (i + 1)) fun i ↦ Pi.single (i + 1) (-ed.s i)) + (prevD (i + 1)) fun i ↦ Pi.single (i + 1) (-ed.s i)) +
      (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))).f (i + 1)

Tactic:
Homotopy.prevD_chainComplex,

Goal state after:
case succ
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
i : ℕ
⊢ (AlternatingFaceMapComplex.ε.app X ≫
          ((AlternatingFaceMapComplex.obj (drop.obj X)).fromSingle₀Equiv (point.obj X)).symm ed.s').f
      (i + 1) =
    ((dNext (i + 1)) fun i ↦ Pi.single (i + 1) (-ed.s i)) +
        Pi.single (i + 1 + 1) (-ed.s (i + 1)) (i + 1 + 1) ≫
          (AlternatingFaceMapComplex.obj (drop.obj X)).d (i + 1 + 1) (i + 1) +
      (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))).f (i + 1)
Module: Mathlib.Algebra.Homology.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
i✝¹ : I₁
i✝ : I₂
⊢ (F.obj (K₁.X i✝¹)).map (𝟙 (K₂.X i✝)) = 𝟙 ((F.obj (K₁.X i✝¹)).obj (K₂.X i✝))

Tactic:
Functor.map_id

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
i✝¹ : I₁
i✝ : I₂
⊢ 𝟙 ((F.obj (K₁.X i✝¹)).obj (K₂.X i✝)) = 𝟙 ((F.obj (K₁.X i✝¹)).obj (K₂.X i✝))
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
i j k : A
h : i + j = k
X : t.Category
⊢ (shiftFunctorAdd' t.Category i j k h).hom.app X =
    ↑(t.z i j) •
      (t.shiftIso k).hom.app X ≫
        (shiftFunctorAdd' C i j k h).hom.app X ≫
          (shiftFunctor C j).map ((t.shiftIso i).inv.app X) ≫ (t.shiftIso j).inv.app ((shiftFunctor t.Category i).obj X)

Tactic:
have : (shiftFunctorAdd' t.Category i j k h).hom.app X =
      (t.z i j).val • (shiftFunctorAdd' C i j k h).hom.app X := by
    dsimp [shiftFunctorAdd']
    cat_disch
  rw [this]
  congr
  change _ = 𝟙 _ ≫ _ ≫ (shiftFunctor C j).map (𝟙 _) ≫ 𝟙 _
  simp

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
⊢ biprod.inr ≫ biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ =
    biprod.inr ≫ s.π

Tactic:
simp only [biprod.inr_desc_assoc]

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
⊢ inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = biprod.inr ≫ s.π
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 ⋯).inr ≫ m =
    (PushoutCocone.mk inl inr ⋯).inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯

Tactic:
replace hm := biprod.inr ≫= hm
          dsimp at hm ⊢
          simp only [biprod.inr_desc_assoc] at hm
          rw [hm]
          symm
          apply PushoutCocone.IsColimit.inr_desc h

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₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit sq.cokernelCofork
s : PushoutCocone f g
⊢ biprod.lift f (-g) ≫ biprod.desc s.inl s.inr = 0

Tactic:
by simp [s.condition]

Goal state after:
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 ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
⊢ (fun h ↦ homotopyOp h) ((fun h ↦ homotopyUnop h) h) = h

Tactic:
by
    ext p q
    simp [homotopyOp_hom_eq _ p q (-p) (-q),
      homotopyUnop_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₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit sq.cokernelCofork
s : PushoutCocone f g
m : X₄ ⟶ s.pt
hm₁ : inl ≫ m = s.inl
hm₂ : inr ≫ m = s.inr
⊢ biprod.lift f (-g) ≫ biprod.desc s.inl s.inr = 0

Tactic:
by simp [s.condition]

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 sq.kernelFork
s : PullbackCone f g
⊢ biprod.lift s.fst s.snd ≫ biprod.desc f (-g) = 0

Tactic:
by simp [s.condition]

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 sq.kernelFork
s : PullbackCone f g
m : s.pt ⟶ X₁
hm₁ : m ≫ fst = s.fst
hm₂ : m ≫ snd = s.snd
⊢ biprod.lift s.fst s.snd ≫ biprod.desc f (-g) = 0

Tactic:
by simp [s.condition]

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

Goal state before:
pp: case pos.h
C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²² : Category.{v_1, u_1} C₁
inst✝²¹ : Category.{v_2, u_2} C₂
inst✝²⁰ : Category.{v_3, u_5} C₃
inst✝¹⁹ : Category.{v_4, u_6} C₄
inst✝¹⁸ : Category.{v_6, u_4} C₂₃
inst✝¹⁷ : HasZeroMorphisms C₁
inst✝¹⁶ : HasZeroMorphisms C₂
inst✝¹⁵ : HasZeroMorphisms C₃
inst✝¹⁴ : Preadditive C₂₃
inst✝¹³ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹² : G₂₃.PreservesZeroMorphisms
inst✝¹¹ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁰ : F.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁸ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁷ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁶ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁵ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁴ : TotalComplexShape c₁ c₂₃ c₄
inst✝³ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝² : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝¹ : DecidableEq ι₂₃
inst✝ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : c₁.Rel i₁ (c₁.next i₁)
h₂ : c₁.π c₂₃ c₄ (c₁.next i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = j'
⊢ c₁.r c₂ c₃ c₁₂ c₄ (c₁.next i₁, i₂, i₃) = j'

Tactic:
rw [← h₂, ← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄]

Goal state after:
case pos.h
C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²² : Category.{v_1, u_1} C₁
inst✝²¹ : Category.{v_2, u_2} C₂
inst✝²⁰ : Category.{v_3, u_5} C₃
inst✝¹⁹ : Category.{v_4, u_6} C₄
inst✝¹⁸ : Category.{v_6, u_4} C₂₃
inst✝¹⁷ : HasZeroMorphisms C₁
inst✝¹⁶ : HasZeroMorphisms C₂
inst✝¹⁵ : HasZeroMorphisms C₃
inst✝¹⁴ : Preadditive C₂₃
inst✝¹³ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹² : G₂₃.PreservesZeroMorphisms
inst✝¹¹ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁰ : F.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁸ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁷ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁶ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁵ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁴ : TotalComplexShape c₁ c₂₃ c₄
inst✝³ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝² : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝¹ : DecidableEq ι₂₃
inst✝ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : c₁.Rel i₁ (c₁.next i₁)
h₂ : c₁.π c₂₃ c₄ (c₁.next i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = j'
⊢ c₁.r c₂ c₃ c₁₂ c₄ (c₁.next i₁, i₂, i₃) = c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (c₁.next i₁, i₂), i₃)
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
⊢ ⋯.lift ≫ g = v ≫ t

Tactic:
rw [CommSq.fac_right]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
⊢ ∃ α, δ m n α = ↑z

Tactic:
obtain ⟨φ, hφ⟩ := (Cocycle.equivHom ..).surjective (z.rightShift n 0 (zero_add n))

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
hφ : (Cocycle.equivHom K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)) φ = z.rightShift n 0 ⋯
⊢ ∃ α, δ m n α = ↑z
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
X✝ Y✝ Z✝ : C
i : X✝ ⟶ Y✝
j : Y✝ ⟶ Z✝
hi : T.llp i
hj : T.llp j
x✝¹ x✝ : C
p : x✝¹ ⟶ x✝
hp : T p
⊢ HasLiftingProperty (i ≫ j) p

Tactic:
have := hi _ hp
    have := hj _ hp
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
X✝ Y✝ Z✝ : C
i : X✝ ⟶ Y✝
j : Y✝ ⟶ Z✝
hi : T.rlp i
hj : T.rlp j
x✝¹ x✝ : C
p : x✝¹ ⟶ x✝
hp : T p
⊢ HasLiftingProperty p (i ≫ j)

Tactic:
have := hi _ hp
    have := hj _ hp
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithCofibrations C
inst✝ : Cofibration f
⊢ Fibration f.op

Tactic:
fibration_op_iff

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithCofibrations C
inst✝ : Cofibration f
⊢ Cofibration f
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : (cofibrations C).IsStableUnderRetracts
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (trivialCofibrations C).IsStableUnderRetracts

Tactic:
by
  dsimp [trivialCofibrations]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
A : C
inst✝⁷ : CategoryWithWeakEquivalences C
P : PathObject A
inst✝⁶ : HasBinaryProduct A A
inst✝⁵ : CategoryWithFibrations C
inst✝⁴ : HasTerminal C
inst✝³ : (fibrations C).IsStableUnderComposition
inst✝² : (fibrations C).IsStableUnderBaseChange
inst✝¹ : IsFibrant A
inst✝ : P.IsGood
⊢ Fibration P.p₁

Tactic:
by
  rw [← P.p_snd]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
P : Cylinder X
f g : X ⟶ Y
h : P.LeftHomotopy f g
⊢ ∃ P', P'.IsGood ∧ Nonempty (P'.LeftHomotopy f g)

Tactic:
by
  let d := MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.i
  exact
   ⟨{ I := d.Z
      i₀ := coprod.inl ≫ d.i
      i₁ := coprod.inr ≫ d.i
      π := d.p ≫ P.π }, ⟨by
        rw [cofibration_iff]
        convert! d.hi
        aesop⟩, ⟨{ h := d.p ≫ h.h }⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
⊢ Injective I → (MorphismProperty.monomorphisms C).rlp 0

pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
⊢ (MorphismProperty.monomorphisms C).rlp 0 → Injective I

Tactic:
· intro _ A B i (_ : Mono i)
    exact Injective.hasLiftingProperty_of_isZero i 0 hZ

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
⊢ (MorphismProperty.monomorphisms C).rlp 0 → Injective I
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
this✝³ : Preadditive D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
this✝² : Preadditive D₂ := Localization.preadditive L₂ B.trW
this✝¹ : L₁.Additive
this✝ : L₂.Additive
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
X₁ X₂ : A.FullSubcategory
f : X₁ ⟶ X₂
X₃ : C
s : X₂.obj ⟶ X₃
hs : B.trW s
fac : f.hom ≫ s = 0 ≫ s
X₄ : C
t : X₂.obj ⟶ X₄
a : X₃ ⟶ X₄
hX₄ : A X₄
ht : (A ⊓ B).trW t
fac' : s ≫ a = t
t' : X₂ ⟶ { obj := X₄, property := hX₄ } := homMk t
this : IsIso (L₁.map t')
⊢ L₁.map f = 0

Tactic:
rw [← cancel_mono (L₁.map t'), zero_comp, ← L₁.map_comp, ← L₁.map_zero]

Goal state after:
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
this✝³ : Preadditive D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
this✝² : Preadditive D₂ := Localization.preadditive L₂ B.trW
this✝¹ : L₁.Additive
this✝ : L₂.Additive
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
X₁ X₂ : A.FullSubcategory
f : X₁ ⟶ X₂
X₃ : C
s : X₂.obj ⟶ X₃
hs : B.trW s
fac : f.hom ≫ s = 0 ≫ s
X₄ : C
t : X₂.obj ⟶ X₄
a : X₃ ⟶ X₄
hX₄ : A X₄
ht : (A ⊓ B).trW t
fac' : s ≫ a = t
t' : X₂ ⟶ { obj := X₄, property := hX₄ } := homMk t
this : IsIso (L₁.map t')
⊢ L₁.map (f ≫ t') = L₁.map 0
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
h : t.IsGE X n
e : (contractibleTriangle X).invRotate ≅ (t.triangleLTGE n).obj X
he : e.hom.hom₂ = 𝟙 X
⊢ (t.truncGEπ n).app X = e.hom.hom₃

Tactic:
have := e.hom.comm₂

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
h : t.IsGE X n
e : (contractibleTriangle X).invRotate ≅ (t.triangleLTGE n).obj X
he : e.hom.hom₂ = 𝟙 X
this : (contractibleTriangle X).invRotate.mor₂ ≫ e.hom.hom₃ = e.hom.hom₂ ≫ ((t.triangleLTGE n).obj X).mor₂
⊢ (t.truncGEπ n).app X = e.hom.hom₃
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₁ i : ℤ
hn₁ : i + 1 = n₁
hi : i ≤ i
⊢ QuasiIsoAt (π K L n₁) i

Tactic:
rw [quasiIsoAt_iff_isIso_homologyMap]

Goal state after:
case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₁ i : ℤ
hn₁ : i + 1 = n₁
hi : i ≤ i
⊢ IsIso (homologyMap (π K L n₁) i)