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 : realSpace K
simp_rw :
  Real.exp (x w₀) ^ finrank ℚ K *
      ∏ x_1 : { w : InfinitePlace K // w ≠ w₀ },
        ∏ x_2 : InfinitePlace K,
          HPow.hPow (α := ℝ)
              ((x_2 : (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))
                              x_1)) :
                        𝓞 K) :
                    K) :
                ℝ)
              x_2.mult ^
            x (↑x_1 : InfinitePlace K) =
    Real.exp (x w₀) ^ finrank ℚ K
simp_rw₁ :
  Real.exp (x w₀) ^ finrank ℚ K *
      ∏ x_1 : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          (∏ i : InfinitePlace K,
            HPow.hPow (α := ℝ)
              ((i : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K
                            (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                              x_1)) :
                        𝓞 K) :
                    K) :
                ℝ)
              i.mult)
          (x (↑x_1 : InfinitePlace K)) =
    Real.exp (x w₀) ^ finrank ℚ K
⊢ Real.exp (x w₀) ^ finrank ℚ K *
      ∏ y : { w : InfinitePlace K // w ≠ w₀ },
        ∏ x_1 : InfinitePlace K,
          HPow.hPow (α := ℝ)
              ((x_1 : (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))
                              y)) :
                        𝓞 K) :
                    K) :
                ℝ)
              (x (↑y : InfinitePlace K)) ^
            x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K
have simp_rw₂ : Real.exp (x w₀) ^ finrank ℚ K *
    ∏ x_1 : { w : InfinitePlace K // w ≠ w₀ },
      HPow.hPow (α := ℝ)
        (↑|(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))
                            x_1)) :
                      𝓞 K) :
                  K)| :
          ℝ)
        (x (↑x_1 : InfinitePlace K)) =
  Real.exp (x w₀) ^ finrank ℚ K
Tactic: simp_rw [Real.rpow_pow_comm (apply_nonneg _ _), Real.finsetProd_rpow _ _
    fun _ _ ↦ pow_nonneg (apply_nonneg _ _) _, prod_eq_abs_norm, Units.norm, Rat.cast_one,
    Real.one_rpow, prod_const_one, mul_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
⊢ Membership.mem (γ := Set (logSpace K))
      (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
      (logMap
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMapBasis : realSpace K → realSpace K) x))) ↔
    ∀ (w : InfinitePlace K), w ≠ w₀ → Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)
have simp_rw : (∀ (a : InfinitePlace K) (b : a ≠ w₀),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
      (((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                    logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
                  (a : logSpace K) → Fin (rank K) →₀ ℝ)
                (logMap
                  ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
                    ((↑expMapBasis : realSpace K → realSpace K) x))) :
              Fin (rank K) →₀ ℝ) :
            (a : Fin (rank 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 (a : InfinitePlace K) ↦ a ≠ w₀) a b) :
            Fin (rank K)) :
        ℝ)) ↔
  ∀ (w : InfinitePlace K), w ≠ w₀ → Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)
Tactic: simp_rw [ZSpan.mem_fundamentalDomain, equivFinRank.forall_congr_left, Subtype.forall]
-- 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
⊢ (∀ (a : InfinitePlace K) (b : a ≠ w₀),
      Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
        (((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                      logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
                    (a : logSpace K) → Fin (rank K) →₀ ℝ)
                  (logMap
                    ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
                      ((↑expMapBasis : realSpace K → realSpace K) x))) :
                Fin (rank K) →₀ ℝ) :
              (a : Fin (rank 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 (a : InfinitePlace K) ↦ a ≠ w₀) a b) :
              Fin (rank K)) :
          ℝ)) ↔
    ∀ (w : InfinitePlace K), w ≠ w₀ → Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)
