awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.EquivReindex (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
⊢ 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 →+* ℂ) → ℂ)
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.EquivReindex (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
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
have 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
Tactic: rw [← (latticeBasis K).sum_repr (canonicalEmbedding K α), ← Equiv.sum_comp (equivReindex K)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.EquivReindex (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
⊢ ((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) :
      ℂ)
have 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) :
    ℂ)
Tactic: rw [inv_mulVec_eq_vec (canonicalEmbedding_eq_basisMatrix_mulVec ((algebraMap (𝓞 K) K) α))]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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
⊢ ∃ (P : Ideal 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
have this : IsDomain 𝒪
Tactic: have := (IsIntegralClosure.algebraMap_injective 𝒪 ℤ K).isDomain
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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 𝒪
⊢ ∃ (P : Ideal 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
have this₁ : IsDedekindDomain 𝒪
Tactic: have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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 𝒪
⊢ ∃ (P : Ideal 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
have this₁ : CharZero 𝒪
Tactic: have := CharZero.of_module (R := 𝒪) K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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 𝒪
⊢ ∃ (P : Ideal 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
have this₁ : 0 < Module.finrank ℚ K
Tactic: have := Module.finrank_pos (R := ℚ) (M := K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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
⊢ ∃ (P : Ideal 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
have this₁ : 2 < |discr K|
Tactic: have := NumberField.abs_discr_gt_two (K := K) (by lia)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
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|
⊢ (discr K).natAbs ≠ 1
have zify : |discr K| ≠ 1
Tactic: zify
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
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|
⊢ |discr K| ≠ 1
have linarith : |discr K| = 1 → HMul.hMul (α := ℤ) 2 (-1) + (HAdd.hAdd (α := ℤ) 2 1 - |discr K|) + (|discr K| - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
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
⊢ |discr K| ≠ 1
have linarith₁ : |discr K| = 1 → GT.gt (α := ℤ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
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|
⊢ ∃ (P : Ideal 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
have obtain : ∀ (q : ℤ) (hq : Prime q) (hqK : q ∣ discr K), ∃ (P : Ideal 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
Tactic: obtain ⟨q, hq, hqK⟩ := Int.exists_prime_and_dvd (n := discr K) (by zify; linarith)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
have this₁ : ¬∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑q : 𝒪) ∈ P → Algebra.IsUnramifiedAt ℤ P
Tactic: have := (not_dvd_discr_iff_forall_mem K 𝒪 hq).not_right.mp hqK
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
have this₁ : ∃ (P : Ideal 𝒪) (h : P.IsPrime), (↑q : 𝒪) ∈ P ∧ ¬Algebra.IsUnramifiedAt ℤ P
Tactic: push Not at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
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
⊢ ∃ (P : Ideal 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
have obtain : ∀ (P : Ideal 𝒪) (hP : P.IsPrime) (h : (↑q : 𝒪) ∈ P) (H : ¬Algebra.IsUnramifiedAt ℤ P),
  ∃ (P : Ideal 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
Tactic: obtain ⟨P, hP, h, H⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
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 ℤ 𝒪
⊢ Module.finrank ℚ K = 1
have by_contra : ∀ (H : ¬Module.finrank ℚ K = 1), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
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
⊢ False
have obtain : ∀ (P : Ideal 𝒪) (w : P.IsMaximal) (H : ¬Algebra.IsUnramifiedAt ℤ P), False
Tactic: obtain ⟨P, _, H⟩ := NumberField.exists_not_isUnramifiedAt_int (𝒪 := 𝒪) H
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
Goal:
𝒪 : Type u_2
inst : CommRing 𝒪
inst_1 : Module.Finite ℤ 𝒪
inst_2 : Algebra.Unramified ℤ 𝒪
inst_3 : IsDomain 𝒪
inst_4 : FaithfulSMul ℤ 𝒪
⊢ Function.Bijective (α := ℤ) (β := 𝒪) (⇑(algebraMap ℤ 𝒪) : (a : ℤ) → 𝒪)
have this : IsDedekindDomain 𝒪
Tactic: have := isDedekindDomain.of_formallyUnramified ℤ 𝒪
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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
⊢ Function.Bijective (α := ℤ) (β := 𝒪) (⇑(algebraMap ℤ 𝒪) : (a : ℤ) → 𝒪)
have this₁ : CharZero 𝒪
Tactic: have : CharZero 𝒪 := Algebra.charZero_of_charZero ℤ _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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 𝒪
⊢ Function.Bijective (α := ℤ) (β := 𝒪) (⇑(algebraMap ℤ 𝒪) : (a : ℤ) → 𝒪)
have this₁ : NumberField K
Tactic: have : NumberField K := { to_finiteDimensional := Module.Finite.of_isLocalization ℤ 𝒪 ℤ⁰ }
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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
⊢ Function.Bijective (α := ℤ) (β := 𝒪) (⇑(algebraMap ℤ 𝒪) : (a : ℤ) → 𝒪)
have this₁ : Module.finrank ℚ K = 1
Tactic: have := NumberField.finrank_eq_one_of_unramified (K := K) (𝒪 := 𝒪)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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
⊢ Function.Bijective (α := ℤ) (β := 𝒪) (⇑(algebraMap ℤ 𝒪) : (a : ℤ) → 𝒪)
have this₁ : IsIntegralClosure ℤ ℤ K
Tactic: have : IsIntegralClosure ℤ ℤ K := .of_algEquiv _ (.ofBijective (IsScalarTower.toAlgHom _ _ _)
    (Algebra.finrank_eq_one_iff_bijective_algebraMap.mp this)) (by simp)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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
⊢ ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
have this : IsDomain 𝒪
Tactic: have := (IsIntegralClosure.algebraMap_injective 𝒪 ℤ K).isDomain
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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 𝒪
⊢ ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
have this₁ : IsDedekindDomain 𝒪
Tactic: have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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 𝒪
⊢ ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
have this₁ : IsFractionRing 𝒪 K
Tactic: have := IsIntegralClosure.isFractionRing_of_finite_extension ℤ ℚ K 𝒪
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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
⊢ ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
have this₁ : Module.Finite ℤ 𝒪
Tactic: have := IsIntegralClosure.finite ℤ ℚ K 𝒪
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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 ℤ 𝒪
⊢ ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
have this₁ : CharZero 𝒪
Tactic: have := CharZero.of_module (R := 𝒪) K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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 𝒪
⊢ ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
have this₁ : IsGaloisGroup.{u_1, 0, u_2} Gal(K/ℚ) ℤ 𝒪
Tactic: have := IsGaloisGroup.of_isFractionRing Gal(K/ℚ) ℤ 𝒪 ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
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 : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
have obtain : ∀ (P : Ideal 𝒪) (w : P.IsMaximal) (hP' : ¬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'
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
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
⊢ ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
have 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
Tactic: obtain ⟨p, hp : _ = Ideal.span _⟩ := IsPrincipalIdealRing.principal (P.under ℤ)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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
p : ℤ
hp : Eq (α := Ideal ℤ) (Ideal.under ℤ P) (Ideal.span {p})
⊢ ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
have hp0 : p ≠ 0
Tactic: have hp0 : p ≠ 0 := fun hp0 ↦ Ideal.IsMaximal.ne_bot_of_isIntegral_int _
    (Ideal.eq_bot_of_comap_eq_bot (hp.trans (by aesop)))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
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
p : ℤ
hp : Eq (α := Ideal ℤ) (Ideal.under ℤ P) (Ideal.span {p})
hp0 : p ≠ 0
⊢ Prime p
have rw : Ideal.IsPrime (Ideal.under ℤ P)
Tactic: rw [← Ideal.span_singleton_prime hp0, ← hp]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
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
p : ℤ
hp : Eq (α := Ideal ℤ) (Ideal.under ℤ P) (Ideal.span {p})
hp0 : p ≠ 0
⊢ ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
have this₁ : Prime p
Tactic: have : Prime p := by rw [← Ideal.span_singleton_prime hp0, ← hp]; infer_instance