awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : X.IsStrictlyLE n
X' : CochainComplex.{v, u, 0} C ℤ
s : X' ⟶ X
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
⊢ ∃ (X'_1 : CochainComplex.{v, u, 0} C ℤ) (_ : X'_1.IsStrictlyLE n) (s_1 : X'_1 ⟶ X) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X'_1) (CategoryTheory.Functor.map Q s_1)) (g_1 :
    X'_1 ⟶ Y),
    Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
      (inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g)
      (inv (CategoryTheory.Functor.map Q s_1) ≫ CategoryTheory.Functor.map Q g_1)
have this : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncLE n)) (Y := Functor.obj Q (X.truncLE n))
  (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s n))
Tactic: have : IsIso (Q.map (CochainComplex.truncLEMap s n)) := by
    rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncLEMap_iff]
    rw [isIso_Q_map_iff_quasiIso] at hs
    infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : X.IsStrictlyLE n
X' : CochainComplex.{v, u, 0} C ℤ
s : X' ⟶ X
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncLE n)) (Y := Functor.obj Q (X.truncLE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s n))
⊢ ∃ (X'_1 : CochainComplex.{v, u, 0} C ℤ) (_ : X'_1.IsStrictlyLE n) (s_1 : X'_1 ⟶ X) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X'_1) (CategoryTheory.Functor.map Q s_1)) (g_1 :
    X'_1 ⟶ Y),
    Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
      (inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g)
      (inv (CategoryTheory.Functor.map Q s_1) ≫ CategoryTheory.Functor.map Q g_1)
have refine_1 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncLE n))
  (CategoryTheory.Functor.map Q (CategoryStruct.comp (Y := X.truncLE n) (CochainComplex.truncLEMap s n) (X.ιTruncLE n)))
Tactic: refine ⟨X'.truncLE n, inferInstance, CochainComplex.truncLEMap s n ≫ X.ιTruncLE n, ?_,
      CochainComplex.truncLEMap g n ≫ Y.ιTruncLE n, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : X.IsStrictlyLE n
X' : CochainComplex.{v, u, 0} C ℤ
s : X' ⟶ X
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncLE n)) (Y := Functor.obj Q (X.truncLE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s n))
refine_1 :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncLE n))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := X.truncLE n) (CochainComplex.truncLEMap s n) (X.ιTruncLE n)))
⊢ ∃ (X'_1 : CochainComplex.{v, u, 0} C ℤ) (_ : X'_1.IsStrictlyLE n) (s_1 : X'_1 ⟶ X) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X'_1) (CategoryTheory.Functor.map Q s_1)) (g_1 :
    X'_1 ⟶ Y),
    Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
      (inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g)
      (inv (CategoryTheory.Functor.map Q s_1) ≫ CategoryTheory.Functor.map Q g_1)
have refine_2 : Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
  (inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g)
  (CategoryStruct.comp (Y := Functor.obj Q (X'.truncLE n))
    (inv
      (CategoryTheory.Functor.map Q
        (CategoryStruct.comp (Y := X.truncLE n) (CochainComplex.truncLEMap s n) (X.ιTruncLE n))))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := Y.truncLE n) (CochainComplex.truncLEMap g n) (Y.ιTruncLE n))))
Tactic: refine ⟨X'.truncLE n, inferInstance, CochainComplex.truncLEMap s n ≫ X.ιTruncLE n, ?_,
      CochainComplex.truncLEMap g n ≫ Y.ιTruncLE n, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : X.IsStrictlyLE n
X' : CochainComplex.{v, u, 0} C ℤ
s : X' ⟶ X
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncLE n)) (Y := Functor.obj Q (X.truncLE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s n))
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncLE n))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := X.truncLE n) (CochainComplex.truncLEMap s n) (X.ιTruncLE n)))
have refine_1 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncLE n))
  (CategoryStruct.comp (Y := Functor.obj Q (X.truncLE n)) (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s n))
    (CategoryTheory.Functor.map Q (X.ιTruncLE n)))
Tactic: rw [Q.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
n : ℤ
inst_3 : Y.IsStrictlyGE n
⊢ ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (_ : Y'.IsStrictlyGE n) (g : X ⟶ Y') (s : Y ⟶ Y') (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)),
    f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)
have obtain : ∀ (Y' : CochainComplex.{v, u, 0} C ℤ) (g : X ⟶ Y') (s : Y ⟶ Y')
  (hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)),
  ∃ (Y'_1 : CochainComplex.{v, u, 0} C ℤ) (_ : Y'_1.IsStrictlyGE n) (g_1 : X ⟶ Y'_1) (s_1 : Y ⟶ Y'_1) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s_1)),
    Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
      (CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s))
      (CategoryTheory.Functor.map Q g_1 ≫ inv (CategoryTheory.Functor.map Q s_1))