have refine : ∀ (w : InfinitePlace K) (hw : w ≠ w₀),
  Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
      (((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                    logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
                  (a : logSpace K) → Fin (rank K) →₀ ℝ)
                (logMap
                  ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
                    ((↑expMapBasis : realSpace K → realSpace K) x))) :
              Fin (rank K) →₀ ℝ) :
            (a : Fin (rank 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 (a : InfinitePlace K) ↦ a ≠ w₀) w hw) :
            Fin (rank K)) :
        ℝ) ↔
    Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)
Tactic: refine forall₂_congr fun w hw ↦ ?_
-- 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 : InfinitePlace K
hw : w ≠ w₀
⊢ Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
            ((↑expMap : realSpace K → realSpace K)
              ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K)
                fun (i : InfinitePlace K) ↦ if i = w₀ then 0 else x i)) :
          mixedSpace K) :
      ℝ)
    (1 : ℝ)
have rw : Eq (α := ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
          ((↑expMapBasis : realSpace K → realSpace K) fun (i : InfinitePlace K) ↦ if i = w₀ then 0 else x i) :
        mixedSpace K) :
    ℝ)
  (1 : ℝ)
Tactic: rw [← expMapBasis_apply,
    norm_expMapBasis, if_pos rfl, Real.exp_zero, one_pow]
-- 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 : InfinitePlace K
hw : w ≠ w₀
rw :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
            ((↑expMapBasis : realSpace K → realSpace K) fun (i : InfinitePlace K) ↦ if i = w₀ then 0 else x i) :
          mixedSpace K) :
      ℝ)
    (1 : ℝ)
⊢ Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
            ((↑expMap : realSpace K → realSpace K)
              ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K)
                fun (i : InfinitePlace K) ↦ if i = w₀ then 0 else x i)) :
          mixedSpace K) :
      ℝ)
    (1 : ℝ)
have rw₁ : Real.exp (if Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then 0 else x w₀) ^ finrank ℚ K = 1
Tactic: rw [← expMapBasis_apply,
    norm_expMapBasis, if_pos rfl, Real.exp_zero, one_pow]
-- 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 : InfinitePlace K
hw : w ≠ w₀
rw :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
            ((↑expMapBasis : realSpace K → realSpace K) fun (i : InfinitePlace K) ↦ if i = w₀ then 0 else x i) :
          mixedSpace K) :
      ℝ)
    (1 : ℝ)
rw₁ : Real.exp (if Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then 0 else x w₀) ^ finrank ℚ K = 1
⊢ Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
            ((↑expMap : realSpace K → realSpace K)
              ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K)
                fun (i : InfinitePlace K) ↦ if i = w₀ then 0 else x i)) :
          mixedSpace K) :
      ℝ)
    (1 : ℝ)
have rw₂ : Real.exp 0 ^ finrank ℚ K = 1
Tactic: rw [← expMapBasis_apply,
    norm_expMapBasis, if_pos rfl, Real.exp_zero, one_pow]
-- 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 : InfinitePlace K
hw : w ≠ w₀
rw :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
            ((↑expMapBasis : realSpace K → realSpace K) fun (i : InfinitePlace K) ↦ if i = w₀ then 0 else x i) :
          mixedSpace K) :
      ℝ)
    (1 : ℝ)
rw₁ : Real.exp (if Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then 0 else x w₀) ^ finrank ℚ K = 1
rw₂ : Real.exp 0 ^ finrank ℚ K = 1
⊢ Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
            ((↑expMap : realSpace K → realSpace K)
              ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K)
                fun (i : InfinitePlace K) ↦ if i = w₀ then 0 else x i)) :
          mixedSpace K) :
      ℝ)
    (1 : ℝ)
have rw₃ : HPow.hPow (α := ℝ) 1 (finrank ℚ K) = 1
Tactic: rw [← expMapBasis_apply,
    norm_expMapBasis, if_pos rfl, Real.exp_zero, one_pow]
