[GOAL]
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ↑(canonicalEmbedding K))
⊢ ↑(starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
[PROOFSTEP]
refine Submodule.span_induction hx ?_ ?_ (fun _ _ hx hy => ?_) (fun a _ hx => ?_)
[GOAL]
case refine_1
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ↑(canonicalEmbedding K))
⊢ ∀ (x : (K →+* ℂ) → ℂ),
    x ∈ Set.range ↑(canonicalEmbedding K) → ↑(starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case refine_1.intro
K : Type u_1
inst✝ : Field K
x✝ : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x✝ ∈ Submodule.span ℝ (Set.range ↑(canonicalEmbedding K))
x : K
⊢ ↑(starRingEnd ℂ) (↑(canonicalEmbedding K) x φ) = ↑(canonicalEmbedding K) x (ComplexEmbedding.conjugate φ)
[PROOFSTEP]
rw [apply_at, apply_at, ComplexEmbedding.conjugate_coe_eq]
[GOAL]
case refine_2
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ↑(canonicalEmbedding K))
⊢ ↑(starRingEnd ℂ) (OfNat.ofNat 0 φ) = OfNat.ofNat 0 (ComplexEmbedding.conjugate φ)
[PROOFSTEP]
rw [Pi.zero_apply, Pi.zero_apply, map_zero]
[GOAL]
case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ↑(canonicalEmbedding K))
x✝¹ x✝ : (K →+* ℂ) → ℂ
hx : ↑(starRingEnd ℂ) (x✝¹ φ) = x✝¹ (ComplexEmbedding.conjugate φ)
hy : ↑(starRingEnd ℂ) (x✝ φ) = x✝ (ComplexEmbedding.conjugate φ)
⊢ ↑(starRingEnd ℂ) ((x✝¹ + x✝) φ) = (x✝¹ + x✝) (ComplexEmbedding.conjugate φ)
[PROOFSTEP]
rw [Pi.add_apply, Pi.add_apply, map_add, hx, hy]
[GOAL]
case refine_4
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ↑(canonicalEmbedding K))
a : ℝ
x✝ : (K →+* ℂ) → ℂ
hx : ↑(starRingEnd ℂ) (x✝ φ) = x✝ (ComplexEmbedding.conjugate φ)
⊢ ↑(starRingEnd ℂ) ((a • x✝) φ) = (a • x✝) (ComplexEmbedding.conjugate φ)
[PROOFSTEP]
rw [Pi.smul_apply, Complex.real_smul, map_mul, Complex.conj_ofReal]
[GOAL]
case refine_4
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ↑(canonicalEmbedding K))
a : ℝ
x✝ : (K →+* ℂ) → ℂ
hx : ↑(starRingEnd ℂ) (x✝ φ) = x✝ (ComplexEmbedding.conjugate φ)
⊢ ↑a * ↑(starRingEnd ℂ) (x✝ φ) = (a • x✝) (ComplexEmbedding.conjugate φ)
[PROOFSTEP]
exact congrArg ((a : ℂ) * ·) hx
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ‖↑(canonicalEmbedding K) x‖₊ = Finset.sup Finset.univ fun φ => ‖↑φ x‖₊
[PROOFSTEP]
simp_rw [Pi.nnnorm_def, apply_at]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
⊢ ‖↑(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
obtain hr | hr := lt_or_le r 0
[GOAL]
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
⊢ ‖↑(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
obtain ⟨φ⟩ := (inferInstance : Nonempty (K →+* ℂ))
[GOAL]
case inl.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ‖↑(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
refine iff_of_false ?_ ?_
[GOAL]
case inl.intro.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬‖↑(canonicalEmbedding K) x‖ ≤ r
case inl.intro.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
exact (hr.trans_le (norm_nonneg _)).not_le
[GOAL]
case inl.intro.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
exact fun h => hr.not_le (le_trans (norm_nonneg _) (h φ))
[GOAL]
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : 0 ≤ r
⊢ ‖↑(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
lift r to NNReal using hr
[GOAL]
case inr.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : NNReal
⊢ ‖↑(canonicalEmbedding K) x‖ ≤ ↑r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ ↑r
[PROOFSTEP]
simp_rw [← coe_nnnorm, nnnorm_eq, NNReal.coe_le_coe, Finset.sup_le_iff, Finset.mem_univ, forall_true_left]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
⊢ Set.Finite (↑(integerLattice K) ∩ Metric.closedBall 0 r)
[PROOFSTEP]
obtain hr | _ := lt_or_le r 0
[GOAL]
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : r < 0
⊢ Set.Finite (↑(integerLattice K) ∩ Metric.closedBall 0 r)
[PROOFSTEP]
simp [Metric.closedBall_eq_empty.2 hr]
[GOAL]
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
⊢ Set.Finite (↑(integerLattice K) ∩ Metric.closedBall 0 r)
[PROOFSTEP]
have heq : ∀ x, canonicalEmbedding K x ∈ Metric.closedBall 0 r ↔ ∀ φ : K →+* ℂ, ‖φ x‖ ≤ r := by intro x;
  rw [← norm_le_iff, mem_closedBall_zero_iff]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
⊢ ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
intro x
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
x : K
⊢ ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
rw [← norm_le_iff, mem_closedBall_zero_iff]
[GOAL]
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
⊢ Set.Finite (↑(integerLattice K) ∩ Metric.closedBall 0 r)
[PROOFSTEP]
convert (Embeddings.finite_of_norm_le K ℂ r).image (canonicalEmbedding K)
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
⊢ ↑(integerLattice K) ∩ Metric.closedBall 0 r =
    ↑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r}
[PROOFSTEP]
ext
[GOAL]
case h.e'_2.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
x✝ : (K →+* ℂ) → ℂ
⊢ x✝ ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r ↔
    x✝ ∈ ↑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r}
[PROOFSTEP]
constructor
[GOAL]
case h.e'_2.h.mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
x✝ : (K →+* ℂ) → ℂ
⊢ x✝ ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r →
    x✝ ∈ ↑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r}
[PROOFSTEP]
rintro ⟨⟨_, ⟨x, rfl⟩, rfl⟩, hx⟩
[GOAL]
case h.e'_2.h.mp.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
x : { x // x ∈ 𝓞 K }
hx : ↑(canonicalEmbedding K) (↑(algebraMap { x // x ∈ 𝓞 K } K) x) ∈ Metric.closedBall 0 r
⊢ ↑(canonicalEmbedding K) (↑(algebraMap { x // x ∈ 𝓞 K } K) x) ∈
    ↑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r}
[PROOFSTEP]
exact ⟨↑x, ⟨SetLike.coe_mem x, fun φ => (heq x).mp hx φ⟩, rfl⟩
[GOAL]
case h.e'_2.h.mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
x✝ : (K →+* ℂ) → ℂ
⊢ x✝ ∈ ↑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r} →
    x✝ ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r
[PROOFSTEP]
rintro ⟨x, ⟨hx1, hx2⟩, rfl⟩
[GOAL]
case h.e'_2.h.mpr.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
x : K
hx1 : IsIntegral ℤ x
hx2 : ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
⊢ ↑(canonicalEmbedding K) x ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r
[PROOFSTEP]
exact ⟨⟨x, ⟨⟨x, hx1⟩, rfl⟩, rfl⟩, (heq x).mpr hx2⟩
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Basis (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
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) :=
  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, ← is_basis_iff_det] at this 
  refine basisOfLinearIndependentOfCardEqFinrank ((linearIndependent_equiv e.symm).mpr this.1) ?_
  rw [← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, finrank_fintype_fun_eq_card, Embeddings.card]
    -- 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 ℂ _ _ _ 2 (by norm_num)]
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
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Basis (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
let B := Pi.basisFun ℂ (K →+* ℂ)
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
⊢ Basis (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
let e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) :=
  equivOfCardEq ((Embeddings.card K ℂ).trans (finrank_eq_card_basis (integralBasis K)))
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
⊢ Basis (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
let M := B.toMatrix (fun i => canonicalEmbedding K (integralBasis K (e i)))
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
⊢ Basis (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
suffices M.det ≠ 0 by
  rw [← isUnit_iff_ne_zero, ← Basis.det_apply, ← is_basis_iff_det] at this 
  refine basisOfLinearIndependentOfCardEqFinrank ((linearIndependent_equiv e.symm).mpr this.1) ?_
  rw [← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, finrank_fintype_fun_eq_card, Embeddings.card]
    -- 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
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
this : Matrix.det M ≠ 0
⊢ Basis (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
rw [← isUnit_iff_ne_zero, ← Basis.det_apply, ← is_basis_iff_det] at this 
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
this :
  (LinearIndependent ℂ fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))) ∧
    Submodule.span ℂ (Set.range fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))) = ⊤
⊢ Basis (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
refine basisOfLinearIndependentOfCardEqFinrank ((linearIndependent_equiv e.symm).mpr this.1) ?_
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
this :
  (LinearIndependent ℂ fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))) ∧
    Submodule.span ℂ (Set.range fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))) = ⊤
⊢ card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) = finrank ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
rw [← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, finrank_fintype_fun_eq_card, Embeddings.card]
  -- 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
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
⊢ Matrix.det M ≠ 0
[PROOFSTEP]
let N := Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => integralBasis K (e i)) RingHom.equivRatAlgHom
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ Matrix.det M ≠ 0
[PROOFSTEP]
rw [show M = N.transpose by {ext : 2; rfl
  }]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ M = Matrix.transpose N
[PROOFSTEP]
{ext : 2; rfl
}
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ M = Matrix.transpose N
[PROOFSTEP]
ext : 2
[GOAL]
case a.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
i✝ x✝ : K →+* ℂ
⊢ M i✝ x✝ = Matrix.transpose N i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ Matrix.det (Matrix.transpose N) ≠ 0
[PROOFSTEP]
rw [Matrix.det_transpose, ← @pow_ne_zero_iff ℂ _ _ _ 2 (by norm_num)]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ Matrix.det N ^ 2 ≠ 0
[PROOFSTEP]
convert (map_ne_zero_iff _ (algebraMap ℚ ℂ).injective).mpr (Algebra.discr_not_zero_of_basis ℚ (integralBasis K))
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ Matrix.det N ^ 2 = ↑(algebraMap ℚ ℂ) (Algebra.discr ℚ ↑(integralBasis K))
[PROOFSTEP]
rw [← Algebra.discr_reindex ℚ (integralBasis K) e.symm]
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ Matrix.det N ^ 2 = ↑(algebraMap ℚ ℂ) (Algebra.discr ℚ (↑(integralBasis K) ∘ ↑e.symm.symm))
[PROOFSTEP]
exact
  (Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two ℚ ℂ (fun i => integralBasis K (e i))
      RingHom.equivRatAlgHom).symm
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }
⊢ ↑(latticeBasis K) i = ↑(canonicalEmbedding K) (↑(integralBasis K) i)
[PROOFSTEP]
simp only [latticeBasis, integralBasis_apply, coe_basisOfLinearIndependentOfCardEqFinrank, Function.comp_apply,
  Equiv.apply_symm_apply]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈ Submodule.span ℤ (Set.range ↑(latticeBasis K)) ↔ x ∈ ↑(canonicalEmbedding K) '' ↑(𝓞 K)
