-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i : 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))) ⋯
suffices :
  Eq (α := K →ₗ[ℚ] 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) →₀ ℚ)
    ((↑(Basis.repr (integralBasis K)) : K →ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
      K →ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
⊢ Eq (α := ℚ)
    (((((Basis.repr (Basis.restrictScalars ℚ (latticeBasis K)) :
                  ↥(Submodule.span ℚ
                        (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
                          (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
                            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))) ≃ₗ[ℚ]
                    Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                (a :
                    ↥(Submodule.span ℚ
                        (Set.range (⇑(latticeBasis K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))) →
                  Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
              (Subtype.mk (p := fun (x : (K →+* ℂ) → ℂ) ↦
                  Membership.mem (γ := Submodule ℚ ((K →+* ℂ) → ℂ))
                    (Submodule.span ℚ
                      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
                        (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
                          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
                    x)
                  ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x) ⋯ :
                ↥(Submodule.span ℚ
                    (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
                      (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
                        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))) :
            Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
        i :
      ℚ)
    (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                (a : K) → Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
              x :
            Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
        i :
      ℚ)

Tactic:
suffices ((latticeBasis K).restrictScalars ℚ).repr.toLinearMap ∘ₗ f =
    (integralBasis K).repr.toLinearMap from DFunLike.congr_fun (LinearMap.congr_fun this x) i