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
w i : InfinitePlace K
hw : w = w₀
pos : Eq (α := ℝ) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀ i) (↑i.mult : ℝ)
pos₁ pos₂ : Eq (α := ℝ) ((fun (w : InfinitePlace K) ↦ ((↑w.mult : ℝ) : ℝ)) i) (↑i.mult : ℝ)
⊢ Eq (α := ℝ) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w i) (↑i.mult : ℝ)

Tactic:
rw [hw, completeBasis_apply_of_eq]

Premises used: NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_eq
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w i : InfinitePlace K
hw : ¬w = w₀
neg :
  (↑(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 hw))) :
              𝓞 K))))
      i =
    (↑i.mult : ℝ) *
      Real.log
        ((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))
                      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw))) :
                𝓞 K) :
            K))
neg₁ :
  (↑i.mult : ℝ) *
      Real.log
        (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 hw))) :
                𝓞 K)))
          i) =
    (↑i.mult : ℝ) *
      Real.log
        ((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))
                      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw))) :
                𝓞 K) :
            K))
⊢ (completeBasis K : (a : InfinitePlace K) → realSpace K) w i =
    (↑i.mult : ℝ) *
      Real.log
        ((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))
                      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw))) :
                𝓞 K) :
            K))

Tactic:
simp_rw [completeBasis_apply_of_ne K ⟨w, hw⟩, expMap_symm_apply, normAtAllPlaces_mixedEmbedding]

Premises used: NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, NumberField.mixedEmbedding.fundamentalCone.expMap_symm_apply, Subtype.mk, NumberField.mixedEmbedding.normAtAllPlaces_mixedEmbedding
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq.{u_1 + 1} (α := Set (realSpace K)) (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv expMapBasis))
    Set.univ

Tactic:
simp [expMapBasis, expMap_source]

Premises used: NumberField.mixedEmbedding.fundamentalCone.expMap_source, NumberField.mixedEmbedding.fundamentalCone.expMapBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := realSpace K) (↑expMapBasis : realSpace K → realSpace K)

Tactic:
(injective_expMap K).comp (completeBasis K).equivFun.symm.injective

Premises used: LinearEquiv.symm, OpenPartialHomeomorph.toFun', Pi.map, Real.exp, Function.Injective.comp, LinearEquiv.injective, NumberField.mixedEmbedding.fundamentalCone.injective_expMap, Module.Basis.equivFun, NumberField.mixedEmbedding.fundamentalCone.completeBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Continuous.{u_1, u_1} (X := realSpace K) (↑expMapBasis : realSpace K → realSpace K)

Tactic:
(continuous_expMap K).comp (ContinuousLinearEquiv.continuous _)

Premises used: Continuous.comp, NumberField.mixedEmbedding.fundamentalCone.continuous_expMap, OpenPartialHomeomorph.toFun', Pi.map, Real.exp, ContinuousLinearEquiv.continuous
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
w : InfinitePlace K
⊢ 0 < (↑expMapBasis : realSpace K → realSpace K) x w

Tactic:
expMap_pos _ _

Premises used: Multiset.sum, Multiset.foldr, Homeomorph.transOpenPartialHomeomorph, PartialEquiv.copy, Finsupp.sum, OpenPartialHomeomorph.pi, OpenPartialHomeomorph.toFun', Pi.map, Real.exp, NumberField.mixedEmbedding.fundamentalCone.expMap, PartialEquiv.pi, NumberField.mixedEmbedding.fundamentalCone.expMapBasis, NumberField.mixedEmbedding.fundamentalCone.expMap_pos, Finset.sum, Equiv.transPartialEquiv
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
w : InfinitePlace K
⊢ 0 ≤ (↑expMapBasis : realSpace K → realSpace K) x w

Tactic:
(expMapBasis_pos _ _).le

Premises used: LT.lt.le, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_pos
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
⊢ (↑expMapBasis : realSpace K → realSpace K) x =
    (↑expMap : realSpace K → realSpace K)
      ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Homeomorph.transOpenPartialHomeomorph, PartialEquiv.copy, Finsupp.sum, OpenPartialHomeomorph.pi, OpenPartialHomeomorph.toFun', Pi.map, Real.exp, NumberField.mixedEmbedding.fundamentalCone.expMap, PartialEquiv.pi, NumberField.mixedEmbedding.fundamentalCone.expMapBasis, Finset.sum, rfl, Equiv.transPartialEquiv
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
rw :
  (HSMul.hSMul (β := (w : InfinitePlace K) → ℝ) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
      ∏ i : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          ((w : (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))
                          i)) :
                    𝓞 K) :
                K) :
            ℝ)
          (x (↑i : InfinitePlace K))) =
    HSMul.hSMul (β := realSpace K) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
      ∏ i : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          ((w : (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))
                          i)) :
                    𝓞 K) :
                K) :
            ℝ)
          (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
⊢ (↑expMapBasis : realSpace K → realSpace K) x =
    HSMul.hSMul (β := realSpace K) (Real.exp (x w₀))
      ((↑expMapBasis : realSpace K → realSpace K) fun (i : InfinitePlace K) ↦ if i = w₀ then 0 else x i)

Tactic:
rw [expMapBasis_apply', expMapBasis_apply', if_pos rfl, smul_smul, ← Real.exp_add, add_zero]

Premises used: NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', smul_smul, if_pos, add_zero, Real.exp_add, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
h :
  ∀ (w : InfinitePlace K) (i : { w : InfinitePlace K // w ≠ w₀ }),
    HPow.hPow (α := ℝ)
      ((w : (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))
                      i)) :
                𝓞 K) :
            K) :
        ℝ)
      (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
| HSMul.hSMul (β := realSpace K) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
    ∏ i : { w : InfinitePlace K // w ≠ w₀ },
      HPow.hPow (α := ℝ)
        ((w : (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))
                        i)) :
                  𝓞 K) :
              K) :
          ℝ)
        (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))

