awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
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
⊢ 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
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
hx :
  Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) : (K →+* ℂ) → ℂ)
⊢ Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ))
    (Set.image (α := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)
      {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r})
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) : (K →+* ℂ) → ℂ)

Tactic:
⟨x, ⟨SetLike.coe_mem x, fun φ => (heq _).mp hx φ⟩, rfl⟩

Premises used: Algebra.algebraMap, SetLike.coe_mem, Set.Mem, setOf, NumberField.RingOfIntegers.val, And.intro, Exists.intro, Iff.mp, Set.image, NumberField.RingOfIntegers, DFunLike.coe, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
hx :
  Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) : (K →+* ℂ) → ℂ)
⊢ Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ))
    (Set.image (α := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)
      {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r})
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) : (K →+* ℂ) → ℂ)

Tactic:
exact ⟨x, ⟨SetLike.coe_mem x, fun φ => (heq _).mp hx φ⟩, rfl⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
hx1 : IsIntegral ℤ x
hx2 : ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
⊢ Membership.mem (α := (K →+* ℂ) → ℂ) ((↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r)
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ)

Tactic:
⟨⟨x, ⟨⟨x, hx1⟩, rfl⟩, rfl⟩, (heq x).mpr hx2⟩

Premises used: Iff.mpr, Set.Mem, setOf, Set.inter, Subtype.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
hx1 : IsIntegral ℤ x
hx2 : ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
⊢ Membership.mem (α := (K →+* ℂ) → ℂ) ((↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r)
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ)

Tactic:
exact ⟨⟨x, ⟨⟨x, hx1⟩, rfl⟩, rfl⟩, (heq x).mpr hx2⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
⊢ (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

Premises used: isUnit_iff_ne_zero, Module.Basis.is_basis_iff_det, Module.Basis.det_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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 :
  (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)))
      ⊤
⊢ Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)

Tactic:
exact (basisOfPiSpaceOfLinearIndependent this.1).reindex e

Premises used: And.left, Module.Basis.reindex, basisOfPiSpaceOfLinearIndependent
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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)
suffices : M.det ≠ 0
⊢ Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)

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
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
a : ∀ (i j : K →+* ℂ), M i j = N.transpose i j
⊢ M = N.transpose

Tactic:
ext : 2
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
i j : K →+* ℂ
⊢ M i j = N.transpose i j

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
a a₁ : ∀ (i j : K →+* ℂ), M i j = N.transpose i j
⊢ M = N.transpose

Tactic:
{ ext : 2; rfl }
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
rw : N.transpose.det ≠ 0
⊢ M.det ≠ 0

Tactic:
rw [show M = N.transpose by { ext : 2; rfl }]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
rw : HPow.hPow (β := ℕ) N.det 2 ≠ 0
⊢ N.transpose.det ≠ 0

Tactic:
rw [Matrix.det_transpose, ← pow_ne_zero_iff two_ne_zero]

Premises used: Matrix.det_transpose, two_ne_zero, pow_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
⊢ Ne (α := ℂ)
    ((algebraMap ℚ ℂ : (a : ℚ) → ℂ)
        (Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
      ℂ)
    (0 : ℂ)

Tactic:
(map_ne_zero_iff _ (algebraMap ℚ ℂ).injective).mpr
        (Algebra.discr_not_zero_of_basis ℚ (integralBasis K))

Premises used: Iff.mpr, NumberField.integralBasis, Algebra.algebraMap, Rat, RingHom.injective, Algebra.discr_not_zero_of_basis, map_ne_zero_iff, Complex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
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))
⊢ HPow.hPow (β := ℕ) N.det 2 ≠ 0

Tactic:
convert!
      (map_ne_zero_iff _ (algebraMap ℚ ℂ).injective).mpr
        (Algebra.discr_not_zero_of_basis ℚ (integralBasis K))

Premises used: Iff.mpr, NumberField.integralBasis, Algebra.algebraMap, Rat, RingHom.injective, Algebra.discr_not_zero_of_basis, map_ne_zero_iff, Complex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
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))))
⊢ 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:
rw [← Algebra.discr_reindex ℚ (integralBasis K) e.symm]

Premises used: NumberField.integralBasis, Rat, Equiv.symm, Algebra.discr_reindex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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 (ι := 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:
(Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two ℚ ℂ
      (fun i => integralBasis K (e i)) RingHom.equivRatAlgHom).symm

Premises used: NumberField.integralBasis, Rat, Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, Complex, Eq.symm, DFunLike.coe, RingHom.equivRatAlgHom
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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 (ι := 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:
exact (Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two ℚ ℂ
      (fun i => integralBasis K (e i)) RingHom.equivRatAlgHom).symm

Premises used: NumberField.integralBasis, Rat, Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, Complex, Eq.symm, DFunLike.coe, RingHom.equivRatAlgHom
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ Eq (α := (K →+* ℂ) → ℂ)
    (((latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)
        i :
      (K →+* ℂ) → ℂ)
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ)
        (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) i :
          K) :
      (K →+* ℂ) → ℂ)

Tactic:
simp [latticeBasis, integralBasis_apply, coe_basisOfPiSpaceOfLinearIndependent,
    Function.comp_apply, Equiv.apply_symm_apply]

Premises used: NumberField.canonicalEmbedding.latticeBasis, NumberField.integralBasis_apply, Equiv.apply_symm_apply, coe_basisOfPiSpaceOfLinearIndependent, Function.comp_apply