awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₁₂ c₃ c
inst_2 : TotalComplexShape c₂ c₃ c₂₃
inst_3 : TotalComplexShape c₁ c₂₃ c
inst_4 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ c₁₂.ε₂ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₂ c₃ c₂₃ (i₂, i₃)

Tactic:
apply Associative.ε₂_eq_mul

Premises used: ComplexShape.Associative.ε₂_eq_mul
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
x x_1 x_2 : I
rw rw₁ : Eq (α := ℤˣ) 1 1
⊢ 1 = HMul.hMul (α := ℤˣ) 1 1

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
x x_1 x_2 : I
dsimp : c.ε x * 1 = 1 * c.ε x
⊢ c.ε₂ c c (x, c.π c c (x_1, x_2)) * c.ε₁ c c (x_1, x_2) = c.ε₁ c c (c.π c c (x, x_1), x_2) * c.ε₂ c c (x, x_1)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
x x_1 x_2 : I
rw : c.ε x * 1 = c.ε x
rw₁ rw₂ : c.ε x = c.ε x
⊢ c.ε x * 1 = 1 * c.ε x

Tactic:
rw [one_mul, mul_one]

Premises used: mul_one, one_mul
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
x x_1 x_2 : I
dsimp : c.ε (x + x_1) = c.ε x * c.ε x_1
⊢ c.ε₂ c c (c.π c c (x, x_1), x_2) = c.ε₂ c c (x, c.π c c (x_1, x_2)) * c.ε₂ c c (x_1, x_2)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
x x_1 x_2 : I
rw rw₁ : c.ε x * c.ε x_1 = c.ε x * c.ε x_1
⊢ c.ε (x + x_1) = c.ε x * c.ε x_1

Tactic:
rw [ε_add]

