awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} 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
⊢ HSub.hSub (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n) =
    (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk
        (Cocycle.toSingleMk
          ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f - (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯
          (-(↑m : ℤ)) ⋯ ⋯))
have rw : HSub.hSub (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
    ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry sorry)) :
      Ext.{w, v, u} X Y n)
    ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ g) sorry (-(↑m : ℤ)) sorry sorry)) :
      Ext.{w, v, u} X Y n) =
  (Equiv.symm R.extEquivCohomologyClass :
      (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
    (CohomologyClass.mk
      (HSub.hSub (α := Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
        (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry sorry)
        (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ g) sorry (-(↑m : ℤ)) sorry sorry)))
Tactic: rw [Cocycle.toSingleMk_sub _ _ _ _ _
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (-R.extMk f m hm hf) (R.extMk (-f) m hm ⋯)
have simp : Eq.{w + 1} (α := Ext.{w, v, u} X Y n)
  (-(Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry sorry)) :
    Ext.{w, v, u} X Y n)
  ((Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk (Cocycle.toSingleMk (-(R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry sorry)) :
    Ext.{w, v, u} X Y n)
Tactic: simp only [extMk, Preadditive.comp_neg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y n)
    (-(Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
      Ext.{w, v, u} X Y n)
    ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk (-(R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
      Ext.{w, v, u} X Y n)
have rw : Eq.{w + 1} (α := Ext.{w, v, u} X Y n)
  (-(Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry sorry)) :
    Ext.{w, v, u} X Y n)
  ((Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk (-Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry sorry)) :
    Ext.{w, v, u} X Y n)
Tactic: rw [Cocycle.toSingleMk_neg _ _ _ _
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} 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
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (R.extMk f m hm hf) 0 ↔ ∃ (g : R.complex.X p ⟶ Y), R.complex.d n p ≫ g = f
have simp : Membership.mem (γ := AddSubgroup (Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)))
    (coboundaries R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry sorry) ↔
  ∃ (g : R.complex.X p ⟶ Y), R.complex.d n p ≫ g = f
Tactic: simp only [← R.extEquivCohomologyClass.apply_eq_iff_eq,
    extEquivCohomologyClass_extMk, extEquivCohomologyClass_zero,
    CohomologyClass.mk_eq_zero_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} 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
⊢ Membership.mem (γ := AddSubgroup (Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)))
      (coboundaries R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
      (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯) ↔
    ∃ (g : R.complex.X p ⟶ Y), R.complex.d n p ≫ g = f
have rw : (∃ (g : R.cochainComplex.X (-(↑p : ℤ)) ⟶ Y),
    ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p sorry).inv) ≫ g =
      (R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) ↔
  ∃ (g : R.complex.X p ⟶ Y), R.complex.d n p ≫ g = f
Tactic: rw [Cocycle.toSingleMk_mem_coboundaries_iff _ _ _ _ _ (-p) (by lia),
    R.cochainComplex_d _ _ _ _ rfl rfl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} 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.cochainComplex.X (-(↑p : ℤ)) ⟶ Y),
      ((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.X p ⟶ Y), R.complex.d n p ≫ g = f
have refine : (∃ (g : R.cochainComplex.X (-(↑p : ℤ)) ⟶ Y),
    ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p sorry).inv) ≫ g =
      (R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) →
  ∀ (g : R.cochainComplex.X (-(↑p : ℤ)) ⟶ Y)
    (hg :
      ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p sorry).inv) ≫ g =
        (R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f),
    R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p sorry).inv ≫ g = f
Tactic: refine ⟨fun ⟨g, hg⟩ ↦ ⟨(R.cochainComplexXIso (-p) p rfl).inv ≫ g, ?_⟩,
    fun ⟨g, hg⟩ ↦ ⟨(R.cochainComplexXIso (-p) p rfl).hom ≫ g, by simpa⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} 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
h :
  ∃ (g : R.cochainComplex.X (-(↑p : ℤ)) ⟶ Y),
    ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p ⋯).inv) ≫ g =
      (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f
g : R.cochainComplex.X (-(↑p : ℤ)) ⟶ Y
hg :
  ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p ⋯).inv) ≫ g =
    (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f
⊢ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p ⋯).inv ≫ g = f
have rw : (R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p sorry).inv ≫ g =
  (R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f
Tactic: rw [← cancel_epi (R.cochainComplexXIso (-n) n rfl).hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
α : Ext.{w, v, u} X Y n
m : ℕ
hm : n + 1 = m
⊢ ∃ (f : R.complex.X n ⟶ Y) (hf : R.complex.d m n ≫ f = 0), R.extMk f m hm hf = α
have obtain : ∀ (x : CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)),
  ∃ (f : R.complex.X n ⟶ Y) (hf : R.complex.d m n ≫ f = 0),
    Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (R.extMk f m hm hf)
      ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        x)
