awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ Eq (α := op (L.X (-n)) ⟶ op (K.X (-n)))
    (Quiver.Hom.op (CategoryStruct.comp (Y := L.X (-(n + 1))) (h.hom (-n) (-(n + 1))) (L.d (-(n + 1)) (-n))))
    (((dNext.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
            (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
            (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
          ((i j : ℤ) →
              ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
            (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
              ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
        (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
      fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)))
have e_a : Eq.{v_1 + 1} (α := op (L.X (-n)) ⟶ op (K.X (-n)))
  (((dNext.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
            (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
            (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
          ((i j : ℤ) →
              ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
            (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
              ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
        (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
      fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)) :
    op (L.X (-n)) ⟶ op (K.X (-n)))
  (Quiver.Hom.op (CategoryStruct.comp (Y := L.X (-(n + 1))) (h.hom (-n) (-(n + 1))) (L.d (-(n + 1)) (-n))) :
    op (L.X (-n)) ⟶ op (K.X (-n)))
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ Eq (α := op (L.X (-n)) ⟶ op (K.X (-n)))
    (Quiver.Hom.op ((dNext (-n) : (a : (i j : ℤ) → K.X i ⟶ L.X j) → K.X (-n) ⟶ L.X (-n)) h.hom) :
      op (L.X (-n)) ⟶ op (K.X (-n)))
    (((prevD.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
              (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
              (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
            ((i j : ℤ) →
                ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                  ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
              (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
          (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
        fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)) :
      op (L.X (-n)) ⟶ op (K.X (-n)))
have e_a : Eq (α := op (L.X (-n)) ⟶ op (K.X (-n)))
  (Quiver.Hom.op (CategoryStruct.comp (Y := K.X (-(n - 1))) (K.d (-n) (-(n - 1))) (h.hom (-(n - 1)) (-n))))
  (((prevD.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
          (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
          (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
        ((i j : ℤ) →
            ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
              ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
          (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
            ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
      (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
    fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)))
Tactic: rw [dNext_eq _ (i' := - (n - 1)) (by dsimp; lia)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ Eq (α := op (L.X (-n)) ⟶ op (K.X (-n)))
    (Quiver.Hom.op (CategoryStruct.comp (Y := K.X (-(n - 1))) (K.d (-n) (-(n - 1))) (h.hom (-(n - 1)) (-n))))
    (((prevD.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
            (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
            (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
          ((i j : ℤ) →
              ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
            (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
              ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
        (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
      fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)))
have e_a : Eq.{v_1 + 1} (α := op (L.X (-n)) ⟶ op (K.X (-n)))
  (((prevD.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
            (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
            (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
          ((i j : ℤ) →
              ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
            (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
              ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
        (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
      fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)) :
    op (L.X (-n)) ⟶ op (K.X (-n)))
  (Quiver.Hom.op (CategoryStruct.comp (Y := K.X (-(n - 1))) (K.d (-n) (-(n - 1))) (h.hom (-(n - 1)) (-n))) :
    op (L.X (-n)) ⟶ op (K.X (-n)))
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
p q p' q' : ℤ
hp : p + p' = 0
hq : q + q' = 0
⊢ (homotopyOp h).hom p q =
    (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ (h.hom q' p').op ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
have obtain : ∀ (hp : p + -p = 0),
  (homotopyOp h).hom p q =
    (HomologicalComplex.XIsoOfEq L sorry).hom.op ≫ Quiver.Hom.op (h.hom q' (-p)) ≫ (HomologicalComplex.XIsoOfEq K sorry).hom.op
Tactic: obtain rfl : p' = -p := by lia
Cleared hypotheses: p', hp
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
p q q' : ℤ
hq : q + q' = 0
hp : p + -p = 0
⊢ (homotopyOp h).hom p q =
    (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ Quiver.Hom.op (h.hom q' (-p)) ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
have obtain : ∀ (hq : q + -q = 0),
  (homotopyOp h).hom p q =
    (HomologicalComplex.XIsoOfEq L sorry).hom.op ≫
      Quiver.Hom.op (h.hom (-q) (-p)) ≫ (HomologicalComplex.XIsoOfEq K sorry).hom.op
Tactic: obtain rfl : q' = -q := by lia
Cleared hypotheses: q', hq
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h :
  Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)
p q : ℤ
hpq : ¬(ComplexShape.up ℤ).Rel q p
⊢ (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ Quiver.Hom.unop (h.hom (-q) (-p)) ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom = 0
have a : ¬(ComplexShape.up ℤ).Rel (-p) (-q)
Tactic: rw [h.zero, unop_zero, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h :
  Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)
n p q p' q' : ℤ
hp : p = p'
hq : q = q'
⊢ h.hom p q =
    Quiver.Hom.op (Iso.hom (HomologicalComplex.XIsoOfEq L ⋯)) ≫
      h.hom p' q' ≫ Quiver.Hom.op (Iso.hom (HomologicalComplex.XIsoOfEq K ⋯))
have subst : h.hom p q =
  Quiver.Hom.op (Iso.hom (HomologicalComplex.XIsoOfEq L sorry)) ≫
    h.hom p q ≫ Quiver.Hom.op (Iso.hom (HomologicalComplex.XIsoOfEq K sorry))
Tactic: subst hp hq
Cleared hypotheses: p', q', hp, hq
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h :
  Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)
n : ℤ
⊢ (f.f n).op =
    (HAdd.hAdd (α := K.X n ⟶ L.X n) (β := K.X n ⟶ L.X n)
          ((dNext n : (a : (i j : ℤ) → K.X i ⟶ L.X j) → K.X n ⟶ L.X n) fun (p q : ℤ) ↦
              (HomologicalComplex.XIsoOfEq K ⋯).hom ≫
                Quiver.Hom.unop (h.hom (-q) (-p)) ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom :
            K.X n ⟶ L.X n)
          ((prevD n : (a : (i j : ℤ) → K.X i ⟶ L.X j) → K.X n ⟶ L.X n) fun (p q : ℤ) ↦
              (HomologicalComplex.XIsoOfEq K ⋯).hom ≫
                Quiver.Hom.unop (h.hom (-q) (-p)) ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom :
            K.X n ⟶ L.X n) +
        g.f n).op
have H : ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
  h.hom p q =
    Quiver.Hom.op (Iso.hom (HomologicalComplex.XIsoOfEq L sorry)) ≫
      h.hom p' q' ≫ Quiver.Hom.op (Iso.hom (HomologicalComplex.XIsoOfEq K sorry))
Tactic: have H (p q p' q' : ℤ) (hp : p = p') (hq : q = q') :
      h.hom p q = (L.XIsoOfEq (by simpa using hp.symm)).hom.op ≫ h.hom p' q' ≫
        (K.XIsoOfEq (by simpa)).hom.op := by
      subst hp hq
      simp
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h :
  Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)
n : ℤ
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q =
      Quiver.Hom.op (Iso.hom (HomologicalComplex.XIsoOfEq L ⋯)) ≫
        h.hom p' q' ≫ Quiver.Hom.op (Iso.hom (HomologicalComplex.XIsoOfEq K ⋯))
⊢ (f.f n).op =
    (HAdd.hAdd (α := K.X n ⟶ L.X n) (β := K.X n ⟶ L.X n)
          ((dNext n : (a : (i j : ℤ) → K.X i ⟶ L.X j) → K.X n ⟶ L.X n) fun (p q : ℤ) ↦
              (HomologicalComplex.XIsoOfEq K ⋯).hom ≫
                Quiver.Hom.unop (h.hom (-q) (-p)) ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom :
            K.X n ⟶ L.X n)
          ((prevD n : (a : (i j : ℤ) → K.X i ⟶ L.X j) → K.X n ⟶ L.X n) fun (p q : ℤ) ↦
              (HomologicalComplex.XIsoOfEq K ⋯).hom ≫
                Quiver.Hom.unop (h.hom (-q) (-p)) ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom :
            K.X n ⟶ L.X n) +
        g.f n).op
have obtain : ∀ (n : ℤ),
  Quiver.Hom.op (f.f (-n)) =
    (HAdd.hAdd (α := K.X (-n) ⟶ L.X (-n)) (β := K.X (-n) ⟶ L.X (-n))
          ((dNext (-n) : (a : (i j : ℤ) → K.X i ⟶ L.X j) → K.X (-n) ⟶ L.X (-n)) fun (p q : ℤ) ↦
              (HomologicalComplex.XIsoOfEq K sorry).hom ≫
                Quiver.Hom.unop (h.hom (-q) (-p)) ≫ (HomologicalComplex.XIsoOfEq L sorry).hom :
            K.X (-n) ⟶ L.X (-n))
          ((prevD (-n) : (a : (i j : ℤ) → K.X i ⟶ L.X j) → K.X (-n) ⟶ L.X (-n)) fun (p q : ℤ) ↦
              (HomologicalComplex.XIsoOfEq K sorry).hom ≫
                Quiver.Hom.unop (h.hom (-q) (-p)) ≫ (HomologicalComplex.XIsoOfEq L sorry).hom :
            K.X (-n) ⟶ L.X (-n)) +
        g.f (-n)).op
Tactic: obtain ⟨n, rfl⟩ : ∃ (m : ℤ), n = -m := ⟨-n , by simp⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h :
  Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)
p q p' q' : ℤ
hp : p + p' = 0
hq : q + q' = 0
⊢ (homotopyUnop h).hom p q =
    (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom q' p').unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom
have obtain : ∀ (hp : p + -p = 0),
  (homotopyUnop h).hom p q =
    (HomologicalComplex.XIsoOfEq K sorry).hom ≫ Quiver.Hom.unop (h.hom q' (-p)) ≫ (HomologicalComplex.XIsoOfEq L sorry).hom
Tactic: obtain rfl : p' = -p := by lia
Cleared hypotheses: p', hp
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h :
  Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)
p q q' : ℤ
hq : q + q' = 0
hp : p + -p = 0
⊢ (homotopyUnop h).hom p q =
    (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ Quiver.Hom.unop (h.hom q' (-p)) ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom
have obtain : ∀ (hq : q + -q = 0),
  (homotopyUnop h).hom p q =
    (HomologicalComplex.XIsoOfEq K sorry).hom ≫ Quiver.Hom.unop (h.hom (-q) (-p)) ≫ (HomologicalComplex.XIsoOfEq L sorry).hom
Tactic: obtain rfl : q' = -q := by lia
Cleared hypotheses: q', hq
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
⊢ (fun
          (h :
            Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
              Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
              Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
              (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
              (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)) ↦
        homotopyUnop h)
      ((fun (h : Homotopy f g) ↦ homotopyOp h) h) =
    h
have hom : ∀ (p q : ℤ),
  Homotopy.hom (f := f) (g := g)
      ((fun
            (h :
              Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
                Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
                Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
                (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
                (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)) ↦
          homotopyUnop h)
        ((fun (h : Homotopy f g) ↦ homotopyOp h) h))
      p q =
    h.hom p q
Tactic: ext p q
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h :
  Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)
⊢ (fun (h : Homotopy f g) ↦ homotopyOp h)
      ((fun
            (h :
              Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
                Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
                Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
                (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
                (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)) ↦
          homotopyUnop h)
        h) =
    h
have hom : ∀ (p q : ℤ),
  Homotopy.hom.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
      Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
      Functor.obj (Equivalence.functor (opEquivalence C)) (op K)) (f :=
      CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op) (g :=
      CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)
      ((fun (h : Homotopy f g) ↦ homotopyOp h)
        ((fun
              (h :
                Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
                  Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
                  Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
                  (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
                  (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)) ↦
            homotopyUnop h)
          h))
      p q =
    h.hom p q
Tactic: ext p q
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hK : HomologicalComplex.ExactAt K n
m : ℤ
hm : n + m = 0
⊢ HomologicalComplex.ExactAt (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)) m
have hK₁ : HomologicalComplex.ExactAt K (-m)
Tactic: obtain rfl : n = -m := by lia
Cleared hypotheses: n, hK, hm
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hK : HomologicalComplex.ExactAt K n
m : ℤ
hm : n + m = 0
hK₁ : HomologicalComplex.ExactAt K (-m)
⊢ HomologicalComplex.ExactAt (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)) m
have hm₁ : -m + m = 0
Tactic: obtain rfl : n = -m := by lia
Cleared hypotheses: n, hK, hm
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
m : ℤ
hK : HomologicalComplex.ExactAt K (-m)
hm : -m + m = 0
⊢ HomologicalComplex.ExactAt (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)) m
have rw : (HomologicalComplex.sc' (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)) (m - 1) m (m + 1)).unop.Exact
Tactic: rw [HomologicalComplex.exactAt_iff' _ (m - 1) m (m + 1) (by simp) (by simp),
    ← ShortComplex.exact_unop_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
m : ℤ
hK : HomologicalComplex.ExactAt K (-m)
hm : -m + m = 0
⊢ (HomologicalComplex.sc' (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)) (m - 1) m (m + 1)).unop.Exact
have rwa : ∀ (hK : (HomologicalComplex.sc' K (-(m + 1)) (-m) (-(m - 1))).Exact) (hm : -m + m = 0),
  (HomologicalComplex.sc' (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)) (m - 1) m (m + 1)).unop.Exact
Tactic: rwa [HomologicalComplex.exactAt_iff' _ (-(m + 1)) (-m) (-(m - 1)) (by grind [prev])
    (by grind [next])] at hK
Cleared hypotheses: hK, hm
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexPlus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasLimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.LimitOfShape (CochainComplex.plus C) J K
⊢ ∃ (n : ℤ), ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
have choose : ∀ (n : (j : J) → ℤ)
  (hn : ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE (n j)),
  ∃ (n : ℤ), ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
Tactic: choose n hn using p.prop_diag_obj
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexPlus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasLimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.LimitOfShape (CochainComplex.plus C) J K
⊢ CochainComplex.plus C K
have obtain : ∀ (n : ℤ) (hn : ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n),
  CochainComplex.plus C K
Tactic: obtain ⟨n, hn⟩ : ∃ (n : ℤ), ∀ (j : J), (p.diag.obj j).IsStrictlyGE n := by
      choose n hn using p.prop_diag_obj
      exact ⟨Finset.min' (Finset.image n ⊤ ∪ {0}) ⟨0, by grind⟩, fun j ↦
        (p.diag.obj j).isStrictlyGE_of_ge _ _ (Finset.min'_le _ (n j) (by simp))⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexPlus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasLimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.LimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
⊢ CochainComplex.plus C K
have refine : K.IsStrictlyGE n
Tactic: refine ⟨n, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexPlus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasLimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.LimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
⊢ K.IsStrictlyGE n
have rw : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
Tactic: rw [isStrictlyGE_iff]