awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
f :
  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)
refine_2 :
  ∀ (f : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L),
    ∃ (a : CohomologyClass 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))
            a :
          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))
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f :
          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))
⊢ ∃ (a : CohomologyClass K L n),
    (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))
        a =
      f

Tactic:
obtain ⟨f, rfl⟩ := Functor.map_surjective _ f

Premises used: rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
f : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L
⊢ Eq.{v + 1} (α :=
    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
          ((Cocycle.equivHomShift :
              (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K L n)
            f)) :
      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))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f :
      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))

Tactic:
simp [toHom_mk]

Premises used: CochainComplex.HomComplex.CohomologyClass.toHom_mk
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
f : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L
⊢ ∃ (a : CohomologyClass 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))
          a :
        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))
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f :
        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))

Tactic:
exact ⟨mk (Cocycle.equivHomShift f), by simp [toHom_mk]⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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 p : ℤ
hm : n + 1 = m
hp : m + 1 = p
hf :
  ∀ (x : (↑(KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt : Type v)),
    Eq (α := (↑(AddCommGrpCat.of (CohomologyClass K L m)) : Type v))
      ((AddCommGrpCat.Hom.hom
              ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯) ≫
                AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) :
            (a : (↑(KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt : Type v)) →
              (↑(AddCommGrpCat.of (CohomologyClass K L m)) : Type v))
          x :
        (↑(AddCommGrpCat.of (CohomologyClass K L m)) : Type v))
      ((AddCommGrpCat.Hom.hom 0 :
            (a : (↑(KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt : Type v)) →
              (↑(AddCommGrpCat.of (CohomologyClass K L m)) : Type v))
          x :
        (↑(AddCommGrpCat.of (CohomologyClass K L m)) : Type v))
⊢ Eq (α :=
    (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt ⟶ AddCommGrpCat.of (CohomologyClass K L m))
    ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯) ≫
      AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m))
    0

Tactic:
ext x
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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 p : ℤ
hm : n + 1 = m
hp : m + 1 = p
x : (↑(KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt : Type v)
hf :
  Membership.mem (α := Cocycle K L m) (coboundaries K L m)
    (((AddCommGrpCat.Hom.hom ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι ((K.HomComplex L).d n m) ⋯)) :
            (↑(AddCommGrpCat.of (Cochain K L n)) : Type v) →+ (↑(AddCommGrpCat.of (Cocycle K L m)) : Type v)) :
          (a : Cochain K L n) → Cocycle K L m)
        x :
      Cocycle K L m)
⊢ Eq.{v + 1} (α := CohomologyClass K L m)
    (CohomologyClass.mk
      (((AddCommGrpCat.Hom.hom ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι ((K.HomComplex L).d n m) ⋯)) :
            (↑(AddCommGrpCat.of (Cochain K L n)) : Type v) →+ (↑(AddCommGrpCat.of (Cocycle K L m)) : Type v)) :
          (a : Cochain K L n) → Cocycle K L m)
        x))
    0

Tactic:
rw [CohomologyClass.mk_eq_zero_iff]

Premises used: CochainComplex.HomComplex.CohomologyClass.mk_eq_zero_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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 p : ℤ
hm : n + 1 = m
hp : m + 1 = p
x : (↑(KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt : Type v)
⊢ Membership.mem (α := Cocycle K L m) (coboundaries K L m)
    (((AddCommGrpCat.Hom.hom ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι ((K.HomComplex L).d n m) ⋯)) :
            (↑(AddCommGrpCat.of (Cochain K L n)) : Type v) →+ (↑(AddCommGrpCat.of (Cocycle K L m)) : Type v)) :
          (a : Cochain K L n) → Cocycle K L m)
        x :
      Cocycle K L m)

