awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
inst_2 : IsGalois.{0, u_3} ℚ ↥K₁
h : IsCoprime (discr.{u_3} ↥K₁) (discr.{u_3} ↥K₂)
⊢ K₁ ⊓ K₂ = ⊥
have h₁ : IsUnit (discr.{u_3} ↥(K₁ ⊓ K₂))
Tactic: suffices IsUnit (discr ↥(K₁ ⊓ K₂)) by
    contrapose! this
    have : 1 < Module.finrank ℚ ↥(K₁ ⊓ K₂) := by
      refine Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨Module.finrank_pos.ne', ?_⟩
      rwa [ne_eq, ← IntermediateField.finrank_eq_one_iff] at this
    exact Int.isUnit_iff_abs_eq.not.mpr <| by linarith [abs_discr_gt_two this]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (hypothesis)
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 ↥K₁) (F := 𝓞 ↥K₁ →+* 𝓞 L) (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (R := 𝓞 ↥K₂) (F := 𝓞 ↥K₂ →+* 𝓞 L) (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
⊢ (discr L).natAbs =
    (discr.{u_3} ↥K₁).natAbs ^ finrank.{0, u_3} ℚ ↥K₂ * (discr.{u_3} ↥K₂).natAbs ^ finrank.{0, u_3} ℚ ↥K₁
have h_main : (discr L).natAbs =
  HMul.hMul (α := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 L)) → ℕ) (differentIdeal (𝓞 ↥K₂) (𝓞 L)) : ℕ)
    ((discr.{u_3} ↥K₂).natAbs ^ finrank (↥K₂) L)
Tactic: have h_main := natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow K₂ (𝓞 K₂) L (𝓞 L)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 ↥K₁) (F := 𝓞 ↥K₁ →+* 𝓞 L) (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (R := 𝓞 ↥K₂) (F := 𝓞 ↥K₂ →+* 𝓞 L) (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main :
  (discr L).natAbs =
    HMul.hMul (α := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 L)) → ℕ) (differentIdeal (𝓞 ↥K₂) (𝓞 L)) : ℕ)
      ((discr.{u_3} ↥K₂).natAbs ^ finrank (↥K₂) L)
⊢ K₂.LinearDisjoint ↥K₁
have rwa : K₁.LinearDisjoint ↥K₂
Tactic: rwa [linearDisjoint_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 ↥K₁) (F := 𝓞 ↥K₁ →+* 𝓞 L) (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (R := 𝓞 ↥K₂) (F := 𝓞 ↥K₂ →+* 𝓞 L) (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main :
  (discr L).natAbs =
    HMul.hMul (α := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 L)) → ℕ) (differentIdeal (𝓞 ↥K₂) (𝓞 L)) : ℕ)
      ((discr.{u_3} ↥K₂).natAbs ^ finrank (↥K₂) L)
⊢ (discr L).natAbs =
    (discr.{u_3} ↥K₁).natAbs ^ finrank.{0, u_3} ℚ ↥K₂ * (discr.{u_3} ↥K₂).natAbs ^ finrank.{0, u_3} ℚ ↥K₁
have rwa : ∀
  (h_main :
    (discr L).natAbs =
      (discr.{u_3} ↥K₁).natAbs ^ finrank.{u_3, u_3} (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) *
        (discr.{u_3} ↥K₂).natAbs ^ finrank.{0, u_3} ℚ ↥K₁),
  Eq (α := FractionRing (𝓞 ↥K₁) →+* L)
    (@RingHom.comp _ ↥K₁ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥K₁) L)
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 ↥K₁) ↥K₁))))
    (RingHom.comp (β := FractionRing (𝓞 L)) (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 L) L)))
      (algebraMap (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L))))
Tactic: rwa [differentIdeal_eq_map_differentIdeal ℤ (𝓞 L) (𝓞 K₂) (𝓞 K₁) (F₁ := K₂) (F₂ := K₁)
    (by rwa [linearDisjoint_comm]) (by rwa [sup_comm]) (by rwa [isCoprime_comm]),
    Ideal.absNorm_algebraMap, absNorm_differentIdeal K₁, h₁.finrank_right_eq_finrank h₂,
    Algebra.finrank_eq_of_equiv_equiv (FractionRing.algEquiv _ K₁).toRingEquiv
    (FractionRing.algEquiv _ L).toRingEquiv, h₁.finrank_left_eq_finrank h₂] at h_main
Cleared hypotheses: h_main
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 ↥K₁) (F := 𝓞 ↥K₁ →+* 𝓞 L) (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (R := 𝓞 ↥K₂) (F := 𝓞 ↥K₂ →+* 𝓞 L) (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main :
  (discr L).natAbs =
    (discr.{u_3} ↥K₁).natAbs ^ finrank.{u_3, u_3} (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) *
      (discr.{u_3} ↥K₂).natAbs ^ finrank.{0, u_3} ℚ ↥K₁
⊢ Eq (α := FractionRing (𝓞 ↥K₁) →+* L)
    (@RingHom.comp _ ↥K₁ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥K₁) L)
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 ↥K₁) ↥K₁))))
    (RingHom.comp (β := FractionRing (𝓞 L)) (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 L) L)))
      (algebraMap (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L))))
