awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
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₂)
⊢ 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₂)
have rw₄ : 1 * 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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
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₂)
⊢ 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₂)
have rw₅ : 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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
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₂)
⊢ 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₂)
have rw₆ : 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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
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₂)
⊢ 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₂)
have rw₇ : 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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
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₂
⊢ 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₂)
have rw₈ : c₁.σ c₂ c₁₂ i₁' i₂ = 1 * 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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
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₂
⊢ 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₂)
have rw₉ : 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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Basic (goal)
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 := DerivedCategory.{w, v, u} C) Qh
    (ObjectProperty.trW (HomotopyCategory.subcategoryAcyclic C))
have rw : Functor.IsLocalization (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (D := DerivedCategory.{w, v, u} C) Qh
  (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
Tactic: rw [← HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
⊢ Functor.Additive (C := DerivedCategory.{w, v, u} C) (shiftFunctor (DerivedCategory.{w, v, u} C) n)
have rw : Functor.Additive (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (D := DerivedCategory.{w, v, u} C)
  (Qh ⋙ shiftFunctor (DerivedCategory.{w, v, u} C) n)
Tactic: rw [Localization.functor_additive_iff
    Qh (HomotopyCategory.subcategoryAcyclic C).trW]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (DerivedCategory.{w, v, u} C)
⊢ Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
      (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T ↔
    ∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
      Nonempty.{w + 1} (T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f))
have mp : Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C))) (@distinguishedTriangles _ _ sorry _ instPreadditive sorry _)
    T →
  ∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
    Nonempty.{w + 1} (T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (DerivedCategory.{w, v, u} C)
mp :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
      (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T →
    ∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
      Nonempty.{w + 1} (T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f))
⊢ Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
      (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T ↔
    ∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
      Nonempty.{w + 1} (T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f))
have mpr : (∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
    Nonempty.{w + 1} (T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f))) →
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ sorry _ instPreadditive sorry _) T
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (DerivedCategory.{w, v, u} C)
T' : Triangle (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
e : T ≅ Functor.obj (Functor.mapTriangle Qh) T'
X Y : CochainComplex.{v, u, 0} C ℤ
f : X ⟶ Y
e' : T' ≅ CochainComplex.mappingCone.triangleh f
⊢ ∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
    Nonempty.{w + 1} (T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f))
have mp : T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f)
Tactic: refine ⟨_, _, f, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (DerivedCategory.{w, v, u} C)
X Y : CochainComplex.{v, u, 0} C ℤ
f : X ⟶ Y
e : T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f)
⊢ Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T
have mpr : Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))))
  (@distinguishedTriangles _ _ sorry _ (HomotopyCategory.instPreadditive C (ComplexShape.up ℤ)) sorry _)
  (Functor.obj (Functor.mapTriangle (HomotopyCategory.quotient C (ComplexShape.up ℤ)))
    (CochainComplex.mappingCone.triangle f))
Tactic: refine isomorphic_distinguished _ (Qh.map_distinguished _ ?_) _
      (e ≪≫ (Functor.mapTriangleIso (quotientCompQhIso C)).symm.app _ ≪≫
      (Functor.mapTriangleCompIso (HomotopyCategory.quotient C _) Qh).app _)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Basic (goal)
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 ℤ
φ : K ⟶ L
⊢ Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) (Functor.obj (Functor.mapTriangle Q) (mappingCone.triangle φ))
have rw : ∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
  Nonempty.{w + 1}
    (Iso (C := Triangle (DerivedCategory.{w, v, u} C)) (Functor.obj (Functor.mapTriangle Q) (mappingCone.triangle φ))
      (Functor.obj (Functor.mapTriangle Q) (mappingCone.triangle f)))
Tactic: rw [mem_distTriang_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Basic (goal)
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 ℤ
φ : K ⟶ L
⊢ Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle Q) (mappingCocone.triangle φ))
have rw : Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C))) (@distinguishedTriangles _ _ sorry _ instPreadditive sorry _)
  (Triangle.rotate (Functor.obj (Functor.mapTriangle Q) (mappingCocone.triangle φ)))
Tactic: rw [rotate_distinguished_triangle]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
⊢ Eq (α :=
    Quiver.Hom (V := C ⥤ DerivedCategory.{w, v, u} C) (SingleFunctors.functor (singleFunctors C) n)
      (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n))
    (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) n)
    (𝟙 (SingleFunctors.functor (singleFunctors C) n))
have w : ∀ (X : C),
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
      (Functor.obj (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n) X))
    (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) n) X)
    (NatTrans.app (𝟙 (SingleFunctors.functor (singleFunctors C) n)) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X : C
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
      (Functor.obj (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n) X))
    (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) n) X)
    (NatTrans.app (𝟙 (SingleFunctors.functor (singleFunctors C) n)) X)
have w : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
    (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
  (CategoryTheory.Functor.map Qh (𝟙 (Functor.obj (SingleFunctors.functor (HomotopyCategory.singleFunctors C) n) X)) ≫
      𝟙 (Functor.obj (singleFunctor C n) X) ≫
        𝟙
          (Functor.obj HomologicalComplexUpToQuasiIso.Q
            (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)) :
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
      (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
  (𝟙 (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X) :
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
      (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))
Tactic: dsimp [singleFunctorsPostcompQIso, HomotopyCategory.singleFunctorsPostcompQuotientIso,
    quotientCompQhIso, HomologicalComplexUpToQuasiIso.quotientCompQhIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X : C
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
      (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (CategoryTheory.Functor.map Qh (𝟙 (Functor.obj (SingleFunctors.functor (HomotopyCategory.singleFunctors C) n) X)) ≫
        𝟙 (Functor.obj (singleFunctor C n) X) ≫
          𝟙
            (Functor.obj HomologicalComplexUpToQuasiIso.Q
              (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)) :
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
        (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (𝟙 (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X) :
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
        (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))
have w : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
    (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
  (𝟙 (Functor.obj Qh (Functor.obj (SingleFunctors.functor (HomotopyCategory.singleFunctors C) n) X)) ≫
    𝟙
      (Functor.obj HomologicalComplexUpToQuasiIso.Q
        (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
  (𝟙 (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))
Tactic: rw [CategoryTheory.Functor.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X : C
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
      (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (𝟙 (Functor.obj Qh (Functor.obj (SingleFunctors.functor (HomotopyCategory.singleFunctors C) n) X)) ≫
      𝟙
        (Functor.obj HomologicalComplexUpToQuasiIso.Q
          (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (𝟙 (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))
have w : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
    (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
  (𝟙
    (Functor.obj HomologicalComplexUpToQuasiIso.Q
      (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
  (𝟙 (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))
Tactic: erw [Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
⊢ Eq (α :=
    Quiver.Hom (V := C ⥤ DerivedCategory.{w, v, u} C)
      (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n)
      (SingleFunctors.functor (singleFunctors C) n))
    (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) n)
    (𝟙 (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n))
have w : ∀ (X : C),
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C)
      (Functor.obj (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n) X)
      (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))
    (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) n) X)
    (NatTrans.app (𝟙 (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n)) X)
Tactic: ext X