Tactic:
⟨n, hm, x, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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 p : ℤ
hm : n + 1 = m
hp : m + 1 = p
x : (↑(KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt : Type v)
⊢ Membership.mem (α := Cocycle K L m) (coboundaries K L m)
    (((AddCommGrpCat.Hom.hom ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι ((K.HomComplex L).d n m) ⋯)) :
            (↑(AddCommGrpCat.of (Cochain K L n)) : Type v) →+ (↑(AddCommGrpCat.of (Cocycle K L m)) : Type v)) :
          (a : Cochain K L n) → Cocycle K L m)
        x :
      Cocycle K L m)

Tactic:
exact ⟨n, hm, x, rfl⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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 p : ℤ
hm : n + 1 = m
hp : m + 1 = p
s :
  Cofork (X := (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt)
    ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯)) 0
q : ℤ
hq : q + 1 = m
y : Cochain K L q
property : δ q m y ∈ cocycle K L m
⊢ n = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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 p : ℤ
hm : n + 1 = m
hp : m + 1 = p
s :
  Cofork (X := (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt)
    ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯)) 0
q : ℤ
hq : q + 1 = m
y : Cochain K L q
property : δ q m y ∈ cocycle K L m
obtain :
  ∀ (hq : n + 1 = m) (y : Cochain K L n) (property : δ n m y ∈ cocycle K L m),
    Subtype.mk (p := fun (x : Cochain K L m) ↦ x ∈ cocycle K L m) (δ n m y) property ∈ (AddCommGrpCat.Hom.hom s.π).ker
⊢ Subtype.mk (p := fun (x : Cochain K L m) ↦ x ∈ cocycle K L m) (δ q m y) property ∈ (AddCommGrpCat.Hom.hom s.π).ker

Tactic:
obtain rfl : n = q := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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 p : ℤ
hm : n + 1 = m
hp : m + 1 = p
s :
  Cofork (X := (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt)
    ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯)) 0
hq : n + 1 = m
y : Cochain K L n
property : δ n m y ∈ cocycle K L m
⊢ Subtype.mk (p := fun (x : Cochain K L m) ↦ x ∈ cocycle K L m) (δ n m y) property ∈ (AddCommGrpCat.Hom.hom s.π).ker

Tactic:
simpa only [zero_comp] using ConcreteCategory.congr_hom s.condition y

Premises used: CategoryTheory.Limits.Cofork.condition, CategoryTheory.Limits.zero_comp, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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 p : ℤ
hm : n + 1 = m
hp : m + 1 = p
s :
  Cofork (X := (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt)
    ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯)) 0
l : (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt ⟶ s.pt
hl : Cofork.π (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯) ≫ l = s.π
hf :
  ∀ (x : (↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt : Type v)),
    Eq (α := (↑s.pt : Type v))
      ((AddCommGrpCat.Hom.hom l :
            (a : (↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt : Type v)) →
              (↑s.pt : Type v))
          x :
        (↑s.pt : Type v))
      ((AddCommGrpCat.Hom.hom
              ((fun
                    (s :
                      Cofork (X := (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt)
                        ((Cocycle.isKernel K L m p hp).lift
                          (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯))
                        0) ↦
                  AddCommGrpCat.ofHom (CohomologyClass.descAddMonoidHom (AddCommGrpCat.Hom.hom s.π) ⋯))
                s) :
            (a : (↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt : Type v)) →
              (↑s.pt : Type v))
          x :
        (↑s.pt : Type v))
⊢ l =
    (fun
          (s :
            Cofork (X := (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt)
              ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯))
              0) ↦
        AddCommGrpCat.ofHom (CohomologyClass.descAddMonoidHom (AddCommGrpCat.Hom.hom s.π) ⋯))
      s

Tactic:
ext x
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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 p : ℤ
hm : n + 1 = m
hp : m + 1 = p
s :
  Cofork (X := (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt)
    ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯)) 0
l : (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt ⟶ s.pt
hl : Cofork.π (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯) ≫ l = s.π
x : (↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt : Type v)
hf :
  ∀ (y : Cocycle K L m),
    Eq (α := (↑s.pt : Type v))
      ((AddCommGrpCat.Hom.hom l :
            (a : (↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt : Type v)) →
              (↑s.pt : Type v))
          (CohomologyClass.mk y) :
        (↑s.pt : Type v))
      ((AddCommGrpCat.Hom.hom
              ((fun
                    (s :
                      Cofork (X := (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt)
                        ((Cocycle.isKernel K L m p hp).lift
                          (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯))
                        0) ↦
                  AddCommGrpCat.ofHom (CohomologyClass.descAddMonoidHom (AddCommGrpCat.Hom.hom s.π) ⋯))
                s) :
            (a : (↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt : Type v)) →
              (↑s.pt : Type v))
          (CohomologyClass.mk y) :
        (↑s.pt : Type v))
⊢ Eq (α := (↑s.pt : Type v))
    ((AddCommGrpCat.Hom.hom l :
          (a : (↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt : Type v)) →
            (↑s.pt : Type v))
        x :
      (↑s.pt : Type v))
    ((AddCommGrpCat.Hom.hom
            ((fun
                  (s :
                    Cofork (X := (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt)
                      ((Cocycle.isKernel K L m p hp).lift
                        (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯))
                      0) ↦
                AddCommGrpCat.ofHom (CohomologyClass.descAddMonoidHom (AddCommGrpCat.Hom.hom s.π) ⋯))
              s) :
          (a : (↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt : Type v)) →
            (↑s.pt : Type v))
        x :
      (↑s.pt : Type v))

Tactic:
obtain ⟨y, rfl⟩ := x.mk_surjective

Premises used: CochainComplex.HomComplex.CohomologyClass.mk_surjective, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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 p : ℤ
hm : n + 1 = m
hp : m + 1 = p
s :
  Cofork (X := (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt)
    ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯)) 0
l : (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt ⟶ s.pt
hl : Cofork.π (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯) ≫ l = s.π
y : Cocycle K L m
⊢ Eq (α := (↑s.pt : Type v))
    ((AddCommGrpCat.Hom.hom l :
          (a : (↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt : Type v)) →
            (↑s.pt : Type v))
        (CohomologyClass.mk y) :
      (↑s.pt : Type v))
    ((AddCommGrpCat.Hom.hom
            ((fun
                  (s :
                    Cofork (X := (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt)
                      ((Cocycle.isKernel K L m p hp).lift
                        (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯))
                      0) ↦
                AddCommGrpCat.ofHom (CohomologyClass.descAddMonoidHom (AddCommGrpCat.Hom.hom s.π) ⋯))
              s) :
          (a : (↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt : Type v)) →
            (↑s.pt : Type v))
        (CohomologyClass.mk y) :
      (↑s.pt : Type v))

Tactic:
simpa using ConcreteCategory.congr_hom hl y

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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 p : ℤ
⊢ (ComplexShape.up ℤ).prev n + 1 = n

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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 p : ℤ
⊢ n + 1 = (ComplexShape.up ℤ).next n

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → (↑(X n) : Type v) → (↑(X (n + 1)) : Type v)
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : (↑(X n) : Type v)), (↑(φ n x) : Cochain K L d).EqUpTo (↑x : Cochain K L d) (p₀ + (↑n : ℤ))
x₀ : (↑(X 0) : Type v)
n₁ n₂ : ℕ
h : n₁ ≤ n₂
obtain :
  ∀ (k : ℕ) (h : n₁ ≤ n₁ + k),
    (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).EqUpTo (↑(sequence (X := X) φ x₀ (n₁ + k)) : Cochain K L d)
      (p₀ + (↑n₁ : ℤ))
⊢ (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).EqUpTo (↑(sequence (X := X) φ x₀ n₂) : Cochain K L d) (p₀ + (↑n₁ : ℤ))

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → (↑(X n) : Type v) → (↑(X (n + 1)) : Type v)
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : (↑(X n) : Type v)), (↑(φ n x) : Cochain K L d).EqUpTo (↑x : Cochain K L d) (p₀ + (↑n : ℤ))
x₀ : (↑(X 0) : Type v)
n₁ : ℕ
p : ℤ
zero :
  ∀ (q : ℤ) (hpq : p + d = q),
    p ≤ p₀ + (↑n₁ : ℤ) →
      (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).v p q hpq =
        (↑(sequence (X := X) φ x₀ (n₁ + 0)) : Cochain K L d).v p q hpq
⊢ ∀ (q : ℤ) (hpq : p + d = q),
    p ≤ p₀ + (↑n₁ : ℤ) →
      (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).v p q hpq =
        (↑(sequence (X := X) φ x₀ (n₁ + 0)) : Cochain K L d).v p q hpq

Tactic:
_
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → (↑(X n) : Type v) → (↑(X (n + 1)) : Type v)
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : (↑(X n) : Type v)), (↑(φ n x) : Cochain K L d).EqUpTo (↑x : Cochain K L d) (p₀ + (↑n : ℤ))
x₀ : (↑(X 0) : Type v)
n₁ : ℕ
p q : ℤ
zero :
  ∀ (hpq : p + d = q),
    p ≤ p₀ + (↑n₁ : ℤ) →
      (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).v p q hpq =
        (↑(sequence (X := X) φ x₀ (n₁ + 0)) : Cochain K L d).v p q hpq
⊢ ∀ (hpq : p + d = q),
    p ≤ p₀ + (↑n₁ : ℤ) →
      (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).v p q hpq =
        (↑(sequence (X := X) φ x₀ (n₁ + 0)) : Cochain K L d).v p q hpq

Tactic:
_
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → (↑(X n) : Type v) → (↑(X (n + 1)) : Type v)
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : (↑(X n) : Type v)), (↑(φ n x) : Cochain K L d).EqUpTo (↑x : Cochain K L d) (p₀ + (↑n : ℤ))
x₀ : (↑(X 0) : Type v)
n₁ : ℕ
p q : ℤ
hpq : p + d = q
zero :
  p ≤ p₀ + (↑n₁ : ℤ) →
    (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).v p q hpq =
      (↑(sequence (X := X) φ x₀ (n₁ + 0)) : Cochain K L d).v p q hpq