-- 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 : InfinitePlace K
hw : w ≠ w₀
rw :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
            ((↑expMapBasis : realSpace K → realSpace K) fun (i : InfinitePlace K) ↦ if i = w₀ then 0 else x i) :
          mixedSpace K) :
      ℝ)
    (1 : ℝ)
rw₁ : Real.exp (if Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then 0 else x w₀) ^ finrank ℚ K = 1
rw₂ : Real.exp 0 ^ finrank ℚ K = 1
rw₃ : HPow.hPow (α := ℝ) 1 (finrank ℚ K) = 1
⊢ Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
            ((↑expMap : realSpace K → realSpace K)
              ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K)
                fun (i : InfinitePlace K) ↦ if i = w₀ then 0 else x i)) :
          mixedSpace K) :
      ℝ)
    (1 : ℝ)
have rw₄ : Eq (α := ℝ) 1 1
Tactic: rw [← expMapBasis_apply,
    norm_expMapBasis, if_pos rfl, Real.exp_zero, one_pow]
-- 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 : InfinitePlace K
hw : w ≠ w₀
⊢ Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
      (((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                    logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
                  (a : logSpace K) → Fin (rank K) →₀ ℝ)
                (logMap
                  ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
                    ((↑expMapBasis : realSpace K → realSpace K) x))) :
              Fin (rank K) →₀ ℝ) :
            (a : Fin (rank 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 (a : InfinitePlace K) ↦ a ≠ w₀) w hw) :
            Fin (rank K)) :
        ℝ) ↔
    Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)
have rw : Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
    ((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
              (a : logSpace K) → Fin (rank K) →₀ ℝ)
            fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
            (∑ i : { i : InfinitePlace K // i ≠ w₀ },
                HSMul.hSMul (β := realSpace K) (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
                  ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K))
              (↑w : InfinitePlace K) :
          (a : Fin (rank 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 (a : InfinitePlace K) ↦ a ≠ w₀) w hw) :
          Fin (rank K)) :
      ℝ) ↔
  Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)
Tactic: rw [expMapBasis_apply'', map_smul, logMap_real_smul (norm_expMapBasis_ne_zero _)
    (Real.exp_ne_zero _), expMapBasis_apply, logMap_expMap (by rw [← expMapBasis_apply,
    norm_expMapBasis, if_pos rfl, Real.exp_zero, one_pow]), Basis.equivFun_symm_apply,
    Fintype.sum_eq_add_sum_subtype_ne _ w₀, if_pos rfl, zero_smul, zero_add]
-- 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 : InfinitePlace K
hw : w ≠ w₀
| Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
    ((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
              (a : logSpace K) → Fin (rank K) →₀ ℝ)
            fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
            (∑ i : { i : InfinitePlace K // i ≠ w₀ },
                HSMul.hSMul (β := realSpace K) (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
                  ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K))
              (↑w : InfinitePlace K) :
          (a : Fin (rank 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 (a : InfinitePlace K) ↦ a ≠ w₀) w hw) :
          Fin (rank K)) :
      ℝ)
