-- 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 : 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 (α :=
    ↥(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 →+* ℂ) → ℂ))))
have a : Eq.{u_1 + 1} (α := (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)) :
    (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) :
    (K →+* ℂ) → ℂ)
Tactic: apply Subtype.val_injective