mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ ((ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
          (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)) ⋯).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X')).comp
      (((ShiftedHom.mk₀ 0 ⋯ ((singleFunctor C 0).map g)).map DerivedCategory.Q).comp
        ((ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
              DerivedCategory.Q).comp
          (ShiftedHom.mk₀ 0 ⋯
            (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
          ⋯)
        ⋯)
      ⋯

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ ((ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
          (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)) ⋯).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X')).comp
      (((ShiftedHom.mk₀ 0 ⋯ ((singleFunctor C 0).map g)).map DerivedCategory.Q).comp
        ((ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
              DerivedCategory.Q).comp
          (ShiftedHom.mk₀ 0 ⋯
            (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
          ⋯)
        ⋯)
      ⋯
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hp : ⟦p⟧ = pbar
this : ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧
R : C
x : R ⟶ (Over.mk (p.hom ≫ f)).left
y : R ⟶ (Over.mk (𝟙 Q)).left
w✝ : Epi x
ey : Epi y
comm : x ≫ p.hom ≫ f = y ≫ 𝟙 Q
⊢ y ≫ 𝟙 Q = y

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hp : ⟦p⟧ = pbar
this : ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧
R : C
x : R ⟶ (Over.mk (p.hom ≫ f)).left
y : R ⟶ (Over.mk (𝟙 Q)).left
w✝ : Epi x
ey : Epi y
comm : x ≫ p.hom ≫ f = y ≫ 𝟙 Q
⊢ y ≫ 𝟙 Q = y
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
⊢ QuasiIso R.π'

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
⊢ QuasiIso R.π'
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pullback.fst (Abelian.factorThruImage S.f) c ≫ S.f = pullback.fst (Abelian.factorThruImage S.f) c ≫ S.f

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ (pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f) =
    (pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pullback.snd (Abelian.factorThruImage S.f) c ≫ c ≫ kernel.ι (cokernel.π S.f) =
    pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pullback.snd (Abelian.factorThruImage S.f) c ≫ c ≫ kernel.ι (cokernel.π S.f) =
    pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
a : Over S.X₁
ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
ha' : ⟦a⟧ = a'
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
a : Over S.X₁
ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
ha' : ⟦a⟧ = a'
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)) +
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯ +
          Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯))

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)) +
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯ +
          Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯))
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          ((inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y) ≫
            (DerivedCategory.singleFunctor C 0).map g))
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          (DerivedCategory.Q.map φ.hom' ≫
            inv (DerivedCategory.Q.map R'.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'))
        ⋯)
      ⋯

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          ((inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y) ≫
            (DerivedCategory.singleFunctor C 0).map g))
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          (DerivedCategory.Q.map φ.hom' ≫
            inv (DerivedCategory.Q.map R'.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'))
        ⋯)
      ⋯
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this✝ : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
a : Over S.X₁
ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
ha' : ⟦a⟧ = a'
Z : C
r : Z ⟶ ((fun g ↦ app S.f g) a).left
q : Z ⟶ (Over.mk (kernel.ι S.g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g ↦ app S.f g) a).hom = q ≫ (Over.mk (kernel.ι S.g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
left✝ : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g :=
  pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
pe : Epi j
this : IsIso j
⊢ ((asIso j).inv ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ≫ kernel.ι (cokernel.π S.f)) ≫
      cokernel.π S.f =
    0

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this✝ : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
a : Over S.X₁
ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
ha' : ⟦a⟧ = a'
Z : C
r : Z ⟶ ((fun g ↦ app S.f g) a).left
q : Z ⟶ (Over.mk (kernel.ι S.g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g ↦ app S.f g) a).hom = q ≫ (Over.mk (kernel.ι S.g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
left✝ : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g :=
  pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
pe : Epi j
this : IsIso j
⊢ ((asIso j).inv ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ≫ kernel.ι (cokernel.π S.f)) ≫
      cokernel.π S.f =
    0
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)) -
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯ -
          Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯))

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)) -
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯ -
          Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯))
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: case e_g
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ (inv (DerivedCategory.Q.map R.ι') ≫ (singleFunctor C 0 ⋙ DerivedCategory.Q).map g) ≫
      (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y' =
    (DerivedCategory.Q.map φ.hom' ≫ inv (DerivedCategory.Q.map R'.ι')) ≫
      (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'

Tactic:
]

Goal state after:
case e_g
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ (inv (DerivedCategory.Q.map R.ι') ≫ (singleFunctor C 0 ⋙ DerivedCategory.Q).map g) ≫
      (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y' =
    (DerivedCategory.Q.map φ.hom' ≫ inv (DerivedCategory.Q.map R'.ι')) ≫
      (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategory (ComplexShape.up ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) ≫
        (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app J.cocomplex =
    (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫
        (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategory (ComplexShape.up ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) ≫
        (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app J.cocomplex =
    (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫
        (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫
        (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ =
    (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫
        (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫
        (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ =
    (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫
        (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ -R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk (-Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ -R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk (-Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ F.rightDerivedToHomotopyCategory.map f =
    (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ ≫
        (J.isoRightDerivedToHomotopyCategoryObj F).inv

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ F.rightDerivedToHomotopyCategory.map f =
    (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ ≫
        (J.isoRightDerivedToHomotopyCategoryObj F).inv
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ F.rightDerivedToHomotopyCategory.map f = F.rightDerivedToHomotopyCategory.map f

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
p : ℕ
hp : p + 1 = n
⊢ (∃ g,
      ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-↑p) p ⋯).inv) ≫ g =
        (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ↔
    ∃ g, R.complex.d n p ≫ g = f

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
p : ℕ
hp : p + 1 = n
⊢ (∃ g,
      ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-↑p) p ⋯).inv) ≫ g =
        (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ↔
    ∃ g, R.complex.d n p ≫ g = f