awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
this_1 : IsScalarTower R Rₘ K
h : IsFractionRing Rₘ K := ⋯
this_2 : IsScalarTower S Sₘ L
this : IsScalarTower Rₘ Sₘ L
h_1 : IsFractionRing Sₘ L := ⋯
a' : Sₘ
a : S
ha : a ∈ I
s : R
hs : s ∈ (↑M : Set R)
has :
  Eq.{u_3 + 1} (α := L)
    (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L)
        (HMul.hMul (β := Sₘ) a' ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) s : S) : Sₘ)) :
      L)
    (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) ((algebraMap S Sₘ : (a : S) → Sₘ) a) : L)
⊢ HMul.hMul (α := Rₘ) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a' : Rₘ)
      (HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) s : Rₘ) (finrank K L)) =
    (algebraMap R Rₘ : (a : R) → Rₘ) ((Algebra.intNorm R S : (a : S) → R) a : R)
have has₁ : Eq.{u_1 + 1} (α := K)
  ((Algebra.norm K : (a : L) → K)
      (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L)
        (HMul.hMul (β := Sₘ) a' ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) s : S) : Sₘ))) :
    K)
  ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) ((algebraMap S Sₘ : (a : S) → Sₘ) a)) :
    K)
Tactic: apply_fun Algebra.norm K at has
Cleared hypotheses: has
-- 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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
this_1 : IsScalarTower R Rₘ K
h : IsFractionRing Rₘ K := ⋯
this_2 : IsScalarTower S Sₘ L
this : IsScalarTower Rₘ Sₘ L
h_1 : IsFractionRing Sₘ L := ⋯
a' : Sₘ
a : S
ha : a ∈ I
s : R
hs : s ∈ (↑M : Set R)
has :
  Eq.{u_1 + 1} (α := K)
    ((Algebra.norm K : (a : L) → K)
        (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L)
          (HMul.hMul (β := Sₘ) a' ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) s : S) : Sₘ))) :
      K)
    ((Algebra.norm K : (a : L) → K)
        (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) ((algebraMap S Sₘ : (a : S) → Sₘ) a)) :
      K)
⊢ HMul.hMul (α := Rₘ) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a' : Rₘ)
      (HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) s : Rₘ) (finrank K L)) =
    (algebraMap R Rₘ : (a : R) → Rₘ) ((Algebra.intNorm R S : (a : S) → R) a : R)
have has₁ : HMul.hMul (α := K) (β := K) ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) a') : K)
    ((Algebra.norm K : (a : L) → K)
        (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L)
          ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) s : S))) :
      K) =
  (Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) ((algebraMap S Sₘ : (a : S) → Sₘ) a))
Tactic: simp only [map_mul] at has
Cleared hypotheses: has
-- 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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
this_1 : IsScalarTower R Rₘ K
h : IsFractionRing Rₘ K := ⋯
this_2 : IsScalarTower S Sₘ L
this : IsScalarTower Rₘ Sₘ L
h_1 : IsFractionRing Sₘ L := ⋯
a' : Sₘ
a : S
ha : a ∈ I
s : R
hs : s ∈ (↑M : Set R)
has :
  HMul.hMul (α := K) (β := K) ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) a') : K)
      ((Algebra.norm K : (a : L) → K)
          (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L)
            ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) s : S))) :
        K) =
    (Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) ((algebraMap S Sₘ : (a : S) → Sₘ) a))
⊢ HMul.hMul (α := Rₘ) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a' : Rₘ)
      (HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) s : Rₘ) (finrank K L)) =
    (algebraMap R Rₘ : (a : R) → Rₘ) ((Algebra.intNorm R S : (a : S) → R) a : R)
have has₁ : HMul.hMul (α := K) ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) a') : K)
    (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) s : K) (finrank K L)) =
  (Algebra.norm K : (a : L) → K) ((algebraMap S L : (a : S) → L) a)
Tactic: rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
      ← IsScalarTower.algebraMap_apply,
      IsScalarTower.algebraMap_apply R K L,
      Algebra.norm_algebraMap] at has
Cleared hypotheses: has
-- 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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
this_1 : IsScalarTower R Rₘ K
h : IsFractionRing Rₘ K := ⋯
this_2 : IsScalarTower S Sₘ L
this : IsScalarTower Rₘ Sₘ L
h_1 : IsFractionRing Sₘ L := ⋯
a' : Sₘ
a : S
ha : a ∈ I
s : R
hs : s ∈ (↑M : Set R)
has :
  HMul.hMul (α := K) ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) a') : K)
      (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) s : K) (finrank K L)) =
    (Algebra.norm K : (a : L) → K) ((algebraMap S L : (a : S) → L) a)
