awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℤ
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
have 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))
Tactic: obtain ⟨f, rfl⟩ := Functor.map_surjective _ f
Cleared hypotheses: f
-- 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 p : ℤ
hm : n + 1 = m
hp : m + 1 = p
⊢ 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
have hf : ∀ (x : (↑(KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f sorry).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 sorry) ≫
              AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) :
          (a : (↑(KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f sorry).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 sorry).pt : Type v)) →
            (↑(AddCommGrpCat.of (CohomologyClass K L m)) : Type v))
        x :
      (↑(AddCommGrpCat.of (CohomologyClass K L m)) : Type v))
Tactic: ext x
-- 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 p : ℤ
hm : n + 1 = m
hp : m + 1 = p
x : (↑(KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt : Type v)
⊢ 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
have 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) sorry)) :
          (↑(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: rw [CohomologyClass.mk_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
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
⊢ Subtype.mk (p := fun (x : Cochain K L m) ↦ x ∈ cocycle K L m) (δ q m y) property ∈ (AddCommGrpCat.Hom.hom s.π).ker
have 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
Tactic: obtain rfl : n = q := by lia
Cleared hypotheses: q, hq, y, property
-- 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 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.π
⊢ 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
have hf : ∀ (x : (↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) sorry).pt : Type v)),
  Eq (α := (↑s.pt : Type v))
    ((AddCommGrpCat.Hom.hom l :
          (a : (↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) sorry).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 sorry).pt)
                      ((Cocycle.isKernel K L m p hp).lift
                        (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f sorry))
                      0) ↦
                AddCommGrpCat.ofHom (CohomologyClass.descAddMonoidHom (AddCommGrpCat.Hom.hom s.π) sorry))
              s) :
          (a : (↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) sorry).pt : Type v)) →
            (↑s.pt : Type v))
        x :
      (↑s.pt : Type v))
Tactic: ext x
-- 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 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)
⊢ 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))
have 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)) sorry).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 sorry).pt)
                      ((Cocycle.isKernel K L m p hp).lift
                        (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f sorry))
                      0) ↦
                AddCommGrpCat.ofHom (CohomologyClass.descAddMonoidHom (AddCommGrpCat.Hom.hom s.π) sorry))
              s) :
          (a : (↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) sorry).pt : Type v)) →
            (↑s.pt : Type v))
        (CohomologyClass.mk y) :
      (↑s.pt : Type v))
Tactic: obtain ⟨y, rfl⟩ := x.mk_surjective
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction (goal)
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₂
⊢ (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).EqUpTo (↑(sequence (X := X) φ x₀ n₂) : Cochain K L d) (p₀ + (↑n₁ : ℤ))
have 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₁ : ℤ))
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
Cleared hypotheses: n₂, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction (goal)
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₁ : ℤ)
⊢ (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).v p q hpq =
    (↑(sequence (X := X) φ x₀ (n₁ + (k + 1))) : Cochain K L d).v p q hpq
have succ : (↑(φ (n₁ + k) (sequence (X := X) φ x₀ (n₁ + k))) : Cochain K L d).v p q hpq =
  (↑(sequence (X := X) φ x₀ (n₁ + (k + 1))) : Cochain K L d).v p q hpq