Premises used: ComplexShape.ε_add
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₂
i₂ i₂' : I₁
h₂ : c₂.Rel i₁ i₁'
h₁ : c₁.Rel i₂ i₂'
rw :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ) =
    -HMul.hMul (α := ℤˣ) (β := ℤˣ)
        (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
          | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
          ℤˣ)
        (match (motive := I₂ × I₁ → ℤˣ) (i₁', i₂) with
          | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
          ℤˣ)
rw₁ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ) =
    -(-c₁.ε₁ c₂ c₁₂ (i₂, i₁) * c₁.ε₂ c₂ c₁₂ (i₂', i₁))
rw₂ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ) =
    - -(c₁.ε₁ c₂ c₁₂ (i₂, i₁) * c₁.ε₂ c₂ c₁₂ (i₂', i₁))
rw₃ rw₄ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ) =
    c₁.ε₁ c₂ c₁₂ (i₂, i₁) * c₁.ε₂ c₂ c₁₂ (i₂', i₁)
⊢ HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (-match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
          | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁', i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)

Tactic:
rw [neg_mul, ComplexShape.ε₂_ε₁ c₁₂ h₁ h₂, neg_mul, neg_neg]

Premises used: neg_neg, ComplexShape.ε₂_ε₁, neg_mul
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
this : TotalComplexShape c₂ c₁ c₁₂ := symm c₁ c₂ c₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
x : I₂
⊢ 1 * c₁.ε₁ c₂ c₁₂ (i₁, x) = c₂.ε₂ c₁ c₁₂ (x, i₁) * 1

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
this : TotalComplexShape c₂ c₁ c₁₂ := symm c₁ c₂ c₁₂
x : I₁
x_1 : I₂
⊢ ∀ {i₂' : I₂} (h₂ : c₂.Rel x_1 i₂'), 1 * c₁.ε₂ c₂ c₁₂ (x, x_1) = c₂.ε₁ c₁ c₁₂ (x_1, x) * 1

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₁ : I₁
i₂ : I₂
⊢ c₂.π c₁ c₁₂ (i₂, i₁) = c₁.π c₂ c₁₂ (i₁, i₂)

Tactic:
apply TotalComplexShapeSymmetry.symm

Premises used: TotalComplexShapeSymmetry.symm
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
j : I₁₂
x : (↑(c₂.π c₁ c₁₂ ⁻¹' {j}) : Type (max u_1 u_2))
i₂ : I₂
i₁ : I₁
h : (i₂, i₁) ∈ c₂.π c₁ c₁₂ ⁻¹' {j}
⊢ (i₁, i₂) ∈ c₁.π c₂ c₁₂ ⁻¹' {j}

Tactic:
simpa [π_symm] using h

Premises used: ComplexShape.π_symm
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
j : I₁₂
x : (↑(c₁.π c₂ c₁₂ ⁻¹' {j}) : Type (max u_1 u_2))
i₁ : I₁
i₂ : I₂
h : (i₁, i₂) ∈ c₁.π c₂ c₁₂ ⁻¹' {j}
⊢ (i₂, i₁) ∈ c₂.π c₁ c₁₂ ⁻¹' {j}

Tactic:
simpa [π_symm] using h

Premises used: ComplexShape.π_symm
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
i₂ : I₂
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂) = c₂.ε₂ c₁ c₁₂ (i₂, i₁) * c₁.σ c₂ c₁₂ i₁' i₂

Tactic:
TotalComplexShapeSymmetry.σ_ε₁ h₁ i₂

Premises used: TotalComplexShapeSymmetry.σ_ε₁
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₁ : I₁
i₂ i₂' : I₂
h₂ : c₂.Rel i₂ i₂'
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * c₁.ε₂ c₂ c₁₂ (i₁, i₂) = c₂.ε₁ c₁ c₁₂ (i₂, i₁) * c₁.σ c₂ c₁₂ i₁ i₂'

Tactic:
TotalComplexShapeSymmetry.σ_ε₂ i₁ h₂

Premises used: TotalComplexShapeSymmetry.σ_ε₂
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
rw : (p * q).negOnePow = q.negOnePow * ((p + 1) * q).negOnePow
rw₁ : (p * q).negOnePow = (q + (p + 1) * q).negOnePow
rw₂ : (p * q).negOnePow = ((p + 1) * q + q).negOnePow
rw₃ : (p * q).negOnePow = (p * q + 1 * q + q).negOnePow
rw₄ : (p * q).negOnePow = (p * q + q + q).negOnePow
rw₅ : (p * q).negOnePow = (p * q + q).negOnePow * q.negOnePow
rw₆ : (p * q).negOnePow = (p * q).negOnePow * q.negOnePow * q.negOnePow
rw₇ : (p * q).negOnePow = (p * q).negOnePow * (q.negOnePow * q.negOnePow)
rw₈ : (p * q).negOnePow = (p * q).negOnePow * 1
rw₉ rw₁₀ : (p * q).negOnePow = (p * q).negOnePow
⊢ (p * q).negOnePow * 1 = q.negOnePow * ((p + 1) * q).negOnePow

Tactic:
rw [mul_one, ← Int.negOnePow_add, add_comm q, add_mul, one_mul, Int.negOnePow_add,
      Int.negOnePow_add, mul_assoc, Int.units_mul_self, mul_one]

Premises used: add_mul, mul_assoc, Int.negOnePow_add, add_comm, mul_one, one_mul, Int.units_mul_self
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
rw : (p * q).negOnePow * p.negOnePow = (p * (q + 1)).negOnePow
rw₁ : (p * q + p).negOnePow = (p * (q + 1)).negOnePow
rw₂ : (p * q + p).negOnePow = (p * q + p * 1).negOnePow
rw₃ rw₄ : (p * q + p).negOnePow = (p * q + p).negOnePow
⊢ (p * q).negOnePow * p.negOnePow = 1 * (p * (q + 1)).negOnePow

Tactic:
rw [one_mul, ← Int.negOnePow_add, mul_add, mul_one]

Premises used: Int.negOnePow_add, mul_add, mul_one, one_mul
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ i₂' : I₂
h₂ : c₂.Rel i₂ i₂'
i₁ : I₁
apply :
  c₁.σ c₂ c₁₂ i₁ i₂ * c₂.ε₁ c₁ c₁₂ (i₂, i₁) * c₁.ε₂ c₂ c₁₂ (i₁, i₂) =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * c₂.ε₁ c₁ c₁₂ (i₂, i₁) = c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂'

Tactic:
apply mul_right_cancel (b := ComplexShape.ε₂ c₁ c₂ c₁₂ (i₁, i₂))

Premises used: mul_right_cancel
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ i₂' : I₂
h₂ : c₂.Rel i₂ i₂'
i₁ : I₁
rw :
  c₁.σ c₂ c₁₂ i₁ i₂ * (c₂.ε₁ c₁ c₁₂ (i₂, i₁) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)) =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * c₂.ε₁ c₁ c₁₂ (i₂, i₁) * c₁.ε₂ c₂ c₁₂ (i₁, i₂) =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ i₂' : I₂
h₂ : c₂.Rel i₂ i₂'
i₁ : I₁
nth_rw :
  c₁.σ c₂ c₁₂ i₁ i₂ * (c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₂.ε₁ c₁ c₁₂ (i₂, i₁)) =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * (c₂.ε₁ c₁ c₁₂ (i₂, i₁) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)) =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)

Tactic:
nth_rw 2 [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ i₂' : I₂
h₂ : c₂.Rel i₂ i₂'
i₁ : I₁
rw :
  c₁.σ c₂ c₁₂ i₁ i₂ * c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₂.ε₁ c₁ c₁₂ (i₂, i₁) =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)
rw₁ :
  c₂.ε₁ c₁ c₁₂ (i₂, i₁) * c₁.σ c₂ c₁₂ i₁ i₂' * c₂.ε₁ c₁ c₁₂ (i₂, i₁) =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)
rw₂ :
  c₂.ε₁ c₁ c₁₂ (i₂, i₁) * (c₂.ε₁ c₁ c₁₂ (i₂, i₁) * c₁.σ c₂ c₁₂ i₁ i₂') =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)
rw₃ :
  c₂.ε₁ c₁ c₁₂ (i₂, i₁) * c₂.ε₁ c₁ c₁₂ (i₂, i₁) * c₁.σ c₂ c₁₂ i₁ i₂' =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)
rw₄ : 1 * c₁.σ c₂ c₁₂ i₁ i₂' = c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)
rw₅ : c₁.σ c₂ c₁₂ i₁ i₂' = c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)
rw₆ : c₁.σ c₂ c₁₂ i₁ i₂' = c₁.ε₂ c₂ c₁₂ (i₁, i₂) * (c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂')
rw₇ : c₁.σ c₂ c₁₂ i₁ i₂' = c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂'
rw₈ : c₁.σ c₂ c₁₂ i₁ i₂' = 1 * c₁.σ c₂ c₁₂ i₁ i₂'
rw₉ rw₁₀ : c₁.σ c₂ c₁₂ i₁ i₂' = c₁.σ c₂ c₁₂ i₁ i₂'
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * (c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₂.ε₁ c₁ c₁₂ (i₂, i₁)) =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)

Tactic:
rw [← mul_assoc, ComplexShape.σ_ε₂ c₁ c₁₂ i₁ h₂, mul_comm, ← mul_assoc,
      Int.units_mul_self, one_mul, mul_comm, ← mul_assoc, Int.units_mul_self, one_mul]

Premises used: mul_assoc, ComplexShape.σ_ε₂, mul_comm, one_mul, Int.units_mul_self
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ : I₂
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
apply :
  c₁.σ c₂ c₁₂ i₁ i₂ * c₂.ε₂ c₁ c₁₂ (i₂, i₁) * c₁.ε₁ c₂ c₁₂ (i₁, i₂) =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * c₂.ε₂ c₁ c₁₂ (i₂, i₁) = c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂

Tactic:
apply mul_right_cancel (b := ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂))

Premises used: mul_right_cancel
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ : I₂
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
rw :
  c₁.σ c₂ c₁₂ i₁ i₂ * (c₂.ε₂ c₁ c₁₂ (i₂, i₁) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)) =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * c₂.ε₂ c₁ c₁₂ (i₂, i₁) * c₁.ε₁ c₂ c₁₂ (i₁, i₂) =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ : I₂
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
nth_rw :
  c₁.σ c₂ c₁₂ i₁ i₂ * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₂.ε₂ c₁ c₁₂ (i₂, i₁)) =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * (c₂.ε₂ c₁ c₁₂ (i₂, i₁) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)) =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)

