awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
I P : Ideal R
hPd : P.IsMaximal
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
K : Type u_1 := FractionRing R
e_s :
  Eq (α := K)
    ((Algebra.norm K : (a : FractionRing S) → K)
        ((algebraMap (Localization (M := S) P') (FractionRing S) : (a : Localization P') → FractionRing S)
          ((algebraMap Rₚ (Localization (M := S) P') : (a : Rₚ) → Localization P')
            (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I)))) :
      K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
          (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))) :
      K)
⊢ Eq (α := K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
            (a : Localization P') → Localization.AtPrime P)
          ((algebraMap Rₚ (Localization (M := S) P') : (a : Rₚ) → Localization P')
            (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I)))) :
      K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
          (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))) :
      K)
have e_s₁ : Eq (α := K)
  ((Algebra.norm K : (a : FractionRing S) → K)
      ((algebraMap Rₚ (FractionRing S) : (a : Rₚ) → FractionRing S)
        (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))) :
    K)
  ((algebraMap Rₚ K : (a : Rₚ) → K)
      (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
        (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))) :
    K)
Tactic: rw [Algebra.algebraMap_intNorm (L := FractionRing S), ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply Rₚ K, Algebra.norm_algebraMap, map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
I P : Ideal R
hPd : P.IsMaximal
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
K : Type u_1 := FractionRing R
e_s :
  Eq (α := K)
    ((Algebra.norm K : (a : FractionRing S) → K)
        ((algebraMap (Localization (M := S) P') (FractionRing S) : (a : Localization P') → FractionRing S)
          ((algebraMap Rₚ (Localization (M := S) P') : (a : Rₚ) → Localization P')
            (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I)))) :
      K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
          (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))) :
      K)
e_s₁ :
  Eq (α := K)
    ((Algebra.norm K : (a : FractionRing S) → K)
        ((algebraMap Rₚ (FractionRing S) : (a : Rₚ) → FractionRing S)
          (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))) :
      K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
          (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))) :
      K)
⊢ Eq (α := K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
            (a : Localization P') → Localization.AtPrime P)
          ((algebraMap Rₚ (Localization (M := S) P') : (a : Rₚ) → Localization P')
            (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I)))) :
      K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
          (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))) :
      K)
have e_s₂ : Eq (α := K)
  ((Algebra.norm K : (a : FractionRing S) → K)
      ((algebraMap K (FractionRing S) : (a : K) → FractionRing S)
        ((algebraMap Rₚ K : (a : Rₚ) → K) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I)))) :
    K)
  ((algebraMap Rₚ K : (a : Rₚ) → K)
      (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
        (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))) :
    K)
Tactic: rw [Algebra.algebraMap_intNorm (L := FractionRing S), ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply Rₚ K, Algebra.norm_algebraMap, map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
I P : Ideal R
hPd : P.IsMaximal
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
K : Type u_1 := FractionRing R
e_s :
  Eq (α := K)
    ((Algebra.norm K : (a : FractionRing S) → K)
        ((algebraMap (Localization (M := S) P') (FractionRing S) : (a : Localization P') → FractionRing S)
          ((algebraMap Rₚ (Localization (M := S) P') : (a : Rₚ) → Localization P')
            (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I)))) :
      K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
          (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))) :
      K)
e_s₁ :
  Eq (α := K)
    ((Algebra.norm K : (a : FractionRing S) → K)
        ((algebraMap Rₚ (FractionRing S) : (a : Rₚ) → FractionRing S)
          (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))) :
      K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
          (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))) :
      K)
e_s₂ :
  Eq (α := K)
    ((Algebra.norm K : (a : FractionRing S) → K)
        ((algebraMap K (FractionRing S) : (a : K) → FractionRing S)
          ((algebraMap Rₚ K : (a : Rₚ) → K) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I)))) :
      K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
          (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))) :
      K)
⊢ Eq (α := K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
            (a : Localization P') → Localization.AtPrime P)
          ((algebraMap Rₚ (Localization (M := S) P') : (a : Rₚ) → Localization P')
            (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I)))) :
      K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
          (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))) :
      K)
have e_s₃ : HPow.hPow (α := K) ((algebraMap Rₚ K : (a : Rₚ) → K) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I)))
    (finrank.{u_1, u_3} K (FractionRing S)) =
  (algebraMap Rₚ K : (a : Rₚ) → K)
    (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
      (finrank.{u_1, u_3} (FractionRing R) (FractionRing S)))
