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
x : K
hx : x ≠ 0
w : { w : InfinitePlace K // w ≠ w₀ }
h :
  HSub.hSub (α := ℝ)
      ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
          (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) (↑w : InfinitePlace K) :
        ℝ)
      (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)
          (∑ w' : InfinitePlace K,
            (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
              (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w') *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
h₁ :
  HSub.hSub (α := ℝ)
      ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
          (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) (↑w : InfinitePlace K) :
        ℝ)
      ((↑(↑w : InfinitePlace K).mult : ℝ) * Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
h₂ :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
        Real.log (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x) (↑w : InfinitePlace K)) -
      (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹ =
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
h₃ :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
        Real.log (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x) (↑w : InfinitePlace K)) -
      (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹ =
    (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log
          ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ)
            ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K)) -
        Real.log
            ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K)) *
          (↑(finrank ℚ K) : ℝ)⁻¹)
⊢ (realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ)
      ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)))
      w =
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
have h₄ : (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log (((↑w : InfinitePlace K) : (a : K) → ℝ) x) -
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹ =
  (↑(↑w : InfinitePlace K).mult : ℝ) *
    (Real.log (((↑w : InfinitePlace K) : (a : K) → ℝ) x) -
      Real.log
          ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
            ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K)) *
        (↑(finrank ℚ K) : ℝ)⁻¹)
Tactic: simp_rw [realSpaceToLogSpace_apply, sum_expMap_symm_apply hx, expMap_symm_apply,
    logMap, normAtPlace_apply, mul_sub, mul_assoc, norm_eq_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := { w : InfinitePlace K // w ≠ w₀ } → ℝ)
    ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ) (completeFamily K w₀) :
      { w : InfinitePlace K // w ≠ w₀ } → ℝ)
    (0 : { w : InfinitePlace K // w ≠ w₀ } → ℝ)
have h : ∀ (x : { w : InfinitePlace K // w ≠ w₀ }),
  Eq (α := ℝ)
    ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ) (completeFamily K w₀) x) (0 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : { w : InfinitePlace K // w ≠ w₀ }
⊢ Eq (α := ℝ)
    ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ) (completeFamily K w₀) x) (0 x)
have h : completeFamily K w₀ (↑x : InfinitePlace K) -
    HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, completeFamily K w₀ w') *
      (↑(finrank ℚ K) : ℝ)⁻¹ =
  0 x
Tactic: rw [realSpaceToLogSpace_apply, completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq,
    mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr Module.finrank_pos.ne'), sub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  completeFamily K w₀ (↑x : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, completeFamily K w₀ w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
⊢ Eq (α := ℝ)
    ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ) (completeFamily K w₀) x) (0 x)
have h₁ : (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
      else
        (↑(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₀ hi))) :
                  𝓞 K)))))
      (↑x : InfinitePlace K) -
    HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ)
        (∑ w' : InfinitePlace K,
          (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
            else
              (↑(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₀ hi))) :
                        𝓞 K)))))
            w') *
      (↑(finrank ℚ K) : ℝ)⁻¹ =
  0 x
Tactic: rw [realSpaceToLogSpace_apply, completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq,
    mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr Module.finrank_pos.ne'), sub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  completeFamily K w₀ (↑x : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, completeFamily K w₀ w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₁ :
  (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
        else
          (↑(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₀ hi))) :
                    𝓞 K)))))
        (↑x : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ)
          (∑ w' : InfinitePlace K,
            (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
              else
                (↑(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₀ hi))) :
                          𝓞 K)))))
              w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
⊢ Eq (α := ℝ)
    ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ) (completeFamily K w₀) x) (0 x)
have h₂ : (↑(↑x : InfinitePlace K).mult : ℝ) -
    HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, (↑w'.mult : ℝ)) *
      (↑(finrank ℚ K) : ℝ)⁻¹ =
  0 x
Tactic: rw [realSpaceToLogSpace_apply, completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq,
    mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr Module.finrank_pos.ne'), sub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  completeFamily K w₀ (↑x : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, completeFamily K w₀ w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₁ :
  (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
        else
          (↑(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₀ hi))) :
                    𝓞 K)))))
        (↑x : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ)
          (∑ w' : InfinitePlace K,
            (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
              else
                (↑(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₀ hi))) :
                          𝓞 K)))))
              w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, (↑w'.mult : ℝ)) *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
⊢ Eq (α := ℝ)
    ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ) (completeFamily K w₀) x) (0 x)