have h : ∀ (w i : { i : InfinitePlace K // i ≠ w₀ }),
  HSMul.hSMul (β := realSpace K) (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
    ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K)
Tactic: enter [2, 1, 2, w, 2, i]
-- 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_1 : InfinitePlace K
hw : w_1 ≠ w₀
w i : { i : InfinitePlace K // i ≠ w₀ }
| HSMul.hSMul (β := realSpace K) (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
    ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K)
have h : HSMul.hSMul (β := realSpace K) (x (↑i : InfinitePlace K))
  ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K)
Tactic: rw [if_neg i.prop]
-- 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 : InfinitePlace K
hw : w ≠ w₀
| Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
    ((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
              (a : logSpace K) → Fin (rank K) →₀ ℝ)
            fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
            (∑ i : { i : InfinitePlace K // i ≠ w₀ },
                HSMul.hSMul (β := realSpace K) (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
                  ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K))
              (↑w : InfinitePlace K) :
          (a : Fin (rank 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 (a : InfinitePlace K) ↦ a ≠ w₀) w hw) :
          Fin (rank K)) :
      ℝ)
have h : ∀ (w i : { i : InfinitePlace K // i ≠ w₀ }),
  HSMul.hSMul (β := realSpace K) (x (↑i : InfinitePlace K))
    ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K)
Tactic: enter [2, 1, 2, w, 2, i]
    rw [if_neg i.prop]
-- 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 : InfinitePlace K
hw : w ≠ w₀
⊢ Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
      ((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                  logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
                (a : logSpace K) → Fin (rank K) →₀ ℝ)
              fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
              (∑ i : { i : InfinitePlace K // i ≠ w₀ },
                  HSMul.hSMul (β := realSpace K) (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
                    ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K))
                (↑w : InfinitePlace K) :
            (a : Fin (rank 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 (a : InfinitePlace K) ↦ a ≠ w₀) w hw) :
            Fin (rank K)) :
        ℝ) ↔
    Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)
have conv_lhs : Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
    ((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
              (a : logSpace K) → Fin (rank K) →₀ ℝ)
            fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
            (∑ i : { i : InfinitePlace K // i ≠ w₀ },
                HSMul.hSMul (β := realSpace K) (x (↑i : InfinitePlace K))
                  ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K))
              (↑w : InfinitePlace K) :
          (a : Fin (rank 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 (a : InfinitePlace K) ↦ a ≠ w₀) w hw) :
          Fin (rank K)) :
      ℝ) ↔
  Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)
Tactic: conv_lhs =>
    enter [2, 1, 2, w, 2, i]
    rw [if_neg i.prop]
-- 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
⊢ Membership.mem (γ := Set (logSpace K))
      (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
      (logMap
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMapBasis : realSpace K → realSpace K) x))) ↔
    ∀ (w : InfinitePlace K), w ≠ w₀ → Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)
have simp_rw : (∀ (i : Fin (rank K)),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
      (((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                    logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
                  (a : logSpace K) → Fin (rank K) →₀ ℝ)
                (logMap
                  ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
                    ((↑expMapBasis : realSpace K → realSpace K) x))) :
              Fin (rank K) →₀ ℝ) :
            (a : Fin (rank K)) → ℝ)
          i :
        ℝ)) ↔
  ∀ (w : InfinitePlace K), w ≠ w₀ → Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)
Tactic: classical
  simp_rw [ZSpan.mem_fundamentalDomain, equivFinRank.forall_congr_left, Subtype.forall]
  refine forall₂_congr fun w hw ↦ ?_
  rw [expMapBasis_apply'', map_smul, logMap_real_smul (norm_expMapBasis_ne_zero _)
    (Real.exp_ne_zero _), expMapBasis_apply, logMap_expMap (by rw [← expMapBasis_apply,
    norm_expMapBasis, if_pos rfl, Real.exp_zero, one_pow]), Basis.equivFun_symm_apply,
    Fintype.sum_eq_add_sum_subtype_ne _ w₀, if_pos rfl, zero_smul, zero_add]
  conv_lhs =>
    enter [2, 1, 2, w, 2, i]
    rw [if_neg i.prop]
  simp_rw [sum_apply, ← sum_fn, map_sum, Pi.smul_apply, ← Pi.smul_def, map_smul,
    completeBasis_apply_of_ne, expMap_symm_apply, normAtAllPlaces_mixedEmbedding,
    ← logEmbedding_component, logEmbedding_fundSystem, Finsupp.coe_finsetSum, Finsupp.coe_smul,
    sum_apply, Pi.smul_apply, Basis.ofZLatticeBasis_repr_apply, Basis.repr_self,
    Finsupp.single_apply, EmbeddingLike.apply_eq_iff_eq, Int.cast_ite, Int.cast_one, Int.cast_zero,
    smul_ite, smul_eq_mul, mul_one, mul_zero, Fintype.sum_ite_eq']