awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this : IsFractionRing 𝒪 K
⊢ Module.Finite ℤ 𝒪

Tactic:
have := IsIntegralClosure.finite ℤ ℚ K 𝒪
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this : Module.Finite ℤ 𝒪
⊢ CharZero 𝒪

Tactic:
have := CharZero.of_module (R := 𝒪) K
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this : CharZero 𝒪
simp_rw : ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪), P.IsMaximal → P.LiesOver (A := ℤ) (Ideal.span {p}) → ¬P ∣ differentIdeal ℤ 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (A := ℤ) (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P

Tactic:
simp_rw [← not_dvd_differentIdeal_iff]

Premises used: not_dvd_differentIdeal_iff
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this : CharZero 𝒪
contrapose! : p ∣ discr K ↔ ∃ (P : Ideal 𝒪), P.IsMaximal ∧ P.LiesOver (A := ℤ) (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪), P.IsMaximal → P.LiesOver (A := ℤ) (Ideal.span {p}) → ¬P ∣ differentIdeal ℤ 𝒪

Tactic:
contrapose!
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this : CharZero 𝒪
mp : p ∣ discr K → ∃ (P : Ideal 𝒪), P.IsMaximal ∧ P.LiesOver (A := ℤ) (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪
mpr : (∃ (P : Ideal 𝒪), P.IsMaximal ∧ P.LiesOver (A := ℤ) (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪) → p ∣ discr K
⊢ p ∣ discr K ↔ ∃ (P : Ideal 𝒪), P.IsMaximal ∧ P.LiesOver (A := ℤ) (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪

Tactic:
constructor
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this : CharZero 𝒪
h : p ∣ discr K
⊢ p ∣ (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : ℤ)

Tactic:
rw [← Int.dvd_natAbs, ← absNorm_differentIdeal K 𝒪] at h

Premises used: Int.dvd_natAbs, NumberField.absNorm_differentIdeal
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this : CharZero 𝒪
h : p ∣ (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : ℤ)
mp :
  ∀ (P : Ideal 𝒪) (hP : P.IsMaximal) (h₁ : Eq (α := Ideal ℤ) (Ideal.under ℤ P) (Ideal.span {p}))
    (h₂ : P ∣ differentIdeal ℤ 𝒪),
    ∃ (P : Ideal 𝒪), P.IsMaximal ∧ P.LiesOver (A := ℤ) (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪
⊢ ∃ (P : Ideal 𝒪), P.IsMaximal ∧ P.LiesOver (A := ℤ) (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪

Tactic:
obtain ⟨P, hP, h₁, h₂⟩ := Ideal.exists_isMaximal_dvd_of_dvd_absNorm hp _ h

Premises used: Ideal.exists_isMaximal_dvd_of_dvd_absNorm
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this : CharZero 𝒪
h : p ∣ (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : ℤ)
P : Ideal 𝒪
hP : P.IsMaximal
h₁ : Eq (α := Ideal ℤ) (Ideal.under ℤ P) (Ideal.span {p})
h₂ : P ∣ differentIdeal ℤ 𝒪
⊢ ∃ (P : Ideal 𝒪), P.IsMaximal ∧ P.LiesOver (A := ℤ) (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪

Tactic:
⟨P, hP, ⟨h₁.symm⟩, h₂⟩

Premises used: Ideal.LiesOver.mk, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this : CharZero 𝒪
h : p ∣ (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : ℤ)
P : Ideal 𝒪
hP : P.IsMaximal
h₁ : Eq (α := Ideal ℤ) (Ideal.under ℤ P) (Ideal.span {p})
h₂ : P ∣ differentIdeal ℤ 𝒪
⊢ ∃ (P : Ideal 𝒪), P.IsMaximal ∧ P.LiesOver (A := ℤ) (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪

Tactic:
exact ⟨P, hP, ⟨h₁.symm⟩, h₂⟩
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this : CharZero 𝒪
P : Ideal 𝒪
hP : P.IsMaximal
hP' : P.LiesOver (A := ℤ) (Ideal.span {p})
hP'' : P ∣ differentIdeal ℤ 𝒪
⊢ Dvd.dvd (α := ℕ) ((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) P : ℕ)
    ((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪) : ℕ)

Tactic:
have := Ideal.absNorm_dvd_absNorm_of_le (Ideal.dvd_iff_le.mp hP'')
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this_5 : CharZero 𝒪
P : Ideal 𝒪
hP : P.IsMaximal
hP' : P.LiesOver (A := ℤ) (Ideal.span {p})
hP'' : P ∣ differentIdeal ℤ 𝒪
this :
  Dvd.dvd (α := ℕ) ((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) P : ℕ)
    ((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪) : ℕ)
⊢ p ^ Ideal.inertiaDeg (R := ℤ) (Ideal.span {p}) P ∣ discr K

Tactic:
rw [absNorm_differentIdeal K, Ideal.absNorm_eq_pow_inertiaDeg P hp,
      ← Int.natAbs_pow, Int.natAbs_dvd_natAbs] at this

Premises used: Int.natAbs_pow, Int.natAbs_dvd_natAbs, NumberField.absNorm_differentIdeal, Ideal.absNorm_eq_pow_inertiaDeg
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this_5 : CharZero 𝒪
P : Ideal 𝒪
hP : P.IsMaximal
hP' : P.LiesOver (A := ℤ) (Ideal.span {p})
hP'' : P ∣ differentIdeal ℤ 𝒪
this : p ^ Ideal.inertiaDeg (R := ℤ) (Ideal.span {p}) P ∣ discr K
⊢ p ∣ discr K

Tactic:
(dvd_pow_self _ (Ideal.inertiaDeg_pos' ..).ne').trans this

Premises used: Ideal.inertiaDeg_pos', dvd_pow_self, LT.lt.ne', Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this_5 : CharZero 𝒪
P : Ideal 𝒪
hP : P.IsMaximal
hP' : P.LiesOver (A := ℤ) (Ideal.span {p})
hP'' : P ∣ differentIdeal ℤ 𝒪
this : p ^ Ideal.inertiaDeg (R := ℤ) (Ideal.span {p}) P ∣ discr K
⊢ p ∣ discr K

Tactic:
exact (dvd_pow_self _ (Ideal.inertiaDeg_pos' ..).ne').trans this

Premises used: Ideal.inertiaDeg_pos', dvd_pow_self, LT.lt.ne', Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this : IsDedekindDomain 𝒪
⊢ CharZero 𝒪

Tactic:
have := CharZero.of_module (R := 𝒪) K
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this : CharZero 𝒪
rw :
  (∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (A := ℤ) (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P) ↔
    ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → Algebra.IsUnramifiedAt ℤ P
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → Algebra.IsUnramifiedAt ℤ P

Tactic:
rw [NumberField.not_dvd_discr_iff_forall_liesOver K 𝒪 hp]

Premises used: NumberField.not_dvd_discr_iff_forall_liesOver
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this : CharZero 𝒪
H : ∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (A := ℤ) (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P
P : Ideal 𝒪
hP : P.IsPrime
h : (↑p : 𝒪) ∈ P
⊢ P ≠ ⊥

Tactic:
aesop
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this : CharZero 𝒪
⊢ (∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (A := ℤ) (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P) ↔
    ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → Algebra.IsUnramifiedAt ℤ P

Tactic:
exact ⟨fun H P hP h ↦ H P (hP.isMaximal (by aesop))
    ((Ideal.liesOver_span_iff hP.ne_top hp).mpr h),
    fun H P _ h ↦ H P _ (h.1.le (Ideal.mem_span_singleton_self _))⟩
-- Module: Mathlib.NumberTheory.NumberField.EquivReindex
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : finrank ℚ K = Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K))
rw₁ : finrank ℚ K = finrank.{0, u_1} ℤ (𝓞 K)
rw₂ rw₃ : finrank ℚ K = finrank ℚ K
⊢ Fintype.card.{u_1} (K →+* ℂ) = Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K))

Tactic:
rw [Embeddings.card, ← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank]

Premises used: NumberField.Embeddings.card, NumberField.RingOfIntegers.rank, Module.finrank_eq_card_chooseBasisIndex
-- Module: Mathlib.NumberTheory.NumberField.EquivReindex
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a :
  ∀ (i j : K →+* ℂ),
    basisMatrix K i j =
      Algebra.embeddingsMatrixReindex ℚ ℂ
        (Function.comp (β := ChooseBasisIndex ℤ (𝓞 K))
          (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K)
          (⇑(equivReindex K : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) : (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K)))
        RingHom.equivRatAlgHom i j
⊢ Eq (α := Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (basisMatrix K)
    (Algebra.embeddingsMatrixReindex ℚ ℂ
      (Function.comp (β := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K)
        (⇑(equivReindex K : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) : (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K)))
      RingHom.equivRatAlgHom)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.EquivReindex
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i j : K →+* ℂ
⊢ basisMatrix K i j =
    Algebra.embeddingsMatrixReindex ℚ ℂ
      (Function.comp (β := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K)
        (⇑(equivReindex K : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) : (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K)))
      RingHom.equivRatAlgHom i j

Tactic:
simp [Algebra.embeddingsMatrixReindex]

Premises used: Algebra.embeddingsMatrixReindex
-- Module: Mathlib.NumberTheory.NumberField.EquivReindex
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a :
  ∀ (i j : K →+* ℂ),
    Eq (α := ℂ) (Matrix.map (basisMatrix K) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) i j)
      ((reindex (Equiv.refl (K →+* ℂ)) (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯) :
          (a : Matrix (K →+* ℂ) (K →+* ℂ) ℂ) → Matrix (K →+* ℂ) (K →+* ℂ) ℂ)
        (basisMatrix K) i j)
⊢ Eq (α := Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Matrix.map (basisMatrix K) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ))
    ((reindex (Equiv.refl (K →+* ℂ)) (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯) :
        (a : Matrix (K →+* ℂ) (K →+* ℂ) ℂ) → Matrix (K →+* ℂ) (K →+* ℂ) ℂ)
      (basisMatrix K))

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.EquivReindex
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i j : K →+* ℂ
⊢ Eq (α := ℂ) (Matrix.map (basisMatrix K) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) i j)
    ((reindex (Equiv.refl (K →+* ℂ)) (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯) :
        (a : Matrix (K →+* ℂ) (K →+* ℂ) ℂ) → Matrix (K →+* ℂ) (K →+* ℂ) ℂ)
      (basisMatrix K) i j)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.EquivReindex
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
rw :
  HPow.hPow (β := ℕ)
      (det (n := K →+* ℂ)
        (Algebra.embeddingsMatrixReindex ℚ ℂ
          (Function.comp (β := ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K)
            (⇑(equivReindex K : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) : (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K)))
          RingHom.equivRatAlgHom))
      2 ≠
    0
⊢ det (n := K →+* ℂ) (basisMatrix K) ≠ 0

Tactic:
rw [basisMatrix_eq_embeddingsMatrixReindex, ← pow_ne_zero_iff two_ne_zero]

Premises used: NumberField.basisMatrix_eq_embeddingsMatrixReindex, two_ne_zero, pow_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.EquivReindex
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
⊢ Ne (α := ℂ)
    ((algebraMap ℚ ℂ : (a : ℚ) → ℂ)
        (Algebra.discr (ι := ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
          (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : 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.EquivReindex
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
h :
  HPow.hPow (β := ℕ)
      (det (n := K →+* ℂ)
        (Algebra.embeddingsMatrixReindex ℚ ℂ
          (Function.comp (β := ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K)
            (⇑(equivReindex K : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) : (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K)))
          RingHom.equivRatAlgHom))
      2 =
    (algebraMap ℚ ℂ : (a : ℚ) → ℂ)
      (Algebra.discr (ι := ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
        (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K))
⊢ HPow.hPow (β := ℕ)
      (det (n := K →+* ℂ)
        (Algebra.embeddingsMatrixReindex ℚ ℂ
          (Function.comp (β := ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K)
            (⇑(equivReindex K : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) : (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K)))
          RingHom.equivRatAlgHom))
      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.EquivReindex
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
h :
  HPow.hPow (β := ℕ)
      (det (n := K →+* ℂ)
        (Algebra.embeddingsMatrixReindex ℚ ℂ
          (Function.comp (β := ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K)
            (⇑(equivReindex K : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) : (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K)))
          RingHom.equivRatAlgHom))
      2 =
    (algebraMap ℚ ℂ : (a : ℚ) → ℂ)
      (Algebra.discr (ι := K →+* ℂ) ℚ (B := K)
        (Function.comp (β := ChooseBasisIndex ℤ (𝓞 K))
          (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K)
          (⇑(Equiv.symm (Equiv.symm (equivReindex K)) : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) :
            (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K))))
⊢ HPow.hPow (β := ℕ)
      (det (n := K →+* ℂ)
        (Algebra.embeddingsMatrixReindex ℚ ℂ
          (Function.comp (β := ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K)
            (⇑(equivReindex K : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) : (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K)))
          RingHom.equivRatAlgHom))
      2 =
    (algebraMap ℚ ℂ : (a : ℚ) → ℂ)
      (Algebra.discr (ι := ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
        (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K))

Tactic:
rw [← Algebra.discr_reindex ℚ (integralBasis K) (equivReindex K).symm]

Premises used: NumberField.integralBasis, Rat, Equiv.symm, NumberField.equivReindex, Algebra.discr_reindex
-- Module: Mathlib.NumberTheory.NumberField.EquivReindex
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
⊢ HPow.hPow (β := ℕ)
      (det (n := K →+* ℂ)
        (Algebra.embeddingsMatrixReindex ℚ ℂ
          (Function.comp (β := ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K)
            (⇑(equivReindex K : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) : (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K)))
          RingHom.equivRatAlgHom))
      2 =
    (algebraMap ℚ ℂ : (a : ℚ) → ℂ)
      (Algebra.discr (ι := K →+* ℂ) ℚ (B := K)
        (Function.comp (β := ChooseBasisIndex ℤ (𝓞 K))
          (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K)
          (⇑(Equiv.symm (Equiv.symm (equivReindex K)) : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) :
            (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K))))

Tactic:
(Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two ℚ ℂ
    (integralBasis K ∘ (equivReindex K)) RingHom.equivRatAlgHom).symm

Premises used: NumberField.integralBasis, Rat, Function.comp, Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, Complex, Eq.symm, DFunLike.coe, RingHom.equivRatAlgHom, NumberField.equivReindex
-- Module: Mathlib.NumberTheory.NumberField.EquivReindex
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
⊢ HPow.hPow (β := ℕ)
      (det (n := K →+* ℂ)
        (Algebra.embeddingsMatrixReindex ℚ ℂ
          (Function.comp (β := ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K)
            (⇑(equivReindex K : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) : (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K)))
          RingHom.equivRatAlgHom))
      2 =
    (algebraMap ℚ ℂ : (a : ℚ) → ℂ)
      (Algebra.discr (ι := K →+* ℂ) ℚ (B := K)
        (Function.comp (β := ChooseBasisIndex ℤ (𝓞 K))
          (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K)
          (⇑(Equiv.symm (Equiv.symm (equivReindex K)) : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) :
            (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K))))

Tactic:
exact (Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two ℚ ℂ
    (integralBasis K ∘ (equivReindex K)) RingHom.equivRatAlgHom).symm

Premises used: NumberField.integralBasis, Rat, Function.comp, Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, Complex, Eq.symm, DFunLike.coe, RingHom.equivRatAlgHom, NumberField.equivReindex
-- Module: Mathlib.NumberTheory.NumberField.EquivReindex
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
h :
  ∀ (i : K →+* ℂ),
    (canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α i =
      ((basisMatrix K)ᵀ *ᵥ fun (i : K →+* ℂ) ↦
          (↑(((((Basis.repr
                            (Basis.reindex (ι := ChooseBasisIndex ℤ (𝓞 K))
                              (integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K)
                              (Equiv.symm (equivReindex K) : ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ))) :
                          K ≃ₗ[ℚ] (K →+* ℂ) →₀ ℚ) :
                        (a : K) → (K →+* ℂ) →₀ ℚ)
                      α :
                    (K →+* ℂ) →₀ ℚ) :
                  (a : K →+* ℂ) → ℚ)
                i) :
            ℂ))
        i
⊢ Eq (α := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α : (K →+* ℂ) → ℂ)
    ((basisMatrix K)ᵀ *ᵥ fun (i : K →+* ℂ) ↦
        (↑(((((Basis.repr
                          (Basis.reindex (ι := ChooseBasisIndex ℤ (𝓞 K))
                            (integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K)
                            (Equiv.symm (equivReindex K) : ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ))) :
                        K ≃ₗ[ℚ] (K →+* ℂ) →₀ ℚ) :
                      (a : K) → (K →+* ℂ) →₀ ℚ)
                    α :
                  (K →+* ℂ) →₀ ℚ) :
                (a : K →+* ℂ) → ℚ)
              i) :
          ℂ) :
      (K →+* ℂ) → ℂ)

Tactic:
ext i