Tactic:
enter [2, w, 2, i]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
w : InfinitePlace K
i : { w : InfinitePlace K // w ≠ w₀ }
h :
  HPow.hPow (α := ℝ)
    ((w : (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))
                    i)) :
              𝓞 K) :
          K) :
      ℝ)
    (x (↑i : InfinitePlace K))
| HPow.hPow (α := ℝ)
    ((w : (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))
                    i)) :
              𝓞 K) :
          K) :
      ℝ)
    (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))

Tactic:
rw [if_neg i.prop]

Premises used: Subtype.prop, if_neg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
h :
  ∀ (w : InfinitePlace K) (i : { w : InfinitePlace K // w ≠ w₀ }),
    HPow.hPow (α := ℝ)
      ((w : (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))
                      i)) :
                𝓞 K) :
            K) :
        ℝ)
      (x (↑i : InfinitePlace K))
| HSMul.hSMul (β := realSpace K) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
    ∏ i : { w : InfinitePlace K // w ≠ w₀ },
      HPow.hPow (α := ℝ)
        ((w : (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))
                        i)) :
                  𝓞 K) :
              K) :
          ℝ)
        (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))

Tactic:
enter [2, w, 2, i]
    rw [if_neg i.prop]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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 : InfinitePlace K,
        ∏ x_2 : { w : InfinitePlace K // w ≠ w₀ },
          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))
                              x_2)) :
                        𝓞 K) :
                    K) :
                ℝ)
              (x (↑x_2 : InfinitePlace K)) ^
            x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K
⊢ ∏ w : InfinitePlace K, (↑expMapBasis : realSpace K → realSpace K) x w ^ w.mult = Real.exp (x w₀) ^ finrank ℚ K

Tactic:
simp_rw [expMapBasis_apply', Pi.smul_def, smul_eq_mul, mul_pow, prod_mul_distrib,
    prod_pow_eq_pow_sum, sum_mult_eq, ← prod_pow]

Premises used: NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', NumberField.InfinitePlace.sum_mult_eq, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum, smul_eq_mul, Pi.smul_def, Finset.prod_pow, mul_pow
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
rw :
  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
⊢ Real.exp (x w₀) ^ finrank ℚ K *
      ∏ x_1 : InfinitePlace K,
        ∏ x_2 : { w : InfinitePlace K // w ≠ w₀ },
          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))
                              x_2)) :
                        𝓞 K) :
                    K) :
                ℝ)
              (x (↑x_2 : InfinitePlace K)) ^
            x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K

Tactic:
rw [prod_comm]

Premises used: Finset.prod_comm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
⊢ (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMapBasis : realSpace K → realSpace K) x) :
        mixedSpace K) =
    Real.exp (x w₀) ^ finrank ℚ K

Tactic:
simpa only [mixedEmbedding.norm_apply,
    normAtPlace_mixedSpaceOfRealSpace (expMapBasis_pos _ _).le] using prod_expMapBasis_pow x

Premises used: LT.lt.le, NumberField.mixedEmbedding.fundamentalCone.prod_expMapBasis_pow, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_pos, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace, NumberField.mixedEmbedding.norm_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
⊢ Ne (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMapBasis : realSpace K → realSpace K) x) :
          mixedSpace K) :
      ℝ)
    (0 : ℝ)

Tactic:
norm_expMapBasis x ▸ pow_ne_zero _ (Real.exp_ne_zero _)

Premises used: pow_ne_zero, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, Eq.rec, Eq.symm, Real.exp_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
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)
⊢ 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)

Tactic:
simp_rw [ZSpan.mem_fundamentalDomain, equivFinRank.forall_congr_left, Subtype.forall]

Premises used: Equiv.forall_congr_left, NumberField.mixedEmbedding.fundamentalCone.equivFinRank, Subtype.forall, ZSpan.mem_fundamentalDomain
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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)

Tactic:
forall₂_congr fun w hw ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
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)
⊢ (∀ (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:
refine forall₂_congr fun w hw ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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
rw₄ rw₅ : Eq (α := ℝ) 1 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 : ℝ)

Tactic:
rw [← expMapBasis_apply,
    norm_expMapBasis, if_pos rfl, Real.exp_zero, one_pow]

Premises used: one_pow, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, if_pos, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply, Real.exp_zero, rfl