mathlib-initiative/mathlib-tactics huggingface dataset:
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
J : Type u_2
A B : J → C
inst✝² : HasProduct A
inst✝¹ : HasProduct B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst✝ : ∀ (j : J), HasLiftingProperty p (f j)
t : X ⟶ ∏ᶜ A
b : Y ⟶ ∏ᶜ B
sq : CommSq t p (Limits.Pi.map f) b
sq' : ∀ (j : J), CommSq (t ≫ Pi.π A j) p (f j) (b ≫ Pi.π B j)
⊢ sq.HasLift

Tactic:
exact ⟨⟨{ l := Pi.lift (fun j ↦ (sq' j).lift) }⟩⟩

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
d : (cofibrations C).MapFactorizationData (trivialFibrations C) P.i :=
  (cofibrations C).factorizationData (trivialFibrations C) P.i
⊢ { I := d.Z, i₀ := coprod.inl ≫ d.i, i₁ := coprod.inr ≫ d.i, π := d.p ≫ P.π, i₀_π := ⋯, i₁_π := ⋯,
        weakEquivalence_π := ⋯ }.i =
    d.i

Tactic:
aesop

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

Goal state before:
pp: case h_obj
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
r : HomRel C
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Quotient r ⥤ E
h : functor r ⋙ F₁ = functor r ⋙ F₂
X : C
⊢ F₁.obj { as := X } = F₂.obj { as := X }

Tactic:
exact Functor.congr_obj h X

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
P : PathObject Y
f g : X ⟶ Y
h : P.RightHomotopy f g
d : (trivialCofibrations C).MapFactorizationData (fibrations C) P.p :=
  (trivialCofibrations C).factorizationData (fibrations C) P.p
⊢ { P := d.Z, p₀ := d.p ≫ prod.fst, p₁ := d.p ≫ prod.snd, ι := P.ι ≫ d.i, ι_p₀ := ⋯, ι_p₁ := ⋯,
        weakEquivalence_ι := ⋯ }.p =
    d.p

Tactic:
aesop

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

Goal state before:
pp: 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
⊢ (Triangle.mk u₂₃ v₂₃ w₂₃).mor₁.unop ≫ (Triangle.mk u₁₂ v₁₂ w₁₂).mor₁.unop = (Triangle.mk u₁₃ v₁₃ w₁₃).mor₁.unop

Tactic:
aesop

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

Goal state before:
pp: case refine_1
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₃ :
  ((((opShiftFunctorEquivalence C 1).unitIso.inv.app (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁).unop ≫
          (shiftFunctor C 1).map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃.unop) ≫
        (shiftFunctor C 1).map o.m₃).op =
    (((opShiftFunctorEquivalence C 1).unitIso.inv.app (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁).unop ≫
        (shiftFunctor C 1).map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₃.unop).op
⊢ o.m₃.op ≫ w₁₃ = w₁₂

Tactic:
dsimp at eq₃

Goal state after:
case refine_1
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 o.m₃).op ≫
      ((shiftFunctor C 1).map w₁₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₁ =
    ((shiftFunctor C 1).map w₁₂.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₁
⊢ o.m₃.op ≫ w₁₃ = w₁₂
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated

Goal state before:
pp: case refine_3
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' ⋯ ⋯ ⋯ ⋯
⊢ Triangle.mk o.m₃.op o.m₁.op (w₂₃ ≫ (shiftFunctor Cᵒᵖ 1).map v₁₂) ∈ Pretriangulated.distinguishedTriangles

Tactic:
have := op_distinguished _ o.mem
      dsimp at this
      convert! this using 2
      rw [Category.assoc, Functor.map_comp, Functor.map_comp,
        ← opShiftFunctorEquivalence_counitIso_hom_app_shift,
        ← opShiftFunctorEquivalence_counitIso_inv_naturality_assoc, Iso.inv_hom_id_app_assoc]

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
x✝ : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
hs : B.trW s
⊢ ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'

pp: case refine_2
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
hA : ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
X Y : C
f : X ⟶ Y
hX : B X
hY : A Y
⊢ ∃ Z a b, A Z ∧ B Z ∧ a ≫ b = f

Tactic:
· rw [ObjectProperty.trW_iff'] at hs
    obtain ⟨W, a, b, hT, hW⟩ := hs
    obtain ⟨W', c, d, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac a hW hX
    obtain ⟨U, hU, e, f, hT'⟩ := A.distinguished_cocone_triangle d h₁ hX
    obtain ⟨g, hg, _⟩ := Pretriangulated.complete_distinguished_triangle_morphism _ _ hT hT'
      c (𝟙 _) (by cat_disch)
    refine ⟨U, e, g, hU, ?_, by cat_disch⟩
    rw [ObjectProperty.trW_iff']
    exact ⟨_, _, _, hT', h₁, h₂⟩

Goal state after:
case refine_2
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
hA : ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
X Y : C
f : X ⟶ Y
hX : B X
hY : A Y
⊢ ∃ Z a b, A Z ∧ B Z ∧ a ≫ b = f
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 Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ (σ₂.s ≫ σ₁.s) ≫
      { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.g =
    𝟙 { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.X₃

Tactic:
simp [reassoc_of% σ₁.s_g, σ₂.s_g]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i j : ℕ
h : i = j
⊢ f i = eqToHom ⋯ ≫ f j ≫ eqToHom ⋯

Tactic:
by
  subst h
  simp

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
hX : ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0
⊢ t.IsLE ((t.truncLT n₁).obj X) n₀

Tactic:
by rw [← h]; infer_instance

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 g : X ⟶ Y
h : Relation.EqvGen homRel f g
⊢ W f ↔ W g

Tactic:
by
  induction h with
  | rel _ _ h => exact iff W h
  | refl => rfl
  | symm _ _ _ h => exact h.symm
  | trans _ _ _ _ _ h₁ h₂ => exact h₁.trans h₂

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

Goal state before:
pp: case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
f₁ : LeftHomotopyClass X Y
f₀ : X ⟶ Y
h : (fun f ↦ f.postcomp g) (mk f₀) = (fun f ↦ f.postcomp g) f₁
⊢ mk f₀ = f₁

Tactic:
obtain ⟨f₁, rfl⟩ := f₁.mk_surjective

Goal state after:
case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h : (fun f ↦ f.postcomp g) (mk f₀) = (fun f ↦ f.postcomp g) (mk f₁)
⊢ mk f₀ = mk f₁
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: case left
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₁ : RightHomotopyClass Y Z
f₀ : Y ⟶ Z
h : (fun g ↦ g.precomp f) (mk f₀) = (fun g ↦ g.precomp f) f₁
⊢ mk f₀ = f₁

Tactic:
obtain ⟨f₁, rfl⟩ := f₁.mk_surjective

Goal state after:
case left
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 : (fun g ↦ g.precomp f) (mk f₀) = (fun g ↦ g.precomp f) (mk f₁)
⊢ mk f₀ = mk f₁
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 i : ℤ
hi : i + 1 = n
⊢ ((cokernel f).truncGE n).d i n ≫ Injective.ι (((cokernel f).truncGE n).X n) = 0

Tactic:
exact (isZero_of_isStrictlyGE _ n _).eq_of_src _ _

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) :=
  TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv
this : Nonempty (w.CostructuredArrowDownwards y)
c : C₁
g : X₂ ⟶ Φ.functor.obj c
x : (Φ.functor ⋙ L).obj c ⟶ X₃
fac : L.map g ≫ w.app c ≫ (𝟭 D).map x = y
⊢ ∃ Y, Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac) ((fromRightResolution Φ L y).obj Y)

Tactic:
dsimp [w] at x fac

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) :=
  TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv
this : Nonempty (w.CostructuredArrowDownwards y)
c : C₁
g : X₂ ⟶ Φ.functor.obj c
x : L.obj (Φ.functor.obj c) ⟶ X₃
fac : L.map g ≫ 𝟙 (L.obj (Φ.functor.obj c)) ≫ x = y
⊢ ∃ Y, Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac) ((fromRightResolution Φ L y).obj Y)
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
a✝ : Φ.op.IsRightDerivabilityStructure
⊢ Φ.HasLeftResolutions

Tactic:
rw [hasLeftResolutions_iff_op]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
a✝ : Φ.op.IsRightDerivabilityStructure
⊢ Φ.op.HasRightResolutions
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : W₁.ContainsIdentities
⊢ (id W₁).IsLeftDerivabilityStructure

Tactic:
rw [(LocalizerMorphism.id W₁).isLeftDerivabilityStructure_iff W₁.Q W₁.Q (𝟭 W₁.Localization)
    (Iso.refl _)]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : W₁.ContainsIdentities
⊢ TwoSquare.GuitartExact (Iso.refl ((id W₁).functor ⋙ W₁.Q)).inv
Module: Mathlib.CategoryTheory.GuitartExact.KanExtension

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
inst✝² : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
F : C₂ ⥤ D
E : R.LeftExtension F
w : TwoSquare T L R B
inst✝¹ : w.GuitartExact
inst✝ : B.EssSurj
x✝ : (E.compTwoSquare w).IsPointwiseLeftKanExtension
⊢ (fun h ↦ h.compTwoSquare w) ((fun h ↦ E.isPointwiseLeftKanExtensionOfCompTwoSquare w h) x✝) = x✝

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.KanExtension

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
inst✝² : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
F : C₂ ⥤ D
E : R.LeftExtension F
w : TwoSquare T L R B
inst✝¹ : w.GuitartExact
inst✝ : B.EssSurj
x✝ : E.IsPointwiseLeftKanExtension
⊢ (fun h ↦ E.isPointwiseLeftKanExtensionOfCompTwoSquare w h) ((fun h ↦ h.compTwoSquare w) x✝) = x✝

Tactic:
by subsingleton

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.obj.IsStrictlyGE n
L : CochainComplex C ℤ
i : K.obj ⟶ L
w✝¹ : QuasiIso i
w✝ : ∀ (n : ℤ), Injective (L.X n)
h✝ : L.IsStrictlyGE n
L' : CochainComplex (InjectiveObject C) ℤ := HomologicalComplex.liftObjectProperty (isInjective C) L ⋯
⊢ L'.IsStrictlyGE n

Tactic:
← isStrictlyGE_mapHomologicalComplex_obj_iff _ (InjectiveObject.ι _)

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.obj.IsStrictlyGE n
L : CochainComplex C ℤ
i : K.obj ⟶ L
w✝¹ : QuasiIso i
w✝ : ∀ (n : ℤ), Injective (L.X n)
h✝ : L.IsStrictlyGE n
L' : CochainComplex (InjectiveObject C) ℤ := HomologicalComplex.liftObjectProperty (isInjective C) L ⋯
⊢ IsStrictlyGE (((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj L') n
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
obj✝ : CochainComplex C ℤ
n : ℤ
h✝ : obj✝.IsStrictlyGE n
property✝ : fibrantObjects (Plus C) { obj := obj✝, property := ⋯ }
⊢ ((HomologicalComplex.liftFunctorObjectProperty (isInjective C) (FibrantObject.ι ⋙ ι C) ⋯).obj
        { obj := { obj := obj✝, property := ⋯ }, property := property✝ }).IsStrictlyGE
    n

Tactic:
← isStrictlyGE_mapHomologicalComplex_obj_iff _ (InjectiveObject.ι _)

Goal state after:
C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
obj✝ : CochainComplex C ℤ
n : ℤ
h✝ : obj✝.IsStrictlyGE n
property✝ : fibrantObjects (Plus C) { obj := obj✝, property := ⋯ }
⊢ IsStrictlyGE
    (((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj
      ((HomologicalComplex.liftFunctorObjectProperty (isInjective C) (FibrantObject.ι ⋙ ι C) ⋯).obj
        { obj := { obj := obj✝, property := ⋯ }, property := property✝ }))
    n
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughProjectives C
inst✝ : F.PreservesProjectiveObjects
Y : C
n : ℕ
hn : ∀ (X : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
X : C
P : ProjectivePresentation X := Classical.arbitrary (ProjectivePresentation X)
S : ShortComplex C := { X₁ := Limits.kernel P.f, X₂ := P.p, X₃ := X, f := kernel.ι P.f, g := P.f, zero := ⋯ }
this : Projective (S.map F).X₂
hS : S.ShortExact
x₃ : Ext S.X₃ Y (n + 1)
⊢ (Ext.mk₀ S.g).comp x₃ ⋯ = 0

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughProjectives C
inst✝ : F.PreservesProjectiveObjects
Y : C
n : ℕ
hn : ∀ (X : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
X : C
P : ProjectivePresentation X := Classical.arbitrary (ProjectivePresentation X)
S : ShortComplex C := { X₁ := Limits.kernel P.f, X₂ := P.p, X₃ := X, f := kernel.ι P.f, g := P.f, zero := ⋯ }
this : Projective (S.map F).X₂
hS : S.ShortExact
y₃ : Ext (F.obj S.X₃) (F.obj Y) (n + 1)
⊢ (Ext.mk₀ (S.map F).g).comp y₃ ⋯ = 0

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughInjectives C
inst✝ : F.PreservesInjectiveObjects
X : C
n : ℕ
hn : ∀ (Y : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
Y : C
I : InjectivePresentation Y := Classical.arbitrary (InjectivePresentation Y)
S : ShortComplex C := { X₁ := Y, X₂ := I.J, X₃ := cokernel I.f, f := I.f, g := cokernel.π I.f, zero := ⋯ }
this : Injective (S.map F).X₂
hS : S.ShortExact
x₁ : Ext X S.X₁ (n + 1)
⊢ x₁.comp (Ext.mk₀ S.f) ⋯ = 0

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughInjectives C
inst✝ : F.PreservesInjectiveObjects
X : C
n : ℕ
hn : ∀ (Y : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
Y : C
I : InjectivePresentation Y := Classical.arbitrary (InjectivePresentation Y)
S : ShortComplex C := { X₁ := Y, X₂ := I.J, X₃ := cokernel I.f, f := I.f, g := cokernel.π I.f, zero := ⋯ }
this : Injective (S.map F).X₂
hS : S.ShortExact
y₁ : Ext (F.obj X) (F.obj S.X₁) (n + 1)
⊢ y₁.comp (Ext.mk₀ (S.map F).f) ⋯ = 0

Tactic:
by subsingleton

Goal state after: