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
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 (β := Sₘ) a'
      ((algebraMap S Sₘ : (a : S) → Sₘ)
          ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                  ((algebraMap R S : (a : R) → S) s) ⋯) :
              S) :
            S) :
        Sₘ) =
    (algebraMap S Sₘ : (a : S) → Sₘ) (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ I) a ha) : S)
refine_1 :
  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)
⊢ HMul.hMul (α := Rₘ) (β := Rₘ) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a' : Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) (s ^ finrank K L) ⋯) : R) : Rₘ) =
    (algebraMap R Rₘ : (a : R) → Rₘ)
      ((↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Ideal R) (spanNorm R I) x)
              ((Algebra.intNorm R S : (a : S) → R) a) ⋯) :
          R) :
        R)

Tactic:
simp only [map_pow] at has ⊢

Premises used: map_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
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 (β := Sₘ) a' ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) s : S) : Sₘ) =
    (algebraMap S Sₘ : (a : S) → Sₘ) a
⊢ 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)

Tactic:
apply_fun algebraMap _ L at has

Premises used: Algebra.algebraMap
-- 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
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)
⊢ 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

Premises used: Algebra.norm
-- 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
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 (α := 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

Premises used: map_mul
-- 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
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 (α := 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

Premises used: Algebra.norm_algebraMap, IsScalarTower.algebraMap_apply
-- 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
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 :
  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)
⊢ 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)

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
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) (((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))
⊢ 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:
simp only [map_mul, map_pow]

Premises used: map_pow, map_mul
-- 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
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)
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ₘ)
⊢ 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

Tactic:
rw [Set.mem_preimage, Function.comp_apply, Algebra.intNorm_eq_of_isLocalization M (Bₘ := Sₘ)]

Premises used: Algebra.intNorm_eq_of_isLocalization, Function.comp_apply, Set.mem_preimage
-- 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
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 (α := 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:
subset_span (Set.mem_image_of_mem _ (mem_map_of_mem _ ha))

Premises used: Ideal.subset_span, Ideal.mem_map_of_mem, Set.Mem, Set.mem_image_of_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
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 (α := 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:
exact subset_span (Set.mem_image_of_mem _ (mem_map_of_mem _ ha))

Premises used: Ideal.subset_span, Ideal.mem_map_of_mem, Set.mem_image_of_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
I J : Ideal S
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))
⊢ 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)

Tactic:
rw [Ideal.span_mul_span', ← Set.image_mul]

Premises used: Ideal.span_mul_span', Set.image_mul
-- 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
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))

Tactic:
Ideal.span_mono (Set.monotone_image ?_)

Premises used: Set.Mem, Ideal.span_mono, Set.monotone_image