awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : CochainComplex.{v_1, u_1, 0} C ℕ
inst_2 : ∀ (n : ℕ), Injective.{v_1, u_1} (K.X n)
⊢ IsKInjective (HomologicalComplex.extend K ComplexShape.embeddingUpNat)

Tactic:
isKInjective_of_injective _ 0

Premises used: CochainComplex.isKInjective_of_injective, 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
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
obtain :
  ∀ (φ : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L)
    (hφ :
      (Cocycle.equivHom K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) :
            (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) →
              Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) 0)
          φ =
        z.rightShift n 0 ⋯),
    ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)
⊢ ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)

Tactic:
obtain ⟨φ, hφ⟩ := (Cocycle.equivHom ..).surjective (z.rightShift n 0 (zero_add n))

Premises used: zero_add, AddEquiv.surjective, CochainComplex.HomComplex.Cocycle.rightShift, CochainComplex.HomComplex.Cocycle.equivHom, 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
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L
hφ :
  (Cocycle.equivHom K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) :
        (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) →
          Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) 0)
      φ =
    z.rightShift n 0 ⋯
⊢ (↑((Cocycle.equivHom K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) :
            (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) →
              Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) 0)
          φ) :
      Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) 0) =
    (↑(z.rightShift n 0 ⋯) : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) 0)

Tactic:
rw [Cocycle.ext_iff] at hφ

Premises used: CochainComplex.HomComplex.Cocycle.ext_iff
-- 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 ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L
hφ : Cochain.ofHom φ = (↑z : Cochain K L n).rightShift n 0 ⋯
obtain : ∀ (h : Homotopy φ 0), ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)
⊢ ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)

Tactic:
obtain ⟨h⟩ := IsKInjective.nonempty_homotopy_zero φ hK

Premises used: CochainComplex.IsKInjective.nonempty_homotopy_zero
-- 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 ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L
hφ : Cochain.ofHom φ = (↑z : Cochain K L n).rightShift n 0 ⋯
h : Homotopy φ 0
obtain :
  ∀ (f : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) (-1))
    (hf : Cochain.ofHom φ = δ (-1) 0 f + Cochain.ofHom 0), ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)
⊢ ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)

Tactic:
obtain ⟨f, hf⟩ := Cochain.equivHomotopy _ _ h

Premises used: CochainComplex.HomComplex.Cochain.equivHomotopy, DFunLike.coe
-- 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 ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L
hφ : Cochain.ofHom φ = (↑z : Cochain K L n).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f + Cochain.ofHom 0
⊢ Cochain.ofHom φ = δ (-1) 0 f

Tactic:
simp only [Int.reduceNeg, Cochain.ofHom_zero, add_zero] at hf

Premises used: Int.reduceNeg, CochainComplex.HomComplex.Cochain.ofHom_zero, add_zero
-- 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 ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L
hφ : Cochain.ofHom φ = (↑z : Cochain K L n).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
⊢ -1 + n = m

Tactic:
lia
-- 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 ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L
hφ : Cochain.ofHom φ = (↑z : Cochain K L n).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
refine : δ m n (n.negOnePow • f.rightUnshift m ⋯) = (↑z : Cochain K L n)
⊢ ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)

Tactic:
refine ⟨n.negOnePow • Cochain.rightUnshift f m (by lia), ?_⟩
-- 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 ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L
hφ : Cochain.ofHom φ = (↑z : Cochain K L n).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
⊢ 0 + n = n

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
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L
hφ : Cochain.ofHom φ = (↑z : Cochain K L n).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
a :
  Eq (α := Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) 0)
    ((Cochain.rightShiftAddEquiv K L n n 0 ⋯ :
          (a : Cochain K L n) → Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) 0)
        (δ m n (n.negOnePow • f.rightUnshift m ⋯)) :
      Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) 0)
    ((Cochain.rightShiftAddEquiv K L n n 0 ⋯ :
          (a : Cochain K L n) → Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) 0)
        (↑z : Cochain K L n) :
      Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) 0)
⊢ δ m n (n.negOnePow • f.rightUnshift m ⋯) = (↑z : Cochain K L n)

Tactic:
apply (Cochain.rightShiftAddEquiv _ _ _ n 0 (by simp)).injective

Premises used: AddEquiv.injective, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv, 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
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L
hφ : Cochain.ofHom φ = (↑z : Cochain K L n).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
a : (δ m n (n.negOnePow • f.rightUnshift m ⋯)).rightShift n 0 ⋯ = (↑z : Cochain K L n).rightShift n 0 ⋯
⊢ Eq (α := Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) 0)
    ((Cochain.rightShiftAddEquiv K L n n 0 ⋯ :
          (a : Cochain K L n) → Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) 0)
        (δ m n (n.negOnePow • f.rightUnshift m ⋯)) :
      Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) 0)
    ((Cochain.rightShiftAddEquiv K L n n 0 ⋯ :
          (a : Cochain K L n) → Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) 0)
        (↑z : Cochain K L n) :
      Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) 0)

