awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
have h₂ : completeFamily K w₀ ∉
  Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K))
Tactic: have h₂ : completeFamily K w₀ ∉ Submodule.span ℝ
      (Set.range (fun w : {w // w ≠ w₀} ↦ completeFamily K w.1)) := by
    intro h
    have := sum_eq_zero_of_mem_span_completeFamily h
    rw [completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq, Nat.cast_eq_zero] at this
    exact Module.finrank_pos.ne' this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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₂ :
  completeFamily K w₀ ∉
    Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K))
⊢ LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
have rw : LinearIndependent (ι := { b : InfinitePlace K // b ≠ w₀ }) ℝ (M := realSpace K)
    ((completeFamily K ∘
        (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K)) ∘
      some) ∧
  Function.comp (α := Option { b : InfinitePlace K // b ≠ w₀ }) (completeFamily K)
      (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K) none ∉
    Submodule.span ℝ
      (Set.range (ι := { b : InfinitePlace K // b ≠ w₀ })
        ((completeFamily K ∘
            (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K)) ∘
          some))
Tactic: rw [← linearIndependent_equiv (Equiv.optionSubtypeNe w₀), linearIndependent_option]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
have have : LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
  completeFamily K (↑w : InfinitePlace K)
Tactic: classical
  have h₁ : LinearIndependent ℝ (fun w : {w // w ≠ w₀} ↦ completeFamily K w.1) := by
    refine LinearIndependent.of_comp realSpaceToLogSpace ?_
    simp_rw [Function.comp_def, realSpaceToLogSpace_completeFamily_of_ne]
    convert! (((basisUnitLattice K).ofZLatticeBasis ℝ _).reindex equivFinRank).linearIndependent
    simp
  have h₂ : completeFamily K w₀ ∉ Submodule.span ℝ
      (Set.range (fun w : {w // w ≠ w₀} ↦ completeFamily K w.1)) := by
    intro h
    have := sum_eq_zero_of_mem_span_completeFamily h
    rw [completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq, Nat.cast_eq_zero] at this
    exact Module.finrank_pos.ne' this
  rw [← linearIndependent_equiv (Equiv.optionSubtypeNe w₀), linearIndependent_option]
  exact ⟨h₁, h₂⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
have :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
⊢ LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
have have₁ : ∀
  (h₁ :
    LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
      completeFamily K (↑w : InfinitePlace K)),
  LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
Tactic: classical
  have h₁ : LinearIndependent ℝ (fun w : {w // w ≠ w₀} ↦ completeFamily K w.1) := by
    refine LinearIndependent.of_comp realSpaceToLogSpace ?_
    simp_rw [Function.comp_def, realSpaceToLogSpace_completeFamily_of_ne]
    convert! (((basisUnitLattice K).ofZLatticeBasis ℝ _).reindex equivFinRank).linearIndependent
    simp
  have h₂ : completeFamily K w₀ ∉ Submodule.span ℝ
      (Set.range (fun w : {w // w ≠ w₀} ↦ completeFamily K w.1)) := by
    intro h
    have := sum_eq_zero_of_mem_span_completeFamily h
    rw [completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq, Nat.cast_eq_zero] at this
    exact Module.finrank_pos.ne' this
  rw [← linearIndependent_equiv (Equiv.optionSubtypeNe w₀), linearIndependent_option]
  exact ⟨h₁, h₂⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
have :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
have₁ :
  ∀
    (h₁ :
      LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        completeFamily K (↑w : InfinitePlace K)),
    LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
have₂ :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
have₃ have₄ :
  ∀
    (h₁ :
      LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        completeFamily K (↑w : InfinitePlace K)),
    LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
⊢ LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
have have₅ : ∀
  (h₁ :
    LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
      completeFamily K (↑w : InfinitePlace K))
  (h₂ :
    completeFamily K w₀ ∉
      Submodule.span ℝ
        (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K))),
  LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
Tactic: classical
  have h₁ : LinearIndependent ℝ (fun w : {w // w ≠ w₀} ↦ completeFamily K w.1) := by
    refine LinearIndependent.of_comp realSpaceToLogSpace ?_
    simp_rw [Function.comp_def, realSpaceToLogSpace_completeFamily_of_ne]
    convert! (((basisUnitLattice K).ofZLatticeBasis ℝ _).reindex equivFinRank).linearIndependent
    simp
  have h₂ : completeFamily K w₀ ∉ Submodule.span ℝ
      (Set.range (fun w : {w // w ≠ w₀} ↦ completeFamily K w.1)) := by
    intro h
    have := sum_eq_zero_of_mem_span_completeFamily h
    rw [completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq, Nat.cast_eq_zero] at this
    exact Module.finrank_pos.ne' this
  rw [← linearIndependent_equiv (Equiv.optionSubtypeNe w₀), linearIndependent_option]
  exact ⟨h₁, h₂⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
have :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
have₁ :
  ∀
    (h₁ :
      LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        completeFamily K (↑w : InfinitePlace K)),
    LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
have₂ :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
have₃ have₄ :
  ∀
    (h₁ :
      LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        completeFamily K (↑w : InfinitePlace K)),
    LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
have₅ :
  ∀
    (h₁ :
      LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        completeFamily K (↑w : InfinitePlace K))
    (h₂ :
      completeFamily K w₀ ∉
        Submodule.span ℝ
          (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K))),
    LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
⊢ LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
have have₆ : ∀
  (h₁ :
    LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
      completeFamily K (↑w : InfinitePlace K))
  (h₂ :
    completeFamily K w₀ ∉
      Submodule.span ℝ
        (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K))),
  LinearIndependent (ι := { b : InfinitePlace K // b ≠ w₀ }) ℝ (M := realSpace K)
      ((completeFamily K ∘
          (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K)) ∘
        some) ∧
    Function.comp (α := Option { b : InfinitePlace K // b ≠ w₀ }) (completeFamily K)
        (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K) none ∉
      Submodule.span ℝ
        (Set.range (ι := { b : InfinitePlace K // b ≠ w₀ })
          ((completeFamily K ∘
              (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K)) ∘
            some))
Tactic: classical
  have h₁ : LinearIndependent ℝ (fun w : {w // w ≠ w₀} ↦ completeFamily K w.1) := by
    refine LinearIndependent.of_comp realSpaceToLogSpace ?_
    simp_rw [Function.comp_def, realSpaceToLogSpace_completeFamily_of_ne]
    convert! (((basisUnitLattice K).ofZLatticeBasis ℝ _).reindex equivFinRank).linearIndependent
    simp
  have h₂ : completeFamily K w₀ ∉ Submodule.span ℝ
      (Set.range (fun w : {w // w ≠ w₀} ↦ completeFamily K w.1)) := by
    intro h
    have := sum_eq_zero_of_mem_span_completeFamily h
    rw [completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq, Nat.cast_eq_zero] at this
    exact Module.finrank_pos.ne' this
  rw [← linearIndependent_equiv (Equiv.optionSubtypeNe w₀), linearIndependent_option]
  exact ⟨h₁, h₂⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀ : realSpace K)
    fun (w : InfinitePlace K) ↦ ((↑w.mult : ℝ) : ℝ)
have rw : Eq (α := realSpace K)
  ((basisOfLinearIndependentOfCardEqFinrank (b := completeFamily K) sorry sorry : (a : InfinitePlace K) → realSpace K) w₀ :
    realSpace K)
  fun (w : InfinitePlace K) ↦ ((↑w.mult : ℝ) : ℝ)
Tactic: rw [completeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, completeFamily, dif_pos rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Eq (α := realSpace K)
    ((basisOfLinearIndependentOfCardEqFinrank (b := completeFamily K) ⋯ ⋯ : (a : InfinitePlace K) → realSpace K) w₀ :
      realSpace K)
    fun (w : InfinitePlace K) ↦ ((↑w.mult : ℝ) : ℝ)
⊢ Eq (α := realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀ : realSpace K)
    fun (w : InfinitePlace K) ↦ ((↑w.mult : ℝ) : ℝ)
have rw₁ : Eq (α := realSpace K) (completeFamily K w₀) fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
Tactic: rw [completeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, completeFamily, dif_pos rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Eq (α := realSpace K)
    ((basisOfLinearIndependentOfCardEqFinrank (b := completeFamily K) ⋯ ⋯ : (a : InfinitePlace K) → realSpace K) w₀ :
      realSpace K)
    fun (w : InfinitePlace K) ↦ ((↑w.mult : ℝ) : ℝ)
rw₁ : Eq (α := realSpace K) (completeFamily K w₀) fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
⊢ Eq (α := realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀ : realSpace K)
    fun (w : InfinitePlace K) ↦ ((↑w.mult : ℝ) : ℝ)
have rw₂ : Eq.{u_1 + 1} (α := realSpace 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)))))
  fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
Tactic: rw [completeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, completeFamily, dif_pos rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Eq (α := realSpace K)
    ((basisOfLinearIndependentOfCardEqFinrank (b := completeFamily K) ⋯ ⋯ : (a : InfinitePlace K) → realSpace K) w₀ :
      realSpace K)
    fun (w : InfinitePlace K) ↦ ((↑w.mult : ℝ) : ℝ)
rw₁ : Eq (α := realSpace K) (completeFamily K w₀) fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
rw₂ :
  Eq.{u_1 + 1} (α := realSpace 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)))))
    fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
⊢ Eq (α := realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀ : realSpace K)
    fun (w : InfinitePlace K) ↦ ((↑w.mult : ℝ) : ℝ)
have rw₃ : Eq.{u_1 + 1} (α := realSpace K) (fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)) fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
Tactic: rw [completeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, completeFamily, dif_pos rfl]
-- 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 (α := realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace 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)))) :
      realSpace K)
have rw : Eq (α := realSpace K)
  ((basisOfLinearIndependentOfCardEqFinrank (b := completeFamily K) sorry sorry : (a : InfinitePlace K) → realSpace K)
      (↑i : InfinitePlace 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)))) :
    realSpace K)
Tactic: rw [completeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, completeFamily, dif_neg]
-- 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 (α := realSpace K)
    ((basisOfLinearIndependentOfCardEqFinrank (b := completeFamily K) ⋯ ⋯ : (a : InfinitePlace K) → realSpace K)
        (↑i : InfinitePlace 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)))) :
      realSpace K)
⊢ Eq (α := realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace 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)))) :
      realSpace K)
have rw₁ : completeFamily K (↑i : 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))
                  i)) :
            𝓞 K))))
Tactic: rw [completeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, completeFamily, dif_neg]
-- 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 (α := realSpace K)
    ((basisOfLinearIndependentOfCardEqFinrank (b := completeFamily K) ⋯ ⋯ : (a : InfinitePlace K) → realSpace K)
        (↑i : InfinitePlace 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)))) :
      realSpace K)