Tactic: rw [Algebra.algebraMap_intNorm (L := FractionRing S), ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply Rₚ K, Algebra.norm_algebraMap, map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
R' : Type u_4
inst_11 : CommRing R'
I : Ideal R'
inst_12 : Algebra R' R
inst_13 : Algebra R' S
inst_14 : IsScalarTower R' R S
⊢ (relNorm R : (a : Ideal S) → Ideal R) (map (F := R' →+* S) (algebraMap R' S) I) =
    HPow.hPow (α := Ideal R) (map (F := R' →+* R) (algebraMap R' R) I)
      (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
have rw : Eq.{u_1 + 1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) (map (F := R' →+* S) (algebraMap R' S) I) : Ideal R)
  ((relNorm R : (a : Ideal S) → Ideal R)
      (map (R := R) (F := R →+* S) (algebraMap R S) (map (F := R' →+* R) (algebraMap R' R) I)) :
    Ideal R)
Tactic: rw [← relNorm_algebraMap, Ideal.map_map, IsScalarTower.algebraMap_eq R' R S]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
R' : Type u_4
inst_11 : CommRing R'
I : Ideal R'
inst_12 : Algebra R' R
inst_13 : Algebra R' S
inst_14 : IsScalarTower R' R S
rw :
  Eq.{u_1 + 1} (α := Ideal R)
    ((relNorm R : (a : Ideal S) → Ideal R) (map (F := R' →+* S) (algebraMap R' S) I) : Ideal R)
    ((relNorm R : (a : Ideal S) → Ideal R)
        (map (R := R) (F := R →+* S) (algebraMap R S) (map (F := R' →+* R) (algebraMap R' R) I)) :
      Ideal R)
⊢ (relNorm R : (a : Ideal S) → Ideal R) (map (F := R' →+* S) (algebraMap R' S) I) =
    HPow.hPow (α := Ideal R) (map (F := R' →+* R) (algebraMap R' R) I)
      (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
have rw₁ : Eq.{u_1 + 1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) (map (F := R' →+* S) (algebraMap R' S) I) : Ideal R)
  ((relNorm R : (a : Ideal S) → Ideal R)
      (map (F := R' →+* S) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R S) (algebraMap R' R)) I) :
    Ideal R)
Tactic: rw [← relNorm_algebraMap, Ideal.map_map, IsScalarTower.algebraMap_eq R' R S]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
R' : Type u_4
inst_11 : CommRing R'
I : Ideal R'
inst_12 : Algebra R' R
inst_13 : Algebra R' S
inst_14 : IsScalarTower R' R S
rw :
  Eq.{u_1 + 1} (α := Ideal R)
    ((relNorm R : (a : Ideal S) → Ideal R) (map (F := R' →+* S) (algebraMap R' S) I) : Ideal R)
    ((relNorm R : (a : Ideal S) → Ideal R)
        (map (R := R) (F := R →+* S) (algebraMap R S) (map (F := R' →+* R) (algebraMap R' R) I)) :
      Ideal R)
rw₁ :
  Eq.{u_1 + 1} (α := Ideal R)
    ((relNorm R : (a : Ideal S) → Ideal R) (map (F := R' →+* S) (algebraMap R' S) I) : Ideal R)
    ((relNorm R : (a : Ideal S) → Ideal R)
        (map (F := R' →+* S) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R S) (algebraMap R' R))
          I) :
      Ideal R)
⊢ (relNorm R : (a : Ideal S) → Ideal R) (map (F := R' →+* S) (algebraMap R' S) I) =
    HPow.hPow (α := Ideal R) (map (F := R' →+* R) (algebraMap R' R) I)
      (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
have rw₂ : Eq.{u_1 + 1} (α := Ideal R)
  ((relNorm R : (a : Ideal S) → Ideal R)
      (map (F := R' →+* S) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R S) (algebraMap R' R)) I) :
    Ideal R)
  ((relNorm R : (a : Ideal S) → Ideal R)
      (map (F := R' →+* S) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R S) (algebraMap R' R)) I) :
    Ideal R)
