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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
inst_19 : IsDedekindDomain R
inst_20 : IsDedekindDomain T
inst_21 : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP_1 : P.IsMaximal
hP : ¬P = ⊥
Rₚ : Type u_1 := Localization.AtPrime P
Tₚ : Type u_4 := Localization (M := T) (algebraMapSubmonoid T P.primeCompl)
Sₚ : Type u_3 := Localization (M := S) (algebraMapSubmonoid S P.primeCompl)
this : NeZero P
h : LE.le (α := Submonoid T) (algebraMapSubmonoid T P.primeCompl) T⁰
neg :
  Eq (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (S := Tₚ) (map (F := T →+* Tₚ) (algebraMap T Tₚ) (spanNorm T I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (spanNorm T I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
have neg₁ : Eq (α := Ideal (Localization.AtPrime P))
  (spanNorm (Localization.AtPrime P) (spanNorm Tₚ (S := Sₚ) (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)))
  (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
Tactic: rw [← spanIntNorm_localization R (spanNorm T I) _ (primeCompl_le_nonZeroDivisors P) Tₚ,
    ← spanIntNorm_localization T (Rₘ := Tₚ) I _ h Sₚ, ← spanIntNorm_localization R (Rₘ := Rₚ) I _
    (primeCompl_le_nonZeroDivisors P) Sₚ, ← (I.map _).span_singleton_generator, spanNorm_singleton,
    spanNorm_singleton, intNorm_intNorm, spanNorm_singleton]
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
inst_19 : IsDedekindDomain R
inst_20 : IsDedekindDomain T
inst_21 : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP_1 : P.IsMaximal
hP : ¬P = ⊥
Rₚ : Type u_1 := Localization.AtPrime P
Tₚ : Type u_4 := Localization (M := T) (algebraMapSubmonoid T P.primeCompl)
Sₚ : Type u_3 := Localization (M := S) (algebraMapSubmonoid S P.primeCompl)
this : NeZero P
h : LE.le (α := Submonoid T) (algebraMapSubmonoid T P.primeCompl) T⁰
neg :
  Eq (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (S := Tₚ) (map (F := T →+* Tₚ) (algebraMap T Tₚ) (spanNorm T I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
neg₁ :
  Eq (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (spanNorm Tₚ (S := Sₚ) (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (spanNorm T I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
have neg₂ : Eq (α := Ideal (Localization.AtPrime P))
  (spanNorm (Localization.AtPrime P) (spanNorm Tₚ (S := Sₚ) (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)))
  (spanNorm Rₚ (S := Sₚ) (map (F := S →+* Sₚ) (algebraMap S Sₚ) I))
Tactic: rw [← spanIntNorm_localization R (spanNorm T I) _ (primeCompl_le_nonZeroDivisors P) Tₚ,
    ← spanIntNorm_localization T (Rₘ := Tₚ) I _ h Sₚ, ← spanIntNorm_localization R (Rₘ := Rₚ) I _
    (primeCompl_le_nonZeroDivisors P) Sₚ, ← (I.map _).span_singleton_generator, spanNorm_singleton,
    spanNorm_singleton, intNorm_intNorm, spanNorm_singleton]
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
inst_19 : IsDedekindDomain R
inst_20 : IsDedekindDomain T
inst_21 : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP_1 : P.IsMaximal
hP : ¬P = ⊥
Rₚ : Type u_1 := Localization.AtPrime P
Tₚ : Type u_4 := Localization (M := T) (algebraMapSubmonoid T P.primeCompl)
Sₚ : Type u_3 := Localization (M := S) (algebraMapSubmonoid S P.primeCompl)
this : NeZero P
h : LE.le (α := Submonoid T) (algebraMapSubmonoid T P.primeCompl) T⁰
neg :
  Eq (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (S := Tₚ) (map (F := T →+* Tₚ) (algebraMap T Tₚ) (spanNorm T I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
neg₁ :
  Eq (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (spanNorm Tₚ (S := Sₚ) (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
neg₂ :
  Eq (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (spanNorm Tₚ (S := Sₚ) (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)))
    (spanNorm Rₚ (S := Sₚ) (map (F := S →+* Sₚ) (algebraMap S Sₚ) I))
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (spanNorm T I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
have neg₃ : Eq (α := Ideal (Localization.AtPrime P))
  (spanNorm (Localization.AtPrime P)
    (spanNorm Tₚ (S := Sₚ) (span {IsPrincipal.generator (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)})))
  (spanNorm Rₚ (S := Sₚ) (span {IsPrincipal.generator (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)}))
Tactic: rw [← spanIntNorm_localization R (spanNorm T I) _ (primeCompl_le_nonZeroDivisors P) Tₚ,
    ← spanIntNorm_localization T (Rₘ := Tₚ) I _ h Sₚ, ← spanIntNorm_localization R (Rₘ := Rₚ) I _
    (primeCompl_le_nonZeroDivisors P) Sₚ, ← (I.map _).span_singleton_generator, spanNorm_singleton,
    spanNorm_singleton, intNorm_intNorm, spanNorm_singleton]
-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
inst_19 : IsDedekindDomain R
inst_20 : IsDedekindDomain T
inst_21 : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP_1 : P.IsMaximal
hP : ¬P = ⊥
Rₚ : Type u_1 := Localization.AtPrime P
Tₚ : Type u_4 := Localization (M := T) (algebraMapSubmonoid T P.primeCompl)
Sₚ : Type u_3 := Localization (M := S) (algebraMapSubmonoid S P.primeCompl)
this : NeZero P
h : LE.le (α := Submonoid T) (algebraMapSubmonoid T P.primeCompl) T⁰
neg :
  Eq (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (S := Tₚ) (map (F := T →+* Tₚ) (algebraMap T Tₚ) (spanNorm T I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
neg₁ :
  Eq (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (spanNorm Tₚ (S := Sₚ) (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
neg₂ :
  Eq (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (spanNorm Tₚ (S := Sₚ) (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)))
    (spanNorm Rₚ (S := Sₚ) (map (F := S →+* Sₚ) (algebraMap S Sₚ) I))
neg₃ :
  Eq (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P)
      (spanNorm Tₚ (S := Sₚ) (span {IsPrincipal.generator (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)})))
    (spanNorm Rₚ (S := Sₚ) (span {IsPrincipal.generator (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)}))
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (spanNorm T I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
have neg₄ : Eq (α := Ideal (Localization.AtPrime P))
  (spanNorm (Localization.AtPrime P) (S := Tₚ)
    (span
      (singleton (α := Tₚ)
        (((intNorm Tₚ Sₚ : Sₚ →* Tₚ) : (a : Sₚ) → Tₚ)
            (IsPrincipal.generator (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)) :
          Tₚ))))
  (spanNorm Rₚ (S := Sₚ) (span {IsPrincipal.generator (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)}))
Tactic: rw [← spanIntNorm_localization R (spanNorm T I) _ (primeCompl_le_nonZeroDivisors P) Tₚ,
    ← spanIntNorm_localization T (Rₘ := Tₚ) I _ h Sₚ, ← spanIntNorm_localization R (Rₘ := Rₚ) I _
    (primeCompl_le_nonZeroDivisors P) Sₚ, ← (I.map _).span_singleton_generator, spanNorm_singleton,
    spanNorm_singleton, intNorm_intNorm, spanNorm_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
S_1 : Type u_2
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
⊢ Eq (α := Ideal R) (spanNorm.{u_1, u_3} R (S := S) 1) 1
have rw : Eq (α := Ideal R) (spanNorm.{u_1, u_3} R (S := S) ⊤) 1
Tactic: rw [one_eq_top, spanNorm_top R, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
S_1 : Type u_2
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
rw : Eq (α := Ideal R) (spanNorm.{u_1, u_3} R (S := S) ⊤) 1
⊢ Eq (α := Ideal R) (spanNorm.{u_1, u_3} R (S := S) 1) 1
have rw₁ : Eq.{u_1 + 1} (α := Ideal R) ⊤ 1
Tactic: rw [one_eq_top, spanNorm_top R, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
S_1 : Type u_2
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
rw : Eq (α := Ideal R) (spanNorm.{u_1, u_3} R (S := S) ⊤) 1
rw₁ : Eq.{u_1 + 1} (α := Ideal R) ⊤ 1
⊢ Eq (α := Ideal R) (spanNorm.{u_1, u_3} R (S := S) 1) 1
have rw₂ : Eq.{u_1 + 1} (α := Ideal R) ⊤ ⊤
Tactic: rw [one_eq_top, spanNorm_top R, one_eq_top]
-- 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
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
⊢ Membership.mem (α := S) (↑I : Set S) ((σ.toRingEquiv.symm : (a : T) → S) x : S)
have rwa : Membership.mem (α := S) I ((σ.toRingEquiv.symm : (a : T) → S) x : S)
Tactic: rwa [SetLike.mem_coe, Ideal.symm_apply_mem_of_equiv_iff]
-- 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
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)
⊢ Membership.mem (α := S) (↑I : Set S) ((σ.toRingEquiv.symm : (a : T) → S) x : S)
have rwa₁ : Membership.mem (γ := Ideal T) (map σ.toRingEquiv I) x
Tactic: rwa [SetLike.mem_coe, Ideal.symm_apply_mem_of_equiv_iff]
-- 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
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)
have 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)
Tactic: refine le_antisymm (relNorm_map_algEquiv_aux σ I) ?_
-- 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
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) I : Ideal R)
    ((relNorm R : (a : Ideal T) → Ideal R) (map σ I) : Ideal R)
have h : I = map (R := T) σ.symm (map σ I)
Tactic: convert! relNorm_map_algEquiv_aux σ.symm (I.map σ)
-- 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
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 (map σ I)
have h : I = map (R := T) (↑σ.symm : T →ₐ[R] S) (map (↑σ : S →ₐ[R] T) I)
Tactic: change I = map σ.symm.toAlgHom (map σ.toAlgHom I)
-- 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 : 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)
have 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)))
Tactic: refine eq_of_localization_maximal (fun P hPd ↦ ?_)
-- 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
⊢ 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)))
have 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))})
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]
-- 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
⊢ 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))})
have 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))
Tactic: congr 2
-- 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
⊢ (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))
have 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)
Tactic: apply IsFractionRing.injective Rₚ K
-- 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
⊢ 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 (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)
Tactic: rw [Algebra.algebraMap_intNorm (L := FractionRing S), ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply Rₚ K, Algebra.norm_algebraMap, map_pow]