awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} 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''
α : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)
hα : δ (n - 1) n α = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)
g : K.X p'' ⟶ X
hg : Cochain.toSingleMk g ⋯ = α
hα₁ :
  HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) n) n.negOnePow
      (Cochain.toSingleMk (K.d p p'' ≫ g) h) =
    Cochain.toSingleMk f h
⊢ Cochain.toSingleMk g ⋯ = α

Tactic:
rw [← hg, toSingleMk_coe, Cochain.δ_toSingleMk _ _ _ _ h] at hα

Premises used: CochainComplex.HomComplex.Cocycle.toSingleMk_coe, CochainComplex.HomComplex.Cochain.δ_toSingleMk
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} 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''
α : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)
g : K.X p'' ⟶ X
hα :
  HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) n) n.negOnePow
      (Cochain.toSingleMk (K.d p p'' ≫ g) h) =
    Cochain.toSingleMk f h
hg : Cochain.toSingleMk g ⋯ = α
⊢ Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) n)
    ((AddEquiv.symm (Cochain.toSingleEquiv h) : (a : K.X p ⟶ X) → Cochain K ((singleFunctor C q).obj X) n)
        (K.d p p'' ≫ (n.negOnePow • g)) :
      Cochain K (Functor.obj (singleFunctor C q) X) n)
    ((AddEquiv.symm (Cochain.toSingleEquiv h) : (a : K.X p ⟶ X) → Cochain K ((singleFunctor C q).obj X) n) f :
      Cochain K (Functor.obj (singleFunctor C q) X) n)

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} 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''
α : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)
g : K.X p'' ⟶ X
hα :
  HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) n) n.negOnePow
      (Cochain.toSingleMk (K.d p p'' ≫ g) h) =
    Cochain.toSingleMk f h
hg : Cochain.toSingleMk g ⋯ = α
⊢ K.d p p'' ≫ (n.negOnePow • g) = f

Tactic:
exact (Cochain.toSingleEquiv h).symm.injective (by simpa)

Premises used: CochainComplex.HomComplex.Cochain.toSingleEquiv, AddEquiv.injective, AddEquiv.symm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
p'' : ℤ
hp'' : p + 1 = p''
g : K.X p'' ⟶ X
hf : K.d p' p ≫ K.d p p'' ≫ g = 0
⊢ p'' + (n - 1) = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
p'' : ℤ
hp'' : p + 1 = p''
g : K.X p'' ⟶ X
hf : K.d p' p ≫ K.d p p'' ≫ g = 0
⊢ δ (n - 1) n
      (HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)) n.negOnePow (Cochain.toSingleMk g ⋯)) =
    (↑(toSingleMk (K.d p p'' ≫ g) h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)

Tactic:
simp [Cochain.δ_toSingleMk _ _ _ _ h, smul_smul]

Premises used: smul_smul, CochainComplex.HomComplex.Cochain.δ_toSingleMk
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
p'' : ℤ
hp'' : p + 1 = p''
g : K.X p'' ⟶ X
hf : K.d p' p ≫ K.d p p'' ≫ g = 0
⊢ ∃ (β : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)),
    δ (n - 1) n β = (↑(toSingleMk (K.d p p'' ≫ g) h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)

Tactic:
exact ⟨n.negOnePow • Cochain.toSingleMk g (by lia),
      by simp [Cochain.δ_toSingleMk _ _ _ _ h, smul_smul]⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@CategoryTheory.Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
⊢ ∃ (S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)) (σ :
    (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))),
    Nonempty.{v_1 + 1} (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)

Tactic:
rw [distinguished_iff_iso_trianglehOfDegreewiseSplit] at hT

Premises used: HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT_1 :
  Membership.mem (γ := Set (Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@CategoryTheory.Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
hT :
  ∃ (S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)) (σ :
    (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))),
    Nonempty.{v_1 + 1} (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)
