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_1 : IsFractionRing Rₘ K := ⋯
this : IsScalarTower S Sₘ L
h :
  Eq (α := Rₘ →+* L) (algebraMap Rₘ L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₘ L) (algebraMap Rₘ Sₘ))
⊢ IsScalarTower Rₘ Sₘ L

Tactic:
apply IsScalarTower.of_algebraMap_eq'

Premises used: IsScalarTower.of_algebraMap_eq'
-- 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_1 : IsFractionRing Rₘ K := ⋯
this : IsScalarTower S Sₘ L
h :
  Eq (α := R →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ L) (algebraMap R Rₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₘ L) (algebraMap Rₘ Sₘ)) (algebraMap R Rₘ))
⊢ Eq (α := Rₘ →+* L) (algebraMap Rₘ L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₘ L) (algebraMap Rₘ Sₘ))

Tactic:
apply IsLocalization.ringHom_ext M

Premises used: IsLocalization.ringHom_ext
-- 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 : IsScalarTower S Sₘ L
⊢ IsScalarTower Rₘ Sₘ L

Tactic:
have : IsScalarTower Rₘ Sₘ L := by
    apply IsScalarTower.of_algebraMap_eq'
    apply IsLocalization.ringHom_ext M
    rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra (R := Sₘ), RingHom.comp_assoc,
      RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R S Sₘ,
      IsLocalization.map_comp, RingHom.comp_id, ← RingHom.comp_assoc, IsLocalization.map_comp,
      RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-- 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 := ⋯
rw :
  Eq (α := Ideal Rₘ) (spanNorm.{u_4, u_5} Rₘ (S := Sₘ) (map (F := S →+* Sₘ) (algebraMap S Sₘ) I))
    (span
      (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) ''
        (↑I : Set S)))
⊢ Eq (α := Ideal Rₘ) (spanNorm.{u_4, u_5} Rₘ (S := Sₘ) (map (F := S →+* Sₘ) (algebraMap S Sₘ) I))
    (map (F := R →+* Rₘ) (algebraMap R Rₘ) (spanNorm R I))

Tactic:
rw [map_spanIntNorm]

Premises used: Ideal.map_spanIntNorm
-- 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 := ⋯
⊢ Eq (α := Ideal Rₘ) (spanNorm.{u_4, u_5} Rₘ (S := Sₘ) (map (F := S →+* Sₘ) (algebraMap S Sₘ) I))
    (span
      (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) ''
        (↑I : Set S)))

Tactic:
span_eq_span (Set.image_subset_iff.mpr ?_) (Set.image_subset_iff.mpr ?_)

Premises used: Iff.mpr, Ideal.map, Ideal.spanNorm, Submodule.span, Set.image_subset_iff, Submodule.span_eq_span
-- 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 := ⋯
refine_1 :
  (↑(map (F := S →+* Sₘ) (algebraMap S Sₘ) I) : Set Sₘ) ⊆
    (⇑(Algebra.intNorm Rₘ Sₘ) : (a : Sₘ) → Rₘ) ⁻¹'
      (↑(Submodule.span Rₘ
            (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) ''
              (↑I : Set S))) :
        Set Rₘ)
refine_2 :
  (↑I : 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ₘ)
⊢ Eq (α := Ideal Rₘ) (spanNorm.{u_4, u_5} Rₘ (S := Sₘ) (map (F := S →+* Sₘ) (algebraMap S Sₘ) I))
    (span
      (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) ''
        (↑I : Set S)))

Tactic:
refine span_eq_span (Set.image_subset_iff.mpr ?_) (Set.image_subset_iff.mpr ?_)

