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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
⊢ ∀ ⦃X_1 Y : SimplexCategory⦄ (f : X_1 ⟶ Y),
    F.augmentedCechConerve.right.map f ≫
        WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app Y) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const Y i)) ⋯ =
      WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app X_1) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const X_1 i))
          ⋯ ≫
        X.right.map f

Tactic:
intro x y f
        dsimp
        ext
        · simp only [WidePushout.ι_desc_assoc, WidePushout.ι_desc]
          rw [Category.assoc, ← X.right.map_comp]
          rfl
        · simp [← NatTrans.naturality]

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

Goal state before:
pp: X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ IsIso (f.app X✝)

Tactic:
isIso_iff_bijective

Goal state after:
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Function.Bijective ⇑(ConcreteCategory.hom (f.app X✝))
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
z : ↑(X.nonDegenerate m)
hy : { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.toN = y
⊢ y = N.mk ↑z ⋯

Tactic:
rw [toN_eq_iff] at hy

Goal state after:
X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
z : ↑(X.nonDegenerate m)
hy : y.subcomplex = { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.subcomplex
⊢ y = N.mk ↑z ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
z : ↑(X.nonDegenerate m)
hy : { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.toN = y
⊢ y = N.mk ↑z ⋯

Tactic:
rw [toN_eq_iff] at hy
    rw [← N.subcomplex_injective_iff, hy]
    exact subcomplex_eq_of_epi _ _ f rfl

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

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2 ≫ σ₂ 1 _proof_2 Edge._proof_2).op)) e.edge = (id y).edge

Tactic:
δ₂_zero_comp_σ₂_one

Goal state after:
X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom
        (X.map
          (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4 ≫
              δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3).op))
      e.edge =
    (id y).edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : Category.{v, u} D
x y : C
f : x ⟶ y
F : C ⥤ D
⊢ homEquiv ((edgeMk f).map (nerveMap F)) = F.map f

Tactic:
by
  simp [homEquiv, nerveMap_app]

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c✝ : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
x✝² x✝¹ x✝ : I
⊢ c.ε x✝² * 1 = 1 * c.ε x✝²

Tactic:
rw [one_mul, mul_one]

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