Tactic: rw [← relNorm_algebraMap, Ideal.map_map, IsScalarTower.algebraMap_eq R' R S]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsPrime
⊢ ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
have pos : ∀ (hp : p = ⊥), ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
Tactic: by_cases hp : p = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsPrime
pos : ∀ (hp : p = ⊥), ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
⊢ ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
have neg : ∀ (hp : ¬p = ⊥), ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
Tactic: by_cases hp : p = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsPrime
hp : p = ⊥
⊢ ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
have pos : (relNorm R : (a : Ideal S) → Ideal R) P = HPow.hPow (β := ℕ) p 1
Tactic: refine ⟨1, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsPrime
hp : p = ⊥
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = HPow.hPow (β := ℕ) p 1
have this : LiesOver.{u_1, u_3} (A := R) P ⊥
Tactic: have : P.LiesOver ⊥ := hp ▸ hPp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsPrime
hp : p = ⊥
this : LiesOver.{u_1, u_3} (A := R) P ⊥
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = HPow.hPow (β := ℕ) p 1
have pos : (relNorm R : (a : Ideal S) → Ideal R) P = HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 1
Tactic: rw [hp, eq_bot_of_liesOver_bot R P, relNorm_bot, bot_pow (one_ne_zero)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsPrime
hp : p = ⊥
this : LiesOver.{u_1, u_3} (A := R) P ⊥
pos : (relNorm R : (a : Ideal S) → Ideal R) P = HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 1
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = HPow.hPow (β := ℕ) p 1
have pos₁ : (relNorm R : (a : Ideal S) → Ideal R) ⊥ = HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 1
Tactic: rw [hp, eq_bot_of_liesOver_bot R P, relNorm_bot, bot_pow (one_ne_zero)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsPrime
hp : p = ⊥
this : LiesOver.{u_1, u_3} (A := R) P ⊥
pos : (relNorm R : (a : Ideal S) → Ideal R) P = HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 1
pos₁ : (relNorm R : (a : Ideal S) → Ideal R) ⊥ = HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 1
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = HPow.hPow (β := ℕ) p 1
have pos₂ : ⊥ = HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 1
Tactic: rw [hp, eq_bot_of_liesOver_bot R P, relNorm_bot, bot_pow (one_ne_zero)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsPrime
hp : p = ⊥
this : LiesOver.{u_1, u_3} (A := R) P ⊥
pos : (relNorm R : (a : Ideal S) → Ideal R) P = HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 1
pos₁ : (relNorm R : (a : Ideal S) → Ideal R) ⊥ = HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 1
pos₂ : ⊥ = HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 1
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = HPow.hPow (β := ℕ) p 1
have pos₃ : Eq.{u_1 + 1} (α := Ideal R) ⊥ ⊥
Tactic: rw [hp, eq_bot_of_liesOver_bot R P, relNorm_bot, bot_pow (one_ne_zero)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsPrime
hp : ¬p = ⊥
⊢ ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
have h : LE.le.{u_1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) (map (F := R →+* S) (algebraMap R S) p) : Ideal R)
  ((relNorm R : (a : Ideal S) → Ideal R) P : Ideal R)
Tactic: have h : relNorm R (map (algebraMap R S) p) ≤ relNorm R P :=
    relNorm_mono _ <| map_le_iff_le_comap.mpr <| le_of_eq <| (liesOver_iff _ _).mp hPp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsPrime
hp : ¬p = ⊥
h :
  LE.le.{u_1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) (map (F := R →+* S) (algebraMap R S) p) : Ideal R)
    ((relNorm R : (a : Ideal S) → Ideal R) P : Ideal R)
⊢ ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
have h₁ : ∃ i ≤ finrank.{u_1, u_3} (FractionRing R) (FractionRing S), Associated ((relNorm R : (a : Ideal S) → Ideal R) P) (p ^ i)
Tactic: rw [relNorm_algebraMap S, ← dvd_iff_le, dvd_prime_pow (prime_of_isPrime hp inferInstance)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsPrime
hp : ¬p = ⊥
h :
  ∃ i ≤ finrank.{u_1, u_3} (FractionRing R) (FractionRing S),
    Associated ((relNorm R : (a : Ideal S) → Ideal R) P) (p ^ i)
⊢ ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
have neg : ∀ s ≤ finrank.{u_1, u_3} (FractionRing R) (FractionRing S),
  ∀ (hs : Associated ((relNorm R : (a : Ideal S) → Ideal R) P) (p ^ s)),
    ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
Tactic: obtain ⟨s, _, hs⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsPrime
hp : ¬p = ⊥
s : ℕ
left : s ≤ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)
hs : Associated ((relNorm R : (a : Ideal S) → Ideal R) P) (p ^ s)
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
have rwa : ∀ (hs : (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
Tactic: rwa [associated_iff_eq] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsMaximal
inst_12 : P.IsPrime
inst_13 : IsGalois.{u_1, u_3} (FractionRing R) (FractionRing S)
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
have this₁ : IsGaloisGroup G R S
Tactic: have := IsGaloisGroup.of_isFractionRing G R S (FractionRing R) (FractionRing S)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst_11 : p.IsMaximal
inst_12 : P.IsPrime
inst_13 : IsGalois.{u_1, u_3} (FractionRing R) (FractionRing S)
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this_1 : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
have pos : ∀ (hp : p = ⊥), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ p.inertiaDeg P
Tactic: by_cases hp : p = ⊥