Premises used: Iff.mpr, Set.image_subset_iff, Submodule.span_eq_span
-- 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' ∈ (↑(map (F := S →+* Sₘ) (algebraMap S Sₘ) I) : Set Sₘ)
refine_1 :
  ∀
    (ha' :
      ∃ (a : ↥I) (b : ↥(Algebra.algebraMapSubmonoid S M)),
        HMul.hMul (β := Sₘ) a' ((algebraMap S Sₘ : (a : S) → Sₘ) (↑b : S) : Sₘ) =
          (algebraMap S Sₘ : (a : S) → Sₘ) (↑a : S)),
    ∃ (a : ↥(spanNorm R I)) (b : ↥M),
      HMul.hMul (α := Rₘ) (β := Rₘ) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a' : Rₘ)
          ((algebraMap R Rₘ : (a : R) → Rₘ) (↑b : R) : Rₘ) =
        (algebraMap R Rₘ : (a : R) → Rₘ) (↑a : R)
⊢ Membership.mem (γ := Set Sₘ)
    ((⇑(Algebra.intNorm Rₘ Sₘ) : (a : Sₘ) → Rₘ) ⁻¹'
      (↑(Submodule.span Rₘ
            (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) ''
              (↑I : Set S))) :
        Set Rₘ))
    a'

Tactic:
simp only [Set.mem_preimage, submodule_span_eq, ← map_spanIntNorm, SetLike.mem_coe,
      IsLocalization.mem_map_algebraMap_iff (Algebra.algebraMapSubmonoid S M) Sₘ,
      IsLocalization.mem_map_algebraMap_iff M Rₘ, Prod.exists] at ha' ⊢

Premises used: Ideal.submodule_span_eq, Ideal.map_spanIntNorm, SetLike.mem_coe, Algebra.algebraMapSubmonoid, IsLocalization.mem_map_algebraMap_iff, Prod.exists, 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) (b : ↥(Algebra.algebraMapSubmonoid S M)),
    HMul.hMul (β := Sₘ) a' ((algebraMap S Sₘ : (a : S) → Sₘ) (↑b : S) : Sₘ) = (algebraMap S Sₘ : (a : S) → Sₘ) (↑a : S)
refine_1 :
  ∀ (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)),
    ∃ (a : ↥(spanNorm R I)) (b : ↥M),
      HMul.hMul (α := Rₘ) (β := Rₘ) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a' : Rₘ)
          ((algebraMap R Rₘ : (a : R) → Rₘ) (↑b : R) : Rₘ) =
        (algebraMap R Rₘ : (a : R) → Rₘ) (↑a : R)
⊢ ∃ (a : ↥(spanNorm R I)) (b : ↥M),
    HMul.hMul (α := Rₘ) (β := Rₘ) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a' : Rₘ)
        ((algebraMap R Rₘ : (a : R) → Rₘ) (↑b : R) : Rₘ) =
      (algebraMap R Rₘ : (a : R) → Rₘ) (↑a : R)

Tactic:
obtain ⟨⟨a, ha⟩, ⟨_, ⟨s, hs, rfl⟩⟩, has⟩ := ha'

Premises used: rfl
-- 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)
⊢ ∃ (a : ↥(spanNorm R I)) (b : ↥M),
    HMul.hMul (α := Rₘ) (β := Rₘ) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a' : Rₘ)
        ((algebraMap R Rₘ : (a : R) → Rₘ) (↑b : R) : Rₘ) =
      (algebraMap R Rₘ : (a : R) → Rₘ) (↑a : R)

Tactic:
⟨⟨Algebra.intNorm R S a, intNorm_mem_spanNorm _ ha⟩,
      ⟨s ^ Module.finrank K L, pow_mem hs _⟩, ?_⟩

Premises used: Ideal.intNorm_mem_spanNorm, Subtype.mk, Algebra.intNorm, HPow.hPow, Exists.intro, pow_mem, DFunLike.coe, Module.finrank
-- 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ₘ) (β := 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)
⊢ ∃ (a : ↥(spanNorm R I)) (b : ↥M),
    HMul.hMul (α := Rₘ) (β := Rₘ) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a' : Rₘ)
        ((algebraMap R Rₘ : (a : R) → Rₘ) (↑b : R) : Rₘ) =
      (algebraMap R Rₘ : (a : R) → Rₘ) (↑a : R)

Tactic:
refine ⟨⟨Algebra.intNorm R S a, intNorm_mem_spanNorm _ ha⟩,
      ⟨s ^ Module.finrank K L, pow_mem hs _⟩, ?_⟩