Goal state before:
pp: case neg
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : ¬c.Rel j j'
⊢ (K.totalFlipIsoX c j).hom ≫ K.D₁ c j j' = K.flip.D₂ c j j' ≫ (K.totalFlipIsoX c j').hom

Tactic:
· rw [K.D₁_shape _ _ _ h₀, K.flip.D₂_shape c _ _ h₀, zero_comp, comp_zero]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : P.leftOrthogonal T.obj₁
h₃ : P.leftOrthogonal T.obj₃
Y : C
f : T.obj₂ ⟶ Y
hY : P Y
⊢ f = 0

Tactic:
obtain ⟨g, rfl⟩ := Pretriangulated.Triangle.yoneda_exact₂ T hT f (h₁ _ hY)
    simp [h₃ g hY]

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
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i : ι
this :
  (K.extendXIso e ⋯).hom ≫ f.f i ≫ (L.extendXIso e ⋯).inv =
    (dNext (e.f i)) h.hom + (prevD (e.f i)) h.hom + (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv
hi : ¬c.Rel i (c.next i)
hi' : c'.Rel (e.f i) (c'.next (e.f i))
⊢ (dNext (e.f i)) h.hom = (K.extendXIso e ⋯).hom ≫ 0 ≫ (L.extendXIso e ⋯).inv

Tactic:
simp [dNext_eq _ hi', extend_d_from_eq_zero _ _ _ _ _ rfl hi]

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

Goal state before:
pp: case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst✝ : Injective (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
p : ℤ
hp✝ : p ≤ n + 1
hpq : p + 0 = p
hp : p < n + 1
⊢ (δ (-1) 0 (α + Cochain.single β (-1))).v p p hpq = (Cochain.ofHom f).v p p hpq

Tactic:
rw [δ_add, Cochain.add_v, hα p p (by lia) (by lia), add_eq_left,
      δ_v (-1) 0 (neg_add_cancel 1) _ p p hpq (p - 1) (p + 1) rfl rfl,
      Cochain.single_v_eq_zero _ _ _ _ _ (by lia),
      Cochain.single_v_eq_zero _ _ _ _ _ (by lia)]
    simp

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

Goal state before:
pp: case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst✝ : Injective (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
hp : n + 1 ≤ n + 1
hpq : n + 1 + 0 = n + 1
⊢ (δ (-1) 0 (α + Cochain.single β (-1))).v (n + 1) (n + 1) hpq = (Cochain.ofHom f).v (n + 1) (n + 1) hpq

Tactic:
δ_v (-1) 0 (neg_add_cancel 1) _ (n + 1) (n + 1) (by lia) n (n + 2)
      (by lia) (by lia),

Goal state after:
case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst✝ : Injective (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
hp : n + 1 ≤ n + 1
hpq : n + 1 + 0 = n + 1
⊢ (α + Cochain.single β (-1)).v (n + 1) n ⋯ ≫ L.d n (n + 1) +
      Int.negOnePow 0 • K.d (n + 1) (n + 2) ≫ (α + Cochain.single β (-1)).v (n + 2) (n + 1) ⋯ =
    (Cochain.ofHom f).v (n + 1) (n + 1) hpq
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 : ι
⊢ f.f i =
    (((dNext i) fun i j ↦ (K.extendXIso e ⋯).inv ≫ h.hom (e.f i) (e.f j) ≫ (L.extendXIso e ⋯).hom) +
        (prevD i) fun i j ↦ (K.extendXIso e ⋯).inv ≫ h.hom (e.f i) (e.f j) ≫ (L.extendXIso e ⋯).hom) +
      g.f i

Tactic:
have := h.comm (e.f i)
    simp only [extendMap_f _ _ rfl] at this
    simp only [← cancel_mono (L.extendXIso e rfl).inv,
      ← cancel_epi (K.extendXIso e rfl).hom, this, Preadditive.add_comp,
      Preadditive.comp_add, add_left_inj]
    congr 1
    · by_cases hi : c.Rel i (c.next i)
      · have hi' : c'.Rel (e.f i) (e.f (c.next i)) := by rwa [e.rel_iff]
        simp [dNext_eq _ hi, dNext_eq _ hi', K.extend_d_eq _ rfl rfl]
      · rw [dNext_eq_zero _ _ hi]
        by_cases hi' : c'.Rel (e.f i) (c'.next (e.f i))
        · simp [dNext_eq _ hi', extend_d_from_eq_zero _ _ _ _ _ rfl hi]
        · simp [dNext_eq_zero _ _ hi']
    · by_cases hi : c.Rel (c.prev i) i
      · have hi' : c'.Rel (e.f (c.prev i)) (e.f i) := by rwa [e.rel_iff]
        simp [prevD_eq _ hi, prevD_eq _ hi', L.extend_d_eq _ rfl rfl]
      · rw [prevD_eq_zero _ _ hi]
        by_cases hi' : c'.Rel (c'.prev (e.f i)) (e.f i)
        · simp [prevD_eq _ hi', extend_d_to_eq_zero _ _ _ _ _ rfl hi]
        · simp [prevD_eq_zero _ _ hi']

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : CategoryWithCofibrations C
inst✝¹ : HasInitial C
inst✝ : (cofibrations C).RespectsIso
A X : C
i : A ⟶ X
hA : IsInitial A
⊢ Arrow.mk (initial.to X) ≅ Arrow.mk i

Tactic:
exact Arrow.isoMk (IsInitial.uniqueUpToIso initialIsInitial hA) (Iso.refl _)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h✝¹ : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject Y
left✝ : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject Z
h✝ : Q.IsVeryGood
⊢ RightHomotopyRel (f ≫ p) (g ≫ p)

Tactic:
(Tactic.tacticHave__
 "have"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId `sq)
   []
   [(Term.typeSpec
     ":"
     (Term.app
      `CommSq
      [(Term.paren (Term.hygienicLParen "(" (hygieneInfo `[anonymous])) (CategoryTheory.«term_≫_» `p "≫" `Q.ι) ")")
       `P.ι
       `Q.p
       (Term.paren
        (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
        (Term.app
         `prod.lift
         [(Term.paren (Term.hygienicLParen "(" (hygieneInfo `[anonymous])) (CategoryTheory.«term_≫_» `P.p₀ "≫" `p) ")")
          (Term.paren
           (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
           (CategoryTheory.«term_≫_» `P.p₁ "≫" `p)
           ")")])
        ")")]))]
   ":="
   (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))))

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h✝¹ : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject Y
left✝ : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject Z
h✝ : Q.IsVeryGood
sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
⊢ RightHomotopyRel (f ≫ p) (g ≫ p)
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
K L : CochainComplex.Plus C
f₁ : K ⟶ L
f₀ : K.obj ⟶ L.obj
hf : (quotient C).map (ObjectProperty.homMk f₀) = (quotient C).map f₁
⊢ ∃ P x, (homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C) P.π

Tactic:
obtain ⟨f₁, rfl⟩ := ObjectProperty.homMk_surjective f₁

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
K L : CochainComplex.Plus C
f₀ f₁ : K.obj ⟶ L.obj
hf : (quotient C).map (ObjectProperty.homMk f₀) = (quotient C).map (ObjectProperty.homMk f₁)
⊢ ∃ P x, (homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C) P.π
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₂ :
  ((shiftFunctor C 1).map (w₂₃.unop ≫ o.m₁)).op =
    ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map u₁₂).unop ≫ (shiftFunctor C 1).map w₁₃.unop).op
⊢ w₁₃ ≫ (shiftFunctor Cᵒᵖ 1).map u₁₂ = o.m₁.op ≫ w₂₃

Tactic:
← Functor.map_comp

Goal state after:
case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₂ :
  ((shiftFunctor C 1).map (w₂₃.unop ≫ o.m₁)).op =
    ((shiftFunctor C 1).map (((shiftFunctor Cᵒᵖ 1).map u₁₂).unop ≫ w₁₃.unop)).op
⊢ w₁₃ ≫ (shiftFunctor Cᵒᵖ 1).map u₁₂ = o.m₁.op ≫ w₂₃
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case h₃
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
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
g : (shiftFunctor C 1).obj T.obj₁ ⟶ T'.obj₃
hg : f.hom₃ = T.mor₃ ≫ g
⊢ f.hom₃ = TriangleMorphism.hom₃ 0

Tactic:
simp [hg, t.zero_of_isLE_of_isGE g (a - 1) b (by lia)
      (t.isLE_shift _ a 1 (a - 1)) inferInstance]

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₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ t.IsLE X n₀ ↔ ∀ (Y : C) (f : X ⟶ Y), t.IsGE Y n₁ → f = 0

Tactic:
refine ⟨fun _ Y f _ ↦ t.zero f n₀ n₁ (by lia), fun hX ↦ ?_⟩
  rw [t.isLE_iff_isZero_truncGE_obj n₀ n₁ h, IsZero.iff_id_eq_zero]
  exact t.from_truncGE_obj_ext (by simpa using hX _ _ 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
H : Type u_5
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₂
inst✝¹ : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
Φ : LocalizerMorphism W₁ W₂
inst✝ : Φ.HasLeftResolutions
⊢ Φ.op.HasRightResolutions

Tactic:
← hasLeftResolutions_iff_op

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
H : Type u_5
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₂
inst✝¹ : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
Φ : LocalizerMorphism W₁ W₂
inst✝ : Φ.HasLeftResolutions
⊢ Φ.HasLeftResolutions
Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
⊢ weakEquivalences C (HoCat.iResolutionObj X)

Tactic:
by simpa using mem_weakEquivalences (HoCat.iResolutionObj X)

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} D
inst✝¹ : Category.{v_5, u_2} H
RF RF' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝ : L.IsLocalization W
e : RF ≅ RF'
comm : α ≫ L.whiskerLeft e.hom = α'
⊢ RF.IsLeftKanExtension α ↔ RF'.IsLeftKanExtension α'

Tactic:
exact isLeftKanExtension_iff_of_iso e _ _ comm

Goal state after:
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 : CochainComplex C ℤ
inst✝¹ : EnoughInjectives C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
inst✝ : K.IsStrictlyGE n₁
⊢ ∃ L i, ∃ (_ : Mono i) (_ : QuasiIso i) (_ : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n₀

Tactic:
by
  have : K.IsStrictlyGE (n₀ + 1) := by rw [h]; infer_instance
  obtain ⟨L, hL, i, p, hi, hi', hp, _⟩ := cm5a (0 : K ⟶ 0) n₀
  exact ⟨L, i, hi, hi', (degreewiseEpiWithInjectiveKernel_iff_of_isZero p
    (Limits.isZero_zero _)).1 hp, hL⟩

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

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
Y : C
P : CostructuredArrow L (L.obj Y) → Prop
hP₀ : P (CostructuredArrow.mk (𝟙 (L.obj Y)))
hP₁ :
  ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk (L.map f ≫ φ))
hP₂ :
  ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk ((isoOfHom L W w hw).inv ≫ φ))
g : CostructuredArrow L (L.obj Y)
⊢ P g

Tactic:
by
  let g' := StructuredArrow.mk (T := L.op) (Y := op g.left) g.hom.op
  change P (CostructuredArrow.mk g'.hom.unop)
  induction g' using induction_structuredArrow L.op W.op with
  | hP₀ => exact hP₀
  | hP₁ f φ hφ => exact hP₁ f.unop φ.unop hφ
  | hP₂ w hw φ hφ => simpa [isoOfHom_op_inv L W w hw] using! hP₂ w.unop hw φ.unop hφ

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

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 D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁷ : W₂'.RespectsIso
inst✝⁶ : L.IsLocalizedEquivalence
inst✝⁵ : R.IsLocalizedEquivalence
inst✝⁴ : R.functor.EssSurj
inst✝³ : L.functor.EssSurj
inst✝² : R.functor.Full
inst✝¹ : R.IsInduced
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
x✝ : B.IsLeftDerivabilityStructure
X₂ : C₂
ρ : B.LeftResolution (R.functor.obj X₂) := Classical.arbitrary (B.LeftResolution (R.functor.obj X₂))
⊢ W₂
    (R.functor.preimage
      (iso.hom.app (L.functor.objPreimage ρ.X₁) ≫ B.functor.map (L.functor.objObjPreimageIso ρ.X₁).hom ≫ ρ.w))

Tactic:
simp only [← R.inverseImage_eq, Functor.comp_obj,
          MorphismProperty.inverseImage_iff, Functor.map_preimage]

Goal state after:
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 D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁷ : W₂'.RespectsIso
inst✝⁶ : L.IsLocalizedEquivalence
inst✝⁵ : R.IsLocalizedEquivalence
inst✝⁴ : R.functor.EssSurj
inst✝³ : L.functor.EssSurj
inst✝² : R.functor.Full
inst✝¹ : R.IsInduced
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
x✝ : B.IsLeftDerivabilityStructure
X₂ : C₂
ρ : B.LeftResolution (R.functor.obj X₂) := Classical.arbitrary (B.LeftResolution (R.functor.obj X₂))
⊢ W₂' (iso.hom.app (L.functor.objPreimage ρ.X₁) ≫ B.functor.map (L.functor.objObjPreimageIso ρ.X₁).hom ≫ ρ.w)
Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_4, u_4} D₁
inst✝ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
T' : C₁ ⥤ D₁
B' : C₂ ⥤ D₂
α : T ≅ T'
β : B ≅ B'
⊢ (w.whiskerHorizontal α.inv β.hom).op.GuitartExact ↔ w.op.GuitartExact

Tactic:
← whiskerVertical_iff w.op (NatIso.op α.symm) (NatIso.op β.symm)

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_4, u_4} D₁
inst✝ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
T' : C₁ ⥤ D₁
B' : C₂ ⥤ D₂
α : T ≅ T'
β : B ≅ B'
⊢ (w.whiskerHorizontal α.inv β.hom).op.GuitartExact ↔
    (w.op.whiskerVertical (NatIso.op α.symm).hom (NatIso.op β.symm).inv).GuitartExact
Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} D₁
inst✝³ : Category.{v_5, u_5} D₂
inst✝² : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : C₂ ⥤ C₃
B₂ : D₂ ⥤ D₃
V₃ : C₃ ⥤ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
T₁₂ : C₁ ⥤ C₃
B₁₂ : D₁ ⥤ D₃
eT : T₁ ⋙ T₂ ≅ T₁₂
eB : B₁ ⋙ B₂ ≅ B₁₂
inst✝¹ : w.GuitartExact
inst✝ : w'.GuitartExact
⊢ (w.hComp' w' eT eB).GuitartExact

Tactic:
by
  dsimp only [TwoSquare.hComp']
  infer_instance

Goal state after: