awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.EquivReindex
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
i : K →+* ℂ
h :
  (∑ i : K →+* ℂ,
        HSMul.hSMul (α := ℂ) (β := (K →+* ℂ) → ℂ)
          (((((Basis.repr (latticeBasis K) : ((K →+* ℂ) → ℂ) ≃ₗ[ℂ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℂ) :
                      (a : (K →+* ℂ) → ℂ) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℂ)
                    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α : (K →+* ℂ) → ℂ) :
                  ChooseBasisIndex ℤ (𝓞 K) →₀ ℂ) :
                (a : ChooseBasisIndex ℤ (𝓞 K)) → ℂ)
              (((equivReindex K : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) : (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K)) i :
                ChooseBasisIndex ℤ (𝓞 K)) :
            ℂ)
          (((latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
                (a : ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)
              (((equivReindex K : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) : (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K)) i :
                ChooseBasisIndex ℤ (𝓞 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
⊢ (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

Tactic:
rw [← (latticeBasis K).sum_repr (canonicalEmbedding K α), ← Equiv.sum_comp (equivReindex K)]

Premises used: NumberField.canonicalEmbedding.latticeBasis, Equiv.sum_comp, NumberField.canonicalEmbedding, DFunLike.coe, Module.Basis.sum_repr, NumberField.equivReindex
-- Module: Mathlib.NumberTheory.NumberField.EquivReindex
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
i : K →+* ℂ
⊢ (∑ i : K →+* ℂ,
        HSMul.hSMul (α := ℂ) (β := (K →+* ℂ) → ℂ)
          (((((Basis.repr (latticeBasis K) : ((K →+* ℂ) → ℂ) ≃ₗ[ℂ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℂ) :
                      (a : (K →+* ℂ) → ℂ) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℂ)
                    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α : (K →+* ℂ) → ℂ) :
                  ChooseBasisIndex ℤ (𝓞 K) →₀ ℂ) :
                (a : ChooseBasisIndex ℤ (𝓞 K)) → ℂ)
              (((equivReindex K : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) : (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K)) i :
                ChooseBasisIndex ℤ (𝓞 K)) :
            ℂ)
          (((latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
                (a : ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)
              (((equivReindex K : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) : (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K)) i :
                ChooseBasisIndex ℤ (𝓞 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

Tactic:
simp only [canonicalEmbedding.integralBasis_repr_apply, mulVec, dotProduct,
    transpose_apply, of_apply, Fintype.sum_apply, mul_comm, Basis.repr_reindex,
    Finsupp.mapDomain_equiv_apply, Equiv.symm_symm, Pi.smul_apply, smul_eq_mul]

Premises used: dotProduct, NumberField.canonicalEmbedding.integralBasis_repr_apply, Equiv.symm_symm, Module.Basis.repr_reindex, Matrix.of_apply, Finsupp.mapDomain_equiv_apply, mul_comm, smul_eq_mul, Matrix.transpose_apply, Fintype.sum_apply, Matrix.mulVec, Pi.smul_apply
-- Module: Mathlib.NumberTheory.NumberField.EquivReindex
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
rw rw₁ :
  Eq (α := ℂ)
    ((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 →+* ℂ) →₀ ℚ)
                      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) :
                    (K →+* ℂ) →₀ ℚ) :
                  (a : K →+* ℂ) → ℚ)
                i) :
            ℂ) :
          ℂ))
      i)
    (↑(((((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) :
              (K →+* ℂ) →₀ ℚ) :
            (a : K →+* ℂ) → ℚ)
          i) :
      ℂ)
⊢ ((basisMatrix K)ᵀ⁻¹ *ᵥ fun (j : K →+* ℂ) ↦
        (canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j)
      i =
    (↑(((((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) :
              (K →+* ℂ) →₀ ℚ) :
            (a : K →+* ℂ) → ℚ)
          i) :
      ℂ)

Tactic:
rw [inv_mulVec_eq_vec (canonicalEmbedding_eq_basisMatrix_mulVec ((algebraMap (𝓞 K) K) α))]

Premises used: Algebra.algebraMap, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, NumberField.RingOfIntegers, Matrix.inv_mulVec_eq_vec, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
H : Module.finrank ℚ K ≠ 1
⊢ IsDomain 𝒪

Tactic:
have := (IsIntegralClosure.algebraMap_injective 𝒪 ℤ K).isDomain
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
H : Module.finrank ℚ K ≠ 1
this : IsDomain 𝒪
⊢ IsDedekindDomain 𝒪

Tactic:
have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
H : Module.finrank ℚ K ≠ 1
this_1 : IsDomain 𝒪
this : IsDedekindDomain 𝒪
⊢ CharZero 𝒪

Tactic:
have := CharZero.of_module (R := 𝒪) K
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
H : Module.finrank ℚ K ≠ 1
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this : CharZero 𝒪
⊢ 0 < Module.finrank ℚ K

Tactic:
have := Module.finrank_pos (R := ℚ) (M := K)
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
H : Module.finrank ℚ K ≠ 1
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : CharZero 𝒪
this : 0 < Module.finrank ℚ K
⊢ 1 < Module.finrank ℚ K

Tactic:
lia
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
H : Module.finrank ℚ K ≠ 1
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : CharZero 𝒪
this : 0 < Module.finrank ℚ K
⊢ 2 < |discr K|

Tactic:
have := NumberField.abs_discr_gt_two (K := K) (by lia)
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
H : Module.finrank ℚ K ≠ 1
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : CharZero 𝒪
this_4 : 0 < Module.finrank ℚ K
this : 2 < |discr K|
zify : |discr K| ≠ 1
⊢ (discr K).natAbs ≠ 1

Tactic:
zify
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
H : Module.finrank ℚ K ≠ 1
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : CharZero 𝒪
this_4 : 0 < Module.finrank ℚ K
this : 2 < |discr K|
linarith : |discr K| = 1 → HMul.hMul (α := ℤ) 2 (-1) + (HAdd.hAdd (α := ℤ) 2 1 - |discr K|) + (|discr K| - 1) = 0
linarith₁ : |discr K| = 1 → GT.gt (α := ℤ) 2 0
⊢ |discr K| ≠ 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
H : Module.finrank ℚ K ≠ 1
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : CharZero 𝒪
this_4 : 0 < Module.finrank ℚ K
this : 2 < |discr K|
obtain : ∀ (q : ℤ) (hq : Prime q) (hqK : q ∣ discr K), ∃ (P : Ideal 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
⊢ ∃ (P : Ideal 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
obtain ⟨q, hq, hqK⟩ := Int.exists_prime_and_dvd (n := discr K) (by zify; linarith)

Premises used: Int.exists_prime_and_dvd
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
H : Module.finrank ℚ K ≠ 1
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : CharZero 𝒪
this_4 : 0 < Module.finrank ℚ K
this : 2 < |discr K|
q : ℤ
hq : Prime q
hqK : q ∣ discr K
⊢ ¬∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑q : 𝒪) ∈ P → Algebra.IsUnramifiedAt ℤ P

Tactic:
have := (not_dvd_discr_iff_forall_mem K 𝒪 hq).not_right.mp hqK
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
H : Module.finrank ℚ K ≠ 1
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : CharZero 𝒪
this_4 : 0 < Module.finrank ℚ K
this_5 : 2 < |discr K|
q : ℤ
hq : Prime q
hqK : q ∣ discr K
this : ¬∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑q : 𝒪) ∈ P → Algebra.IsUnramifiedAt ℤ P
⊢ ∃ (P : Ideal 𝒪) (h : P.IsPrime), (↑q : 𝒪) ∈ P ∧ ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
push Not at this

Premises used: Not
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
H : Module.finrank ℚ K ≠ 1
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : CharZero 𝒪
this_4 : 0 < Module.finrank ℚ K
this_5 : 2 < |discr K|
q : ℤ
hq : Prime q
hqK : q ∣ discr K
this : ∃ (P : Ideal 𝒪) (h : P.IsPrime), (↑q : 𝒪) ∈ P ∧ ¬Algebra.IsUnramifiedAt ℤ P
obtain :
  ∀ (P : Ideal 𝒪) (hP : P.IsPrime) (h : (↑q : 𝒪) ∈ P) (H : ¬Algebra.IsUnramifiedAt ℤ P),
    ∃ (P : Ideal 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
⊢ ∃ (P : Ideal 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
obtain ⟨P, hP, h, H⟩ := this
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
H_1 : Module.finrank ℚ K ≠ 1
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : CharZero 𝒪
this_4 : 0 < Module.finrank ℚ K
this : 2 < |discr K|
q : ℤ
hq : Prime q
hqK : q ∣ discr K
P : Ideal 𝒪
hP : P.IsPrime
h : (↑q : 𝒪) ∈ P
H : ¬Algebra.IsUnramifiedAt ℤ P
⊢ P ≠ ⊥

Tactic:
aesop
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
H_1 : Module.finrank ℚ K ≠ 1
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : CharZero 𝒪
this_4 : 0 < Module.finrank ℚ K
this : 2 < |discr K|
q : ℤ
hq : Prime q
hqK : q ∣ discr K
P : Ideal 𝒪
hP : P.IsPrime
h : (↑q : 𝒪) ∈ P
H : ¬Algebra.IsUnramifiedAt ℤ P
⊢ ∃ (P : Ideal 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
exact ⟨P, hP.isMaximal (by aesop), H⟩
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
inst_5 : Algebra.Unramified ℤ 𝒪
by_contra : ∀ (H : ¬Module.finrank ℚ K = 1), False
⊢ Module.finrank ℚ K = 1

Tactic:
by_contra H
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
inst_5 : Algebra.Unramified ℤ 𝒪
H : ¬Module.finrank ℚ K = 1
obtain : ∀ (P : Ideal 𝒪) (w : P.IsMaximal) (H : ¬Algebra.IsUnramifiedAt ℤ P), False
⊢ False

Tactic:
obtain ⟨P, _, H⟩ := NumberField.exists_not_isUnramifiedAt_int (𝒪 := 𝒪) H

Premises used: NumberField.exists_not_isUnramifiedAt_int
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
inst_5 : Algebra.Unramified ℤ 𝒪
H_1 : ¬Module.finrank ℚ K = 1
P : Ideal 𝒪
w : P.IsMaximal
H : ¬Algebra.IsUnramifiedAt ℤ P
⊢ False

Tactic:
H inferInstance

Premises used: inferInstance
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
inst_5 : Algebra.Unramified ℤ 𝒪
H_1 : ¬Module.finrank ℚ K = 1
P : Ideal 𝒪
w : P.IsMaximal
H : ¬Algebra.IsUnramifiedAt ℤ P
⊢ False

Tactic:
exact H inferInstance

Premises used: inferInstance
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
Goal:
𝒪 : Type u_2
inst : CommRing 𝒪
inst_1 : Module.Finite ℤ 𝒪
inst_2 : Algebra.Unramified ℤ 𝒪
inst_3 : IsDomain 𝒪
inst_4 : FaithfulSMul ℤ 𝒪
⊢ IsDedekindDomain 𝒪

Tactic:
have := isDedekindDomain.of_formallyUnramified ℤ 𝒪
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
Goal:
𝒪 : Type u_2
inst : CommRing 𝒪
inst_1 : Module.Finite ℤ 𝒪
inst_2 : Algebra.Unramified ℤ 𝒪
inst_3 : IsDomain 𝒪
inst_4 : FaithfulSMul ℤ 𝒪
this_1 : IsDedekindDomain 𝒪
K : Type u_2 := FractionRing 𝒪
this : Algebra ℤ K := Ring.toIntAlgebra K
⊢ CharZero 𝒪

Tactic:
have : CharZero 𝒪 := Algebra.charZero_of_charZero ℤ _
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
Goal:
𝒪 : Type u_2
inst : CommRing 𝒪
inst_1 : Module.Finite ℤ 𝒪
inst_2 : Algebra.Unramified ℤ 𝒪
inst_3 : IsDomain 𝒪
inst_4 : FaithfulSMul ℤ 𝒪
this_1 : IsDedekindDomain 𝒪
K : Type u_2 := FractionRing 𝒪
this_2 : Algebra ℤ K := Ring.toIntAlgebra K
this : CharZero 𝒪
⊢ NumberField K

Tactic:
have : NumberField K := { to_finiteDimensional := Module.Finite.of_isLocalization ℤ 𝒪 ℤ⁰ }
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
Goal:
𝒪 : Type u_2
inst : CommRing 𝒪
inst_1 : Module.Finite ℤ 𝒪
inst_2 : Algebra.Unramified ℤ 𝒪
inst_3 : IsDomain 𝒪
inst_4 : FaithfulSMul ℤ 𝒪
this_1 : IsDedekindDomain 𝒪
K : Type u_2 := FractionRing 𝒪
this_2 : Algebra ℤ K := Ring.toIntAlgebra K
this_3 : CharZero 𝒪
this : NumberField K
⊢ Module.finrank ℚ K = 1

Tactic:
have := NumberField.finrank_eq_one_of_unramified (K := K) (𝒪 := 𝒪)
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
Goal:
𝒪 : Type u_2
inst : CommRing 𝒪
inst_1 : Module.Finite ℤ 𝒪
inst_2 : Algebra.Unramified ℤ 𝒪
inst_3 : IsDomain 𝒪
inst_4 : FaithfulSMul ℤ 𝒪
this_1 : IsDedekindDomain 𝒪
K : Type u_2 := FractionRing 𝒪
this_2 : Algebra ℤ K := Ring.toIntAlgebra K
this_3 : CharZero 𝒪
this_4 : NumberField K
this : Module.finrank ℚ K = 1
⊢ ∀ (x : ℤ),
    Eq (α := K) ((algebraMap ℤ K : (a : ℤ) → K) x : K)
      ((AlgEquiv.ofBijective (IsScalarTower.toAlgHom ℤ ℚ K) ⋯ : (a : ℚ) → K) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) x : ℚ) : K)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
Goal:
𝒪 : Type u_2
inst : CommRing 𝒪
inst_1 : Module.Finite ℤ 𝒪
inst_2 : Algebra.Unramified ℤ 𝒪
inst_3 : IsDomain 𝒪
inst_4 : FaithfulSMul ℤ 𝒪
this_1 : IsDedekindDomain 𝒪
K : Type u_2 := FractionRing 𝒪
this_2 : Algebra ℤ K := Ring.toIntAlgebra K
this_3 : CharZero 𝒪
this_4 : NumberField K
this : Module.finrank ℚ K = 1
⊢ IsIntegralClosure ℤ ℤ K

Tactic:
have : IsIntegralClosure ℤ ℤ K := .of_algEquiv _ (.ofBijective (IsScalarTower.toAlgHom _ _ _)
    (Algebra.finrank_eq_one_iff_bijective_algebraMap.mp this)) (by simp)
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
Goal:
𝒪 : Type u_2
inst : CommRing 𝒪
inst_1 : Module.Finite ℤ 𝒪
inst_2 : Algebra.Unramified ℤ 𝒪
inst_3 : IsDomain 𝒪
inst_4 : FaithfulSMul ℤ 𝒪
this_1 : IsDedekindDomain 𝒪
K : Type u_2 := FractionRing 𝒪
this_2 : Algebra ℤ K := Ring.toIntAlgebra K
this_3 : CharZero 𝒪
this_4 : NumberField K
this_5 : Module.finrank ℚ K = 1
this : IsIntegralClosure ℤ ℤ K
⊢ Function.Bijective (α := ℤ) (β := 𝒪) (⇑(algebraMap ℤ 𝒪) : (a : ℤ) → 𝒪)

Tactic:
bijective_algebraMap_of_linearEquiv (IsIntegralClosure.equiv ℤ ℤ K 𝒪).toLinearEquiv

Premises used: IsIntegralClosure.equiv, Int, bijective_algebraMap_of_linearEquiv, AlgEquiv.toLinearEquiv
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
Goal:
𝒪 : Type u_2
inst : CommRing 𝒪
inst_1 : Module.Finite ℤ 𝒪
inst_2 : Algebra.Unramified ℤ 𝒪
inst_3 : IsDomain 𝒪
inst_4 : FaithfulSMul ℤ 𝒪
this_1 : IsDedekindDomain 𝒪
K : Type u_2 := FractionRing 𝒪
this_2 : Algebra ℤ K := Ring.toIntAlgebra K
this_3 : CharZero 𝒪
this_4 : NumberField K
this_5 : Module.finrank ℚ K = 1
this : IsIntegralClosure ℤ ℤ K
⊢ Function.Bijective (α := ℤ) (β := 𝒪) (⇑(algebraMap ℤ 𝒪) : (a : ℤ) → 𝒪)

Tactic:
exact bijective_algebraMap_of_linearEquiv (IsIntegralClosure.equiv ℤ ℤ K 𝒪).toLinearEquiv

Premises used: IsIntegralClosure.equiv, Int, bijective_algebraMap_of_linearEquiv, AlgEquiv.toLinearEquiv
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
⊢ IsDomain 𝒪

Tactic:
have := (IsIntegralClosure.algebraMap_injective 𝒪 ℤ K).isDomain
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this : IsDomain 𝒪
⊢ IsDedekindDomain 𝒪

Tactic:
have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this_1 : IsDomain 𝒪
this : IsDedekindDomain 𝒪
⊢ IsFractionRing 𝒪 K

Tactic:
have := IsIntegralClosure.isFractionRing_of_finite_extension ℤ ℚ K 𝒪
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this : IsFractionRing 𝒪 K
⊢ Module.Finite ℤ 𝒪

Tactic:
have := IsIntegralClosure.finite ℤ ℚ K 𝒪
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
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.ExistsRamified
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
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this_5 : CharZero 𝒪
this : MulSemiringAction.{u_1, u_2} Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
⊢ IsGaloisGroup.{u_1, 0, u_2} Gal(K/ℚ) ℤ 𝒪

Tactic:
have := IsGaloisGroup.of_isFractionRing Gal(K/ℚ) ℤ 𝒪 ℚ K
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this_5 : CharZero 𝒪
this_6 : MulSemiringAction.{u_1, u_2} Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this : IsGaloisGroup.{u_1, 0, u_2} Gal(K/ℚ) ℤ 𝒪
obtain :
  ∀ (P : Ideal 𝒪) (w : P.IsMaximal) (hP' : ¬Algebra.IsUnramifiedAt ℤ P),
    ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
⊢ ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
obtain ⟨P, _, hP'⟩ := NumberField.exists_not_isUnramifiedAt_int (𝒪 := 𝒪) H.ne'

Premises used: NumberField.exists_not_isUnramifiedAt_int, LT.lt.ne'
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this_5 : CharZero 𝒪
this_6 : MulSemiringAction.{u_1, u_2} Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this : IsGaloisGroup.{u_1, 0, u_2} Gal(K/ℚ) ℤ 𝒪
P : Ideal 𝒪
w : P.IsMaximal
hP' : ¬Algebra.IsUnramifiedAt ℤ P
obtain :
  ∀ (p : ℤ) (hp : Eq (α := Ideal ℤ) (Ideal.under ℤ P) (Ideal.span {p})),
    ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
⊢ ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
obtain ⟨p, hp : _ = Ideal.span _⟩ := IsPrincipalIdealRing.principal (P.under ℤ)

Premises used: Int, Ideal.span, IsPrincipalIdealRing.principal, Ideal.under