awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i : { w : InfinitePlace K // w ≠ w₀ }
rw :
  Eq.{u_1 + 1} (α := realSpace K)
    ((↑expMap : realSpace K → realSpace K)
      ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces
          ((mixedEmbedding K : (a : K) → mixedSpace K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
              (↑(fundSystem K
                    (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                        (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                      i)) :
                𝓞 K))))))
    (normAtAllPlaces
      ((mixedEmbedding K : (a : K) → mixedSpace K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (↑(fundSystem K
                (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                    (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                  i)) :
            𝓞 K))))
⊢ Eq.{u_1 + 1} (α := realSpace K)
    ((↑expMap : realSpace K → realSpace K)
      ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K)))
    (normAtAllPlaces
      ((mixedEmbedding K : (a : K) → mixedSpace K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (↑(fundSystem K
                (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                    (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                  i)) :
            𝓞 K))))
have rw₁ : Eq.{u_1 + 1} (α := realSpace K)
  (normAtAllPlaces
    ((mixedEmbedding K : (a : K) → mixedSpace K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
        (↑(fundSystem K
              (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                  (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                i)) :
          𝓞 K))))
  (normAtAllPlaces
    ((mixedEmbedding K : (a : K) → mixedSpace K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
        (↑(fundSystem K
              (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                  (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                i)) :
          𝓞 K))))
Tactic: rw [completeBasis_apply_of_ne, expMap.right_inv (by simp [expMap_target, pos_at_place])]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ |ContinuousLinearMap.det (M := InfinitePlace K → ℝ)
        (↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) : (InfinitePlace K → ℝ) →L[ℝ] realSpace K)| =
    (↑(finrank ℚ K) : ℝ) * regulator K
have rw : Eq (α := ℝ)
  |Matrix.det.{0, u_1} (n := InfinitePlace K)
      (Matrix.transpose
        ((LinearMap.toMatrix (completeBasis K) (completeBasis K) :
            (a : realSpace K →ₗ[ℝ] realSpace K) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
          (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
                (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
            (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ)))|
  |Matrix.det (n := InfinitePlace K)
      ((Matrix.of : (a : InfinitePlace K → InfinitePlace K → ℝ) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
          fun (i w : InfinitePlace K) ↦
          if h : i = w₀ then (↑w.mult : ℝ)
          else
            (↑w.mult : ℝ) *
              Real.log
                ((w : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K
                            (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                              (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) i h))) :
                        𝓞 K) :
                    K)) :
        Matrix (InfinitePlace K) (InfinitePlace K) ℝ)|
Tactic: rw [ContinuousLinearMap.det, ← LinearMap.det_toMatrix (completeBasis K), ← Matrix.det_transpose,
    regulator_eq_regOfFamily_fundSystem, finrank_mul_regOfFamily_eq_det _ w₀ equivFinRank.symm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := ℝ)
    |Matrix.det.{0, u_1} (n := InfinitePlace K)
        (Matrix.transpose
          ((LinearMap.toMatrix (completeBasis K) (completeBasis K) :
              (a : realSpace K →ₗ[ℝ] realSpace K) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
            (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
                  (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
              (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ)))|
    |Matrix.det (n := InfinitePlace K)
        ((Matrix.of : (a : InfinitePlace K → InfinitePlace K → ℝ) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
            fun (i w : InfinitePlace K) ↦
            if h : i = w₀ then (↑w.mult : ℝ)
            else
              (↑w.mult : ℝ) *
                Real.log
                  ((w : (a : K) → ℝ)
                    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                        (↑(fundSystem K
                              (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                                  (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                                (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) i h))) :
                          𝓞 K) :
                      K)) :
          Matrix (InfinitePlace K) (InfinitePlace K) ℝ)|
have e_a : ∀ (w i : InfinitePlace K),
  Eq (α := ℝ)
    (Matrix.transpose
        ((LinearMap.toMatrix (completeBasis K) (completeBasis K) :
            (a : realSpace K →ₗ[ℝ] realSpace K) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
          (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
                (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
            (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ))
        w i :
      ℝ)
    ((Matrix.of : (a : InfinitePlace K → InfinitePlace K → ℝ) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
        (fun (i w : InfinitePlace K) ↦
          if h : i = w₀ then (↑w.mult : ℝ)
          else
            (↑w.mult : ℝ) *
              Real.log
                ((w : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K
                            (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                              (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) i h))) :
                        𝓞 K) :
                    K)))
        w i :
      ℝ)
Tactic: congr 2 with w i
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w i : InfinitePlace K
⊢ Eq (α := ℝ)
    (Matrix.transpose
        ((LinearMap.toMatrix (completeBasis K) (completeBasis K) :
            (a : realSpace K →ₗ[ℝ] realSpace K) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
          (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
                (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
            (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ))
        w i :
      ℝ)
    ((Matrix.of : (a : InfinitePlace K → InfinitePlace K → ℝ) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
        (fun (i w : InfinitePlace K) ↦
          if h : i = w₀ then (↑w.mult : ℝ)
          else
            (↑w.mult : ℝ) *
              Real.log
                ((w : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K
                            (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                              (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) i h))) :
                        𝓞 K) :
                    K)))
        w i :
      ℝ)
have e_a : Eq (α := ℝ) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w i)
  (if h : w = w₀ then (↑i.mult : ℝ)
  else
    (↑i.mult : ℝ) *
      Real.log
        ((i : (a : K) → ℝ)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
              (↑(fundSystem K
                    (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                        (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w h))) :
                𝓞 K) :
            K)))
Tactic: rw [Matrix.transpose_apply, LinearMap.toMatrix_apply, Matrix.of_apply, ← Basis.equivFunL_apply,
    ContinuousLinearMap.coe_coe, ContinuousLinearEquiv.coe_apply,
    (completeBasis K).equivFunL.apply_symm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w i : InfinitePlace K
⊢ Eq (α := ℝ) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w i)
    (if h : w = w₀ then (↑i.mult : ℝ)
    else
      (↑i.mult : ℝ) *
        Real.log
          ((i : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                (↑(fundSystem K
                      (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                          (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w h))) :
                  𝓞 K) :
              K)))
have pos : ∀ (hw : w = w₀), Eq (α := ℝ) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w i) (↑i.mult : ℝ)
Tactic: split_ifs with hw
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w i : InfinitePlace K
pos : ∀ (hw : w = w₀), Eq (α := ℝ) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w i) (↑i.mult : ℝ)
⊢ Eq (α := ℝ) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w i)
    (if h : w = w₀ then (↑i.mult : ℝ)
    else
      (↑i.mult : ℝ) *
        Real.log
          ((i : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                (↑(fundSystem K
                      (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                          (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w h))) :
                  𝓞 K) :
              K)))
have neg : ∀ (hw : ¬w = w₀),
  (completeBasis K : (a : InfinitePlace K) → realSpace K) w i =
    (↑i.mult : ℝ) *
      Real.log
        ((i : (a : K) → ℝ)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
              (↑(fundSystem K
                    (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                        (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw))) :
                𝓞 K) :
            K))
Tactic: split_ifs with hw
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w i : InfinitePlace K
hw : w = w₀
⊢ Eq (α := ℝ) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w i) (↑i.mult : ℝ)
have pos : Eq (α := ℝ) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀ i) (↑i.mult : ℝ)
Tactic: rw [hw, completeBasis_apply_of_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w i : InfinitePlace K
hw : w = w₀
pos : Eq (α := ℝ) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀ i) (↑i.mult : ℝ)
⊢ Eq (α := ℝ) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w i) (↑i.mult : ℝ)
have pos₁ : Eq (α := ℝ) ((fun (w : InfinitePlace K) ↦ ((↑w.mult : ℝ) : ℝ)) i) (↑i.mult : ℝ)
Tactic: rw [hw, completeBasis_apply_of_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w i : InfinitePlace K
hw : ¬w = w₀
⊢ (completeBasis K : (a : InfinitePlace K) → realSpace K) w i =
    (↑i.mult : ℝ) *
      Real.log
        ((i : (a : K) → ℝ)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
              (↑(fundSystem K
                    (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                        (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw))) :
                𝓞 K) :
            K))
have neg : (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
    (normAtAllPlaces
      ((mixedEmbedding K : (a : K) → mixedSpace K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (↑(fundSystem K
                (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                    (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                  (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw))) :
            𝓞 K))))
    i =
  (↑i.mult : ℝ) *
    Real.log
      ((i : (a : K) → ℝ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(fundSystem K
                  (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                      (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                    (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw))) :
              𝓞 K) :
          K))
Tactic: simp_rw [completeBasis_apply_of_ne K ⟨w, hw⟩, expMap_symm_apply, normAtAllPlaces_mixedEmbedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w i : InfinitePlace K
hw : ¬w = w₀
neg :
  (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
      (normAtAllPlaces
        ((mixedEmbedding K : (a : K) → mixedSpace K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(fundSystem K
                  (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                      (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                    (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw))) :
              𝓞 K))))
      i =
    (↑i.mult : ℝ) *
      Real.log
        ((i : (a : K) → ℝ)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
              (↑(fundSystem K
                    (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                        (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw))) :
                𝓞 K) :
            K))
⊢ (completeBasis K : (a : InfinitePlace K) → realSpace K) w i =
    (↑i.mult : ℝ) *
      Real.log
        ((i : (a : K) → ℝ)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
              (↑(fundSystem K
                    (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                        (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw))) :
                𝓞 K) :
            K))
have neg₁ : (↑i.mult : ℝ) *
    Real.log
      (normAtAllPlaces
        ((mixedEmbedding K : (a : K) → mixedSpace K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(fundSystem K
                  (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                      (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                    (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw))) :
              𝓞 K)))
        i) =
  (↑i.mult : ℝ) *
    Real.log
      ((i : (a : K) → ℝ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(fundSystem K
                  (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                      (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                    (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw))) :
              𝓞 K) :
          K))
Tactic: simp_rw [completeBasis_apply_of_ne K ⟨w, hw⟩, expMap_symm_apply, normAtAllPlaces_mixedEmbedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ |ContinuousLinearMap.det (M := InfinitePlace K → ℝ)
        (↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) : (InfinitePlace K → ℝ) →L[ℝ] realSpace K)| =
    (↑(finrank ℚ K) : ℝ) * regulator K
have rw : |(LinearMap.det : (a : (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ) → ℝ)
      (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) : (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
        (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ)| =
  (↑(finrank ℚ K) : ℝ) * regulator K
Tactic: classical
  rw [ContinuousLinearMap.det, ← LinearMap.det_toMatrix (completeBasis K), ← Matrix.det_transpose,
    regulator_eq_regOfFamily_fundSystem, finrank_mul_regOfFamily_eq_det _ w₀ equivFinRank.symm]
  congr 2 with w i
  rw [Matrix.transpose_apply, LinearMap.toMatrix_apply, Matrix.of_apply, ← Basis.equivFunL_apply,
    ContinuousLinearMap.coe_coe, ContinuousLinearEquiv.coe_apply,
    (completeBasis K).equivFunL.apply_symm_apply]
  split_ifs with hw
  · rw [hw, completeBasis_apply_of_eq]
  · simp_rw [completeBasis_apply_of_ne K ⟨w, hw⟩, expMap_symm_apply, normAtAllPlaces_mixedEmbedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  |(LinearMap.det : (a : (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ) → ℝ)
        (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
              (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
          (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ)| =
    (↑(finrank ℚ K) : ℝ) * regulator K
⊢ |ContinuousLinearMap.det (M := InfinitePlace K → ℝ)
        (↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) : (InfinitePlace K → ℝ) →L[ℝ] realSpace K)| =
    (↑(finrank ℚ K) : ℝ) * regulator K
have rw₁ : |Matrix.det.{0, u_1} (n := InfinitePlace K)
      ((LinearMap.toMatrix (completeBasis K) (completeBasis K) :
          (a : realSpace K →ₗ[ℝ] realSpace K) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
        (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
              (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
          (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ))| =
  (↑(finrank ℚ K) : ℝ) * regulator K
Tactic: classical
  rw [ContinuousLinearMap.det, ← LinearMap.det_toMatrix (completeBasis K), ← Matrix.det_transpose,
    regulator_eq_regOfFamily_fundSystem, finrank_mul_regOfFamily_eq_det _ w₀ equivFinRank.symm]
  congr 2 with w i
  rw [Matrix.transpose_apply, LinearMap.toMatrix_apply, Matrix.of_apply, ← Basis.equivFunL_apply,
    ContinuousLinearMap.coe_coe, ContinuousLinearEquiv.coe_apply,
    (completeBasis K).equivFunL.apply_symm_apply]
  split_ifs with hw
  · rw [hw, completeBasis_apply_of_eq]
  · simp_rw [completeBasis_apply_of_ne K ⟨w, hw⟩, expMap_symm_apply, normAtAllPlaces_mixedEmbedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  |(LinearMap.det : (a : (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ) → ℝ)
        (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
              (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
          (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ)| =
    (↑(finrank ℚ K) : ℝ) * regulator K
rw₁ :
  |Matrix.det.{0, u_1} (n := InfinitePlace K)
        ((LinearMap.toMatrix (completeBasis K) (completeBasis K) :
            (a : realSpace K →ₗ[ℝ] realSpace K) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
          (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
                (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
            (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ))| =
    (↑(finrank ℚ K) : ℝ) * regulator K
⊢ |ContinuousLinearMap.det (M := InfinitePlace K → ℝ)
        (↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) : (InfinitePlace K → ℝ) →L[ℝ] realSpace K)| =
    (↑(finrank ℚ K) : ℝ) * regulator K
have rw₂ : |Matrix.det.{0, u_1} (n := InfinitePlace K)
      (Matrix.transpose
        ((LinearMap.toMatrix (completeBasis K) (completeBasis K) :
            (a : realSpace K →ₗ[ℝ] realSpace K) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
          (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
                (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
            (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ)))| =
  (↑(finrank ℚ K) : ℝ) * regulator K
Tactic: classical
  rw [ContinuousLinearMap.det, ← LinearMap.det_toMatrix (completeBasis K), ← Matrix.det_transpose,
    regulator_eq_regOfFamily_fundSystem, finrank_mul_regOfFamily_eq_det _ w₀ equivFinRank.symm]
  congr 2 with w i
  rw [Matrix.transpose_apply, LinearMap.toMatrix_apply, Matrix.of_apply, ← Basis.equivFunL_apply,
    ContinuousLinearMap.coe_coe, ContinuousLinearEquiv.coe_apply,
    (completeBasis K).equivFunL.apply_symm_apply]
  split_ifs with hw
  · rw [hw, completeBasis_apply_of_eq]
  · simp_rw [completeBasis_apply_of_ne K ⟨w, hw⟩, expMap_symm_apply, normAtAllPlaces_mixedEmbedding]