Tactic: rw [hk n₁ p q hpq hp, ← hφ (n₁ + k) (sequence φ x₀ (n₁ + k)) p q hpq (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction (goal)
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₁ k : ℕ
⊢ (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).EqUpTo (↑(sequence (X := X) φ x₀ (n₁ + k)) : Cochain K L d)
    (p₀ + (↑n₁ : ℤ))
have zero : ∀ (n₁ : ℕ),
  (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).EqUpTo (↑(sequence (X := X) φ x₀ (n₁ + 0)) : Cochain K L d)
    (p₀ + (↑n₁ : ℤ))
Tactic: induction k generalizing n₁ with
  | zero => intro _ _ _ _; simp
  | succ k hk =>
    intro p q hpq hp
    rw [hk n₁ p q hpq hp, ← hφ (n₁ + k) (sequence φ x₀ (n₁ + k)) p q hpq (by lia)]
    dsimp [sequence]
Cleared hypotheses: n₁, k
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction (goal)
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₁ k : ℕ
zero :
  ∀ (n₁ : ℕ),
    (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).EqUpTo (↑(sequence (X := X) φ x₀ (n₁ + 0)) : Cochain K L d)
      (p₀ + (↑n₁ : ℤ))
⊢ (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).EqUpTo (↑(sequence (X := X) φ x₀ (n₁ + k)) : Cochain K L d)
    (p₀ + (↑n₁ : ℤ))
have succ : ∀ (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₁ : ℕ),
  (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).EqUpTo (↑(sequence (X := X) φ x₀ (n₁ + (k + 1))) : Cochain K L d)
    (p₀ + (↑n₁ : ℤ))
Tactic: induction k generalizing n₁ with
  | zero => intro _ _ _ _; simp
  | succ k hk =>
    intro p q hpq hp
    rw [hk n₁ p q hpq hp, ← hφ (n₁ + k) (sequence φ x₀ (n₁ + k)) p q hpq (by lia)]
    dsimp [sequence]
Cleared hypotheses: n₁, k
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p + n = p'
⊢ p' = q + a
have rw : p + n = q + a
Tactic: rw [← hp', ← hpq, ← hn', add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p + n = p'
rw : p + n = q + a
⊢ p' = q + a
have rw₁ : p + n = p + n' + a
Tactic: rw [← hp', ← hpq, ← hn', add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p + n = p'
rw : p + n = q + a
rw₁ : p + n = p + n' + a
⊢ p' = q + a
have rw₂ : p + (n' + a) = p + n' + a
Tactic: rw [← hp', ← hpq, ← hn', add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p + n = p'
rw : p + n = q + a
rw₁ : p + n = p + n' + a
rw₂ : p + (n' + a) = p + n' + a
⊢ p' = q + a
have rw₃ : p + (n' + a) = p + (n' + a)
Tactic: rw [← hp', ← hpq, ← hn', add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p + n = p'
⊢ (γ.rightShift a n' hn').v p q hpq = γ.v p p' hp' ≫ (L.shiftFunctorObjXIso a q p' ⋯).inv
have subst : (γ.rightShift a n' hn').v p q hpq = γ.v p (p + n) sorry ≫ (L.shiftFunctorObjXIso a q (p + n) sorry).inv
Tactic: subst hp'
Cleared hypotheses: p', hp'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p' + n = q
⊢ p' = p + a
have rw : p' + n = p + a + n
Tactic: rw [← add_left_inj n, hp', add_assoc, add_comm a, hn', hpq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p' + n = q
rw : p' + n = p + a + n
⊢ p' = p + a
have rw₁ : q = p + a + n
Tactic: rw [← add_left_inj n, hp', add_assoc, add_comm a, hn', hpq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p' + n = q
rw : p' + n = p + a + n
rw₁ : q = p + a + n
⊢ p' = p + a
have rw₂ : q = p + (a + n)
Tactic: rw [← add_left_inj n, hp', add_assoc, add_comm a, hn', hpq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p' + n = q
rw : p' + n = p + a + n
rw₁ : q = p + a + n
rw₂ : q = p + (a + n)
⊢ p' = p + a
have rw₃ : q = p + (n + a)
Tactic: rw [← add_left_inj n, hp', add_assoc, add_comm a, hn', hpq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p' + n = q
rw : p' + n = p + a + n
rw₁ : q = p + a + n
rw₂ : q = p + (a + n)
rw₃ : q = p + (n + a)
⊢ p' = p + a
have rw₄ : q = p + n'
Tactic: rw [← add_left_inj n, hp', add_assoc, add_comm a, hn', hpq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p' + n = q
rw : p' + n = p + a + n
rw₁ : q = p + a + n
rw₂ : q = p + (a + n)
rw₃ : q = p + (n + a)
rw₄ : q = p + n'
⊢ p' = p + a
have rw₅ : q = q
Tactic: rw [← add_left_inj n, hp', add_assoc, add_comm a, hn', hpq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p' + n = q
⊢ (γ.leftShift a n' hn').v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p p' ⋯).hom ≫ γ.v p' q hp'
have obtain : ∀ (hp' : p + a + n = q),
  (γ.leftShift a n' hn').v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) sorry).hom ≫ γ.v (p + a) q hp'
Tactic: obtain rfl : p' = p + a := by lia
Cleared hypotheses: p', hp'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (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 M : CochainComplex.{v, u, 0} C ℤ
n_1 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n' a : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ q = p + n' + a
have rw : p + n = p + n' + a
Tactic: rw [← hpq, add_assoc, hn]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (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 M : CochainComplex.{v, u, 0} C ℤ
n_1 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n' a : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
rw : p + n = p + n' + a
⊢ q = p + n' + a
have rw₁ : p + n = p + (n' + a)
Tactic: rw [← hpq, add_assoc, hn]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (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 M : CochainComplex.{v, u, 0} C ℤ
n_1 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n' a : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
rw : p + n = p + n' + a
rw₁ : p + n = p + (n' + a)
⊢ q = p + n' + a
have rw₂ : p + n = p + n
Tactic: rw [← hpq, add_assoc, hn]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (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 M : CochainComplex.{v, u, 0} C ℤ
n_1 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n' a : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p + n' = p'
⊢ q = p' + a
have rw : p + n = p' + a
Tactic: rw [← hpq, ← hn, ← add_assoc, hp']
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (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 M : CochainComplex.{v, u, 0} C ℤ
n_1 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n' a : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p + n' = p'
rw : p + n = p' + a
⊢ q = p' + a
have rw₁ : p + (n' + a) = p' + a
Tactic: rw [← hpq, ← hn, ← add_assoc, hp']