-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i_1 : Free.ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ]
  ↥(Submodule.span ℚ
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))) :=
  LinearMap.codRestrict
    (Submodule.span ℚ
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
    (AlgHom.toLinearMap (RingHom.toRatAlgHom (canonicalEmbedding K))) ⋯
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ Eq (α := Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    ((((↑(Basis.repr (Basis.restrictScalars ℚ (latticeBasis K))) :
                ↥(Submodule.span ℚ
                      (Set.range (⇑(latticeBasis K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))) →ₗ[ℚ]
                  Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) ∘ₗ
              f :
            K →ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : K) → Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
        (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) i :
          K) :
      Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    ((((↑(Basis.repr (integralBasis K)) : K →ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
            K →ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : K) → Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
        (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) i :
          K) :
      Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
have this : Eq (α :=
  ↥(Submodule.span ℚ
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))))
  ((f :
        (a : K) →
          ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))))
      (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) i) :
    ↥(Submodule.span ℚ
        (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
          (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))))
  (((Basis.restrictScalars ℚ (latticeBasis K) :
          Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ
            ↥(Submodule.span ℚ
                (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
                  (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
                    (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) →
          ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))))
      i :
    ↥(Submodule.span ℚ
        (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
          (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))))
Tactic: have : f (integralBasis K i) = ((latticeBasis K).restrictScalars ℚ) i := by
    apply Subtype.val_injective
    rw [LinearMap.codRestrict_apply, AlgHom.toLinearMap_apply, Basis.restrictScalars_apply,
      latticeBasis_apply]
    rfl