Tactic:
nth_rw 2 [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ : I₂
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
rw :
  c₁.σ c₂ c₁₂ i₁ i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₂.ε₂ c₁ c₁₂ (i₂, i₁) =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)
rw₁ :
  c₂.ε₂ c₁ c₁₂ (i₂, i₁) * c₁.σ c₂ c₁₂ i₁' i₂ * c₂.ε₂ c₁ c₁₂ (i₂, i₁) =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)
rw₂ :
  c₂.ε₂ c₁ c₁₂ (i₂, i₁) * (c₂.ε₂ c₁ c₁₂ (i₂, i₁) * c₁.σ c₂ c₁₂ i₁' i₂) =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)
rw₃ :
  c₂.ε₂ c₁ c₁₂ (i₂, i₁) * c₂.ε₂ c₁ c₁₂ (i₂, i₁) * c₁.σ c₂ c₁₂ i₁' i₂ =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)
rw₄ : 1 * c₁.σ c₂ c₁₂ i₁' i₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)
rw₅ : c₁.σ c₂ c₁₂ i₁' i₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)
rw₆ : c₁.σ c₂ c₁₂ i₁' i₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂)
rw₇ : c₁.σ c₂ c₁₂ i₁' i₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂
rw₈ : c₁.σ c₂ c₁₂ i₁' i₂ = 1 * c₁.σ c₂ c₁₂ i₁' i₂
rw₉ rw₁₀ : c₁.σ c₂ c₁₂ i₁' i₂ = c₁.σ c₂ c₁₂ i₁' i₂
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₂.ε₂ c₁ c₁₂ (i₂, i₁)) =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)