[PROOFSTEP]
rw [show Set.range (latticeBasis K) = (canonicalEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (integralBasis K)) by
    rw [← Set.range_comp]; exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ Set.range ↑(latticeBasis K) =
    ↑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) '' Set.range ↑(integralBasis K)
[PROOFSTEP]
rw [← Set.range_comp]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ Set.range ↑(latticeBasis K) =
    Set.range (↑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) ∘ ↑(integralBasis K))
[PROOFSTEP]
exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈
      Submodule.span ℤ
        (↑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) '' Set.range ↑(integralBasis K)) ↔
    x ∈ ↑(canonicalEmbedding K) '' ↑(𝓞 K)
[PROOFSTEP]
rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈
      ↑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) ''
        ↑(Submodule.span ℤ (Set.range ↑(integralBasis K))) ↔
    x ∈ ↑(canonicalEmbedding K) '' ↑(𝓞 K)
[PROOFSTEP]
rw [show (Submodule.span ℤ (Set.range (integralBasis K)) : Set K) = 𝓞 K by ext; exact mem_span_integralBasis K]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ ↑(Submodule.span ℤ (Set.range ↑(integralBasis K))) = ↑(𝓞 K)
[PROOFSTEP]
ext
[GOAL]
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
x✝ : K
⊢ x✝ ∈ ↑(Submodule.span ℤ (Set.range ↑(integralBasis K))) ↔ x✝ ∈ ↑(𝓞 K)
[PROOFSTEP]
exact mem_span_integralBasis K
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈ ↑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) '' ↑(𝓞 K) ↔
    x ∈ ↑(canonicalEmbedding K) '' ↑(𝓞 K)
[PROOFSTEP]
rfl
