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₀ }
⊢ 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)
have 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)
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
i 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)
have 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) sorry))) :
        𝓞 K) :
    K)
  (0 : K)
Tactic: rw [← logEmbedding_fundSystem, ← logMap_eq_logEmbedding, completeFamily, dif_neg,
    realSpaceToLogSpace_expMap_symm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ Eq (α := ℝ) (∑ w : InfinitePlace K, x_1 w) 0
have 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
Tactic: obtain ⟨w, rfl⟩ := h
Cleared hypotheses: x_1, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ Eq (α := ℝ)
    (∑ w_1 : InfinitePlace K,
      (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)) w w_1)
    0
have 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
Tactic: simp_rw [completeFamily, dif_neg w.prop, sum_expMap_symm_apply (coe_ne_zero _),
        Units.norm, Rat.cast_one, Real.log_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ Eq (α := ℝ)
    (∑ w_1 : InfinitePlace K,
      (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)) w w_1)
    0
have 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) sorry))) :
              𝓞 K))))
      x)
  0
Tactic: simp_rw [completeFamily, dif_neg w.prop, sum_expMap_symm_apply (coe_ne_zero _),
        Units.norm, Rat.cast_one, Real.log_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ Eq (α := ℝ)
    (∑ w_1 : InfinitePlace K,
      (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)) w w_1)
    0
have 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) sorry))) :
                  𝓞 K) :
              K)| :
      ℝ) =
  0
Tactic: simp_rw [completeFamily, dif_neg w.prop, sum_expMap_symm_apply (coe_ne_zero _),
        Units.norm, Rat.cast_one, Real.log_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ Eq (α := ℝ)
    (∑ w_1 : InfinitePlace K,
      (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)) w w_1)
    0
have mem₅ : Real.log (↑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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ Eq (α := ℝ)
    (∑ w_1 : InfinitePlace K,
      (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)) w w_1)
    0
have mem₆ : Real.log 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ Eq (α := ℝ) (∑ w : InfinitePlace K, x w) 0
have 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
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]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ Eq (α := ℝ) (∑ w : InfinitePlace K, x w) 0
have zero : Eq (α := ℝ) (∑ w : InfinitePlace K, 0 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]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ Eq (α := ℝ) (∑ w : InfinitePlace K, x w) 0
have 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
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]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ Eq (α := ℝ) (∑ w : InfinitePlace K, x w) 0
have 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
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]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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)
have 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))
Tactic: refine LinearIndependent.of_comp realSpaceToLogSpace ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField 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))
have 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)
Tactic: simp_rw [Function.comp_def, realSpaceToLogSpace_completeFamily_of_ne]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 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)
have h : ∀ (x : { w : InfinitePlace K // w ≠ w₀ }),
  Eq (α := logSpace K)
    ((↑((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) :
      logSpace K)
    ((Basis.reindex (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) equivFinRank :
          (a : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K)
        x :
      logSpace K)
Tactic: convert! (((basisUnitLattice K).ofZLatticeBasis ℝ _).reindex equivFinRank).linearIndependent
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
h :
  Membership.mem (γ := Submodule ℝ (realSpace K))
    (Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)))
    (completeFamily K w₀)
⊢ False
have this : Eq (α := ℝ) (∑ w : InfinitePlace K, completeFamily K w₀ w) 0
Tactic: have := sum_eq_zero_of_mem_span_completeFamily h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
h :
  Membership.mem (γ := Submodule ℝ (realSpace K))
    (Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)))
    (completeFamily K w₀)
this : Eq (α := ℝ) (∑ w : InfinitePlace K, completeFamily K w₀ w) 0
⊢ False
have this₁ : finrank ℚ K = 0
Tactic: rw [completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq, Nat.cast_eq_zero] at this
Cleared hypotheses: this