awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
h : 0 ≤ r
x : K
⊢ Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
      ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
have rw : Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ↔
  norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r
Tactic: rw [← norm_le_iff, mem_closedBall_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
h : 0 ≤ r
x : K
rw :
  Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
      ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ↔
    norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r
⊢ Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
      ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
have rw₁ : norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
  norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r
Tactic: rw [← norm_le_iff, mem_closedBall_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
h : 0 ≤ r
⊢ ((↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r).Finite
have heq : ∀ (x : K),
  Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
      ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
Tactic: have heq : ∀ x, canonicalEmbedding K x ∈ Metric.closedBall 0 r ↔
        ∀ φ : K →+* ℂ, ‖φ x‖ ≤ r := by
      intro x; rw [← norm_le_iff, mem_closedBall_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
h : 0 ≤ r
heq :
  ∀ (x : K),
    Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ↔
      ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
⊢ ((↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r).Finite
have h : (↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r =
  Set.image (α := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r}
Tactic: convert! (Embeddings.finite_of_norm_le K ℂ r).image (canonicalEmbedding K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
h : 0 ≤ r
heq :
  ∀ (x : K),
    Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ↔
      ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
⊢ (↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r =
    Set.image (α := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)
      {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r}
have h : ∀ (x : (K →+* ℂ) → ℂ),
  x ∈ (↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r ↔
    Membership.mem (γ := Set ((K →+* ℂ) → ℂ))
      (Set.image (α := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)
        {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r})
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
h : 0 ≤ r
heq :
  ∀ (x : K),
    Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ↔
      ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
x : (K →+* ℂ) → ℂ
⊢ x ∈ (↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r ↔
    Membership.mem (γ := Set ((K →+* ℂ) → ℂ))
      (Set.image (α := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)
        {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r})
      x
have h : x ∈ (↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r →
  Membership.mem (γ := Set ((K →+* ℂ) → ℂ))
    (Set.image (α := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)
      {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r})
    x
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
h_1 : 0 ≤ r
heq :
  ∀ (x : K),
    Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ↔
      ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
x : (K →+* ℂ) → ℂ
h :
  x ∈ (↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r →
    Membership.mem (γ := Set ((K →+* ℂ) → ℂ))
      (Set.image (α := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)
        {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r})
      x
⊢ x ∈ (↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r ↔
    Membership.mem (γ := Set ((K →+* ℂ) → ℂ))
      (Set.image (α := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)
        {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r})
      x
have h₁ : Membership.mem (γ := Set ((K →+* ℂ) → ℂ))
    (Set.image (α := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)
      {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r})
    x →
  x ∈ (↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
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)
this : M.det ≠ 0
⊢ Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)
have this₁ : (LinearIndependent ℂ (M := (K →+* ℂ) → ℂ) 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)) ∧
  Eq.{u_1 + 1} (α := Submodule ℂ ((K →+* ℂ) → ℂ))
    (Submodule.span ℂ
      (Set.range 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)))
    ⊤
Tactic: rw [← isUnit_iff_ne_zero, ← Basis.det_apply, ← Basis.is_basis_iff_det] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
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)
⊢ Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)
have suffices : M.det ≠ 0
Tactic: 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
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)
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
⊢ M = N.transpose
have a : ∀ (i j : K →+* ℂ), M i j = N.transpose i j
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
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)
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
⊢ M = N.transpose
have a : ∀ (i j : K →+* ℂ), M i j = N.transpose i j
Tactic: { ext : 2; rfl }
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
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)
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
⊢ M.det ≠ 0
have rw : N.transpose.det ≠ 0
Tactic: rw [show M = N.transpose by { ext : 2; rfl }]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
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)
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
have rw : HPow.hPow (β := ℕ) N.det 2 ≠ 0
Tactic: rw [Matrix.det_transpose, ← pow_ne_zero_iff two_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
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)
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
have h : 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))
Tactic: convert!
      (map_ne_zero_iff _ (algebraMap ℚ ℂ).injective).mpr
        (Algebra.discr_not_zero_of_basis ℚ (integralBasis K))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
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)
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))
have h : 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))))
Tactic: rw [← Algebra.discr_reindex ℚ (integralBasis K) e.symm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
Let Let₁ Let₂ Let₃ Let₄ : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)
⊢ Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)
have Let₅ : let B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ);
let e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq sorry;
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
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)
have Let₇ : let e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq sorry;
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
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
-- 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 →+* ℂ) → ℂ
⊢ Eq (α := Set ((K →+* ℂ) → ℂ))
    (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
      (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))
    (Set.image (α := K) (⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) : (a : K) → (K →+* ℂ) → ℂ)
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
have rw : Eq (α := Set ((K →+* ℂ) → ℂ))
  (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
    (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
      (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))
  (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
    (Function.comp (β := K)
      (⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) : (a : K) → (K →+* ℂ) → ℂ)
      (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
Tactic: rw [← Set.range_comp]
-- 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 →+* ℂ) → ℂ
⊢ Membership.mem (γ := Submodule ℤ ((K →+* ℂ) → ℂ))
      (Submodule.span ℤ
        (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
          (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
      x ↔
    Membership.mem (γ := Subring ((K →+* ℂ) → ℂ))
      (RingHom.range (R := 𝓞 K) (RingHom.comp (canonicalEmbedding K) (algebraMap (𝓞 K) K))) x
have rw : Membership.mem (γ := Submodule ℤ ((K →+* ℂ) → ℂ))
    (Submodule.span ℤ
      (Set.image (α := K) (⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) : (a : K) → (K →+* ℂ) → ℂ)
        (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))))
    x ↔
  Membership.mem (γ := Subring ((K →+* ℂ) → ℂ))
    (RingHom.range (R := 𝓞 K) (RingHom.comp (canonicalEmbedding K) (algebraMap (𝓞 K) K))) x
Tactic: 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))]