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 J : Ideal S
inst_11 : Nontrivial R
h : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
this : NeZero P
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
⊢ spanNorm (Localization.AtPrime P)
      (HMul.hMul (α := Ideal (Localization (M := S) P'))
        (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I)
        (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J)) =
    HMul.hMul (α := Ideal (Localization.AtPrime P))
      (spanNorm (Localization.AtPrime P) (S := Localization (M := S) P')
        (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I))
      (spanNorm (Localization.AtPrime P) (S := Localization (M := S) P')
        (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J))
have neg : spanNorm (Localization.AtPrime P)
    (HMul.hMul (α := Ideal (Localization (M := S) P'))
      (span
        {IsPrincipal.generator (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I)})
      (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J)) =
  HMul.hMul (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (S := Localization (M := S) P')
      (span
        {IsPrincipal.generator
            (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I)}))
    (spanNorm (Localization.AtPrime P) (S := Localization (M := S) P')
      (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J))
Tactic: rw [← (I.map _).span_singleton_generator, ← (J.map _).span_singleton_generator,
    span_singleton_mul_span_singleton, spanNorm_singleton, spanNorm_singleton,
    spanNorm_singleton, span_singleton_mul_span_singleton, map_mul]
-- 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 J : Ideal S
inst_11 : Nontrivial R
h : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
this : NeZero P
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
neg :
  spanNorm (Localization.AtPrime P)
      (HMul.hMul (α := Ideal (Localization (M := S) P'))
        (span
          {IsPrincipal.generator
              (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I)})
        (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J)) =
    HMul.hMul (α := Ideal (Localization.AtPrime P))
      (spanNorm (Localization.AtPrime P) (S := Localization (M := S) P')
        (span
          {IsPrincipal.generator
              (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I)}))
      (spanNorm (Localization.AtPrime P) (S := Localization (M := S) P')
        (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J))
⊢ spanNorm (Localization.AtPrime P)
      (HMul.hMul (α := Ideal (Localization (M := S) P'))
        (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I)
        (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J)) =
    HMul.hMul (α := Ideal (Localization.AtPrime P))
      (spanNorm (Localization.AtPrime P) (S := Localization (M := S) P')
        (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I))
      (spanNorm (Localization.AtPrime P) (S := Localization (M := S) P')
        (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J))
have neg₁ : spanNorm (Localization.AtPrime P)
    (HMul.hMul (α := Ideal (Localization (M := S) P'))
      (span
        {IsPrincipal.generator (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I)})
      (span
        {IsPrincipal.generator
            (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J)})) =
  HMul.hMul (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (S := Localization (M := S) P')
      (span
        {IsPrincipal.generator
            (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I)}))
    (spanNorm (Localization.AtPrime P) (S := Localization (M := S) P')
      (span
        {IsPrincipal.generator
            (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J)}))
Tactic: rw [← (I.map _).span_singleton_generator, ← (J.map _).span_singleton_generator,
    span_singleton_mul_span_singleton, spanNorm_singleton, spanNorm_singleton,
    spanNorm_singleton, span_singleton_mul_span_singleton, map_mul]
-- 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
I : Ideal S
⊢ LE.le.{u_1} (α := Ideal R) (span ((⇑(intNorm R S) : (a : S) → R) '' (↑I : Set S)))
    (span ((⇑(intNorm R T) : (a : T) → R) '' (↑(span ((⇑(intNorm T S) : (a : S) → T) '' (↑I : Set S))) : Set T)))
have refine : Subset.{u_1} (α := Set R) ((⇑(intNorm R S) : (a : S) → R) '' (↑I : Set S))
  ((⇑(intNorm R T) : (a : T) → R) '' (↑(span ((⇑(intNorm T S) : (a : S) → T) '' (↑I : Set S))) : Set T))
Tactic: refine span_mono ?_
-- 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
I : Ideal S
x : S
hx : x ∈ (↑I : Set S)
⊢ Eq.{u_1 + 1} (α := R) ((intNorm R T : (a : T) → R) ((intNorm T S : (a : S) → T) x : T) : R)
    ((intNorm R S : (a : S) → R) x : R)
have rw : Eq.{u_1 + 1} (α := R) ((intNorm R S : (a : S) → R) x : R) ((intNorm R S : (a : S) → R) x : R)
Tactic: rw [intNorm_intNorm]
-- 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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I : Ideal S
⊢ Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)
have inl : ∀ (h : Eq (α := Ideal R) (spanNorm R I) ⊥), Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)
Tactic: obtain h | h := eq_bot_or_top (spanNorm R 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
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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I : Ideal S
inl : ∀ (h : Eq (α := Ideal R) (spanNorm R I) ⊥), Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)
⊢ Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)
have inr : ∀ (h : Eq (α := Ideal R) (spanNorm R I) ⊤), Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)
Tactic: obtain h | h := eq_bot_or_top (spanNorm R 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
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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I : Ideal S
h : Eq (α := Ideal R) (spanNorm R I) ⊥
⊢ Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)
have inl : Eq (α := Ideal R) (spanNorm R (spanNorm T I)) ⊥
Tactic: rw [h, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff.mp 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
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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I : Ideal S
h : Eq (α := Ideal R) (spanNorm R I) ⊥
inl : Eq (α := Ideal R) (spanNorm R (spanNorm T I)) ⊥
⊢ Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)
have inl₁ : Eq (α := Ideal T) (spanNorm T I) ⊥
Tactic: rw [h, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff.mp 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
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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I : Ideal S
h : Eq (α := Ideal R) (spanNorm R I) ⊥
inl : Eq (α := Ideal R) (spanNorm R (spanNorm T I)) ⊥
inl₁ : Eq (α := Ideal T) (spanNorm T I) ⊥
⊢ Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)
have inl₂ : I = ⊥
Tactic: rw [h, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff.mp 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
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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I : Ideal S
h : Eq (α := Ideal R) (spanNorm R I) ⊥
inl : Eq (α := Ideal R) (spanNorm R (spanNorm T I)) ⊥
inl₁ : Eq (α := Ideal T) (spanNorm T I) ⊥
inl₂ : I = ⊥
⊢ Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)
have inl₃ : Eq.{u_3 + 1} (α := Ideal S) ⊥ ⊥
Tactic: rw [h, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff.mp 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
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
⊢ Eq (α := Ideal R) (spanNorm R (spanNorm T I)) (spanNorm R I)
have refine : ∀ (P : Ideal R) (hP : P.IsMaximal),
  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))
Tactic: refine eq_of_localization_maximal fun P hP ↦ ?_
-- 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 : P.IsMaximal
⊢ 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 pos : ∀ (hP_1 : P = ⊥),
  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))
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
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 : P.IsMaximal
pos :
  ∀ (hP_1 : P = ⊥),
    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))
⊢ 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 : ∀ (hP_1 : ¬P = ⊥),
  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))
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
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 = ⊥
⊢ 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 pos : ∀ (hP : IsMaximal.{u_1} (α := R) ⊥),
  Eq (α := Ideal (Localization.AtPrime (R := R) ⊥))
    (map (F := R →+* Localization.AtPrime (R := R) ⊥) (algebraMap R (Localization.AtPrime (R := R) ⊥))
      (spanNorm R (spanNorm T I)))
    (map (F := R →+* Localization.AtPrime (R := R) ⊥) (algebraMap R (Localization.AtPrime (R := R) ⊥)) (spanNorm R I))
Tactic: subst hP
Cleared hypotheses: P, hP_1, hP
-- 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
hP : IsMaximal.{u_1} (α := R) ⊥
⊢ Eq (α := Ideal (Localization.AtPrime (R := R) ⊥))
    (map (F := R →+* Localization.AtPrime (R := R) ⊥) (algebraMap R (Localization.AtPrime (R := R) ⊥))
      (spanNorm R (spanNorm T I)))
    (map (F := R →+* Localization.AtPrime (R := R) ⊥) (algebraMap R (Localization.AtPrime (R := R) ⊥)) (spanNorm R I))
have pos : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
Tactic: rw [spanNorm_spanNorm_of_bot_or_top]
-- 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
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)
⊢ 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 this : NeZero P
Tactic: have : NeZero P := ⟨hP⟩
-- 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
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
⊢ 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 h : LE.le (α := Submonoid T) (algebraMapSubmonoid T P.primeCompl) T⁰
Tactic: have h : algebraMapSubmonoid T P.primeCompl ≤ T⁰ :=
      algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _ (primeCompl_le_nonZeroDivisors 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
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⁰
⊢ 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ₚ) (map (F := T →+* Tₚ) (algebraMap T Tₚ) (spanNorm T 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]