-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i_1 : ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ]
  ↥(Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) :=
  LinearMap.codRestrict
    (Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
    (AlgHom.toLinearMap (RingHom.toRatAlgHom (mixedEmbedding K))) ⋯
i : ChooseBasisIndex ℤ (𝓞 K)
this :
  Eq (α :=
    ↥(Submodule.span ℚ
        (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
          (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
    ((f : (a : K) → ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i) :
      ↥(Submodule.span ℚ
          (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
            (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
              (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
    (((Basis.restrictScalars ℚ (latticeBasis K) :
            Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ
              ↥(Submodule.span ℚ
                  (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                    (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                      (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) →
            ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
        i :
      ↥(Submodule.span ℚ
          (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
            (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
              (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
simp_rw :
  Eq (α := ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    (Function.comp (α := K) (β :=
        ↥(Submodule.span ℚ
            (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
              (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
        (⇑((↑(Basis.repr (Basis.restrictScalars ℚ (latticeBasis K))) :
                ↥(Submodule.span ℚ
                      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) →ₗ[ℚ]
                  ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
              ↥(Submodule.span ℚ
                    (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                      (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                        (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) →ₗ[ℚ]
                ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) →
            ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
        ((⇑f :
            (a : K) →
              ↥(Submodule.span ℚ
                  (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                    (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                      (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) :
          (a : K) →
            ↥(Submodule.span ℚ
                (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                  (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                    (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i : K) :
      ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    ((((↑(Basis.repr (integralBasis K)) : K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
            K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i : K) :
      ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
simp_rw₁ :
  Eq (α := ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    (Function.comp (α := K) (β :=
        ↥(Submodule.span ℚ
            (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
              (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
        (⇑(Basis.repr (Basis.restrictScalars ℚ (latticeBasis K)) :
              ↥(Submodule.span ℚ
                    (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                      (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                        (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) ≃ₗ[ℚ]
                ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) →
            ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
        ((⇑f :
            (a : K) →
              ↥(Submodule.span ℚ
                  (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                    (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                      (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) :
          (a : K) →
            ↥(Submodule.span ℚ
                (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                  (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                    (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i : K) :
      ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    (((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) : (a : K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i : K) :
      ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
simp_rw₂ :
  Eq (α := ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    (((Basis.repr (Basis.restrictScalars ℚ (latticeBasis K)) :
            ↥(Submodule.span ℚ
                  (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                    (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                      (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) ≃ₗ[ℚ]
              ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) →
            ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
        ((f :
              (a : K) →
                ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
            (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i) :
          ↥(Submodule.span ℚ
              (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                  (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) :
      ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    (((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) : (a : K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i : K) :
      ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
⊢ Eq (α := ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    ((((↑(Basis.repr (Basis.restrictScalars ℚ (latticeBasis K))) :
                ↥(Submodule.span ℚ
                      (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) →ₗ[ℚ]
                  ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) ∘ₗ
              f :
            K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i : K) :
      ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    ((((↑(Basis.repr (integralBasis K)) : K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
            K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i : K) :
      ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
have simp_rw₃ : Eq (α := ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
  (((Basis.repr (Basis.restrictScalars ℚ (latticeBasis K)) :
          ↥(Submodule.span ℚ
                (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                  (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                    (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) ≃ₗ[ℚ]
            ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
        (a : ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) →
          ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
      (((Basis.restrictScalars ℚ (latticeBasis K) :
              Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ
                ↥(Submodule.span ℚ
                    (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                      (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                        (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) :
            (a : ChooseBasisIndex ℤ (𝓞 K)) →
              ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
          i :
        ↥(Submodule.span ℚ
            (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
              (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) :
    ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
  (((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) : (a : K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
      (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i : K) :
    ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
Tactic: simp_rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, this, Basis.repr_self]