Tactic: obtain ⟨Y', g, s, hs, rfl⟩ := left_fac f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : Y.IsStrictlyGE n
Y' : CochainComplex.{v, u, 0} C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncGE n)) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n))
have rw : ∀ (i : ℤ), n ≤ i → QuasiIsoAt s i
Tactic: rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncGEMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : Y.IsStrictlyGE n
Y' : CochainComplex.{v, u, 0} C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
⊢ ∀ (i : ℤ), n ≤ i → QuasiIsoAt s i
have hs₁ : QuasiIso s
Tactic: rw [isIso_Q_map_iff_quasiIso] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : Y.IsStrictlyGE n
Y' : CochainComplex.{v, u, 0} C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
⊢ ∃ (Y'_1 : CochainComplex.{v, u, 0} C ℤ) (_ : Y'_1.IsStrictlyGE n) (g_1 : X ⟶ Y'_1) (s_1 : Y ⟶ Y'_1) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s_1)),
    Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
      (CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s))
      (CategoryTheory.Functor.map Q g_1 ≫ inv (CategoryTheory.Functor.map Q s_1))
have this : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncGE n)) (Y := Functor.obj Q (Y'.truncGE n))
  (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n))
Tactic: have : IsIso (Q.map (CochainComplex.truncGEMap s n)) := by
    rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncGEMap_iff]
    rw [isIso_Q_map_iff_quasiIso] at hs
    infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : Y.IsStrictlyGE n
Y' : CochainComplex.{v, u, 0} C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncGE n)) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n))
⊢ ∃ (Y'_1 : CochainComplex.{v, u, 0} C ℤ) (_ : Y'_1.IsStrictlyGE n) (g_1 : X ⟶ Y'_1) (s_1 : Y ⟶ Y'_1) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s_1)),
    Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
      (CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s))
      (CategoryTheory.Functor.map Q g_1 ≫ inv (CategoryTheory.Functor.map Q s_1))
have refine_1 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (Y := Functor.obj Q (Y'.truncGE n))
  (CategoryTheory.Functor.map Q (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))
Tactic: refine ⟨Y'.truncGE n, inferInstance, X.πTruncGE n ≫ CochainComplex.truncGEMap g n,
    Y.πTruncGE n ≫ CochainComplex.truncGEMap s n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : Y.IsStrictlyGE n
Y' : CochainComplex.{v, u, 0} C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncGE n)) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n))
refine_1 :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))
⊢ ∃ (Y'_1 : CochainComplex.{v, u, 0} C ℤ) (_ : Y'_1.IsStrictlyGE n) (g_1 : X ⟶ Y'_1) (s_1 : Y ⟶ Y'_1) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s_1)),
    Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
      (CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s))
      (CategoryTheory.Functor.map Q g_1 ≫ inv (CategoryTheory.Functor.map Q s_1))
have refine_2 : Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
  (CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s))
  (CategoryStruct.comp (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := X.truncGE n) (X.πTruncGE n) (CochainComplex.truncGEMap g n)))
    (inv
      (CategoryTheory.Functor.map Q
        (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))))
Tactic: refine ⟨Y'.truncGE n, inferInstance, X.πTruncGE n ≫ CochainComplex.truncGEMap g n,
    Y.πTruncGE n ≫ CochainComplex.truncGEMap s n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : Y.IsStrictlyGE n
