awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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)
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 ⋯))
n : ℤ
this :
  Quiver.Hom.op (f.f (-n)) =
    HAdd.hAdd (α := op (L.X (-n)) ⟶ op (K.X (-n))) (β := 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)))
            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)))
            h.hom :
          op (L.X (-n)) ⟶ op (K.X (-n))) +
      Quiver.Hom.op (g.f (-n))
⊢ - -(n + 1) = n + 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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)
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 ⋯))
n : ℤ
this :
  Quiver.Hom.op (f.f (-n)) =
    HAdd.hAdd (α := op (L.X (-n)) ⟶ op (K.X (-n))) (β := 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)))
            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)))
            h.hom :
          op (L.X (-n)) ⟶ op (K.X (-n))) +
      Quiver.Hom.op (g.f (-n))
⊢ - -n = n

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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 : autoParam (p + p' = 0) homotopyUnop_hom_eq._auto_1
hq : autoParam (q + q' = 0) homotopyUnop_hom_eq._auto_2
⊢ p = -p'

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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 : autoParam (p + p' = 0) homotopyUnop_hom_eq._auto_1
hq : autoParam (q + q' = 0) homotopyUnop_hom_eq._auto_2
⊢ -q' = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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
⊢ p' = -p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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
obtain :
  ∀ (hp : p + -p = 0),
    (homotopyUnop h).hom p q =
      (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ Quiver.Hom.unop (h.hom q' (-p)) ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom
⊢ (homotopyUnop h).hom p q =
    (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom q' p').unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom

Tactic:
obtain rfl : p' = -p := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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
⊢ q' = -q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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
obtain :
  ∀ (hq : q + -q = 0),
    (homotopyUnop h).hom p q =
      (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ Quiver.Hom.unop (h.hom (-q) (-p)) ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom
⊢ (homotopyUnop h).hom p q =
    (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ Quiver.Hom.unop (h.hom q' (-p)) ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom

Tactic:
obtain rfl : q' = -q := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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 : ℤ
hp : p + -p = 0
hq : q + -q = 0
⊢ (homotopyUnop h).hom p q =
    (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ Quiver.Hom.unop (h.hom (-q) (-p)) ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom

Tactic:
simp [homotopyUnop]

Premises used: CochainComplex.homotopyUnop
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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
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
⊢ (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

Tactic:
ext p q
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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 : ℤ
⊢ 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:
simp [homotopyUnop_hom_eq _ p q (-p) (-q),
      homotopyOp_hom_eq _ (-q) (-p) q p]

Premises used: CochainComplex.homotopyUnop_hom_eq, CochainComplex.homotopyOp_hom_eq, Neg.neg
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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)
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
⊢ (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

Tactic:
ext p q
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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 : ℤ
⊢ 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:
simp [homotopyOp_hom_eq _ p q (-p) (-q),
      homotopyUnop_hom_eq _ (-q) (-p) q p]

Premises used: CochainComplex.homotopyUnop_hom_eq, CochainComplex.homotopyOp_hom_eq, Neg.neg
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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
⊢ n = -m

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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 K (-m)

Tactic:
obtain rfl : n = -m := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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)
⊢ -m + m = 0

Tactic:
obtain rfl : n = -m := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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
⊢ (ComplexShape.up ℤ).prev m = m - 1

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

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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
rw : (HomologicalComplex.sc' (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)) (m - 1) m (m + 1)).unop.Exact
⊢ HomologicalComplex.ExactAt (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)) m

Tactic:
rw [HomologicalComplex.exactAt_iff' _ (m - 1) m (m + 1) (by simp) (by simp),
    ← ShortComplex.exact_unop_iff]

Premises used: CategoryTheory.ShortComplex.exact_unop_iff, HSub.hSub, HAdd.hAdd, OfNat.ofNat, HomologicalComplex.exactAt_iff'
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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
⊢ (ComplexShape.up ℤ).prev (-m) = -(m + 1)

Tactic:
grind [prev]

Premises used: CochainComplex.prev
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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
⊢ (ComplexShape.up ℤ).next (-m) = -(m - 1)

Tactic:
grind [next]

Premises used: CochainComplex.next
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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
rwa rwa₁ rwa₂ 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
⊢ (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

Premises used: HSub.hSub, HAdd.hAdd, OfNat.ofNat, HomologicalComplex.exactAt_iff', Neg.neg
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
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 ℤ
hK : HomologicalComplex.Acyclic K
⊢ HomologicalComplex.Acyclic (Functor.obj (Equivalence.functor (opEquivalence C)) (op K))

Tactic:
fun n ↦ exactAt_op (hK (-n)) n

Premises used: CochainComplex.exactAt_op, HomologicalComplex.Acyclic, Neg.neg
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ CochainComplex.plus C K ↔ ∃ (n : ℤ), K.IsStrictlyGE n

Tactic:
Iff.rfl

Premises used: Iff.rfl, CochainComplex.plus
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X Y : CochainComplex.{v_1, u_1, 0} C ℤ
e : X ≅ Y
n : ℤ
h : X.IsStrictlyGE n
⊢ CochainComplex.plus C Y

Tactic:
⟨n, isStrictlyGE_of_iso e n⟩

Premises used: CochainComplex.isStrictlyGE_of_iso, Exists.intro, CochainComplex.plus
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X Y : CochainComplex.{v_1, u_1, 0} C ℤ
e : X ≅ Y
n : ℤ
h : X.IsStrictlyGE n
⊢ CochainComplex.plus C Y

Tactic:
exact ⟨n, isStrictlyGE_of_iso e n⟩
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
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
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
⊢ ∃ (n : ℤ), ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n

Tactic:
choose n hn using p.prop_diag_obj

Premises used: CategoryTheory.ObjectProperty.LimitOfShape.prop_diag_obj
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
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) → ℤ
hn : ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE (n j)
⊢ 0 ∈ Finset.image n ⊤ ∪ {0}

Tactic:
grind
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
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) → ℤ
hn : ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE (n j)
j : J
⊢ n j ∈ Finset.image n ⊤ ∪ {0}

Tactic:
simp