have h₃ : (↑(↑x : InfinitePlace K).mult : ℝ) -
    HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (↑(∑ x : InfinitePlace K, x.mult) : ℝ) *
      (↑(finrank ℚ K) : ℝ)⁻¹ =
  0 x
Tactic: rw [realSpaceToLogSpace_apply, completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq,
    mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr Module.finrank_pos.ne'), sub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  completeFamily K w₀ (↑x : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, completeFamily K w₀ w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₁ :
  (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
        else
          (↑(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₀ hi))) :
                    𝓞 K)))))
        (↑x : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ)
          (∑ w' : InfinitePlace K,
            (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
              else
                (↑(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₀ hi))) :
                          𝓞 K)))))
              w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, (↑w'.mult : ℝ)) *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (↑(∑ x : InfinitePlace K, x.mult) : ℝ) *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
⊢ Eq (α := ℝ)
    ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ) (completeFamily K w₀) x) (0 x)
have h₄ : (↑(↑x : InfinitePlace K).mult : ℝ) -
    HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (↑(finrank ℚ K) : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹ =
  0 x
Tactic: rw [realSpaceToLogSpace_apply, completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq,
    mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr Module.finrank_pos.ne'), sub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  completeFamily K w₀ (↑x : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, completeFamily K w₀ w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₁ :
  (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
        else
          (↑(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₀ hi))) :
                    𝓞 K)))))
        (↑x : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ)
          (∑ w' : InfinitePlace K,
            (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
              else
                (↑(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₀ hi))) :
                          𝓞 K)))))
              w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, (↑w'.mult : ℝ)) *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (↑(∑ x : InfinitePlace K, x.mult) : ℝ) *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₄ :
  (↑(↑x : InfinitePlace K).mult : ℝ) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (↑(finrank ℚ K) : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
⊢ Eq (α := ℝ)
    ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ) (completeFamily K w₀) x) (0 x)
have h₅ : HSub.hSub (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) = 0 x
Tactic: rw [realSpaceToLogSpace_apply, completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq,
    mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr Module.finrank_pos.ne'), sub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  completeFamily K w₀ (↑x : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, completeFamily K w₀ w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₁ :
  (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
        else
          (↑(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₀ hi))) :
                    𝓞 K)))))
        (↑x : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ)
          (∑ w' : InfinitePlace K,
            (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
              else
                (↑(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₀ hi))) :
                          𝓞 K)))))
              w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, (↑w'.mult : ℝ)) *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (↑(∑ x : InfinitePlace K, x.mult) : ℝ) *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₄ :
  (↑(↑x : InfinitePlace K).mult : ℝ) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (↑(finrank ℚ K) : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₅ : HSub.hSub (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) = 0 x
⊢ Eq (α := ℝ)
    ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ) (completeFamily K w₀) x) (0 x)
have h₆ : Eq (α := ℝ) 0 (0 x)
Tactic: rw [realSpaceToLogSpace_apply, completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq,
    mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr Module.finrank_pos.ne'), sub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  completeFamily K w₀ (↑x : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, completeFamily K w₀ w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₁ :
  (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
        else
          (↑(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₀ hi))) :
                    𝓞 K)))))
        (↑x : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ)
          (∑ w' : InfinitePlace K,
            (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
              else
                (↑(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₀ hi))) :
                          𝓞 K)))))
              w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, (↑w'.mult : ℝ)) *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (↑(∑ x : InfinitePlace K, x.mult) : ℝ) *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₄ :
  (↑(↑x : InfinitePlace K).mult : ℝ) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (↑(finrank ℚ K) : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₅ : HSub.hSub (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) = 0 x
h₆ : Eq (α := ℝ) 0 (0 x)
⊢ Eq (α := ℝ)
    ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ) (completeFamily K w₀) x) (0 x)
have h₇ : Eq (α := ℝ) 0 0
Tactic: rw [realSpaceToLogSpace_apply, completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq,
    mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr Module.finrank_pos.ne'), sub_self, Pi.zero_apply]