rw₁ :
  completeFamily K (↑i : 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))
                    i)) :
              𝓞 K))))
⊢ Eq (α := realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace 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)))) :
      realSpace K)
have rw₂ : Eq.{u_1 + 1} (α := realSpace K)
  (if hi : (↑i : 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₀) (↑i : InfinitePlace K) hi))) :
              𝓞 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)))))
Tactic: rw [completeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, completeFamily, dif_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq.{u_1 + 1} (α := realSpace K)
    ((↑expMap : realSpace K → realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀))
    fun (x : InfinitePlace K) ↦ Real.exp 1
have h : ∀ (x : InfinitePlace K),
  (↑expMap : realSpace K → realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀) x = Real.exp 1
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 : InfinitePlace K
⊢ (↑expMap : realSpace K → realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀) x = Real.exp 1
have h : Real.exp (HMul.hMul (α := ℝ) (↑x.mult : ℝ)⁻¹ ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀ x)) =
  Real.exp 1
Tactic: simp_rw [expMap_apply, completeBasis_apply_of_eq, inv_mul_cancel₀ mult_coe_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h :
  Real.exp (HMul.hMul (α := ℝ) (↑x.mult : ℝ)⁻¹ ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀ x)) =
    Real.exp 1
⊢ (↑expMap : realSpace K → realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀) x = Real.exp 1
have h₁ : Real.exp (HMul.hMul (α := ℝ) (↑x.mult : ℝ)⁻¹ (↑x.mult : ℝ)) = Real.exp 1
Tactic: simp_rw [expMap_apply, completeBasis_apply_of_eq, inv_mul_cancel₀ mult_coe_ne_zero]
-- 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.{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)
  ((↑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))))
Tactic: rw [completeBasis_apply_of_ne, expMap.right_inv (by simp [expMap_target, pos_at_place])]