awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c : ComplexShape ι
⊢ c.symm.symm = c

Tactic:
rfl

Premises used: ComplexShape.symm, rfl
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := ComplexShape ι) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, ComplexShape.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i j j' : ι
w : Relation.Comp c₁.Rel c₂.Rel i j
w' : Relation.Comp c₁.Rel c₂.Rel i j'
obtain : ∀ (k : ι) (w₁ : c₁.Rel i k) (w₂ : c₂.Rel k j), j = j'
⊢ j = j'

Tactic:
obtain ⟨k, w₁, w₂⟩ := w
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i j j' : ι
w' : Relation.Comp c₁.Rel c₂.Rel i j'
k : ι
w₁ : c₁.Rel i k
w₂ : c₂.Rel k j
obtain : ∀ (k' : ι) (w₁' : c₁.Rel i k') (w₂' : c₂.Rel k' j'), j = j'
⊢ j = j'

Tactic:
obtain ⟨k', w₁', w₂'⟩ := w'
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i j j' k : ι
w₁ : c₁.Rel i k
w₂ : c₂.Rel k j
k' : ι
w₁' : c₁.Rel i k'
w₂' : c₂.Rel k' j'
⊢ c₂.Rel k' j

Tactic:
rw [c₁.next_eq w₁ w₁'] at w₂

Premises used: ComplexShape.next_eq
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i j j' k : ι
w₁ : c₁.Rel i k
w₂ : c₂.Rel k j
k' : ι
w₁' : c₁.Rel i k'
w₂' : c₂.Rel k' j'
w₃ : c₂.Rel k' j
⊢ c₁.Rel i k'

Tactic:
rw [c₁.next_eq w₁ w₁'] at w₂

Premises used: ComplexShape.next_eq
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i j j' k : ι
w₁ : c₁.Rel i k
w₂ : c₂.Rel k j
k' : ι
w₁' : c₁.Rel i k'
w₂' : c₂.Rel k' j'
w₃ : c₂.Rel k' j
w₁'₁ : c₁.Rel i k'
⊢ c₂.Rel k' j'

Tactic:
rw [c₁.next_eq w₁ w₁'] at w₂

Premises used: ComplexShape.next_eq
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i j j' k : ι
w₁ : c₁.Rel i k
k' : ι
w₂ : c₂.Rel k' j
w₁' : c₁.Rel i k'
w₂' : c₂.Rel k' j'
⊢ j = j'

Tactic:
c₂.next_eq w₂ w₂'

Premises used: ComplexShape.next_eq
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i j j' k : ι
w₁ : c₁.Rel i k
k' : ι
w₂ : c₂.Rel k' j
w₁' : c₁.Rel i k'
w₂' : c₂.Rel k' j'
⊢ j = j'

Tactic:
exact c₂.next_eq w₂ w₂'

Premises used: ComplexShape.next_eq
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i i' j : ι
w : Relation.Comp c₁.Rel c₂.Rel i j
w' : Relation.Comp c₁.Rel c₂.Rel i' j
obtain : ∀ (k : ι) (w₁ : c₁.Rel i k) (w₂ : c₂.Rel k j), i = i'
⊢ i = i'

Tactic:
obtain ⟨k, w₁, w₂⟩ := w
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i i' j : ι
w' : Relation.Comp c₁.Rel c₂.Rel i' j
k : ι
w₁ : c₁.Rel i k
w₂ : c₂.Rel k j
obtain : ∀ (k' : ι) (w₁' : c₁.Rel i' k') (w₂' : c₂.Rel k' j), i = i'
⊢ i = i'

Tactic:
obtain ⟨k', w₁', w₂'⟩ := w'
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i i' j k : ι
w₁ : c₁.Rel i k
w₂ : c₂.Rel k j
k' : ι
w₁' : c₁.Rel i' k'
w₂' : c₂.Rel k' j
⊢ c₁.Rel i k'

Tactic:
rw [c₂.prev_eq w₂ w₂'] at w₁

Premises used: ComplexShape.prev_eq
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i i' j k : ι
w₁ : c₁.Rel i k
w₂ : c₂.Rel k j
k' : ι
w₁' : c₁.Rel i' k'
w₂' : c₂.Rel k' j
w₃ : c₁.Rel i k'
⊢ c₁.Rel i' k'

Tactic:
rw [c₂.prev_eq w₂ w₂'] at w₁

Premises used: ComplexShape.prev_eq
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i i' j k : ι
w₁ : c₁.Rel i k
w₂ : c₂.Rel k j
k' : ι
w₁' : c₁.Rel i' k'
w₂' : c₂.Rel k' j
w₃ : c₁.Rel i k'
w₁'₁ : c₁.Rel i' k'
⊢ c₂.Rel k' j

Tactic:
rw [c₂.prev_eq w₂ w₂'] at w₁

Premises used: ComplexShape.prev_eq
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i i' j k : ι
w₂ : c₂.Rel k j
k' : ι
w₁ : c₁.Rel i k'
w₁' : c₁.Rel i' k'
w₂' : c₂.Rel k' j
⊢ i = i'

Tactic:
c₁.prev_eq w₁ w₁'

Premises used: ComplexShape.prev_eq
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i i' j k : ι
w₂ : c₂.Rel k j
k' : ι
w₁ : c₁.Rel i k'
w₁' : c₁.Rel i' k'
w₂' : c₂.Rel k' j
⊢ i = i'

Tactic:
exact c₁.prev_eq w₁ w₁'

Premises used: ComplexShape.prev_eq
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c : ComplexShape ι
i : ι
allEq : ∀ (a b : { j : ι // c.Rel i j }), a = b
⊢ Subsingleton.{max 1 (u_1 + 1)} { j : ι // c.Rel i j }

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c : ComplexShape ι
i j : ι
rij : c.Rel i j
k : ι
rik : c.Rel i k
allEq : j = k
⊢ Subtype.mk (p := fun (j : ι) ↦ c.Rel i j) j rij = Subtype.mk (p := fun (j : ι) ↦ c.Rel i j) k rik

Tactic:
congr
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c : ComplexShape ι
i j : ι
rij : c.Rel i j
k : ι
rik : c.Rel i k
⊢ j = k

Tactic:
c.next_eq rij rik

Premises used: ComplexShape.next_eq
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c : ComplexShape ι
i j : ι
rij : c.Rel i j
k : ι
rik : c.Rel i k
⊢ j = k

Tactic:
exact c.next_eq rij rik

Premises used: ComplexShape.next_eq
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
apply : c.Rel i (c.next i)
⊢ c.next i = j

Tactic:
apply c.next_eq _ h

Premises used: ComplexShape.next_eq
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
rw : c.Rel i (if h : ∃ (j : ι), c.Rel i j then h.choose (p := c.Rel i) else i)
⊢ c.Rel i (c.next i)

Tactic:
rw [next]

Premises used: ComplexShape.next
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
rw : c.Rel i (⋯.choose (p := c.Rel i))
hc : ∃ (j : ι), c.Rel i j
⊢ c.Rel i (if h : ∃ (j : ι), c.Rel i j then h.choose (p := c.Rel i) else i)

Tactic:
rw [dif_pos]

Premises used: dif_pos
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel i (⋯.choose (p := c.Rel i))

Tactic:
Exists.choose_spec ⟨j, h⟩

Premises used: Exists.choose_spec, Exists.intro
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c : ComplexShape ι
j : ι
hj : ∀ (k : ι), ¬c.Rel j k
⊢ ¬∃ (j_1 : ι), c.Rel j j_1

Tactic:
simpa using hj
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
ι : Type u_1
c : ComplexShape ι
j : ι
hj : ¬c.Rel j (c.next j)
k : ι
hk' : c.Rel j k
⊢ c.Rel j (c.next j)

Tactic:
simpa only [c.next_eq' hk'] using hk'

Premises used: ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
α : Type u_2
inst : Add α
inst_1 : IsRightCancelAdd α
a i j : α
h : i + a = j
⊢ (up' a).Rel i j

Tactic:
h
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
α : Type u_2
inst : Add α
inst_1 : IsRightCancelAdd α
inst_2 : One α
i j : α
h : i + 1 = j
⊢ (up α).Rel i j

Tactic:
up'_mk (1 : α) i j h

Premises used: ComplexShape.up'_mk, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
α : Type u_1
inst : AddRightCancelSemigroup α
inst_1 : DecidableEq α
a x x_1 : α
⊢ Decidable (x + a = x_1)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ComplexShape
Goal:
α : Type u_1
inst : AddRightCancelSemigroup α
inst_1 : DecidableEq α
inst_2 : One α
⊢ DecidableRel (α := α) (Rel (up' 1))

Tactic:
infer_instance
-- 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₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
⊢ c₁₂.Rel (c₁.π c₂ c₁₂ (i₁, i₂)) (c₁.π c₂ c₁₂ (i₁', i₂))

Tactic:
TotalComplexShape.rel₁ h i₂

Premises used: TotalComplexShape.rel₁
-- 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₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
⊢ c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂)) = c₁.π c₂ c₁₂ (i₁', i₂)

Tactic:
c₁₂.next_eq' (rel_π₁ c₂ c₁₂ h i₂)

Premises used: ComplexShape.rel_π₁, ComplexShape.next_eq'
-- 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₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
⊢ c₁₂.prev (c₁.π c₂ c₁₂ (i₁', i₂)) = c₁.π c₂ c₁₂ (i₁, i₂)

Tactic:
c₁₂.prev_eq' (rel_π₁ c₂ c₁₂ h i₂)

Premises used: ComplexShape.prev_eq', ComplexShape.rel_π₁
-- 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₁₂
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
⊢ c₁₂.Rel (c₁.π c₂ c₁₂ (i₁, i₂)) (c₁.π c₂ c₁₂ (i₁, i₂'))

Tactic:
TotalComplexShape.rel₂ i₁ h

Premises used: TotalComplexShape.rel₂
-- 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₁₂
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
⊢ c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂)) = c₁.π c₂ c₁₂ (i₁, i₂')

Tactic:
c₁₂.next_eq' (rel_π₂ c₁ c₁₂ i₁ h)

Premises used: ComplexShape.rel_π₂, ComplexShape.next_eq'
-- 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₁₂
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
⊢ c₁₂.prev (c₁.π c₂ c₁₂ (i₁, i₂')) = c₁.π c₂ c₁₂ (i₁, i₂)

Tactic:
c₁₂.prev_eq' (rel_π₂ c₁ c₁₂ i₁ h)

Premises used: ComplexShape.prev_eq', ComplexShape.rel_π₂
-- 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₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel 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:
TotalComplexShape.ε₂_ε₁ h₁ h₂

Premises used: TotalComplexShape.ε₂_ε₁
-- 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₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel 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₂) * 1 = -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')

Tactic:
rw [← Int.units_mul_self (ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂')), mul_assoc]

Premises used: mul_assoc, Prod.mk, ComplexShape.ε₁, 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₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
arg : 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:
arg 2
-- 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₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel 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₂'))

Tactic:
rw [← mul_assoc, ε₂_ε₁ c₁₂ h₁ h₂]

Premises used: mul_assoc, ComplexShape.ε₂_ε₁
-- 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₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
arg : -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:
arg 2
      rw [← mul_assoc, ε₂_ε₁ c₁₂ h₁ h₂]

Premises used: mul_assoc, ComplexShape.ε₂_ε₁
-- 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₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
conv_lhs :
  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:
conv_lhs =>
      arg 2
      rw [← mul_assoc, ε₂_ε₁ c₁₂ h₁ h₂]

Premises used: mul_assoc, ComplexShape.ε₂_ε₁
-- 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₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel 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₄ :
  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₈ 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₂')

Tactic:
rw [neg_mul, neg_mul, neg_mul, mul_neg, neg_inj, ← mul_assoc, ← mul_assoc,
      Int.units_mul_self, one_mul]

Premises used: mul_assoc, neg_inj, neg_mul, one_mul, mul_neg, Int.units_mul_self
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I : Type u_7
inst : AddMonoid I
c : ComplexShape I
inst_1 : c.TensorSigns
p q : I
hpq : c.Rel p q
r : I
⊢ c.Rel (p + r) (q + r)

Tactic:
TensorSigns.rel_add _ _ _ hpq

Premises used: ComplexShape.TensorSigns.rel_add
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I : Type u_7
inst : AddMonoid I
c : ComplexShape I
inst_1 : c.TensorSigns
r p q : I
hpq : c.Rel p q
⊢ c.Rel (r + p) (r + q)

Tactic:
TensorSigns.add_rel _ _ _ hpq

Premises used: ComplexShape.TensorSigns.add_rel
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I : Type u_7
inst : AddMonoid I
c : ComplexShape I
inst_1 : c.TensorSigns
⊢ c.ε 0 = 1

Tactic:
apply map_one

Premises used: map_one
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I : Type u_7
inst : AddMonoid I
c : ComplexShape I
inst_1 : c.TensorSigns
p q : I
hpq : c.Rel p q
⊢ c.ε q = -c.ε p

Tactic:
TensorSigns.ε'_succ p q hpq

Premises used: ComplexShape.TensorSigns.ε'_succ
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I : Type u_7
inst : AddMonoid I
c : ComplexShape I
inst_1 : c.TensorSigns
p q : I
⊢ c.ε (p + q) = c.ε p * c.ε q

Tactic:
apply map_mul

Premises used: map_mul
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I : Type u_7
inst : AddMonoid I
c : ComplexShape I
inst_1 : c.TensorSigns
p q : I
hp : c.Rel p (c.next p)
⊢ c.next (p + q) = c.next p + q

Tactic:
c.next_eq' (c.rel_add hp q)

Premises used: ComplexShape.rel_add, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
I : Type u_7
inst : AddMonoid I
c : ComplexShape I
inst_1 : c.TensorSigns
p q : I
hq : c.Rel q (c.next q)
⊢ c.next (p + q) = p + c.next q

Tactic:
c.next_eq' (c.add_rel p hq)

Premises used: ComplexShape.add_rel, ComplexShape.next_eq'
-- 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
i₁ i₁' i₂ i₂' : I
h : c.Rel i₁ i₁'
h_1 : c.Rel i₂ i₂'
dsimp : c.ε i₁ * 1 = -1 * c.ε i₁'
⊢ HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I × I → ℤˣ) (i₁, i₂) with
        | (p, snd) => c.ε p :
        ℤˣ)
      (1 : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ)
      (match (motive := I × I → ℤˣ) (i₁', i₂) with
        | (p, snd) => c.ε p :
        ℤˣ)

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
i₁ i₁' i₂ i₂' : I
h : c.Rel i₁ i₁'
h_1 : c.Rel i₂ i₂'
rw : c.ε i₁ * 1 = -(1 * c.ε i₁')
rw₁ : c.ε i₁ * 1 = -c.ε i₁'
rw₂ : c.ε i₁ = -c.ε i₁'
rw₃ : c.ε i₁ = - -c.ε i₁
rw₄ rw₅ : c.ε i₁ = c.ε i₁
⊢ c.ε i₁ * 1 = -1 * c.ε i₁'

Tactic:
rw [neg_mul, one_mul, mul_one, c.ε_succ h, neg_neg]

Premises used: ComplexShape.ε_succ, neg_neg, neg_mul, 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
p q r : ℕ
hpq : q + 1 = p
⊢ q + r + 1 = p + r

Tactic:
lia
-- 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
p q r : ℕ
hpq : q + 1 = p
⊢ r + q + 1 = r + p

Tactic:
lia
-- 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
q : ℕ
rw : HPow.hPow (α := ℤˣ) (-1) q = -(HPow.hPow (α := ℤˣ) (-1) q * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 1)
rw₁ : HPow.hPow (α := ℤˣ) (-1) q = -(HPow.hPow (α := ℤˣ) (-1) q * -1)
rw₂ : HPow.hPow (α := ℤˣ) (-1) q = - -(HPow.hPow (α := ℤˣ) (-1) q * 1)
rw₃ : HPow.hPow (α := ℤˣ) (-1) q = - -HPow.hPow (α := ℤˣ) (-1) q
rw₄ rw₅ : HPow.hPow (α := ℤˣ) (-1) q = HPow.hPow (α := ℤˣ) (-1) q
⊢ HPow.hPow (α := ℤˣ) (-1) q = -HPow.hPow (α := ℤˣ) (-1) (q + 1)

Tactic:
rw [pow_add, pow_one, mul_neg, mul_one, neg_neg]

Premises used: pow_add, neg_neg, pow_one, mul_one, mul_neg
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
n : ℕ
⊢ (down ℕ).ε n = HPow.hPow (α := ℤˣ) (-1) n

Tactic:
rfl

Premises used: rfl
-- 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
p q r : ℤ
hpq : p + 1 = q
⊢ p + r + 1 = q + r

Tactic:
lia
-- 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
p q r : ℤ
hpq : p + 1 = q
⊢ r + p + 1 = r + q

Tactic:
lia
-- 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
p : ℤ
rw rw₁ : -p.negOnePow = -p.negOnePow
⊢ (p + 1).negOnePow = -p.negOnePow

Tactic:
rw [Int.negOnePow_succ]

Premises used: Int.negOnePow_succ
-- Module: Mathlib.Algebra.Homology.ComplexShapeSigns
Goal:
n : ℤ
⊢ (up ℤ).ε n = n.negOnePow

Tactic:
rfl

Premises used: Int.negOnePow, rfl
-- 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₃))

Tactic:
apply Associative.assoc

Premises used: ComplexShape.Associative.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 : 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 (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, 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 : 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 (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₁ c₃ c₂₃ (i₂, i₃) =
    c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)

Tactic:
apply Associative.ε₂_ε₁

Premises used: ComplexShape.Associative.ε₂_ε₁