awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 : S
⊢ Eq.{u_1 + 1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) (span {r}) : Ideal R)
    (span (singleton (α := R) ((Algebra.intNorm R S : (a : S) → R) r : R)) : Ideal R)

Tactic:
spanNorm_singleton R

Premises used: Ideal.map, Ideal.spanNorm, Ideal.spanNorm_singleton, Submodule.span
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 : Ideal S
T : Type u_4
inst_11 : Semiring T
f : R →+* T
⊢ Eq.{u_4 + 1} (α := Ideal T) (map (R := R) f ((relNorm R : (a : Ideal S) → Ideal R) I))
    (span
      (Function.comp.{u_3 + 1, u_1 + 1, u_4 + 1} (β := R) (⇑f : (a : R) → T) (⇑(Algebra.intNorm R S) : (a : S) → R) ''
        (↑I : Set S)))

Tactic:
map_spanIntNorm R I f

Premises used: Ideal.map_spanIntNorm, Ideal.map, Ideal.spanNorm, Submodule.span
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 J : Ideal S
h : I ≤ J
⊢ LE.le.{u_1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R)
    ((relNorm R : (a : Ideal S) → Ideal R) J : Ideal R)

Tactic:
spanNorm_mono R h

Premises used: Ideal.spanNorm_mono, Set.Mem
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
T : Type u_4
inst_11 : CommRing T
inst_12 : IsDedekindDomain T
inst_13 : IsIntegrallyClosed T
inst_14 : Algebra R T
inst_15 : Module.Finite R T
inst_16 : IsTorsionFree R T
σ : S ≃ₐ[R] T
I : Ideal S
x_1 : R
h : Membership.mem (γ := Set R) ((⇑(Algebra.intNorm R T) : (a : T) → R) '' (↑(map σ I) : Set T)) x_1
x : T
hx₁ : x ∈ (↑(map σ I) : Set T)
hx₂ : (Algebra.intNorm R T : (a : T) → R) x = x_1
rwa : Membership.mem (α := S) I ((σ.toRingEquiv.symm : (a : T) → S) x : S)
rwa₁ rwa₂ rwa₃ rwa₄ : Membership.mem (γ := Ideal T) (map σ.toRingEquiv I) x
⊢ Membership.mem (α := S) (↑I : Set S) ((σ.toRingEquiv.symm : (a : T) → S) x : S)

Tactic:
rwa [SetLike.mem_coe, Ideal.symm_apply_mem_of_equiv_iff]

Premises used: Ideal.symm_apply_mem_of_equiv_iff, SetLike.mem_coe
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
T : Type u_4
inst_11 : CommRing T
inst_12 : IsDedekindDomain T
inst_13 : IsIntegrallyClosed T
inst_14 : Algebra R T
inst_15 : Module.Finite R T
inst_16 : IsTorsionFree R T
σ : S ≃ₐ[R] T
I : Ideal S
⊢ Eq.{u_1 + 1} (α := Ideal R) ((relNorm R : (a : Ideal T) → Ideal R) (map σ I) : Ideal R)
    ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R)

Tactic:
le_antisymm (relNorm_map_algEquiv_aux σ I) ?_

Premises used: _private.0.Ideal.relNorm_map_algEquiv_aux, le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
T : Type u_4
inst_11 : CommRing T
inst_12 : IsDedekindDomain T
inst_13 : IsIntegrallyClosed T
inst_14 : Algebra R T
inst_15 : Module.Finite R T
inst_16 : IsTorsionFree R T
σ : S ≃ₐ[R] T
I : Ideal S
refine :
  LE.le.{u_1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R)
    ((relNorm R : (a : Ideal T) → Ideal R) (map σ I) : Ideal R)
⊢ Eq.{u_1 + 1} (α := Ideal R) ((relNorm R : (a : Ideal T) → Ideal R) (map σ I) : Ideal R)
    ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R)

Tactic:
refine le_antisymm (relNorm_map_algEquiv_aux σ I) ?_

Premises used: _private.0.Ideal.relNorm_map_algEquiv_aux, le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
T : Type u_4
inst_11 : CommRing T
inst_12 : IsDedekindDomain T
inst_13 : IsIntegrallyClosed T
inst_14 : Algebra R T
inst_15 : Module.Finite R T
inst_16 : IsTorsionFree R T
σ : S ≃ₐ[R] T
I : Ideal S
⊢ LE.le.{u_1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) (map (R := T) σ.symm (map σ I)) : Ideal R)
    ((relNorm R : (a : Ideal T) → Ideal R) (map σ I) : Ideal R)

