awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
h : p'' = p'
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
have pos : ∀ (hp' : p'' + 1 = p),
  (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' sorry =
    (n + 1).negOnePow • v (single (K.d p'' p ≫ f) (n + 1)) p'' q'' hpq''
Tactic: subst h
Cleared hypotheses: p', hp', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p n q' p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
hp' : p'' + 1 = p
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • v (single (K.d p'' p ≫ f) (n + 1)) p'' q'' hpq''
have pos : ∀ (f : K.X (p'' + 1) ⟶ L.X q'') (hp' : p'' + 1 = p'' + 1),
  (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' sorry =
    (n + 1).negOnePow • v (single (K.d p'' (p'' + 1) ≫ f) (n + 1)) p'' q'' hpq''
Tactic: obtain rfl : p = p'' + 1 := by lia
Cleared hypotheses: p, f, hp'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
h : ¬p'' = p'
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
have neg : p'' + 1 ≠ p
Tactic: rw [single_v_eq_zero _ _ _ _ _ h, single_v_eq_zero, comp_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
⊢ Eq (α :=
    Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F)
      (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) n₁₂)
    ((z₁.comp z₂ h).map Φ :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) n₁₂)
    (comp (G := Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
        (z₁.map Φ :
          Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G) n₁)
        (z₂.map Φ :
          Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
            (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) n₂)
        h :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) n₁₂)
have h₁ : ∀ (p q : ℤ) (hpq : p + n₁₂ = q),
  Eq (α :=
    HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F) p ⟶
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) q)
    (v ((z₁.comp z₂ h).map Φ) p q hpq :
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F) p ⟶
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) q)
    (v
        (comp (G := Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
          (z₁.map Φ :
            Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G) n₁)
          (z₂.map Φ :
            Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
              (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) n₂)
          h)
        p q hpq :
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F) p ⟶
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) q)
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
p q : ℤ
hpq : p + n₁₂ = q
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F) p ⟶
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) q)
    (v ((z₁.comp z₂ h).map Φ) p q hpq :
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F) p ⟶
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) q)
    (v
        (comp (G := Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
          (z₁.map Φ :
            Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G) n₁)
          (z₂.map Φ :
            Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
              (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) n₂)
          h)
        p q hpq :
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F) p ⟶
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) q)
have h₁ : Φ.map ((z₁.comp z₂ h).v p q hpq) =
  v
    (comp (G := Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
      (z₁.map Φ :
        Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) F)
          (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G) n₁)
      (z₂.map Φ :
        Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) G)
          (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) n₂)
      h)
    p q hpq
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
z : Cochain K L n
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
⊢ Eq (α :=
    Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
      (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    (δ n m (z.map Φ) :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    ((δ n m z).map Φ :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
have pos : ∀ (hnm : n + 1 = m),
  Eq (α :=
    Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
      (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    (δ n m (z.map Φ) :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    ((δ n m z).map Φ :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
Tactic: by_cases hnm : n + 1 = m
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
z : Cochain K L n
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
pos :
  ∀ (hnm : n + 1 = m),
    Eq (α :=
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
      (δ n m (z.map Φ) :
        Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
      ((δ n m z).map Φ :
        Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
⊢ Eq (α :=
    Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
      (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    (δ n m (z.map Φ) :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    ((δ n m z).map Φ :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
have neg : ∀ (hnm : ¬n + 1 = m),
  Eq (α :=
    Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
      (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    (δ n m (z.map Φ) :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    ((δ n m z).map Φ :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
Tactic: by_cases hnm : n + 1 = m
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
z : Cochain K L n
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
hnm : n + 1 = m
⊢ Eq (α :=
    Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
      (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    (δ n m (z.map Φ) :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
    ((δ n m z).map Φ :
      Cochain (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) m)
have pos : ∀ (p q : ℤ) (hpq : p + m = q),
  Eq (α :=
    HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) p ⟶
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) q)
    (Cochain.v (δ n m (z.map Φ)) p q hpq :
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) p ⟶
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) q)
    (Cochain.v ((δ n m z).map Φ) p q hpq :
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) p ⟶
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) q)
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
D : Type u_2
inst_2 : Category.{v_1, u_2} D
inst_3 : Preadditive.{v_1, u_2} D
z : Cochain K L n
Φ : CategoryTheory.Functor.{v, v_1, u, u_2} C D
inst_4 : Φ.Additive
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) p ⟶
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) q)
    (Cochain.v (δ n m (z.map Φ)) p q hpq :
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) p ⟶
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) q)
    (Cochain.v ((δ n m z).map Φ) p q hpq :
      HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) K) p ⟶
        HomologicalComplex.X (Functor.obj (Φ.mapHomologicalComplex (ComplexShape.up ℤ)) L) q)
have pos : Cochain.v (δ n m (z.map Φ)) p q hpq = Φ.map ((δ n m z).v p q hpq)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L : CochainComplex.{v, u, 0} C ℤ
n m_1 p : ℤ
α₁ α₂ : Cocycle K L n
m : ℤ
hm : m + 1 = n
β₁ : Cochain K L m
hβ₁ : δ m n β₁ = (↑α₁ : Cochain K L n)
m' : ℤ
hm' : m' + 1 = n
β₂ : Cochain K L m'
hβ₂ : δ m' n β₂ = (↑α₂ : Cochain K L n)
⊢ Membership.mem (γ := Set (Cocycle K L n))
    {α : Cocycle K L n | ∃ (m : ℤ) (_ : m + 1 = n) (β : Cochain K L m), δ m n β = (↑α : Cochain K L n)} (α₁ + α₂)
have obtain : ∀ (hm' : m + 1 = n) (β₂ : Cochain K L m) (hβ₂ : δ m n β₂ = (↑α₂ : Cochain K L n)),
  Membership.mem (γ := Set (Cocycle K L n))
    {α : Cocycle K L n | ∃ (m : ℤ) (_ : m + 1 = n) (β : Cochain K L m), δ m n β = (↑α : Cochain K L n)} (α₁ + α₂)
Tactic: obtain rfl : m = m' := by lia
Cleared hypotheses: m', hm', β₂, hβ₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L : CochainComplex.{v, u, 0} C ℤ
n m_1 p m : ℤ
hm : m + 1 = n
β : Cochain K L m
property : δ m n β ∈ cocycle K L n
⊢ Membership.mem (γ := AddSubgroup (Cocycle K L n))
    (AddMonoidHom.ker (M :=
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
      (AddMonoidHom.comp (Functor.mapAddHom (HomotopyCategory.quotient C (ComplexShape.up ℤ)))
        (AddEquiv.toAddMonoidHom (AddEquiv.symm Cocycle.equivHomShift))))
    (Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n) (δ m n β) property)
have simp : Nonempty.{max 1 (v + 1)}
  (Homotopy
    (Cocycle.rightShift (Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n) (δ m n β) property) n 0 sorry).homOf
    0)
Tactic: simp only [AddMonoidHom.mem_ker, AddMonoidHom.coe_comp, AddMonoidHom.coe_coe,
      AddEquiv.toAddMonoidHom_eq_coe, Function.comp_apply, Cocycle.equivHomShift_symm_apply,
      Functor.mapAddHom_apply, HomotopyCategory.quotient_map_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x : Cocycle K L n
⊢ Eq (α :=
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
      ((toHom :
            (a : CohomologyClass K L n) →
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
                (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                  ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
          (mk x) :
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
      (0 :
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L)) ↔
    x ∈ coboundaries K L n
have refine_1 : ∀
  (h :
    Eq (α :=
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
      ((toHom :
            (a : CohomologyClass K L n) →
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
                (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                  ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
          (mk x) :
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
      (0 :
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))),
  x ∈ coboundaries K L n
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x : Cocycle K L n
h :
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        (mk x) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    (0 :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
⊢ x ∈ coboundaries K L n
have refine_1 : ∃ (m : ℤ), m + 1 = n ∧ ∃ (β : Cochain K L m), δ m n β = (↑x : Cochain K L n)
Tactic: simp only [coboundaries, exists_prop, AddSubgroup.mem_mk, AddSubmonoid.mem_mk,
      AddSubsemigroup.mem_mk, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x : Cocycle K L n
h :
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        (mk x) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    (0 :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
⊢ ∃ (m : ℤ), m + 1 = n ∧ ∃ (β : Cochain K L m), δ m n β = (↑x : Cochain K L n)
have h₁ : Nonempty.{max 1 (v + 1)}
  (Homotopy.{v, u, 0} (ι := ℤ) (V := C) (c := ComplexShape.up ℤ) (C := K) (D :=
    Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)
    ((AddEquiv.symm Cocycle.equivHomShift :
        (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
      x)
    0)
Tactic: rw [toHom_mk, HomotopyCategory.quotient_map_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x : Cocycle K L n
h :
  Nonempty.{max 1 (v + 1)}
    (Homotopy.{v, u, 0} (ι := ℤ) (V := C) (c := ComplexShape.up ℤ) (C := K) (D :=
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)
      ((AddEquiv.symm Cocycle.equivHomShift :
          (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
        x)
      0)
⊢ ∃ (m : ℤ), m + 1 = n ∧ ∃ (β : Cochain K L m), δ m n β = (↑x : Cochain K L n)
have refine_1 : ∀ (γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L) (-1))
  (h :
    Cochain.ofHom
        ((AddEquiv.symm Cocycle.equivHomShift :
            (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
          x) =
      δ (-1) 0 γ + Cochain.ofHom 0),
  ∃ (m : ℤ), m + 1 = n ∧ ∃ (β : Cochain K L m), δ m n β = (↑x : Cochain K L n)
Tactic: obtain ⟨γ, h⟩ := Cochain.equivHomotopy _ _ h.some
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x : Cocycle K L n
h_1 :
  Nonempty.{max 1 (v + 1)}
    (Homotopy.{v, u, 0} (ι := ℤ) (V := C) (c := ComplexShape.up ℤ) (C := K) (D :=
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)
      ((AddEquiv.symm Cocycle.equivHomShift :
          (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
        x)
      0)
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L) (-1)
h :
  Cochain.ofHom
      ((AddEquiv.symm Cocycle.equivHomShift :
          (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
        x) =
    δ (-1) 0 γ + Cochain.ofHom 0
⊢ ∃ (m : ℤ), m + 1 = n ∧ ∃ (β : Cochain K L m), δ m n β = (↑x : Cochain K L n)
have h₁ : (↑x : Cochain K L n).rightShift n 0 sorry = δ (-1) 0 γ
Tactic: simp only [Cochain.ofHom_zero, add_zero, Cocycle.equivHomShift_symm_apply,
      Cocycle.cochain_ofHom_homOf_eq_coe, Cocycle.rightShift_coe] at h
Cleared hypotheses: h