-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)
this :
  Eq (α := ℝ)
    (((Basis.det (latticeBasis K) : mixedSpace K [⋀^ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℝ] ℝ) :
          (a : ChooseBasisIndex ℤ (𝓞 K) → mixedSpace K) → ℝ)
        (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
          (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (⇑(basisOfFractionalIdeal K I :
                  Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
              (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
            (⇑e :
              (a : ChooseBasisIndex ℤ (𝓞 K)) →
                ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))) :
      ℝ)
    ((algebraMap ℚ ℝ : (a : ℚ) → ℝ)
        (((Basis.det.{0, u_1, u_1} (R := ℚ) (M := K) (ι := ChooseBasisIndex ℤ (𝓞 K)) (integralBasis K) :
                K [⋀^ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℚ] ℚ) :
              (a : ChooseBasisIndex ℤ (𝓞 K) → K) → ℚ)
            (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
              (⇑(basisOfFractionalIdeal K I :
                    Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
                (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
              (⇑e :
                (a : ChooseBasisIndex ℤ (𝓞 K)) →
                  ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))) :
          ℚ) :
      ℝ)
rw :
  Eq (α := ℝ)
    (|(algebraMap ℚ ℝ : (a : ℚ) → ℝ)
          (((Basis.det.{0, u_1, u_1} (R := ℚ) (M := K) (ι := ChooseBasisIndex ℤ (𝓞 K)) (integralBasis K) :
                  K [⋀^ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℚ] ℚ) :
                (a : ChooseBasisIndex ℤ (𝓞 K) → K) → ℚ)
              (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
                (⇑(basisOfFractionalIdeal K I :
                      Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
                  (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
                (⇑e :
                  (a : ChooseBasisIndex ℤ (𝓞 K)) →
                    ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))) :
            ℚ)| :
      ℝ)
    ((↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) : ℝ)
rw₁ :
  Eq (α := ℝ)
    |(↑(((Basis.det.{0, u_1, u_1} (R := ℚ) (M := K) (ι := ChooseBasisIndex ℤ (𝓞 K)) (integralBasis K) :
                K [⋀^ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℚ] ℚ) :
              (a : ChooseBasisIndex ℤ (𝓞 K) → K) → ℚ)
            (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
              (⇑(basisOfFractionalIdeal K I :
                    Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
                (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
              (⇑e :
                (a : ChooseBasisIndex ℤ (𝓞 K)) →
                  ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))) :
        ℝ)|
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ)
rw₂ :
  Eq (α := ℝ)
    (↑|((Basis.det.{0, u_1, u_1} (R := ℚ) (M := K) (ι := ChooseBasisIndex ℤ (𝓞 K)) (integralBasis K) :
                K [⋀^ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℚ] ℚ) :
              (a : ChooseBasisIndex ℤ (𝓞 K) → K) → ℚ)
            (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
              (⇑(basisOfFractionalIdeal K I :
                    Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
                (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
              (⇑e :
                (a : ChooseBasisIndex ℤ (𝓞 K)) →
                  ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))| :
      ℝ)
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ)
rw₃ :
  Eq (α := ℝ)
    (↑|((Basis.det.{0, u_1, u_1} (R := ℚ) (M := K) (ι := ChooseBasisIndex ℤ (𝓞 K)) (integralBasis K) :
                K [⋀^ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℚ] ℚ) :
              (a : ChooseBasisIndex ℤ (𝓞 K) → K) → ℚ)
            (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
              (⇑(basisOfFractionalIdeal K I :
                    Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
                (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
              (⇑e.symm.symm :
                (a : ChooseBasisIndex ℤ (𝓞 K)) →
                  ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))| :
      ℝ)
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ)
⊢ Eq (α := ℝ)
    (|((Basis.det (latticeBasis K) : mixedSpace K [⋀^ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℝ] ℝ) :
            (a : ChooseBasisIndex ℤ (𝓞 K) → mixedSpace K) → ℝ)
          (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
            (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
              (⇑(basisOfFractionalIdeal K I :
                    Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
                (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
              (⇑e :
                (a : ChooseBasisIndex ℤ (𝓞 K)) →
                  ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))))| :
      ℝ)
    ((↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) : ℝ)
have rw₄ : Eq (α := ℝ)
  (↑|((Basis.det.{0, u_1, u_1} (R := ℚ) (M := K) (ι := ChooseBasisIndex ℤ (𝓞 K)) (integralBasis K) :
              K [⋀^ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℚ] ℚ) :
            (a : ChooseBasisIndex ℤ (𝓞 K) → K) → ℚ)
          (⇑(Basis.reindex (basisOfFractionalIdeal K I) e.symm : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
            (a : ChooseBasisIndex ℤ (𝓞 K)) → K)| :
    ℝ)
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ)
Tactic: rw [this, eq_ratCast, ← Rat.cast_abs, ← Equiv.symm_symm e, ← Basis.coe_reindex,
      det_basisOfFractionalIdeal_eq_absNorm K I e]