Tactic:
relNorm_map_algEquiv_aux σ.symm (I.map σ)

Premises used: AlgEquiv.symm, _private.0.Ideal.relNorm_map_algEquiv_aux, Ideal.map
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
T : Type u_4
inst_11 : CommRing T
inst_12 : IsDedekindDomain T
inst_13 : IsIntegrallyClosed T
inst_14 : Algebra R T
inst_15 : Module.Finite R T
inst_16 : IsTorsionFree R T
σ : S ≃ₐ[R] T
I : Ideal S
h : I = map (R := T) σ.symm (map σ I)
⊢ LE.le.{u_1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R)
    ((relNorm R : (a : Ideal T) → Ideal R) (map σ I) : Ideal R)

Tactic:
convert! relNorm_map_algEquiv_aux σ.symm (I.map σ)

Premises used: AlgEquiv.symm, _private.0.Ideal.relNorm_map_algEquiv_aux, Ideal.map
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
T : Type u_4
inst_11 : CommRing T
inst_12 : IsDedekindDomain T
inst_13 : IsIntegrallyClosed T
inst_14 : Algebra R T
inst_15 : Module.Finite R T
inst_16 : IsTorsionFree R T
σ : S ≃ₐ[R] T
I : Ideal S
h : I = map (R := T) (↑σ.symm : T →ₐ[R] S) (map (↑σ : S →ₐ[R] T) I)
⊢ I = map (R := T) σ.symm (map σ I)

Tactic:
change I = map σ.symm.toAlgHom (map σ.toAlgHom I)

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, Ideal.map
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
T : Type u_4
inst_11 : CommRing T
inst_12 : IsDedekindDomain T
inst_13 : IsIntegrallyClosed T
inst_14 : Algebra R T
inst_15 : Module.Finite R T
inst_16 : IsTorsionFree R T
σ : S ≃ₐ[R] T
I : Ideal S
⊢ I = map (R := T) (↑σ.symm : T →ₐ[R] S) (map (↑σ : S →ₐ[R] T) I)

Tactic:
simp [map_mapₐ]

Premises used: Ideal.map_mapₐ
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
T : Type u_4
inst_11 : CommRing T
inst_12 : IsDedekindDomain T
inst_13 : IsIntegrallyClosed T
inst_14 : Algebra R T
inst_15 : Module.Finite R T
inst_16 : IsTorsionFree R T
σ : S ≃ₐ[R] T
I : Ideal T
⊢ Eq.{u_1 + 1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) (comap σ I) : Ideal R)
    ((relNorm R : (a : Ideal T) → Ideal R) I : Ideal R)

Tactic:
map_symm σ.toRingEquiv ▸ relNorm_map_algEquiv σ.symm I

Premises used: AlgEquiv.symm, Eq.rec, Ideal.map_symm, AlgEquiv.toRingEquiv, Ideal.comap, Ideal.relNorm_map_algEquiv
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
G : Type u_4
inst_11 : Group G
inst_12 : MulSemiringAction G S
inst_13 : SMulCommClass G R S
g : G
I : Ideal S
⊢ Eq.{u_1 + 1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) (g • I) : Ideal R)
    ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R)

Tactic:
relNorm_map_algEquiv (toAlgEquiv R S g) I

Premises used: MulSemiringAction.toAlgEquiv, MulSemiringAction.toRingHom, Ideal.map, Ideal.relNorm_map_algEquiv
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 : Ideal S
⊢ LE.le.{u_1} (α := Ideal R) ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R)
    (comap (F := R →+* S) (algebraMap R S) I : Ideal R)

Tactic:
spanNorm_le_comap R I

Premises used: Set.Mem, Ideal.spanNorm_le_comap
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
T : Type u_4
inst_11 : CommRing T
inst_12 : IsDedekindDomain T
inst_13 : IsIntegrallyClosed T
inst_14 : Algebra R T
inst_15 : Algebra T S
inst_16 : IsScalarTower R T S
inst_17 : Module.Finite R T
inst_18 : Module.Finite T S
inst_19 : IsTorsionFree R T
inst_20 : IsTorsionFree T S
I : Ideal S
⊢ Eq.{u_1 + 1} (α := Ideal R)
    ((relNorm R : (a : Ideal T) → Ideal R) ((relNorm T : (a : Ideal S) → Ideal T) I) : Ideal R)
    ((relNorm R : (a : Ideal S) → Ideal R) I : Ideal R)