⊢ HMul.hMul (α := Rₘ) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a' : Rₘ)
      (HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) s : Rₘ) (finrank K L)) =
    (algebraMap R Rₘ : (a : R) → Rₘ) ((Algebra.intNorm R S : (a : S) → R) a : R)
have refine_1 : Eq.{u_1 + 1} (α := K)
  (((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K)
      (HMul.hMul (α := Rₘ) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a' : Rₘ)
        (HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) s : Rₘ) (finrank K L))) :
    K)
  (((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K)
      ((algebraMap R Rₘ : (a : R) → Rₘ) ((Algebra.intNorm R S : (a : S) → R) a : R)) :
    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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
this_1 : IsScalarTower R Rₘ K
h : IsFractionRing Rₘ K := ⋯
this_2 : IsScalarTower S Sₘ L
this : IsScalarTower Rₘ Sₘ L
h_1 : IsFractionRing Sₘ L := ⋯
a' : Sₘ
a : S
ha : a ∈ I
s : R
hs : s ∈ (↑M : Set R)
has :
  HMul.hMul (α := K) ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) a') : K)
      (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) s : K) (finrank K L)) =
    (Algebra.norm K : (a : L) → K) ((algebraMap S L : (a : S) → L) a)
⊢ Eq.{u_1 + 1} (α := K)
    (((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K)
        (HMul.hMul (α := Rₘ) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a' : Rₘ)
          (HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) s : Rₘ) (finrank K L))) :
      K)
    (((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K)
        ((algebraMap R Rₘ : (a : R) → Rₘ) ((Algebra.intNorm R S : (a : S) → R) a : R)) :
      K)
have refine_1 : HMul.hMul (α := K) (((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a') : K)
    (HPow.hPow (α := K) (((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K) ((algebraMap R Rₘ : (a : R) → Rₘ) s) : K)
      (finrank K L)) =
  ((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((Algebra.intNorm R S : (a : S) → R) a : R))
Tactic: simp only [map_mul, 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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
this_1 : IsScalarTower R Rₘ K
h : IsFractionRing Rₘ K := ⋯
this_2 : IsScalarTower S Sₘ L
this : IsScalarTower Rₘ Sₘ L
h_1 : IsFractionRing Sₘ L := ⋯
a' : Sₘ
a : S
ha : a ∈ I
s : R
hs : s ∈ (↑M : Set R)
has :
  HMul.hMul (α := K) ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) a') : K)
      (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) s : K) (finrank K L)) =
    (Algebra.norm K : (a : L) → K) ((algebraMap S L : (a : S) → L) a)
⊢ HMul.hMul (α := K) (((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a') : K)
      (HPow.hPow (α := K) (((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K) ((algebraMap R Rₘ : (a : R) → Rₘ) s) : K)
        (finrank K L)) =
    ((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K)
      ((algebraMap R Rₘ : (a : R) → Rₘ) ((Algebra.intNorm R S : (a : S) → R) a : R))
have refine_1 : HMul.hMul (α := K) ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) a') : K)
    (HPow.hPow (α := K) (((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K) ((algebraMap R Rₘ : (a : R) → Rₘ) s) : K)
      (finrank K L)) =
  ((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((Algebra.intNorm R S : (a : S) → R) a : R))
Tactic: rwa [Algebra.algebraMap_intNorm (L := L), ← IsScalarTower.algebraMap_apply,
      ← IsScalarTower.algebraMap_apply, Algebra.algebraMap_intNorm (L := L)]
-- 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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
this_1 : IsScalarTower R Rₘ K
h : IsFractionRing Rₘ K := ⋯
this_2 : IsScalarTower S Sₘ L
this : IsScalarTower Rₘ Sₘ L
h_1 : IsFractionRing Sₘ L := ⋯
a' : Sₘ
a : S
ha : a ∈ I
s : R
hs : s ∈ (↑M : Set R)
has :
  HMul.hMul (α := K) ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) a') : K)
      (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) s : K) (finrank K L)) =
    (Algebra.norm K : (a : L) → K) ((algebraMap S L : (a : S) → L) a)
refine_1 :
  HMul.hMul (α := K) ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) a') : K)
      (HPow.hPow (α := K) (((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K) ((algebraMap R Rₘ : (a : R) → Rₘ) s) : K)
        (finrank K L)) =
    ((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K)
      ((algebraMap R Rₘ : (a : R) → Rₘ) ((Algebra.intNorm R S : (a : S) → R) a : R))
⊢ HMul.hMul (α := K) (((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a') : K)
      (HPow.hPow (α := K) (((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K) ((algebraMap R Rₘ : (a : R) → Rₘ) s) : K)
        (finrank K L)) =
    ((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K)
      ((algebraMap R Rₘ : (a : R) → Rₘ) ((Algebra.intNorm R S : (a : S) → R) a : R))
have refine_1₁ : HMul.hMul (α := K) ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) a') : K)
    (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) s : K) (finrank K L)) =
  ((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((Algebra.intNorm R S : (a : S) → R) a : R))
Tactic: rwa [Algebra.algebraMap_intNorm (L := L), ← IsScalarTower.algebraMap_apply,
      ← IsScalarTower.algebraMap_apply, Algebra.algebraMap_intNorm (L := L)]
-- 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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
this_1 : IsScalarTower R Rₘ K
h : IsFractionRing Rₘ K := ⋯
this_2 : IsScalarTower S Sₘ L
this : IsScalarTower Rₘ Sₘ L
h_1 : IsFractionRing Sₘ L := ⋯
a : S
ha : a ∈ (↑I : Set S)
⊢ Membership.mem (γ := Set S)
    (Function.comp.{u_3 + 1, u_1 + 1, u_4 + 1} (β := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ)
        (⇑(Algebra.intNorm R S) : (a : S) → R) ⁻¹'
      (↑(Submodule.span Rₘ
            ((⇑(Algebra.intNorm Rₘ Sₘ) : (a : Sₘ) → Rₘ) '' (↑(map (F := S →+* Sₘ) (algebraMap S Sₘ) I) : Set Sₘ))) :
        Set Rₘ))
    a
have refine_2 : Membership.mem (α := Rₘ)
  (↑(Submodule.span Rₘ
        ((⇑(Algebra.intNorm Rₘ Sₘ) : (a : Sₘ) → Rₘ) '' (↑(map (F := S →+* Sₘ) (algebraMap S Sₘ) I) : Set Sₘ))) :
    Set Rₘ)
  ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
Tactic: rw [Set.mem_preimage, Function.comp_apply, Algebra.intNorm_eq_of_isLocalization M (Bₘ := 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
I J : Ideal S
⊢ HMul.hMul (α := Ideal R) (span ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S)))
      (span ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑J : Set S))) ≤
    map (F := S →* R) (Algebra.intNorm R S) (I * J)
have rw : LE.le.{u_1} (α := Ideal R) (span ((⇑(Algebra.intNorm R S) : (a : S) → R) '' ((↑I : Set S) * (↑J : Set S))))
  (map (F := S →* R) (Algebra.intNorm R S) (I * J))
Tactic: rw [Ideal.span_mul_span', ← Set.image_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
I J : Ideal S
⊢ LE.le.{u_1} (α := Ideal R) (span ((⇑(Algebra.intNorm R S) : (a : S) → R) '' ((↑I : Set S) * (↑J : Set S))))
    (map (F := S →* R) (Algebra.intNorm R S) (I * J))
have refine : (↑I : Set S) * (↑J : Set S) ≤ (↑(I * J) : Set S)
Tactic: refine Ideal.span_mono (Set.monotone_image ?_)
-- 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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
⊢ spanNorm R (I * J) = HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
have refine : spanNorm R (I * J) ≤ HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
Tactic: refine le_antisymm ?_ (spanNorm_mul_spanNorm_le R _ _)
-- 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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
⊢ spanNorm R (I * J) ≤ HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
have inl : ∀ (hI : Eq (α := Ideal R) (spanNorm R I) ⊥), spanNorm R (I * J) ≤ HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
Tactic: rcases eq_bot_or_top (spanNorm R I) with hI | hI
-- 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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
inl :
  ∀ (hI : Eq (α := Ideal R) (spanNorm R I) ⊥),
    spanNorm R (I * J) ≤ HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
⊢ spanNorm R (I * J) ≤ HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
have inr : ∀ (hI : Eq (α := Ideal R) (spanNorm R I) ⊤), spanNorm R (I * J) ≤ HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
Tactic: rcases eq_bot_or_top (spanNorm R I) with hI | hI