mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Quotient r), F₁.obj X = F₂.obj X

pp: case h_map
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₂
⊢ autoParam (∀ (X Y : Quotient r) (f : X ⟶ Y), F₁.map f = eqToHom ⋯ ≫ F₂.map f ≫ eqToHom ⋯) Functor.ext._auto_1

Tactic:
· rintro ⟨X⟩
      exact Functor.congr_obj h X

Goal state after:
case h_map
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₂
⊢ autoParam (∀ (X Y : Quotient r) (f : X ⟶ Y), F₁.map f = eqToHom ⋯ ≫ F₂.map f ≫ eqToHom ⋯) Functor.ext._auto_1
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
⊢ Fibration
    { P := d.Z, p₀ := d.p ≫ prod.fst, p₁ := d.p ≫ prod.snd, ι := P.ι ≫ d.i, ι_p₀ := ⋯, ι_p₁ := ⋯,
        weakEquivalence_ι := ⋯ }.p

Tactic:
by
        rw [fibration_iff]
        convert! d.hp
        aesop

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
K : Plus C
L : HomologicalComplex C (ComplexShape.up ℤ)
hL : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L = K.obj
⊢ CochainComplex.plus C L

Tactic:
rw [← HomotopyCategory.plus_quotient_obj_iff, hL]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : Plus C
L : HomologicalComplex C (ComplexShape.up ℤ)
hL : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L = K.obj
⊢ plus C K.obj
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: 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
X Y : A.FullSubcategory
f : X ⟶ Y
⊢ (B.inverseImage A.ι).trW f ↔ (A ⊓ B).trW f.hom

Tactic:
simp only [trW_iff]
  constructor
  · rintro ⟨Z, a, b, h, hZ⟩
    exact ⟨_, _, _, A.ι.map_distinguished _ h, Z.property, hZ⟩
  · rintro ⟨Z, a, b, h, hZ⟩
    refine ⟨⟨Z, hZ.1⟩, A.homMk a, A.homMk (b ≫ (A.ι.commShiftIso 1).inv.app _), ?_, hZ.2⟩
    rw [← A.ι.map_distinguished_iff]
    refine isomorphic_distinguished _ h _
      (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_)
    · cat_disch
    · cat_disch
    · simp [dsimp% (A.ι.commShiftIso (1 : ℤ)).inv_hom_id_app X]

Goal state after:
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₂
hf : ∃ Z s, ∃ (_ : B.trW s), f.hom ≫ s = 0 ≫ s
⊢ L₁.map f = 0

Tactic:
obtain ⟨X₃, s, hs, fac⟩ := hf

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
⊢ L₁.map f = 0
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f 0 0 ⋯ = 𝟙 (X 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f 0 (0 + 1) ⋯ = f 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k : ℕ
hij : 0 ≤ 0
hjk : 0 ≤ k
⊢ map f 0 k ⋯ = map f 0 0 hij ≫ map f 0 k hjk

Tactic:
rw [map_id, id_comp]

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

Goal state before:
pp: case zero.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k : ℕ
hij : 0 ≤ 0
hjk : 0 ≤ k
⊢ map f 0 k ⋯ = map f 0 0 hij ≫ map f 0 k hjk

Tactic:
| zero =>

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

Goal state before:
pp: case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
j k : ℕ
hij : 0 ≤ j
hjk : j ≤ k
⊢ map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk

Tactic:
| zero =>

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

Goal state before:
pp: case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ℕ ⥤ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), F.map (homOfLE ⋯) ≫ app (n + 1) = app n ≫ G.map (homOfLE ⋯)
⊢ ∀ ⦃i j : ℕ⦄ (hk : j = i + 0),
    F.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i j 0 hk)) ≫ app j =
      app i ≫ G.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i j 0 hk))

Tactic:
| zero =>

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

Goal state before:
pp: case neg
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
X : C
a b : ℤ
inst✝ : t.IsGE X a
h : ¬a ≤ b
⊢ t.IsGE ((t.truncGE b).obj X) a

Tactic:
· have : t.IsGE X b := t.isGE_of_ge X b a (by lia)
    exact t.isGE_of_iso (show X ≅ _ from asIso ((t.truncGEπ b).app X)) _

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case left
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₁ i : ℤ
hi : i ≠ n₁
⊢ ((π K L n₁).f i ≫ biprod.inr.f i) ≫ biprod.fst.f i = 𝟙 ((mid K L n₁).X i) ≫ biprod.fst.f i

pp: case right
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₁ i : ℤ
hi : i ≠ n₁
⊢ ((π K L n₁).f i ≫ biprod.inr.f i) ≫ biprod.snd.f i = 𝟙 ((mid K L n₁).X i) ≫ biprod.snd.f i

Tactic:
· apply (isZero_single_obj_X (.up ℤ) _ _ _ hi).eq_of_tgt

