-- 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 :
  (∀ (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)
simp_rw₁ :
  (∀ (b : { w : InfinitePlace K // 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))
                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)
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: 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']