have a : ∀ (x : FractionRing (𝓞 ↥K₁)),
  Eq (α := L)
    ((@RingHom.comp _ ↥K₁ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥K₁) L)
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 ↥K₁) ↥K₁))) :
          (a : FractionRing (𝓞 ↥K₁)) → L)
        x :
      L)
    ((RingHom.comp (β := FractionRing (𝓞 L))
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 L) L)))
            (algebraMap (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L))) :
          (a : FractionRing (𝓞 ↥K₁)) → L)
        x :
      L)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (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
p : ℤ
hp : Prime p
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (A := ℤ) (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P
have this : IsDomain 𝒪
Tactic: have := (IsIntegralClosure.algebraMap_injective 𝒪 ℤ K).isDomain
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (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
p : ℤ
hp : Prime p
this : IsDomain 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (A := ℤ) (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P
have this₁ : IsDedekindDomain 𝒪
Tactic: have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (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
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this : IsDedekindDomain 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (A := ℤ) (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P
have this₁ : IsFractionRing 𝒪 K
Tactic: have := IsIntegralClosure.isFractionRing_of_finite_extension ℤ ℚ K 𝒪
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (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
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this : IsFractionRing 𝒪 K
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (A := ℤ) (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P
have this₁ : Module.Finite ℤ 𝒪
Tactic: have := IsIntegralClosure.finite ℤ ℚ K 𝒪
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (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
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this : Module.Finite ℤ 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (A := ℤ) (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P
have this₁ : CharZero 𝒪
Tactic: have := CharZero.of_module (R := 𝒪) K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (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
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this : CharZero 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (A := ℤ) (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P
have simp_rw : ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪), P.IsMaximal → P.LiesOver (A := ℤ) (Ideal.span {p}) → ¬P ∣ differentIdeal ℤ 𝒪
Tactic: simp_rw [← not_dvd_differentIdeal_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (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
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this : CharZero 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪), P.IsMaximal → P.LiesOver (A := ℤ) (Ideal.span {p}) → ¬P ∣ differentIdeal ℤ 𝒪
have contrapose! : p ∣ discr K ↔ ∃ (P : Ideal 𝒪), P.IsMaximal ∧ P.LiesOver (A := ℤ) (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (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
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this : CharZero 𝒪
⊢ p ∣ discr K ↔ ∃ (P : Ideal 𝒪), P.IsMaximal ∧ P.LiesOver (A := ℤ) (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪
have mp : p ∣ discr K → ∃ (P : Ideal 𝒪), P.IsMaximal ∧ P.LiesOver (A := ℤ) (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (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
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 ℤ 𝒪
⊢ p ∣ discr K ↔ ∃ (P : Ideal 𝒪), P.IsMaximal ∧ P.LiesOver (A := ℤ) (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪
have mpr : (∃ (P : Ideal 𝒪), P.IsMaximal ∧ P.LiesOver (A := ℤ) (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪) → p ∣ discr K
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (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
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 𝒪), P.IsMaximal ∧ P.LiesOver (A := ℤ) (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪
have h₁ : p ∣ (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : ℤ)
Tactic: rw [← Int.dvd_natAbs, ← absNorm_differentIdeal K 𝒪] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (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
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 𝒪), P.IsMaximal ∧ P.LiesOver (A := ℤ) (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪
have 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 ℤ 𝒪
Tactic: obtain ⟨P, hP, h₁, h₂⟩ := Ideal.exists_isMaximal_dvd_of_dvd_absNorm hp _ h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (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
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 ℤ 𝒪
⊢ p ∣ discr K
have this₁ : 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'')
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (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
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 ∣ discr K
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (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
p : ℤ
hp : Prime p
⊢ ¬p ∣ discr K ↔ ∀ (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.Discriminant.Different (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
p : ℤ
hp : Prime p
this : IsDomain 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (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.Discriminant.Different (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
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this : IsDedekindDomain 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (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.Discriminant.Different (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
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this : CharZero 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → Algebra.IsUnramifiedAt ℤ P
have 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
Tactic: rw [NumberField.not_dvd_discr_iff_forall_liesOver K 𝒪 hp]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.EquivReindex (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Fintype.card.{u_1} (K →+* ℂ) = Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K))
have rw : finrank ℚ K = Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K))
Tactic: rw [Embeddings.card, ← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.EquivReindex (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : finrank ℚ K = Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K))
⊢ Fintype.card.{u_1} (K →+* ℂ) = Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K))
have rw₁ : finrank ℚ K = finrank.{0, u_1} ℤ (𝓞 K)
Tactic: rw [Embeddings.card, ← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.EquivReindex (goal)
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)
⊢ Fintype.card.{u_1} (K →+* ℂ) = Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K))
have rw₂ : finrank ℚ K = finrank ℚ K
Tactic: rw [Embeddings.card, ← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.EquivReindex (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.EquivReindex (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 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))
have a : ∀ (i j : K →+* ℂ),
  Eq (α := ℂ) (Matrix.map (basisMatrix K) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) i j)
    ((reindex (Equiv.refl (K →+* ℂ)) (Function.Involutive.toPerm ComplexEmbedding.conjugate sorry) :
        (a : Matrix (K →+* ℂ) (K →+* ℂ) ℂ) → Matrix (K →+* ℂ) (K →+* ℂ) ℂ)
      (basisMatrix K) i j)
Tactic: ext
-- 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 →+* ℂ)
⊢ det (n := K →+* ℂ) (basisMatrix K) ≠ 0
have 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
Tactic: rw [basisMatrix_eq_embeddingsMatrixReindex, ← pow_ne_zero_iff two_ne_zero]
-- 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 →+* ℂ)
⊢ 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
have 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))
Tactic: convert!
    (map_ne_zero_iff _ (algebraMap ℚ ℂ).injective).mpr
      (Algebra.discr_not_zero_of_basis ℚ (integralBasis K))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.EquivReindex (goal)
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 (ι := ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
        (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K))
have 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))))
Tactic: rw [← Algebra.discr_reindex ℚ (integralBasis K) (equivReindex K).symm]