Tactic:
rw [← mul_assoc, ComplexShape.σ_ε₁ c₂ c₁₂ h₁ i₂, mul_comm, ← mul_assoc,
      Int.units_mul_self, one_mul, mul_comm, ← mul_assoc, Int.units_mul_self, one_mul]

Premises used: mul_assoc, ComplexShape.σ_ε₁, mul_comm, one_mul, Int.units_mul_self
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
inst_3 : TotalComplexShapeSymmetry c₂ c₁ c₁₂
inst_4 : TotalComplexShapeSymmetrySymmetry c₁ c₂ c₁₂
i₁ : I₁
i₂ : I₂
⊢ c₂.σ c₁ c₁₂ i₂ i₁ = c₁.σ c₂ c₁₂ i₁ i₂

Tactic:
apply TotalComplexShapeSymmetrySymmetry.σ_symm

Premises used: TotalComplexShapeSymmetrySymmetry.σ_symm
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ Functor.IsLocalization (C := CochainComplex.{v, u, 0} C ℤ) (D :=
    HomologicalComplexUpToQuasiIso.{v, u, 0, w} C (ComplexShape.up ℤ)) HomologicalComplexUpToQuasiIso.Q
    (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
f : K ⟶ L
inst_3 : QuasiIso f
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q f)

Tactic:
Localization.inverts Q (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) _
    (inferInstanceAs (QuasiIso f))

Premises used: HomologicalComplex.quasiIso, DerivedCategory.Q, Int, CategoryTheory.Localization.inverts, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
f : K ⟶ L
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C)
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)) (Functor.obj Q L))
    (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f) ≫
      NatTrans.app (Iso.hom (quotientCompQhIso C)) L)
    (NatTrans.app (Iso.hom (quotientCompQhIso C)) K ≫ CategoryTheory.Functor.map Q f)

Tactic:
(quotientCompQhIso C).hom.naturality f

Premises used: CategoryTheory.NatTrans.naturality, DerivedCategory.quotientCompQhIso, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
f : K ⟶ L
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q K)
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)))
    (CategoryTheory.Functor.map Q f ≫ NatTrans.app (Iso.inv (quotientCompQhIso C)) L)
    (NatTrans.app (Iso.inv (quotientCompQhIso C)) K ≫
      CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f))

Tactic:
(quotientCompQhIso C).inv.naturality f

Premises used: CategoryTheory.NatTrans.naturality, DerivedCategory.quotientCompQhIso, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ Functor.IsLocalization (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (D :=
    HomologicalComplexUpToQuasiIso.{v, u, 0, w} C (ComplexShape.up ℤ)) HomologicalComplexUpToQuasiIso.Qh
    (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
rw :
  Functor.IsLocalization (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (D := DerivedCategory.{w, v, u} C) Qh
    (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
⊢ Functor.IsLocalization (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (D := DerivedCategory.{w, v, u} C) Qh
    (ObjectProperty.trW (HomotopyCategory.subcategoryAcyclic C))

Tactic:
rw [← HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic]

Premises used: HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic