-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
Let Let₁ Let₂ Let₃ Let₄ : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)
Let₅ :
  let B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ);
  let e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯;
  let M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
    B.toMatrix fun (i : K →+* ℂ) ↦
      (canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ)
        (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
            ((e : (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)) i : Free.ChooseBasisIndex ℤ (𝓞 K)) :
          K);
  M.det ≠ 0
Let₆ :
  let B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ);
  let e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯;
  let M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
    B.toMatrix fun (i : K →+* ℂ) ↦
      (canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ)
        (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
            ((e : (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)) i : Free.ChooseBasisIndex ℤ (𝓞 K)) :
          K);
  M.det ≠ 0
Let₇ :
  let e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯;
  let N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
    Algebra.embeddingsMatrixReindex ℚ ℂ
      (fun (i : K →+* ℂ) ↦
        ((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
          ((e : (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)) i : Free.ChooseBasisIndex ℤ (𝓞 K)))
      RingHom.equivRatAlgHom;
  N.transpose.det ≠ 0
Let₈ :
  let e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯;
  let N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
    Algebra.embeddingsMatrixReindex ℚ ℂ
      (fun (i : K →+* ℂ) ↦
        ((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
          ((e : (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)) i : Free.ChooseBasisIndex ℤ (𝓞 K)))
      RingHom.equivRatAlgHom;
  HPow.hPow (β := ℕ) N.det 2 ≠ 0
h :
  let e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯;
  let N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
    Algebra.embeddingsMatrixReindex ℚ ℂ
      (fun (i : K →+* ℂ) ↦
        ((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
          ((e : (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)) i : Free.ChooseBasisIndex ℤ (𝓞 K)))
      RingHom.equivRatAlgHom;
  HPow.hPow (β := ℕ) N.det 2 =
    (algebraMap ℚ ℂ : (a : ℚ) → ℂ)
      (Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
        (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))
h₁ :
  let e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯;
  let N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
    Algebra.embeddingsMatrixReindex ℚ ℂ
      (fun (i : K →+* ℂ) ↦
        ((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
          ((e : (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)) i : Free.ChooseBasisIndex ℤ (𝓞 K)))
      RingHom.equivRatAlgHom;
  HPow.hPow (β := ℕ) N.det 2 =
    (algebraMap ℚ ℂ : (a : ℚ) → ℂ)
      (Algebra.discr (ι := K →+* ℂ) ℚ (B := K)
        (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
          (⇑e.symm.symm : (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K))))
⊢ Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)

Tactic:
classical
  -- Let `B` be the canonical basis of `(K →+* ℂ) → ℂ`. We prove that the determinant of
  -- the image by `canonicalEmbedding` of the integral basis of `K` is nonzero. This
  -- will imply the result.
    let B := Pi.basisFun ℂ (K →+* ℂ)
    let e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) :=
      Fintype.equivOfCardEq ((Embeddings.card K ℂ).trans (finrank_eq_card_basis (integralBasis K)))
    let M := B.toMatrix (fun i => canonicalEmbedding K (integralBasis K (e i)))
    suffices M.det ≠ 0 by
      rw [← isUnit_iff_ne_zero, ← Basis.det_apply, ← Basis.is_basis_iff_det] at this
      exact (basisOfPiSpaceOfLinearIndependent this.1).reindex e
  -- In order to prove that the determinant is nonzero, we show that it is equal to the
  -- square of the discriminant of the integral basis and thus it is not zero
    let N := Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => integralBasis K (e i))
      RingHom.equivRatAlgHom
    rw [show M = N.transpose by { ext : 2; rfl }]
    rw [Matrix.det_transpose, ← pow_ne_zero_iff two_ne_zero]
    convert!
      (map_ne_zero_iff _ (algebraMap ℚ ℂ).injective).mpr
        (Algebra.discr_not_zero_of_basis ℚ (integralBasis K))
    rw [← Algebra.discr_reindex ℚ (integralBasis K) e.symm]
    exact (Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two ℚ ℂ
      (fun i => integralBasis K (e i)) RingHom.equivRatAlgHom).symm

Premises used: Iff.mpr, NumberField.integralBasis, Matrix.det_transpose, Algebra.algebraMap, Rat, RingHom.injective, two_ne_zero, Algebra.discr_not_zero_of_basis, map_ne_zero_iff, Complex, pow_ne_zero_iff