Tactic:
spanNorm_spanNorm _ _ _

Premises used: Ideal.spanNorm_spanNorm, Set.Mem, setOf, Ideal.map, Ideal.spanNorm, Submodule.span
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 : Ideal R
⊢ spanNorm.{u_1, u_3} R (S := S) (map (F := R →+* S) (algebraMap R S) I) =
    I ^ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)

Tactic:
eq_of_localization_maximal (fun P hPd ↦ ?_)

Premises used: Ideal.eq_of_localization_maximal
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 : Ideal R
refine :
  ∀ (P : Ideal R) (hPd : P.IsMaximal),
    Eq (α := Ideal (Localization.AtPrime P))
      (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P))
        (spanNorm.{u_1, u_3} R (S := S) (map (F := R →+* S) (algebraMap R S) I)))
      (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P))
        (I ^ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)))
⊢ spanNorm.{u_1, u_3} R (S := S) (map (F := R →+* S) (algebraMap R S) I) =
    I ^ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)

Tactic:
refine eq_of_localization_maximal (fun P hPd ↦ ?_)

Premises used: Ideal.eq_of_localization_maximal
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
rw :
  Eq (α := Ideal (Localization.AtPrime P))
    (span
      {(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)))})
    (span
      {HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
          (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))})
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P))
      (spanNorm.{u_1, u_3} R (S := S) (map (F := R →+* S) (algebraMap R S) I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P))
      (I ^ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)))

Tactic:
rw [← spanIntNorm_localization R _ _ P.primeCompl_le_nonZeroDivisors (Localization P'),
      Ideal.map_pow, I.map_map, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R Rₚ,
      ← I.map_map, ← (I.map _).span_singleton_generator, Ideal.map_span, Set.image_singleton,
      spanNorm_singleton, Ideal.span_singleton_pow]

Premises used: Set.image_singleton, Ideal.spanIntNorm_localization, Ideal.map_span, Ideal.span_singleton_generator, Ideal.map, Localization, Ideal.map_map, Ideal.spanNorm_singleton, IsScalarTower.algebraMap_eq, Ideal.primeCompl_le_nonZeroDivisors, Ideal.map_pow, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 :
  (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))) =
    HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
      (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (span
      {(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)))})
    (span
      {HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
          (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))})

Tactic:
congr 2
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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)
    ((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)
⊢ (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))) =
    HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
      (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))

Tactic:
apply IsFractionRing.injective Rₚ K

Premises used: IsFractionRing.injective
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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)
rw₂ 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)
⊢ (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))

Tactic:
rw [← relNorm_algebraMap, Ideal.map_map, IsScalarTower.algebraMap_eq R' R S]

Premises used: Ideal.relNorm_algebraMap, Ideal.map_map, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
neg : ∀ (hp : ¬p = ⊥), ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s
⊢ ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s

Tactic:
by_cases hp : p = ⊥
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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

Tactic:
⟨1, ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 = ⊥
pos : (relNorm R : (a : Ideal S) → Ideal R) P = HPow.hPow (β := ℕ) p 1
⊢ ∃ (s : ℕ), (relNorm R : (a : Ideal S) → Ideal R) P = p ^ s

Tactic:
refine ⟨1, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 = ⊥
⊢ LiesOver.{u_1, u_3} (A := R) P ⊥

Tactic:
have : P.LiesOver ⊥ := hp ▸ hPp
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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
pos₃ pos₄ : Eq.{u_1 + 1} (α := Ideal R) ⊥ ⊥
⊢ (relNorm R : (a : Ideal S) → Ideal R) P = HPow.hPow (β := ℕ) p 1

Tactic:
rw [hp, eq_bot_of_liesOver_bot R P, relNorm_bot, bot_pow (one_ne_zero)]

Premises used: Ideal.bot_pow, Ideal.relNorm_bot, one_ne_zero, Ideal.eq_bot_of_liesOver_bot
-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
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 = ⊥
⊢ 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