Tactic: obtain ⟨x, rfl⟩ := R.extEquivCohomologyClass.symm.surjective α
Cleared hypotheses: α
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n m : ℕ
hm : n + 1 = m
x : CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)
⊢ ∃ (f : R.complex.X n ⟶ Y) (hf : R.complex.d m n ≫ f = 0),
    Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (R.extMk f m hm hf)
      ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        x)
have obtain : ∀ (x : Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)),
  ∃ (f : R.complex.X n ⟶ Y) (hf : R.complex.d m n ≫ f = 0),
    Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (R.extMk f m hm hf)
      ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk x))
Tactic: obtain ⟨x, rfl⟩ := x.mk_surjective
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n m : ℕ
hm : n + 1 = m
x : Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)
⊢ ∃ (f : R.complex.X n ⟶ Y) (hf : R.complex.d m n ≫ f = 0),
    Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (R.extMk f m hm hf)
      ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk x))
have obtain : ∀ (f : R.cochainComplex.X (-(↑n : ℤ)) ⟶ Y)
  (hf : Eq (α := R.cochainComplex.X (-(↑m : ℤ)) ⟶ Y) (R.cochainComplex.d (-(↑m : ℤ)) (-(↑n : ℤ)) ≫ f) 0),
  ∃ (f_1 : R.complex.X n ⟶ Y) (hf_1 : R.complex.d m n ≫ f_1 = 0),
    Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (R.extMk f_1 m hm hf_1)
      ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk f sorry (-(↑m : ℤ)) sorry hf)))
Tactic: obtain ⟨f, hf, rfl⟩ := Cocycle.toSingleMk_surjective x (-n) (by simp) (-m) (by lia)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n m : ℕ
hm : n + 1 = m
f : R.cochainComplex.X (-(↑n : ℤ)) ⟶ Y
hf : Eq (α := R.cochainComplex.X (-(↑m : ℤ)) ⟶ Y) (R.cochainComplex.d (-(↑m : ℤ)) (-(↑n : ℤ)) ≫ f) 0
⊢ ∃ (f_1 : R.complex.X n ⟶ Y) (hf_1 : R.complex.d m n ≫ f_1 = 0),
    Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (R.extMk f_1 m hm hf_1)
      ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk f ⋯ (-(↑m : ℤ)) ⋯ hf)))
have refine : R.complex.d m n ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n sorry).inv ≫ f = 0
Tactic: refine ⟨(R.cochainComplexXIso (-n) n rfl).inv ≫ f, ?_, by simp [extMk]⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n m : ℕ
hm : n + 1 = m
f : R.cochainComplex.X (-(↑n : ℤ)) ⟶ Y
hf : Eq (α := R.cochainComplex.X (-(↑m : ℤ)) ⟶ Y) (R.cochainComplex.d (-(↑m : ℤ)) (-(↑n : ℤ)) ≫ f) 0
⊢ R.complex.d m n ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).inv ≫ f = 0
have rw : (R.cochainComplexXIso (-(↑m : ℤ)) m sorry).hom ≫ R.complex.d m n ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n sorry).inv ≫ f =
  (R.cochainComplexXIso (-(↑m : ℤ)) m sorry).hom ≫ 0
