awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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 ℤ
d : ℤ
inst_2 : L.IsStrictlyGE d
inst_3 : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : (n : ℕ) → Set (Cochain K L (-1)) :=
  fun (n : ℕ) ↦ {α : Cochain K L (-1) | Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) ((↑n : ℤ) + d - 1)}
x₀ : (↑(X 0) : Type v_1) := Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X 0) 0 ⋯
φ : (n : ℕ) → (α : (↑(X n) : Type v_1)) → (↑(X (n + 1)) : Type v_1) :=
  fun (n : ℕ) (α : (↑(X n) : Type v_1)) ↦
    Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X (n + 1))
      ((↑α : Cochain K L (-1)) +
        Cochain.single
          (⋯.choose (p := fun (h : K.X ((↑n : ℤ) + d - 1 + 2) ⟶ L.X ((↑n : ℤ) + d - 1 + 1)) ↦
            Cochain.EqUpTo (δ (-1) 0 ((↑α : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
              ((↑(n + 1) : ℤ) + d - 1)))
          (-1))
      ⋯
hφ : ∀ (k : ℕ) (x : (↑(X k) : Type v_1)), (↑(φ k x) : Cochain K L (-1)).EqUpTo (↑x : Cochain K L (-1)) (d + (↑k : ℤ))
n : ℤ
k₀ : ℕ := (n - d + 1).toNat
h :
  Cochain.v (δ (-1) 0 (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1))) n n ⋯ =
    Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n ⋯
⊢ (Cochain.ofHom f).v n n ⋯ = Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n ⋯
have h₁ : (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v n (n - 1) sorry ≫ L.d (n - 1) n +
    Int.negOnePow 0 •
      K.d n (n + 1) ≫ (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v (n + 1) n sorry =
  Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n sorry
Tactic: rw [← (sequence φ x₀ k₀).2 n n (add_zero n) (by lia),
      δ_v (-1) 0 (neg_add_cancel 1) _ n n (by lia) (n - 1) (n + 1) rfl (by lia),
      δ_v (-1) 0 (neg_add_cancel 1) _ n n (by lia) (n - 1) (n + 1) rfl (by lia),
      limitSequence_eqUpTo φ hφ x₀ k₀ n (n - 1) (by lia) (by lia),
      limitSequence_eqUpTo φ hφ x₀ k₀ (n + 1) n (by lia) (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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 ℤ
d : ℤ
inst_2 : L.IsStrictlyGE d
inst_3 : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : (n : ℕ) → Set (Cochain K L (-1)) :=
  fun (n : ℕ) ↦ {α : Cochain K L (-1) | Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) ((↑n : ℤ) + d - 1)}
x₀ : (↑(X 0) : Type v_1) := Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X 0) 0 ⋯
φ : (n : ℕ) → (α : (↑(X n) : Type v_1)) → (↑(X (n + 1)) : Type v_1) :=
  fun (n : ℕ) (α : (↑(X n) : Type v_1)) ↦
    Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X (n + 1))
      ((↑α : Cochain K L (-1)) +
        Cochain.single
          (⋯.choose (p := fun (h : K.X ((↑n : ℤ) + d - 1 + 2) ⟶ L.X ((↑n : ℤ) + d - 1 + 1)) ↦
            Cochain.EqUpTo (δ (-1) 0 ((↑α : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
              ((↑(n + 1) : ℤ) + d - 1)))
          (-1))
      ⋯
hφ : ∀ (k : ℕ) (x : (↑(X k) : Type v_1)), (↑(φ k x) : Cochain K L (-1)).EqUpTo (↑x : Cochain K L (-1)) (d + (↑k : ℤ))
n : ℤ
k₀ : ℕ := (n - d + 1).toNat
h :
  Cochain.v (δ (-1) 0 (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1))) n n ⋯ =
    Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n ⋯
h₁ :
  (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v n (n - 1) ⋯ ≫ L.d (n - 1) n +
      Int.negOnePow 0 •
        K.d n (n + 1) ≫ (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v (n + 1) n ⋯ =
    Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n ⋯
⊢ (Cochain.ofHom f).v n n ⋯ = Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n ⋯
have h₂ : (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v n (n - 1) sorry ≫ L.d (n - 1) n +
    Int.negOnePow 0 •
      K.d n (n + 1) ≫ (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v (n + 1) n sorry =
  (limitSequence (X := X) φ hφ x₀).v n (n - 1) sorry ≫ L.d (n - 1) n +
    Int.negOnePow 0 • K.d n (n + 1) ≫ (limitSequence (X := X) φ hφ x₀).v (n + 1) n sorry
Tactic: rw [← (sequence φ x₀ k₀).2 n n (add_zero n) (by lia),
      δ_v (-1) 0 (neg_add_cancel 1) _ n n (by lia) (n - 1) (n + 1) rfl (by lia),
      δ_v (-1) 0 (neg_add_cancel 1) _ n n (by lia) (n - 1) (n + 1) rfl (by lia),
      limitSequence_eqUpTo φ hφ x₀ k₀ n (n - 1) (by lia) (by lia),
      limitSequence_eqUpTo φ hφ x₀ k₀ (n + 1) n (by lia) (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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 ℤ
d : ℤ
inst_2 : L.IsStrictlyGE d
inst_3 : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : (n : ℕ) → Set (Cochain K L (-1)) :=
  fun (n : ℕ) ↦ {α : Cochain K L (-1) | Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) ((↑n : ℤ) + d - 1)}
x₀ : (↑(X 0) : Type v_1) := Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X 0) 0 ⋯
φ : (n : ℕ) → (α : (↑(X n) : Type v_1)) → (↑(X (n + 1)) : Type v_1) :=
  fun (n : ℕ) (α : (↑(X n) : Type v_1)) ↦
    Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X (n + 1))
      ((↑α : Cochain K L (-1)) +
        Cochain.single
          (⋯.choose (p := fun (h : K.X ((↑n : ℤ) + d - 1 + 2) ⟶ L.X ((↑n : ℤ) + d - 1 + 1)) ↦
            Cochain.EqUpTo (δ (-1) 0 ((↑α : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
              ((↑(n + 1) : ℤ) + d - 1)))
          (-1))
      ⋯
hφ : ∀ (k : ℕ) (x : (↑(X k) : Type v_1)), (↑(φ k x) : Cochain K L (-1)).EqUpTo (↑x : Cochain K L (-1)) (d + (↑k : ℤ))
n : ℤ
k₀ : ℕ := (n - d + 1).toNat
h :
  Cochain.v (δ (-1) 0 (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1))) n n ⋯ =
    Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n ⋯
h₁ :
  (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v n (n - 1) ⋯ ≫ L.d (n - 1) n +
      Int.negOnePow 0 •
        K.d n (n + 1) ≫ (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v (n + 1) n ⋯ =
    Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n ⋯
h₂ :
  (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v n (n - 1) ⋯ ≫ L.d (n - 1) n +
      Int.negOnePow 0 •
        K.d n (n + 1) ≫ (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v (n + 1) n ⋯ =
    (limitSequence (X := X) φ hφ x₀).v n (n - 1) ⋯ ≫ L.d (n - 1) n +
      Int.negOnePow 0 • K.d n (n + 1) ≫ (limitSequence (X := X) φ hφ x₀).v (n + 1) n ⋯
⊢ (Cochain.ofHom f).v n n ⋯ = Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n ⋯
have h₃ : (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v n (n - 1) sorry ≫ L.d (n - 1) n +
    Int.negOnePow 0 •
      K.d n (n + 1) ≫ (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v (n + 1) n sorry =
  (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v n (n - 1) sorry ≫ L.d (n - 1) n +
    Int.negOnePow 0 • K.d n (n + 1) ≫ (limitSequence (X := X) φ hφ x₀).v (n + 1) n sorry
Tactic: rw [← (sequence φ x₀ k₀).2 n n (add_zero n) (by lia),
      δ_v (-1) 0 (neg_add_cancel 1) _ n n (by lia) (n - 1) (n + 1) rfl (by lia),
      δ_v (-1) 0 (neg_add_cancel 1) _ n n (by lia) (n - 1) (n + 1) rfl (by lia),
      limitSequence_eqUpTo φ hφ x₀ k₀ n (n - 1) (by lia) (by lia),
      limitSequence_eqUpTo φ hφ x₀ k₀ (n + 1) n (by lia) (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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
⊢ ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)
have 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 sorry),
  ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)
Tactic: obtain ⟨φ, hφ⟩ := (Cocycle.equivHom ..).surjective (z.rightShift n 0 (zero_add n))
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (hypothesis)
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 ⋯
⊢ ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)
have 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)
        φ) :
    Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) 0) =
  (↑(z.rightShift n 0 sorry) : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) 0)
Tactic: rw [Cocycle.ext_iff] at hφ
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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 ⋯
⊢ ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)
have obtain : ∀ (h : Homotopy φ 0), ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)
Tactic: obtain ⟨h⟩ := IsKInjective.nonempty_homotopy_zero φ hK
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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
⊢ ∃ (α : Cochain K L m), δ m n α = (↑z : Cochain K L n)
have 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)
Tactic: obtain ⟨f, hf⟩ := Cochain.equivHomotopy _ _ h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (hypothesis)
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 K L m), δ m n α = (↑z : Cochain K L n)
have hf₁ : Cochain.ofHom φ = δ (-1) 0 f
Tactic: simp only [Int.reduceNeg, Cochain.ofHom_zero, add_zero] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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 K L m), δ m n α = (↑z : Cochain K L n)
have refine : δ m n (n.negOnePow • f.rightUnshift m sorry) = (↑z : Cochain K L n)
Tactic: refine ⟨n.negOnePow • Cochain.rightUnshift f m (by lia), ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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
⊢ δ m n (n.negOnePow • f.rightUnshift m ⋯) = (↑z : Cochain K L n)
have 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 sorry :
        (a : Cochain K L n) → Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) 0)
      (δ m n (n.negOnePow • f.rightUnshift m sorry)) :
    Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L) 0)
  ((Cochain.rightShiftAddEquiv K L n n 0 sorry :
        (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: apply (Cochain.rightShiftAddEquiv _ _ _ n 0 (by simp)).injective
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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
⊢ 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)
have a : (δ m n (n.negOnePow • f.rightUnshift m sorry)).rightShift n 0 sorry = (↑z : Cochain K L n).rightShift n 0 sorry
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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
⊢ (δ m n (n.negOnePow • f.rightUnshift m ⋯)).rightShift n 0 ⋯ = (↑z : Cochain K L n).rightShift n 0 ⋯
have a : n.negOnePow • (n.negOnePow • Cochain.rightUnshift (δ (-1) 0 f) n sorry).rightShift n 0 sorry = δ (-1) 0 f
Tactic: rw [← hφ, hf, δ_units_smul, Cochain.rightShift_units_smul,
    Cochain.δ_rightUnshift _ _ _ _ 0 (by simp)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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 K L m), δ m n α = (↑z : Cochain K L n)
have 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)
Tactic: obtain ⟨β, hβ⟩ :=
    IsKInjective.eq_δ_of_cocycle (Cocycle.ofHom (𝟙 L)) hL (-1) (by simp)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KProjective (goal)
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)
have 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
Tactic: refine ⟨fun _ L f hL ↦ ?_,
      fun hK ↦ ⟨fun {L} f hL ↦ ⟨HomotopyCategory.homotopyOfEq _ _ ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KProjective (goal)
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
⊢ K.IsKProjective ↔
    ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
have 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)
Tactic: refine ⟨fun _ L f hL ↦ ?_,
      fun hK ↦ ⟨fun {L} f hL ↦ ⟨HomotopyCategory.homotopyOfEq _ _ ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KProjective (goal)
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
⊢ f = 0
have 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
Tactic: obtain ⟨L, rfl⟩ := HomotopyCategory.quotient_obj_surjective L
Cleared hypotheses: L, f, hL
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KProjective (goal)
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)
⊢ f = 0
have 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
Tactic: obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KProjective (goal)
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
⊢ 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
have 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
Tactic: rw [HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hL
Cleared hypotheses: hL, f
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KProjective (goal)
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
⊢ 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
have 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
Tactic: rw [HomotopyCategory.eq_of_homotopy f 0 (IsKProjective.homotopyZero f hL), Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KProjective (goal)
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
⊢ 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
have refine_1₁ : Eq.{v_1 + 1} (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
  0 0
Tactic: rw [HomotopyCategory.eq_of_homotopy f 0 (IsKProjective.homotopyZero f hL), Functor.map_zero]