Goal state after:
case right
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₁ i : ℤ
hi : i ≠ n₁
⊢ ((π K L n₁).f i ≫ biprod.inr.f i) ≫ biprod.snd.f i = 𝟙 ((mid K L n₁).X i) ≫ biprod.snd.f i
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: case right
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
⊢ Function.Surjective fun f ↦ f.postcomp g

Tactic:
intro φ

Goal state after:
case right
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
φ : LeftHomotopyClass X Z
⊢ ∃ a, (fun f ↦ f.postcomp g) a = φ
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: case right
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
⊢ Function.Surjective fun g ↦ g.precomp f

Tactic:
intro φ

Goal state after:
case right
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
φ : RightHomotopyClass X Z
⊢ ∃ a, (fun g ↦ g.precomp f) a = φ
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 : (ComplexShape.up ℤ).Rel i n
⊢ ((cokernel f).truncGE n).d i n ≫ Injective.ι (((cokernel f).truncGE n).X n) = 0

Tactic:
simp only [ComplexShape.up_Rel] at hi
    exact (isZero_of_isStrictlyGE _ n _).eq_of_src _ _

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 L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : Mono f
⊢ homologyMap f n ≫ homologyMap (cokernel.π f) n = 0

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

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

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₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : C₂ ⥤ C₃
R₂ : D₂ ⥤ D₃
H₃ : C₃ ⥤ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
L₁₂ : C₁ ⥤ C₃
R₁₂ : D₁ ⥤ D₃
eL : L₁ ⋙ L₂ ≅ L₁₂
eR : R₁ ⋙ R₂ ≅ R₁₂
inst✝¹ : R₁.EssSurj
inst✝ : w.GuitartExact
h : (w.vComp' w' eL eR).GuitartExact
⊢ w'.GuitartExact

Tactic:
dsimp [TwoSquare.vComp'] at h
  rw [whiskerVertical_iff] at h
  exact of_vComp w w'

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case inr.zero
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
this : ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂), i ≤ n₀ + ↑q₁ → q₁ + 1 = q₂ → IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
hi : i ≤ n₀ + ↑q₁
hk : q₁ + 0 = q₂
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)

Tactic:
| zero =>

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 L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
q : ℕ
⊢ ι f n₀ ≫ midπ f n₀ q = ((functor f n₀).obj (op q)).obj.ι

Tactic:
simp [ι, midπ]

Goal state after:
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₁).IsRightDerivabilityStructure

Tactic:
by
  rw [(LocalizerMorphism.id W₁).isRightDerivabilityStructure_iff W₁.Q W₁.Q (𝟭 W₁.Localization)
    (Iso.refl _)]
  dsimp
  exact TwoSquare.guitartExact_id W₁.Q

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝⁵ : Category.{v₁, u₁} C₁
inst✝⁴ : Category.{v₂, u₂} C₂
inst✝³ : Category.{v₃, u₃} H
D₂ : Type u₄
inst✝² : Category.{v₄, u₄} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
h : Φ.Derives F
inst✝¹ : Φ.IsRightDerivabilityStructure
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
RF : D₂ ⥤ H
α : F ⟶ L₂ ⋙ RF
hα : ∀ (X₁ : C₁), IsIso (α.app (Φ.functor.obj X₁))
this✝¹ : F.HasPointwiseRightDerivedFunctor W₂
this✝ :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso ((F.totalRightDerivedUnit L₂ W₂).app (Φ.functor.obj X₁))
this : (Φ.functor ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
Y₂ : D₂
⊢ IsIso (φ.app (L₂.obj (Φ.functor.obj ((Φ.functor ⋙ L₂).objPreimage Y₂))))

Tactic:
simp only [← hφ, NatTrans.comp_app, Functor.whiskerLeft_app, isIso_comp_left_iff] at hα

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝⁵ : Category.{v₁, u₁} C₁
inst✝⁴ : Category.{v₂, u₂} C₂
inst✝³ : Category.{v₃, u₃} H
D₂ : Type u₄
inst✝² : Category.{v₄, u₄} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
h : Φ.Derives F
inst✝¹ : Φ.IsRightDerivabilityStructure
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
RF : D₂ ⥤ H
α : F ⟶ L₂ ⋙ RF
this✝¹ : F.HasPointwiseRightDerivedFunctor W₂
this✝ :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso ((F.totalRightDerivedUnit L₂ W₂).app (Φ.functor.obj X₁))
this : (Φ.functor ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
Y₂ : D₂
hα : ∀ (X₁ : C₁), IsIso (φ.app (L₂.obj (Φ.functor.obj X₁)))
⊢ IsIso (φ.app (L₂.obj (Φ.functor.obj ((Φ.functor ⋙ L₂).objPreimage Y₂))))
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective

Goal state before:
pp: case zero
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 X : C
⊢ Function.Bijective ⇑(F.mapExtAddHom X Y 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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 Y : C
⊢ Function.Bijective ⇑(F.mapExtAddHom X Y 0)

Tactic:
| zero =>

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

Goal state before:
pp: case succ
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 := ⋯ }
⊢ Function.Bijective ⇑(F.mapExtAddHom X Y (n + 1))

Tactic:
have : Injective (S.map F).X₂ := Functor.PreservesInjectiveObjects.injective_obj I.injective

Goal state after:
case succ
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₂
⊢ Function.Bijective ⇑(F.mapExtAddHom X Y (n + 1))
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ { obj := (CategoryTheory.shiftFunctor C n).obj X✝.obj,
          d := (CategoryTheory.shiftFunctor C n).map X✝.d ≫ (shiftComm X✝.obj 1 n).hom, d_squared := ⋯ }.d ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.f) =
    (CategoryTheory.shiftFunctor C n).map f.f ≫
      { obj := (CategoryTheory.shiftFunctor C n).obj Y✝.obj,
          d := (CategoryTheory.shiftFunctor C n).map Y✝.d ≫ (shiftComm Y✝.obj 1 n).hom, d_squared := ⋯ }.d

Tactic:
dsimp
        rw [Category.assoc]
        erw [shiftComm_hom_comp]
        rw [← Functor.map_comp_assoc, f.comm, Functor.map_comp_assoc]
        rfl

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

Goal state before:
pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ¬∃ k, c.Rel j k
⊢ (eval C c j ⋙ coyoneda.obj (op X)).CorepresentableBy ((single C c j).obj X)

Tactic:
apply evalCompCoyonedaCorepresentableBySingle

Goal state after:
case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ¬∃ k, c.Rel j k
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1
Module: Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
w✝⁵ w✝⁴ w✝³ : CochainComplex C ℤ
f : w✝⁵ ⟶ w✝⁴
g : w✝⁴ ⟶ w✝³
w✝² w✝¹ w✝ : CochainComplex C ℤ
f' : w✝² ⟶ w✝¹
g' : w✝¹ ⟶ w✝
φ : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g'
eq :
  map g g' (φ.app 1) (φ.app 2) ⋯ ≫ (triangle g').mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1).map (inr f') =
    ((triangle g).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1).map (inr f)) ≫
      (shiftFunctor (CochainComplex C ℤ) 1).map (map f f' (φ.app 0) (φ.app 1) ⋯)
⊢ (quotient C (ComplexShape.up ℤ)).map (map g g' (φ.app 1) (φ.app 2) ⋯) ≫
      (quotient C (ComplexShape.up ℤ)).map ((triangle g').mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1).map (inr f')) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (CochainComplex.mappingCone f') =
    ((quotient C (ComplexShape.up ℤ)).map ((triangle g).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1).map (inr f)) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (CochainComplex.mappingCone f)) ≫
      (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((quotient C (ComplexShape.up ℤ)).map (map f f' (φ.app 0) (φ.app 1) ⋯))

Tactic:
simp only [Category.assoc, ← Functor.map_comp_assoc]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
w✝⁵ w✝⁴ w✝³ : CochainComplex C ℤ
f : w✝⁵ ⟶ w✝⁴
g : w✝⁴ ⟶ w✝³
w✝² w✝¹ w✝ : CochainComplex C ℤ
f' : w✝² ⟶ w✝¹
g' : w✝¹ ⟶ w✝
φ : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g'
eq :
  map g g' (φ.app 1) (φ.app 2) ⋯ ≫ (triangle g').mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1).map (inr f') =
    ((triangle g).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1).map (inr f)) ≫
      (shiftFunctor (CochainComplex C ℤ) 1).map (map f f' (φ.app 0) (φ.app 1) ⋯)
⊢ (quotient C (ComplexShape.up ℤ)).map
        (map g g' (φ.app 1) (φ.app 2) ⋯ ≫ (triangle g').mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1).map (inr f')) ≫
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (CochainComplex.mappingCone f') =
    (quotient C (ComplexShape.up ℤ)).map ((triangle g).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1).map (inr f)) ≫
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (CochainComplex.mappingCone f) ≫
        (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
          ((quotient C (ComplexShape.up ℤ)).map (map f f' (φ.app 0) (φ.app 1) ⋯))
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
p'' : ℤ
hp'' : p + 1 = p''
⊢ (∃ g, K.d p p'' ≫ g = f) → ∃ β, δ (n - 1) n β = ↑(toSingleMk f h p' hp' hf)

Tactic:
rintro ⟨g, rfl⟩
    exact ⟨n.negOnePow • Cochain.toSingleMk g (by lia),
      by simp [Cochain.δ_toSingleMk _ _ _ _ h, smul_smul]⟩

Goal state after: