awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
hx : x ≠ 0
simp_rw :
  ∑ w : InfinitePlace K,
      (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w =
    Real.log (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
simp_rw₁ :
  Eq (α := ℝ)
    (∑ w : InfinitePlace K,
      (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w)
    (∑ i : InfinitePlace K, Real.log (HPow.hPow (α := ℝ) ((i : (a : K) → ℝ) x : ℝ) i.mult))
simp_rw₂ :
  Eq (α := ℝ)
    (∑ w : InfinitePlace K,
      (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w)
    (∑ x_1 : InfinitePlace K, (↑x_1.mult : ℝ) * Real.log ((x_1 : (a : K) → ℝ) x))
simp_rw₃ :
  Eq (α := ℝ)
    (∑ x_1 : InfinitePlace K,
      (↑x_1.mult : ℝ) * Real.log (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x) x_1))
    (∑ x_1 : InfinitePlace K, (↑x_1.mult : ℝ) * Real.log ((x_1 : (a : K) → ℝ) x))
⊢ ∑ w : InfinitePlace K,
      (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w =
    Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ)

Tactic:
simp_rw [← prod_eq_abs_norm, Real.log_prod (fun _ _ ↦ pow_ne_zero _ ((map_ne_zero _).mpr hx)),
    Real.log_pow, expMap_symm_apply, normAtAllPlaces_mixedEmbedding]

Premises used: Iff.mpr, Real.log_prod, pow_ne_zero, NumberField.mixedEmbedding.fundamentalCone.expMap_symm_apply, NumberField.mixedEmbedding.normAtAllPlaces_mixedEmbedding, map_ne_zero, Real.log_pow, NumberField.InfinitePlace.prod_eq_abs_norm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
⊢ HasFDerivAt (↑expMap : realSpace K → realSpace K) (fderiv_expMap x) x

Tactic:
simpa [expMap, fderiv_expMap, hasFDerivAt_pi', OpenPartialHomeomorph.pi_apply,
    ContinuousLinearMap.proj_pi] using
    fun w ↦ (hasDerivAt_expMap_single w _).hasFDerivAt.comp x (hasFDerivAt_apply w x)

Premises used: HasDerivAt.hasFDerivAt, hasFDerivAt_apply, OpenPartialHomeomorph.pi_apply, NumberField.mixedEmbedding.fundamentalCone.expMap, NumberField.mixedEmbedding.fundamentalCone.hasDerivAt_expMap_single, ContinuousLinearMap.proj_pi, NumberField.mixedEmbedding.fundamentalCone.fderiv_expMap, hasFDerivAt_pi', HasFDerivAt.comp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Fintype.card (Fin (rank K)) =
    Fintype.card.{u_1} (InfinitePlace K) - Fintype.card.{u_1} { x : InfinitePlace K // x = w₀ }
rw₁ : Fintype.card (Fin (rank K)) = Fintype.card.{u_1} (InfinitePlace K) - 1
rw₂ : rank K = Fintype.card.{u_1} (InfinitePlace K) - 1
rw₃ rw₄ : Fintype.card.{u_1} (InfinitePlace K) - 1 = Fintype.card.{u_1} (InfinitePlace K) - 1
⊢ Fintype.card (Fin (rank K)) = Fintype.card.{u_1} { w : InfinitePlace K // w ≠ w₀ }

Tactic:
rw [Fintype.card_subtype_compl, Fintype.card_ofSubsingleton, Fintype.card_fin, rank]

Premises used: Fintype.card_fin, NumberField.Units.rank, Fintype.card_ofSubsingleton, Fintype.card_subtype_compl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x x_1 : realSpace K
x_2 : { w : InfinitePlace K // w ≠ w₀ }
simp :
  x (↑x_2 : InfinitePlace K) + x_1 (↑x_2 : InfinitePlace K) -
      (↑(↑x_2 : InfinitePlace K).mult : ℝ) *
          HAdd.hAdd (α := ℝ) (∑ x_3 : InfinitePlace K, x x_3) (∑ x : InfinitePlace K, x_1 x) *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    x (↑x_2 : InfinitePlace K) -
        HMul.hMul (α := ℝ) (↑(↑x_2 : InfinitePlace K).mult : ℝ) (∑ x_3 : InfinitePlace K, x x_3) *
          (↑(finrank ℚ K) : ℝ)⁻¹ +
      (x_1 (↑x_2 : InfinitePlace K) -
        HMul.hMul (α := ℝ) (↑(↑x_2 : InfinitePlace K).mult : ℝ) (∑ x : InfinitePlace K, x_1 x) * (↑(finrank ℚ K) : ℝ)⁻¹)
⊢ (x + x_1) (↑x_2 : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x_2 : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, (x + x_1) w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    HAdd.hAdd (α := { w : InfinitePlace K // w ≠ w₀ } → ℝ) (β := { w : InfinitePlace K // w ≠ w₀ } → ℝ)
      (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        x (↑w : InfinitePlace K) -
          HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, x w') * (↑(finrank ℚ K) : ℝ)⁻¹)
      (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        x_1 (↑w : InfinitePlace K) -
          HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, x_1 w') *
            (↑(finrank ℚ K) : ℝ)⁻¹)
      x_2

Tactic:
simp [sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x x_1 : realSpace K
x_2 : { w : InfinitePlace K // w ≠ w₀ }
⊢ x (↑x_2 : InfinitePlace K) + x_1 (↑x_2 : InfinitePlace K) -
      (↑(↑x_2 : InfinitePlace K).mult : ℝ) *
          HAdd.hAdd (α := ℝ) (∑ x_3 : InfinitePlace K, x x_3) (∑ x : InfinitePlace K, x_1 x) *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    x (↑x_2 : InfinitePlace K) -
        HMul.hMul (α := ℝ) (↑(↑x_2 : InfinitePlace K).mult : ℝ) (∑ x_3 : InfinitePlace K, x x_3) *
          (↑(finrank ℚ K) : ℝ)⁻¹ +
      (x_1 (↑x_2 : InfinitePlace K) -
        HMul.hMul (α := ℝ) (↑(↑x_2 : InfinitePlace K).mult : ℝ) (∑ x : InfinitePlace K, x_1 x) * (↑(finrank ℚ K) : ℝ)⁻¹)

Tactic:
ring
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : ℝ
x_1 : realSpace K
x_2 : { w : InfinitePlace K // w ≠ w₀ }
simp :
  x * x_1 (↑x_2 : InfinitePlace K) -
      (↑(↑x_2 : InfinitePlace K).mult : ℝ) * (x * ∑ i : InfinitePlace K, x_1 i) * (↑(finrank ℚ K) : ℝ)⁻¹ =
    x *
      (x_1 (↑x_2 : InfinitePlace K) -
        HMul.hMul (α := ℝ) (↑(↑x_2 : InfinitePlace K).mult : ℝ) (∑ i : InfinitePlace K, x_1 i) * (↑(finrank ℚ K) : ℝ)⁻¹)
⊢ (x • x_1) (↑x_2 : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x_2 : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, (x • x_1) w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    HSMul.hSMul (α := ℝ) (β := { w : InfinitePlace K // w ≠ w₀ } → ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) x : ℝ)
      (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        x_1 (↑w : InfinitePlace K) -
          HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, x_1 w') *
            (↑(finrank ℚ K) : ℝ)⁻¹)
      x_2

Tactic:
simp [← mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : ℝ
x_1 : realSpace K
x_2 : { w : InfinitePlace K // w ≠ w₀ }
⊢ x * x_1 (↑x_2 : InfinitePlace K) -
      (↑(↑x_2 : InfinitePlace K).mult : ℝ) * (x * ∑ i : InfinitePlace K, x_1 i) * (↑(finrank ℚ K) : ℝ)⁻¹ =
    x *
      (x_1 (↑x_2 : InfinitePlace K) -
        HMul.hMul (α := ℝ) (↑(↑x_2 : InfinitePlace K).mult : ℝ) (∑ i : InfinitePlace K, x_1 i) * (↑(finrank ℚ K) : ℝ)⁻¹)

Tactic:
ring
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ (realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ) x w =
    x (↑w : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, x w') * (↑(finrank ℚ K) : ℝ)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
hx : x ≠ 0
h :
  ∀ (w : { w : InfinitePlace K // w ≠ w₀ }),
    (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
⊢ Eq.{u_1 + 1} (α := { w : InfinitePlace K // w ≠ w₀ } → ℝ)
    ((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 : InfinitePlace K // w ≠ w₀ } → ℝ)
    (logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) : logSpace K)

Tactic:
ext w
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ (x : { w : InfinitePlace K // w ≠ w₀ }),
    Eq (α := ℝ)
      ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ) (completeFamily K w₀) x) (0 x)
⊢ 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₀ } → ℝ)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i : { w : InfinitePlace K // w ≠ w₀ }
h :
  ∀ (x : { w : InfinitePlace K // w ≠ w₀ }),
    Eq (α := ℝ)
      ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ)
        (completeFamily K (↑i : InfinitePlace K)) x)
      ((↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K))
              (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                    (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                  i :
                Fin (rank K))) :
          logSpace K)
        x)
⊢ Eq (α := { w : InfinitePlace K // w ≠ w₀ } → ℝ)
    ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ)
        (completeFamily K (↑i : InfinitePlace K)) :
      { w : InfinitePlace K // w ≠ w₀ } → ℝ)
    ((↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K))
            (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                  (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                i :
              Fin (rank K))) :
        logSpace K) :
      logSpace K)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i x : { w : InfinitePlace K // w ≠ w₀ }
h :
  Ne (α := 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 : InfinitePlace K) ⋯))) :
          𝓞 K) :
      K)
    (0 : K)
⊢ Eq (α := ℝ)
    ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ)
      (completeFamily K (↑i : InfinitePlace K)) x)
    ((↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K))
            (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                  (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                i :
              Fin (rank K))) :
        logSpace K)
      x)

Tactic:
rw [← logEmbedding_fundSystem, ← logMap_eq_logEmbedding, completeFamily, dif_neg,
    realSpaceToLogSpace_expMap_symm]

Premises used: NumberField.Units.logEmbedding_fundSystem, NumberField.mixedEmbedding.fundamentalCone.completeFamily, NumberField.mixedEmbedding.logMap_eq_logEmbedding, dif_neg, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_expMap_symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i x : { w : InfinitePlace K // w ≠ w₀ }
⊢ Ne (α := 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 : InfinitePlace K) ⋯))) :
          𝓞 K) :
      K)
    (0 : K)

Tactic:
coe_ne_zero _

Premises used: NumberField.Units.coe_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i x : { w : InfinitePlace K // w ≠ w₀ }
⊢ Ne (α := 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 : InfinitePlace K) ⋯))) :
          𝓞 K) :
      K)
    (0 : K)

Tactic:
exact coe_ne_zero _

Premises used: NumberField.Units.coe_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x x_1 : realSpace K
h :
  Membership.mem (γ := Set (realSpace K))
    (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)) x_1
mem :
  ∀ (w : { w : InfinitePlace K // w ≠ w₀ }),
    Eq (α := ℝ)
      (∑ w_1 : InfinitePlace K,
        (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)) w w_1)
      0
⊢ Eq (α := ℝ) (∑ w : InfinitePlace K, x_1 w) 0

Tactic:
obtain ⟨w, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
w : { w : InfinitePlace K // w ≠ w₀ }
mem mem₁ : Eq (α := ℝ) (∑ x : InfinitePlace K, completeFamily K (↑w : InfinitePlace K) x) 0
mem₂ :
  Eq (α := ℝ)
    (∑ x : InfinitePlace K,
      (if hi : (↑w : InfinitePlace K) = 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 : InfinitePlace K) hi))) :
                    𝓞 K)))))
        x)
    0
mem₃ :
  Eq (α := ℝ)
    (∑ x : InfinitePlace 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))
                      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) (↑w : InfinitePlace K) ⋯))) :
                𝓞 K))))
        x)
    0
mem₄ :
  Real.log
      (↑|(Algebra.norm ℚ : (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 : InfinitePlace K) ⋯))) :
                    𝓞 K) :
                K)| :
        ℝ) =
    0
mem₅ : Real.log (↑1 : ℝ) = 0
mem₆ : Real.log 1 = 0
⊢ Eq (α := ℝ)
    (∑ w_1 : InfinitePlace K,
      (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)) w w_1)
    0

Tactic:
simp_rw [completeFamily, dif_neg w.prop, sum_expMap_symm_apply (coe_ne_zero _),
        Units.norm, Rat.cast_one, Real.log_one]

Premises used: NumberField.mixedEmbedding.fundamentalCone.completeFamily, NumberField.Units.norm, Real.log_one, dif_neg, Subtype.prop, NumberField.Units.coe_ne_zero, NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply, Rat.cast_one
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
⊢ Eq (α := ℝ) (∑ w : InfinitePlace K, 0 w) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x x_1 y : realSpace K
hx_1 :
  Membership.mem (γ := Submodule ℝ (realSpace K))
    (Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)))
    x_1
hy_1 :
  Membership.mem (γ := Submodule ℝ (realSpace K))
    (Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)))
    y
hx : Eq (α := ℝ) (∑ w : InfinitePlace K, x_1 w) 0
hy : Eq (α := ℝ) (∑ w : InfinitePlace K, y w) 0
⊢ Eq (α := ℝ) (∑ w : InfinitePlace K, (x_1 + y) w) 0

Tactic:
simp [sum_add_distrib, hx, hy]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
a : ℝ
x_1 : realSpace K
hx_1 :
  Membership.mem (γ := Submodule ℝ (realSpace K))
    (Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)))
    x_1
hx : Eq (α := ℝ) (∑ w : InfinitePlace K, x_1 w) 0
⊢ Eq (α := ℝ) (∑ w : InfinitePlace K, (a • x_1) w) 0

Tactic:
simp [← mul_sum, hx]

Premises used: Finset.mul_sum
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx :
  Membership.mem (γ := Submodule ℝ (realSpace K))
    (Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)))
    x
mem :
  ∀ (x : realSpace K)
    (h :
      Membership.mem (γ := Set (realSpace K))
        (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)) x),
    Eq (α := ℝ) (∑ w : InfinitePlace K, x w) 0
zero : Eq (α := ℝ) (∑ w : InfinitePlace K, 0 w) 0
add :
  ∀ (x y : realSpace K),
    Membership.mem (γ := Submodule ℝ (realSpace K))
        (Submodule.span ℝ
          (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)))
        x →
      Membership.mem (γ := Submodule ℝ (realSpace K))
          (Submodule.span ℝ
            (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)))
          y →
        ∀ (hx : Eq (α := ℝ) (∑ w : InfinitePlace K, x w) 0) (hy : Eq (α := ℝ) (∑ w : InfinitePlace K, y w) 0),
          Eq (α := ℝ) (∑ w : InfinitePlace K, (x + y) w) 0
smul :
  ∀ (a : ℝ) (x : realSpace K),
    Membership.mem (γ := Submodule ℝ (realSpace K))
        (Submodule.span ℝ
          (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)))
        x →
      ∀ (hx : Eq (α := ℝ) (∑ w : InfinitePlace K, x w) 0), Eq (α := ℝ) (∑ w : InfinitePlace K, (a • x) w) 0
⊢ Eq (α := ℝ) (∑ w : InfinitePlace K, x w) 0

Tactic:
induction hx using Submodule.span_induction with
  | mem _ h =>
      obtain ⟨w, rfl⟩ := h
      simp_rw [completeFamily, dif_neg w.prop, sum_expMap_symm_apply (coe_ne_zero _),
        Units.norm, Rat.cast_one, Real.log_one]
  | zero => simp
  | add _ _ _ _ hx hy => simp [sum_add_distrib, hx, hy]
  | smul _ _ _ hx => simp [← mul_sum, hx]

Premises used: Finset.mul_sum, Finset.sum_add_distrib, NumberField.mixedEmbedding.fundamentalCone.completeFamily, NumberField.Units.norm, Real.log_one, NumberField.Units.coe_ne_zero, NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply, rfl, Rat.cast_one
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)

Tactic:
LinearIndependent.of_comp realSpaceToLogSpace ?_

Premises used: LinearIndependent.of_comp, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine :
  LinearIndependent.{u_1, 0, u_1} (ι := { w : InfinitePlace K // w ≠ w₀ }) ℝ (M :=
    { w : InfinitePlace K // w ≠ w₀ } → ℝ)
    (Function.comp (β := realSpace K) (⇑realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ)
      fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K))
⊢ LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)

Tactic:
refine LinearIndependent.of_comp realSpaceToLogSpace ?_

Premises used: LinearIndependent.of_comp, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
simp_rw :
  LinearIndependent ℝ (M := { w : InfinitePlace K // w ≠ w₀ } → ℝ) fun (x : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K))
          (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
              x :
            Fin (rank K))) :
      logSpace K)
⊢ LinearIndependent.{u_1, 0, u_1} (ι := { w : InfinitePlace K // w ≠ w₀ }) ℝ (M :=
    { w : InfinitePlace K // w ≠ w₀ } → ℝ)
    (Function.comp (β := realSpace K) (⇑realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ)
      fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K))

Tactic:
simp_rw [Function.comp_def, realSpaceToLogSpace_completeFamily_of_ne]

Premises used: NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, Function.comp_def
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ LinearIndependent.{u_1, 0, u_1} (ι := { w : InfinitePlace K // w ≠ w₀ }) ℝ (M := logSpace K)
    (⇑(Basis.reindex (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) equivFinRank) :
      (a : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K)

Tactic:
(((basisUnitLattice K).ofZLatticeBasis ℝ _).reindex equivFinRank).linearIndependent

Premises used: NumberField.Units.basisUnitLattice, Real, Module.Basis.ofZLatticeBasis, NumberField.mixedEmbedding.fundamentalCone.equivFinRank, Module.Basis.linearIndependent, Module.Basis.reindex