obtain :
  ∀ (S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ))
    (σ : (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)))
    (e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ),
    ∃ (T' : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))) (e : T ≅ T'),
      ShortComplex.Exact
        ((Pretriangulated.shortComplexOfDistTriangle T' ⋯).map (homologyFunctor C (ComplexShape.up ℤ) n))
⊢ ∃ (T' : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))) (e : T ≅ T'),
    ShortComplex.Exact ((Pretriangulated.shortComplexOfDistTriangle T' ⋯).map (homologyFunctor C (ComplexShape.up ℤ) n))

Tactic:
obtain ⟨S, σ, ⟨e⟩⟩ := hT
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@CategoryTheory.Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
⊢ S.ShortExact

Tactic:
have hS := HomologicalComplex.shortExact_of_degreewise_shortExact S
      (fun n => (σ n).shortExact)
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@CategoryTheory.Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
hS : S.ShortExact
⊢ ∃ (T' : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))) (e : T ≅ T'),
    ShortComplex.Exact ((Pretriangulated.shortComplexOfDistTriangle T' ⋯).map (homologyFunctor C (ComplexShape.up ℤ) n))

Tactic:
⟨_, e, (ShortComplex.exact_iff_of_iso
      (S.mapNatIso (homologyFunctorFactors C (ComplexShape.up ℤ) n))).2 (hS.homology_exact₂ n)⟩

Premises used: Iff.mpr, HomotopyCategory.homologyFunctorFactors, CategoryTheory.ShortComplex.exact_iff_of_iso, Int, Exists.intro, CategoryTheory.ShortComplex.mapNatIso, ComplexShape.up, CategoryTheory.ShortComplex.ShortExact.homology_exact₂
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@CategoryTheory.Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
hS : S.ShortExact
⊢ ∃ (T' : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))) (e : T ≅ T'),
    ShortComplex.Exact ((Pretriangulated.shortComplexOfDistTriangle T' ⋯).map (homologyFunctor C (ComplexShape.up ℤ) n))

Tactic:
exact ⟨_, e, (ShortComplex.exact_iff_of_iso
      (S.mapNatIso (homologyFunctorFactors C (ComplexShape.up ℤ) n))).2 (hS.homology_exact₂ n)⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L₁ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
e : HomotopyEquiv L₁ L₂
inst_2 : L₁.IsKInjective
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L₂
hK : HomologicalComplex.Acyclic K
⊢ f = f ≫ 𝟙 L₂

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L₁ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
e : HomotopyEquiv L₁ L₂
inst_2 : L₁.IsKInjective
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L₂
hK : HomologicalComplex.Acyclic K
⊢ f ≫ e.inv ≫ e.hom = (f ≫ e.inv) ≫ e.hom

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L₁ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
e : HomotopyEquiv L₁ L₂
inst_2 : L₁.IsKInjective
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L₂
hK : HomologicalComplex.Acyclic K
⊢ Eq (α := K ⟶ L₂) (0 ≫ e.hom) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L₁ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
e : L₁ ≅ L₂
inst_2 : L₁.IsKInjective
⊢ L₂.IsKInjective

Tactic:
(HomotopyEquiv.ofIso e).isKInjective

Premises used: HomotopyEquiv.ofIso, HomotopyEquiv.isKInjective
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L₁ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
e : L₁ ≅ L₂
⊢ L₁.IsKInjective ↔ L₂.IsKInjective

Tactic:
⟨fun _ ↦ isKInjective_of_iso e, fun _ ↦ isKInjective_of_iso e.symm⟩

Premises used: CochainComplex.isKInjective_of_iso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ L.IsKInjective ↔
    ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)

Tactic:
⟨fun _ K f hK ↦ ?_,
      fun hL ↦ ⟨fun {K} f hK ↦ ⟨HomotopyCategory.homotopyOfEq _ _ ?_⟩⟩⟩

Premises used: Nonempty.intro, CochainComplex.IsKInjective.mk, Iff.intro, HomotopyCategory.homotopyOfEq, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
refine_1 :
  L.IsKInjective →
    ∀ (K : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
      (f : K ⟶ Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
      (hK : HomotopyCategory.subcategoryAcyclic C K), f = 0
refine_2 :
  ∀
    (hL :
      ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L))
    {K : CochainComplex.{v_1, u_1, 0} C ℤ} (f : K ⟶ L) (hK : HomologicalComplex.Acyclic K),
    Eq (α :=
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)
⊢ L.IsKInjective ↔
    ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)

Tactic:
refine ⟨fun _ K f hK ↦ ?_,
      fun hL ↦ ⟨fun {K} f hK ↦ ⟨HomotopyCategory.homotopyOfEq _ _ ?_⟩⟩⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
h : L.IsKInjective
K : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)
f : K ⟶ Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L
hK : HomotopyCategory.subcategoryAcyclic C K
refine_1 :
  ∀ (K : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ))
    (f :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (hK : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)),
    f = 0
⊢ f = 0

Tactic:
obtain ⟨K, rfl⟩ := HomotopyCategory.quotient_obj_surjective K

Premises used: HomotopyCategory.quotient_obj_surjective, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
h : L.IsKInjective
K : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
f :
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L
hK : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
refine_1 :
  ∀ (f : K ⟶ L),
    Eq (α :=
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f) 0
⊢ f = 0

Tactic:
obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective f

Premises used: HomotopyCategory.quotient, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
h : L.IsKInjective
K : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hK : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
f : K ⟶ L
refine_1 :
  ∀ (hK : K.Acyclic) (f : K ⟶ L),
    Eq (α :=
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f) 0
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f) 0

Tactic:
rw [HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hK

Premises used: HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
h : L.IsKInjective
K : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hK : K.Acyclic
f : K ⟶ L
refine_1 :
  Eq.{v_1 + 1} (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0) 0
refine_1₁ refine_1₂ :
  Eq.{v_1 + 1} (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    0 0
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f) 0

Tactic:
rw [HomotopyCategory.eq_of_homotopy f 0 (IsKInjective.homotopyZero f hK), Functor.map_zero]

Premises used: HomotopyCategory.eq_of_homotopy, CategoryTheory.Functor.map_zero, CochainComplex.IsKInjective.homotopyZero, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
hL :
  ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
⊢ HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)

Tactic:
rw [← HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hK

Premises used: HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
hL :
  ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
refine_2 :
  Eq.{max 1 (v_1 + 1)} (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    0 (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)
refine_2₁ refine_2₂ :
  Eq.{max 1 (v_1 + 1)} (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    0 0
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)

Tactic:
rw [hL ((HomotopyCategory.quotient _ _).map f) hK, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map, HomotopyCategory.quotient
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 rwa rwa₁ rwa₂ rwa₃ : L.IsKInjective
⊢ ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)

Tactic:
rwa [← isKInjective_iff_rightOrthogonal]

Premises used: CochainComplex.isKInjective_iff_rightOrthogonal
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
hL : L.IsKInjective
n : ℤ
rw :
  ∀
    (hL :
      ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L))
    (n : ℤ),
    ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L))
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L).IsKInjective

Tactic:
rw [isKInjective_iff_rightOrthogonal] at hL ⊢

Premises used: CochainComplex.isKInjective_iff_rightOrthogonal
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
hL :
  ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
n : ℤ
⊢ ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L))

