awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := ENNReal)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal)
        (fundamentalDomain (ι := index K) (K := ℝ) (stdBasis K)) :
      ENNReal)
    (1 : ENNReal)
have rw : NullMeasurableSet (α := Fin 2 → ℝ) (Set.pi (α := fun (a : Fin 2) ↦ ℝ) Set.univ fun (x : Fin 2) ↦ Set.Ico 0 1) volume
Tactic: rw [fundamentalDomain_stdBasis, volume_eq_prod, prod_prod, volume_pi, volume_pi, pi_pi, pi_pi,
    Complex.volume_preserving_equiv_pi.measure_preimage ?_, volume_pi, pi_pi, Real.volume_Ico,
    sub_zero, ENNReal.ofReal_one, prod_const_one, prod_const_one, prod_const_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ index K ≃ (K →+* ℂ)
have refine_1 : (c : index K) → K →+* ℂ
Tactic: refine Equiv.ofBijective (fun c => ?_)
    ((Fintype.bijective_iff_surjective_and_card _).mpr ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_1 : (c : index K) → K →+* ℂ
⊢ index K ≃ (K →+* ℂ)
have refine_2 : Function.Surjective (β := K →+* ℂ) fun (c : index K) ↦
  Sum.casesOn (motive :=
    fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
    (h : c = t) → K →+* ℂ) c
    (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
    (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
      Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
        fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
        if j = 0 then (↑w : InfinitePlace K).embedding else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
    sorry
Tactic: refine Equiv.ofBijective (fun c => ?_)
    ((Fintype.bijective_iff_surjective_and_card _).mpr ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_1 : (c : index K) → K →+* ℂ
refine_2 :
  Function.Surjective (β := K →+* ℂ) fun (c : index K) ↦
    Sum.casesOn (motive :=
      fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
      (h : c = t) → K →+* ℂ) c
      (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
      (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
        Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
          fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
          if j = 0 then (↑w : InfinitePlace K).embedding
          else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
      ⋯
⊢ index K ≃ (K →+* ℂ)
have refine_3 : Fintype.card.{u_1} (index K) = Fintype.card.{u_1} (K →+* ℂ)
Tactic: refine Equiv.ofBijective (fun c => ?_)
    ((Fintype.bijective_iff_surjective_and_card _).mpr ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
wj : { w : InfinitePlace K // w.IsComplex } × Fin 2
⊢ K →+* ℂ
have refine_1 : (w : { w : InfinitePlace K // w.IsComplex }) → (j : Fin 2) → K →+* ℂ
Tactic: rcases wj with ⟨w, j⟩
Cleared hypotheses: wj
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : index K
⊢ K →+* ℂ
have refine_1 : (w : { w : InfinitePlace K // w.IsReal }) → K →+* ℂ
Tactic: cases c with
    | inl w => exact w.val.embedding
    | inr wj => rcases wj with ⟨w, j⟩
                exact if j = 0 then w.val.embedding else ComplexEmbedding.conjugate w.val.embedding
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : index K
refine_1 : (w : { w : InfinitePlace K // w.IsReal }) → K →+* ℂ
⊢ K →+* ℂ
have refine_1₁ : (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) → K →+* ℂ
Tactic: cases c with
    | inl w => exact w.val.embedding
    | inr wj => rcases wj with ⟨w, j⟩
                exact if j = 0 then w.val.embedding else ComplexEmbedding.conjugate w.val.embedding
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
⊢ ∃ (a : index K),
    (fun (c : index K) ↦
          (Sum.casesOn (motive :=
              fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
              (h : c = t) → K →+* ℂ) c
              (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
              (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                  fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                  if j = 0 then (↑w : InfinitePlace K).embedding
                  else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
              ⋯ :
            K →+* ℂ))
        a =
      φ
have pos : ∀ (hφ : ComplexEmbedding.IsReal φ),
  ∃ (a : index K),
    (fun (c : index K) ↦
          (Sum.casesOn (motive :=
              fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
              (h : c = t) → K →+* ℂ) c
              (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
              (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                  fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                  if j = 0 then (↑w : InfinitePlace K).embedding
                  else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
              sorry :
            K →+* ℂ))
        a =
      φ
Tactic: by_cases hφ : ComplexEmbedding.IsReal φ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
pos :
  ∀ (hφ : ComplexEmbedding.IsReal φ),
    ∃ (a : index K),
      (fun (c : index K) ↦
            (Sum.casesOn (motive :=
                fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
                (h : c = t) → K →+* ℂ) c
                (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
                (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                  Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                    fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                    if j = 0 then (↑w : InfinitePlace K).embedding
                    else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
                ⋯ :
              K →+* ℂ))
          a =
        φ
⊢ ∃ (a : index K),
    (fun (c : index K) ↦
          (Sum.casesOn (motive :=
              fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
              (h : c = t) → K →+* ℂ) c
              (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
              (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                  fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                  if j = 0 then (↑w : InfinitePlace K).embedding
                  else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
              ⋯ :
            K →+* ℂ))
        a =
      φ
have neg : ∀ (hφ : ¬ComplexEmbedding.IsReal φ),
  ∃ (a : index K),
    (fun (c : index K) ↦
          (Sum.casesOn (motive :=
              fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
              (h : c = t) → K →+* ℂ) c
              (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
              (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                  fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                  if j = 0 then (↑w : InfinitePlace K).embedding
                  else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
              sorry :
            K →+* ℂ))
        a =
      φ
Tactic: by_cases hφ : ComplexEmbedding.IsReal φ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
⊢ ∃ (a : index K),
    (fun (c : index K) ↦
          (Sum.casesOn (motive :=
              fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
              (h : c = t) → K →+* ℂ) c
              (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
              (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                  fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                  if j = 0 then (↑w : InfinitePlace K).embedding
                  else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
              ⋯ :
            K →+* ℂ))
        a =
      φ
have pos : ∀ (hw : (InfinitePlace.mk φ).embedding = φ),
  ∃ (a : index K),
    (fun (c : index K) ↦
          (Sum.casesOn (motive :=
              fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
              (h : c = t) → K →+* ℂ) c
              (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
              (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                  fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                  if j = 0 then (↑w : InfinitePlace K).embedding
                  else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
              sorry :
            K →+* ℂ))
        a =
      φ
Tactic: by_cases hw : (InfinitePlace.mk φ).embedding = φ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
pos :
  ∀ (hw : (InfinitePlace.mk φ).embedding = φ),
    ∃ (a : index K),
      (fun (c : index K) ↦
            (Sum.casesOn (motive :=
                fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
                (h : c = t) → K →+* ℂ) c
                (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
                (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                  Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                    fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                    if j = 0 then (↑w : InfinitePlace K).embedding
                    else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
                ⋯ :
              K →+* ℂ))
          a =
        φ
⊢ ∃ (a : index K),
    (fun (c : index K) ↦
          (Sum.casesOn (motive :=
              fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
              (h : c = t) → K →+* ℂ) c
              (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
              (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                  fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                  if j = 0 then (↑w : InfinitePlace K).embedding
                  else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
              ⋯ :
            K →+* ℂ))
        a =
      φ
have neg : ∀ (hw : ¬(InfinitePlace.mk φ).embedding = φ),
  ∃ (a : index K),
    (fun (c : index K) ↦
          (Sum.casesOn (motive :=
              fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
              (h : c = t) → K →+* ℂ) c
              (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
              (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                  fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                  if j = 0 then (↑w : InfinitePlace K).embedding
                  else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
              sorry :
            K →+* ℂ))
        a =
      φ
Tactic: by_cases hw : (InfinitePlace.mk φ).embedding = φ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Fintype.card.{u_1} (index K) = Fintype.card.{u_1} (K →+* ℂ)
have refine_3 : Fintype.card.{u_1} (index K) = finrank ℚ K
Tactic: rw [Embeddings.card, ← mixedEmbedding.finrank K,
      ← Module.finrank_eq_card_basis (stdBasis K)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_3 : Fintype.card.{u_1} (index K) = finrank ℚ K
⊢ Fintype.card.{u_1} (index K) = Fintype.card.{u_1} (K →+* ℂ)
have refine_3₁ : Fintype.card.{u_1} (index K) = finrank.{0, u_1} ℝ (mixedSpace K)
Tactic: rw [Embeddings.card, ← mixedEmbedding.finrank K,
      ← Module.finrank_eq_card_basis (stdBasis K)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_3 : Fintype.card.{u_1} (index K) = finrank ℚ K
refine_3₁ : Fintype.card.{u_1} (index K) = finrank.{0, u_1} ℝ (mixedSpace K)
⊢ Fintype.card.{u_1} (index K) = Fintype.card.{u_1} (K →+* ℂ)
have refine_3₂ : finrank.{0, u_1} ℝ (mixedSpace K) = finrank.{0, u_1} ℝ (mixedSpace K)
Tactic: rw [Embeddings.card, ← mixedEmbedding.finrank K,
      ← Module.finrank_eq_card_basis (stdBasis K)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 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 := 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)
Tactic: rw [matrixToStdBasis, det_fromBlocks_zero₂₁, det_diagonal, prod_const_one, one_mul,
          det_reindex_self, det_blockDiagonal]
-- 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)
⊢ 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₁ : 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
Tactic: rw [matrixToStdBasis, det_fromBlocks_zero₂₁, det_diagonal, prod_const_one, one_mul,
          det_reindex_self, det_blockDiagonal]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := ℂ)
    (∏ _k : { w : InfinitePlace K // w.IsComplex },
      (HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)).det)
    (∏ _k : { w : InfinitePlace K // w.IsComplex }, 2⁻¹ * I)
have refine : ∀ (x : { w : InfinitePlace K // w.IsComplex }),
  Membership.mem (γ := Finset { w : InfinitePlace K // w.IsComplex }) univ x →
    (HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)).det =
      2⁻¹ * I
Tactic: refine prod_congr (Eq.refl _) (fun _ _ => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : { w : InfinitePlace K // w.IsComplex }
h : Membership.mem (γ := Finset { w : InfinitePlace K // w.IsComplex }) univ x
⊢ (HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)).det = 2⁻¹ * I
have simp : HAdd.hAdd (α := ℂ) 1 1 = 2
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ ∏ _k : { w : InfinitePlace K // w.IsComplex }, 2⁻¹ * I =
    (2⁻¹ * I) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }
have rw : (2⁻¹ * I) ^ card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ =
  (2⁻¹ * I) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }
Tactic: rw [prod_const, Fintype.card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  (2⁻¹ * I) ^ card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ =
    (2⁻¹ * I) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }
⊢ ∏ _k : { w : InfinitePlace K // w.IsComplex }, 2⁻¹ * I =
    (2⁻¹ * I) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }
have rw₁ : (2⁻¹ * I) ^ card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ =
  (2⁻¹ * I) ^ card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ
Tactic: rw [prod_const, Fintype.card]