Tactic:
dsimp
-- 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 ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L
hφ : Cochain.ofHom φ = (↑z : Cochain K L n).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
a : n.negOnePow • (n.negOnePow • Cochain.rightUnshift (δ (-1) 0 f) n ⋯).rightShift n 0 ⋯ = δ (-1) 0 f
⊢ (δ m n (n.negOnePow • f.rightUnshift m ⋯)).rightShift n 0 ⋯ = (↑z : Cochain K L n).rightShift n 0 ⋯

Tactic:
rw [← hφ, hf, δ_units_smul, Cochain.rightShift_units_smul,
    Cochain.δ_rightUnshift _ _ _ _ 0 (by simp)]

Premises used: CochainComplex.HomComplex.δ_units_smul, CochainComplex.HomComplex.Cochain.rightShift_units_smul, CochainComplex.HomComplex.Cochain.δ_rightUnshift, 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
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L
hφ : Cochain.ofHom φ = (↑z : Cochain K L n).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
⊢ n.negOnePow • (n.negOnePow • Cochain.rightUnshift (δ (-1) 0 f) n ⋯).rightShift n 0 ⋯ = δ (-1) 0 f

Tactic:
simp [smul_smul]

Premises used: smul_smul
-- 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 ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
⊢ HAdd.hAdd (α := ℤ) (-1) 1 = 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
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
obtain :
  ∀ (β : Cochain L L (-1)) (hβ : δ (-1) 0 β = (↑(Cocycle.ofHom (𝟙 L)) : Cochain L L 0)),
    ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)
⊢ ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)

Tactic:
obtain ⟨β, hβ⟩ :=
    IsKInjective.eq_δ_of_cocycle (Cocycle.ofHom (𝟙 L)) hL (-1) (by simp)

Premises used: CochainComplex.IsKInjective.eq_δ_of_cocycle, CategoryTheory.CategoryStruct.id, CochainComplex.HomComplex.Cocycle.ofHom, OfNat.ofNat, Neg.neg
-- 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 ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
β : Cochain L L (-1)
hβ : δ (-1) 0 β = (↑(Cocycle.ofHom (𝟙 L)) : Cochain L L 0)
⊢ n + -1 = m

Tactic:
lia
-- 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 ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
β : Cochain L L (-1)
hβ : δ (-1) 0 β = (↑(Cocycle.ofHom (𝟙 L)) : Cochain L L 0)
⊢ HAdd.hAdd (α := ℤ) (-1) 1 = 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
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
β : Cochain L L (-1)
hβ : δ (-1) 0 β = (↑(Cocycle.ofHom (𝟙 L)) : Cochain L L 0)
⊢ δ m n ((↑z : Cochain K L n).comp β ⋯) = (↑z : Cochain K L n)

Tactic:
simp [δ_comp z.1 β _ _ 0 _ hm rfl (by simp), hβ]

Premises used: CochainComplex.HomComplex.δ_comp, OfNat.ofNat, Subtype.val, 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
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
z : Cocycle K L n
inst_2 : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
β : Cochain L L (-1)
hβ : δ (-1) 0 β = (↑(Cocycle.ofHom (𝟙 L)) : Cochain L L 0)
⊢ ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)

Tactic:
exact ⟨z.1.comp β (by lia), by simp [δ_comp z.1 β _ _ 0 _ hm rfl (by simp), hβ]⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K₁ K₂ : CochainComplex.{v_1, u_1, 0} C ℤ
e : HomotopyEquiv K₁ K₂
inst_2 : K₁.IsKProjective
L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K₂ ⟶ L
hL : HomologicalComplex.Acyclic L
⊢ f = 𝟙 K₂ ≫ f

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

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

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

Tactic:
(HomotopyEquiv.ofIso e).isKProjective

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

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

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

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

Premises used: Nonempty.intro, Iff.intro, HomotopyCategory.homotopyOfEq, OfNat.ofNat, CochainComplex.IsKProjective.mk
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
refine_1 :
  K.IsKProjective →
    ∀ (L : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
      (f : Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶ L)
      (hL : HomotopyCategory.subcategoryAcyclic C L), f = 0
refine_2 :
  ∀
    (hK :
      ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
    {L : CochainComplex.{v_1, u_1, 0} C ℤ} (f : K ⟶ L) (hL : HomologicalComplex.Acyclic 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)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)
⊢ K.IsKProjective ↔
    ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)

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

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

Premises used: HomotopyCategory.quotient_obj_surjective, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
h : K.IsKProjective
L : 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
hL : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
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.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
h : K.IsKProjective
L : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hL : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
f : K ⟶ L
refine_1 :
  ∀ (hL : L.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 hL

Premises used: HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
h : K.IsKProjective
L : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hL : L.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 (IsKProjective.homotopyZero f hL), Functor.map_zero]

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

Tactic:
rw [← HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hL

Premises used: HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic