-- 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
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))
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)}))
neg₂ :
  spanNorm (Localization.AtPrime P) (S := Localization (M := S) P')
      (span
        {HMul.hMul (α := Localization (M := S) P')
            (IsPrincipal.generator
              (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I))
            (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)}))
neg₃ :
  span
      (singleton (α := Localization.AtPrime P)
        ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
              (a : Localization P') → Localization.AtPrime P)
            (HMul.hMul (α := Localization (M := S) P')
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I))
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J))) :
          Localization.AtPrime P)) =
    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)}))
neg₄ :
  span
      (singleton (α := Localization.AtPrime P)
        ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
              (a : Localization P') → Localization.AtPrime P)
            (HMul.hMul (α := Localization (M := S) P')
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I))
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J))) :
          Localization.AtPrime P)) =
    HMul.hMul (α := Ideal (Localization.AtPrime P))
      (span
        (singleton (α := Localization.AtPrime P)
          ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
                (a : Localization P') → Localization.AtPrime P)
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I)) :
            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')) J)}))
neg₅ :
  span
      (singleton (α := Localization.AtPrime P)
        ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
              (a : Localization P') → Localization.AtPrime P)
            (HMul.hMul (α := Localization (M := S) P')
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I))
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J))) :
          Localization.AtPrime P)) =
    HMul.hMul (α := Ideal (Localization.AtPrime P))
      (span
        (singleton (α := Localization.AtPrime P)
          ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
                (a : Localization P') → Localization.AtPrime P)
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I)) :
            Localization.AtPrime P)))
      (span
        (singleton (α := Localization.AtPrime P)
          ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
                (a : Localization P') → Localization.AtPrime P)
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J)) :
            Localization.AtPrime P)))
neg₆ :
  Eq (α := Ideal (Localization.AtPrime P))
    (span
      (singleton (α := Localization.AtPrime P)
        ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
              (a : Localization P') → Localization.AtPrime P)
            (HMul.hMul (α := Localization (M := S) P')
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I))
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J))) :
          Localization.AtPrime P)))
    (span
      {HMul.hMul (α := Localization.AtPrime P) (β := Localization.AtPrime P)
          ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
                (a : Localization P') → Localization.AtPrime P)
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I)) :
            Localization.AtPrime P)
          ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
                (a : Localization P') → Localization.AtPrime P)
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J)) :
            Localization.AtPrime P)})
neg₇ neg₈ :
  Eq (α := Ideal (Localization.AtPrime P))
    (span
      {HMul.hMul (α := Localization.AtPrime P) (β := Localization.AtPrime P)
          ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
                (a : Localization P') → Localization.AtPrime P)
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I)) :
            Localization.AtPrime P)
          ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
                (a : Localization P') → Localization.AtPrime P)
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J)) :
            Localization.AtPrime P)})
    (span
      {HMul.hMul (α := Localization.AtPrime P) (β := Localization.AtPrime P)
          ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
                (a : Localization P') → Localization.AtPrime P)
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I)) :
            Localization.AtPrime P)
          ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
                (a : Localization P') → Localization.AtPrime P)
              (IsPrincipal.generator
                (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J)) :
            Localization.AtPrime P)})
⊢ 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))

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]

Premises used: Ideal.span_singleton_generator, Ideal.map, Ideal.span_singleton_mul_span_singleton, map_mul, Ideal.spanNorm_singleton