-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Eq (α := ℂ)
    (det.{0, u_1} (n := index K)
      (fromBlocks (diagonal fun (x : { w : InfinitePlace K // w.IsReal }) ↦ 1) 0 0
        ((reindex (Equiv.prodComm (Fin 2) { w : InfinitePlace K // w.IsComplex })
              (Equiv.prodComm (Fin 2) { w : InfinitePlace K // w.IsComplex }) :
            (a :
                Matrix (Fin 2 × { w : InfinitePlace K // w.IsComplex }) (Fin 2 × { w : InfinitePlace K // w.IsComplex })
                  ℂ) →
              Matrix ({ w : InfinitePlace K // w.IsComplex } × Fin 2) ({ w : InfinitePlace K // w.IsComplex } × Fin 2)
                ℂ)
          (blockDiagonal fun (x : { w : InfinitePlace K // w.IsComplex }) ↦
            HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)))))
    (∏ _k : { w : InfinitePlace K // w.IsComplex },
      (HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)).det)
rw₁ :
  HMul.hMul (α := ℂ)
      (det.{0, u_1} (n := { w : InfinitePlace K // w.IsReal })
        (diagonal fun (x : { w : InfinitePlace K // w.IsReal }) ↦ 1))
      (det.{0, u_1} (n := { w : InfinitePlace K // w.IsComplex } × Fin 2)
        ((reindex (Equiv.prodComm (Fin 2) { w : InfinitePlace K // w.IsComplex })
              (Equiv.prodComm (Fin 2) { w : InfinitePlace K // w.IsComplex }) :
            (a :
                Matrix (Fin 2 × { w : InfinitePlace K // w.IsComplex }) (Fin 2 × { w : InfinitePlace K // w.IsComplex })
                  ℂ) →
              Matrix ({ w : InfinitePlace K // w.IsComplex } × Fin 2) ({ w : InfinitePlace K // w.IsComplex } × Fin 2)
                ℂ)
          (blockDiagonal fun (x : { w : InfinitePlace K // w.IsComplex }) ↦
            HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)))) =
    ∏ _k : { w : InfinitePlace K // w.IsComplex },
      (HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)).det
rw₂ :
  HMul.hMul (α := ℂ) (∏ i : { w : InfinitePlace K // w.IsReal }, 1)
      (det.{0, u_1} (n := { w : InfinitePlace K // w.IsComplex } × Fin 2)
        ((reindex (Equiv.prodComm (Fin 2) { w : InfinitePlace K // w.IsComplex })
              (Equiv.prodComm (Fin 2) { w : InfinitePlace K // w.IsComplex }) :
            (a :
                Matrix (Fin 2 × { w : InfinitePlace K // w.IsComplex }) (Fin 2 × { w : InfinitePlace K // w.IsComplex })
                  ℂ) →
              Matrix ({ w : InfinitePlace K // w.IsComplex } × Fin 2) ({ w : InfinitePlace K // w.IsComplex } × Fin 2)
                ℂ)
          (blockDiagonal fun (x : { w : InfinitePlace K // w.IsComplex }) ↦
            HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)))) =
    ∏ _k : { w : InfinitePlace K // w.IsComplex },
      (HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)).det
rw₃ :
  HMul.hMul (α := ℂ) 1
      (det.{0, u_1} (n := { w : InfinitePlace K // w.IsComplex } × Fin 2)
        ((reindex (Equiv.prodComm (Fin 2) { w : InfinitePlace K // w.IsComplex })
              (Equiv.prodComm (Fin 2) { w : InfinitePlace K // w.IsComplex }) :
            (a :
                Matrix (Fin 2 × { w : InfinitePlace K // w.IsComplex }) (Fin 2 × { w : InfinitePlace K // w.IsComplex })
                  ℂ) →
              Matrix ({ w : InfinitePlace K // w.IsComplex } × Fin 2) ({ w : InfinitePlace K // w.IsComplex } × Fin 2)
                ℂ)
          (blockDiagonal fun (x : { w : InfinitePlace K // w.IsComplex }) ↦
            HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)))) =
    ∏ _k : { w : InfinitePlace K // w.IsComplex },
      (HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)).det
rw₄ :
  Eq (α := ℂ)
    (det.{0, u_1} (n := { w : InfinitePlace K // w.IsComplex } × Fin 2)
      ((reindex (Equiv.prodComm (Fin 2) { w : InfinitePlace K // w.IsComplex })
            (Equiv.prodComm (Fin 2) { w : InfinitePlace K // w.IsComplex }) :
          (a :
              Matrix (Fin 2 × { w : InfinitePlace K // w.IsComplex }) (Fin 2 × { w : InfinitePlace K // w.IsComplex })
                ℂ) →
            Matrix ({ w : InfinitePlace K // w.IsComplex } × Fin 2) ({ w : InfinitePlace K // w.IsComplex } × Fin 2) ℂ)
        (blockDiagonal fun (x : { w : InfinitePlace K // w.IsComplex }) ↦
          HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ))))
    (∏ _k : { w : InfinitePlace K // w.IsComplex },
      (HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)).det)
⊢ det (n := index K) (matrixToStdBasis K) =
    ∏ _k : { w : InfinitePlace K // w.IsComplex },
      (HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)).det
have rw₅ : Eq (α := ℂ)
  (det.{0, u_1} (n := Fin 2 × { w : InfinitePlace K // w.IsComplex })
    (blockDiagonal fun (x : { w : InfinitePlace K // w.IsComplex }) ↦
      HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)))
  (∏ _k : { w : InfinitePlace K // w.IsComplex },
    (HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)).det)
Tactic: rw [matrixToStdBasis, det_fromBlocks_zero₂₁, det_diagonal, prod_const_one, one_mul,
          det_reindex_self, det_blockDiagonal]