Tactic:
ObjectProperty.prop_of_iso _
    (((HomotopyCategory.quotient C (.up ℤ)).commShiftIso n).symm.app L)
    ((HomotopyCategory.subcategoryAcyclic C).rightOrthogonal.le_shift n _ hL)

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.ObjectProperty.rightOrthogonal, Int, CategoryTheory.Iso.symm, HomotopyCategory.subcategoryAcyclic, HomotopyCategory.quotient, CategoryTheory.Iso.app, CategoryTheory.Functor.CommShift.commShiftIso, ComplexShape.up, CategoryTheory.ObjectProperty.le_shift
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
hL :
  ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
n : ℤ
⊢ ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L))

Tactic:
exact ObjectProperty.prop_of_iso _
    (((HomotopyCategory.quotient C (.up ℤ)).commShiftIso n).symm.app L)
    ((HomotopyCategory.subcategoryAcyclic C).rightOrthogonal.le_shift n _ hL)
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L).IsKInjective ↔ L.IsKInjective

Tactic:
⟨fun _ ↦ isKInjective_of_iso (show L⟦n⟧⟦-n⟧ ≅ L from (shiftEquiv _ n).unitIso.symm.app L),
    fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.Equivalence.unitIso, inferInstance, CochainComplex.isKInjective_of_iso, Int, CategoryTheory.shiftEquiv, CochainComplex, Iff.intro, CategoryTheory.Iso.symm, CategoryTheory.Iso.app
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n m : ℤ
hnm : n + 1 = m
hK : HomologicalComplex.ExactAt K m
inst_2 : Injective.{v_1, u_1} (L.X m)
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
subst :
  ∀ (hK : HomologicalComplex.ExactAt K (n + 1)) [Injective.{v_1, u_1} (L.X (n + 1))],
    ∃ (h : K.X (n + 2) ⟶ L.X (n + 1)), Cochain.EqUpTo (δ (-1) 0 (α + Cochain.single h (-1))) (Cochain.ofHom f) (n + 1)
⊢ ∃ (h : K.X (n + 2) ⟶ L.X (n + 1)), Cochain.EqUpTo (δ (-1) 0 (α + Cochain.single h (-1))) (Cochain.ofHom f) m

Tactic:
subst hnm