Tactic: rw [← cancel_epi (R.cochainComplexXIso (-m) m rfl).hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y' n) (Ext.comp (R.extMk f m hm hf) (Ext.mk₀ g) ⋯) (R.extMk (f ≫ g) m hm ⋯)
have have : ∀ (this : HasDerivedCategory C),
  Eq.{w + 1} (α := Ext.{w, v, u} X Y' n) (Ext.comp (R.extMk f m hm hf) (Ext.mk₀ g) sorry) (R.extMk (f ≫ g) m hm sorry)
Tactic: have := HasDerivedCategory.standard C
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y' n) (Ext.comp (R.extMk f m hm hf) (Ext.mk₀ g) ⋯) (R.extMk (f ≫ g) m hm ⋯)
have h : Eq (α :=
  ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
    (Functor.obj (DerivedCategory.singleFunctor C 0) Y') (↑n : ℤ))
  (Ext.hom (Ext.comp (R.extMk f m hm hf) (Ext.mk₀ g) sorry)) (Ext.hom (R.extMk (f ≫ g) m hm sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y') (↑n : ℤ))
    (Ext.hom (Ext.comp (R.extMk f m hm hf) (Ext.mk₀ g) ⋯)) (Ext.hom (R.extMk (f ≫ g) m hm ⋯))
have h : Eq (α :=
  ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
    (Functor.obj (DerivedCategory.singleFunctor C 0) Y') (↑n : ℤ))
  (ShiftedHom.comp
    (ShiftedHom.comp
      (ShiftedHom.mk₀ 0 sorry
        (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫
          inv (Functor.map DerivedCategory.Q R.π')))
      (ShiftedHom.comp
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
            (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry sorry))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 sorry (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y)) sorry)
      sorry)
    (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 (Functor.map (DerivedCategory.singleFunctor C 0) g)) sorry)
  (ShiftedHom.comp
    (ShiftedHom.mk₀ 0 sorry
      (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫ inv (Functor.map DerivedCategory.Q R.π')))
    (ShiftedHom.comp
      (ShiftedHom.map
        ((AddEquiv.symm Cocycle.equivHomShift :
            (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y') (↑n : ℤ)) →
              R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y'))
          (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f ≫ g) sorry (-(↑m : ℤ)) sorry sorry))
        DerivedCategory.Q)
      (ShiftedHom.mk₀ 0 sorry (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y')) sorry)
    sorry)
Tactic: simp only [extMk, Ext.comp_hom, Int.cast_ofNat_Int, Ext.mk₀_hom,
    extEquivCohomologyClass_symm_mk_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X' Y n) (Ext.comp (Ext.mk₀ g) (R.extMk f m hm hf) ⋯) (R'.extMk (φ.hom.f n ≫ f) m hm ⋯)
have have : ∀ (this : HasDerivedCategory C),
  Eq.{w + 1} (α := Ext.{w, v, u} X' Y n) (Ext.comp (Ext.mk₀ g) (R.extMk f m hm hf) sorry) (R'.extMk (φ.hom.f n ≫ f) m hm sorry)
Tactic: have := HasDerivedCategory.standard C
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this : HasDerivedCategory C
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X' Y n) (Ext.comp (Ext.mk₀ g) (R.extMk f m hm hf) ⋯) (R'.extMk (φ.hom.f n ≫ f) m hm ⋯)
have h : Eq (α :=
  ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X')
    (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
  (Ext.hom (Ext.comp (Ext.mk₀ g) (R.extMk f m hm hf) sorry)) (Ext.hom (R'.extMk (φ.hom.f n ≫ f) m hm sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this : HasDerivedCategory C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X')
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
    (Ext.hom (Ext.comp (Ext.mk₀ g) (R.extMk f m hm hf) ⋯)) (Ext.hom (R'.extMk (φ.hom.f n ≫ f) m hm ⋯))
have this₁ : (R'.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ φ.hom.f n =
  φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom
Tactic: have : (R'.cochainComplexXIso (-n) n (by lia)).hom ≫ φ.hom.f n =
      φ.hom'.f (-n) ≫ (R.cochainComplexXIso (-n) n (by lia)).hom := by
    simp [φ.hom'_f _ _ rfl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this_1 : HasDerivedCategory C
this :
  (R'.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ φ.hom.f n =
    φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X')
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
    (Ext.hom (Ext.comp (Ext.mk₀ g) (R.extMk f m hm hf) ⋯)) (Ext.hom (R'.extMk (φ.hom.f n ≫ f) m hm ⋯))
have h : Eq (α :=
  ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X')
    (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
  (ShiftedHom.comp (ShiftedHom.mk₀ (↑0 : ℤ) Ext.mk₀._proof_1 (Functor.map (DerivedCategory.singleFunctor C 0) g))
    (ShiftedHom.comp
      (ShiftedHom.mk₀ 0 sorry
        (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫
          inv (Functor.map DerivedCategory.Q R.π')))
      (ShiftedHom.comp
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
            (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry sorry))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 sorry (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y)) sorry)
      sorry)
    sorry)
  (ShiftedHom.comp
    (ShiftedHom.mk₀ 0 sorry
      (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X' ≫
        inv (Functor.map DerivedCategory.Q R'.π')))
    (ShiftedHom.comp
      (ShiftedHom.map
        ((AddEquiv.symm Cocycle.equivHomShift :
            (a : Cocycle R'.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
              R'.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
          (Cocycle.toSingleMk (φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry
            sorry))
        DerivedCategory.Q)
      (ShiftedHom.mk₀ 0 sorry (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y)) sorry)
    sorry)
Tactic: simp only [Ext.comp_hom, extMk_hom, Ext.mk₀_hom, reassoc_of% this]