⊢ p ≤ p₀ + (↑n₁ : ℤ) →
    (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).v p q hpq =
      (↑(sequence (X := X) φ x₀ (n₁ + 0)) : Cochain K L d).v p q hpq

Tactic:
_
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → (↑(X n) : Type v) → (↑(X (n + 1)) : Type v)
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : (↑(X n) : Type v)), (↑(φ n x) : Cochain K L d).EqUpTo (↑x : Cochain K L d) (p₀ + (↑n : ℤ))
x₀ : (↑(X 0) : Type v)
n₁ : ℕ
p q : ℤ
hpq : p + d = q
h : p ≤ p₀ + (↑n₁ : ℤ)
⊢ (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).v p q hpq =
    (↑(sequence (X := X) φ x₀ (n₁ + 0)) : Cochain K L d).v p q hpq

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → (↑(X n) : Type v) → (↑(X (n + 1)) : Type v)
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : (↑(X n) : Type v)), (↑(φ n x) : Cochain K L d).EqUpTo (↑x : Cochain K L d) (p₀ + (↑n : ℤ))
x₀ : (↑(X 0) : Type v)
k : ℕ
hk :
  ∀ (n₁ : ℕ),
    (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).EqUpTo (↑(sequence (X := X) φ x₀ (n₁ + k)) : Cochain K L d)
      (p₀ + (↑n₁ : ℤ))
n₁ : ℕ
p q : ℤ
hpq : p + d = q
hp : p ≤ p₀ + (↑n₁ : ℤ)
⊢ p ≤ p₀ + (↑(n₁ + k) : ℤ)

Tactic:
lia