Lean4
/-- The obvious `TotalComplexShapeSymmetry c₂ c₁ c₁₂` deduced from a
`TotalComplexShapeSymmetry c₁ c₂ c₁₂`. -/
def symmetry [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂] :
TotalComplexShapeSymmetry c₂ c₁ c₁₂
where
symm i₂ i₁ := (ComplexShape.π_symm c₁ c₂ c₁₂ i₁ i₂).symm
σ i₂ i₁ := ComplexShape.σ c₁ c₂ c₁₂ i₁ i₂
σ_ε₁ {i₂ i₂'} h₂
i₁ := by
apply mul_right_cancel (b := ComplexShape.ε₂ c₁ c₂ c₁₂ (i₁, i₂))
rw [mul_assoc]
nth_rw 2 [mul_comm]
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]
σ_ε₂ i₂ i₁ i₁'
h₁ := by
apply mul_right_cancel (b := ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂))
rw [mul_assoc]
nth_rw 2 [mul_comm]
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]