Y' : CochainComplex.{v, u, 0} C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncGE n)) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n))
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))
have refine_1 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (Y := Functor.obj Q (Y'.truncGE n))
  (CategoryStruct.comp (Y := Functor.obj Q (Y.truncGE n)) (CategoryTheory.Functor.map Q (Y.πTruncGE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n)))
Tactic: rw [Q.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : Y.IsStrictlyGE n
Y' : CochainComplex.{v, u, 0} C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncGE n)) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n))
⊢ Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
    (CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s))
    (CategoryStruct.comp (Y := Functor.obj Q (Y'.truncGE n))
      (CategoryTheory.Functor.map Q
        (CategoryStruct.comp (Y := X.truncGE n) (X.πTruncGE n) (CochainComplex.truncGEMap g n)))
      (inv
        (CategoryTheory.Functor.map Q
          (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))))
have eq : Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q Y) (Functor.obj Q (Y'.truncGE n)))
  (CategoryTheory.Functor.map Q (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))
  (CategoryTheory.Functor.map Q (s ≫ Y'.πTruncGE n))
Tactic: have eq := Q.congr_map (CochainComplex.πTruncGE_naturality s n)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : Y.IsStrictlyGE n
Y' : CochainComplex.{v, u, 0} C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncGE n)) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n))
eq :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q Y) (Functor.obj Q (Y'.truncGE n)))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))
    (CategoryTheory.Functor.map Q (s ≫ Y'.πTruncGE n))
⊢ Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
    (CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s))
    (CategoryStruct.comp (Y := Functor.obj Q (Y'.truncGE n))
      (CategoryTheory.Functor.map Q
        (CategoryStruct.comp (Y := X.truncGE n) (X.πTruncGE n) (CochainComplex.truncGEMap g n)))
      (inv
        (CategoryTheory.Functor.map Q
          (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))))
have eq' : Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q (Y'.truncGE n)))
  (CategoryTheory.Functor.map Q (CategoryStruct.comp (Y := X.truncGE n) (X.πTruncGE n) (CochainComplex.truncGEMap g n)))
  (CategoryTheory.Functor.map Q (g ≫ Y'.πTruncGE n))
Tactic: have eq' := Q.congr_map (CochainComplex.πTruncGE_naturality g n)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : Y.IsStrictlyGE n
Y' : CochainComplex.{v, u, 0} C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncGE n)) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n))
eq :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q Y) (Functor.obj Q (Y'.truncGE n)))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))
    (CategoryTheory.Functor.map Q (s ≫ Y'.πTruncGE n))
eq' :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q (Y'.truncGE n)))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := X.truncGE n) (X.πTruncGE n) (CochainComplex.truncGEMap g n)))
    (CategoryTheory.Functor.map Q (g ≫ Y'.πTruncGE n))
⊢ Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
    (CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s))
    (CategoryStruct.comp (Y := Functor.obj Q (Y'.truncGE n))
      (CategoryTheory.Functor.map Q
        (CategoryStruct.comp (Y := X.truncGE n) (X.πTruncGE n) (CochainComplex.truncGEMap g n)))
      (inv
        (CategoryTheory.Functor.map Q
          (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))))
have eq₁ : Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q Y) (Functor.obj Q (Y'.truncGE n)))
  (CategoryStruct.comp (Y := Functor.obj Q (Y.truncGE n)) (CategoryTheory.Functor.map Q (Y.πTruncGE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n)))
  (CategoryTheory.Functor.map Q s ≫ CategoryTheory.Functor.map Q (Y'.πTruncGE n))
Tactic: simp only [Functor.map_comp] at eq eq'
Cleared hypotheses: eq, eq'
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : Y.IsStrictlyGE n
Y' : CochainComplex.{v, u, 0} C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncGE n)) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n))
eq :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q Y) (Functor.obj Q (Y'.truncGE n)))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))
    (CategoryTheory.Functor.map Q (s ≫ Y'.πTruncGE n))
eq' :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q (Y'.truncGE n)))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := X.truncGE n) (X.πTruncGE n) (CochainComplex.truncGEMap g n)))
    (CategoryTheory.Functor.map Q (g ≫ Y'.πTruncGE n))
eq₁ :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q Y) (Functor.obj Q (Y'.truncGE n)))
    (CategoryStruct.comp (Y := Functor.obj Q (Y.truncGE n)) (CategoryTheory.Functor.map Q (Y.πTruncGE n))
      (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n)))
    (CategoryTheory.Functor.map Q s ≫ CategoryTheory.Functor.map Q (Y'.πTruncGE n))
⊢ Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
    (CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s))
    (CategoryStruct.comp (Y := Functor.obj Q (Y'.truncGE n))
      (CategoryTheory.Functor.map Q
        (CategoryStruct.comp (Y := X.truncGE n) (X.πTruncGE n) (CochainComplex.truncGEMap g n)))
      (inv
        (CategoryTheory.Functor.map Q
          (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))))
have eq'₁ : Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q (Y'.truncGE n)))
  (CategoryStruct.comp (Y := Functor.obj Q (X.truncGE n)) (CategoryTheory.Functor.map Q (X.πTruncGE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap g n)))
  (CategoryTheory.Functor.map Q g ≫ CategoryTheory.Functor.map Q (Y'.πTruncGE n))
Tactic: simp only [Functor.map_comp] at eq eq'
Cleared hypotheses: eq, eq'