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
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 (RingHom.comp (algebraMap K L) f) (algebraMap R Rₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₘ L) (algebraMap Rₘ Sₘ)) (algebraMap R Rₘ))
h₁ :
  Eq (α := R →+* L) (RingHom.comp (RingHom.comp (algebraMap K L) f) (algebraMap R Rₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (g.comp (algebraMap Rₘ Sₘ)) (algebraMap R Rₘ))
h₂ :
  Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (f.comp (algebraMap R Rₘ)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (g.comp (algebraMap Rₘ Sₘ)) (algebraMap R Rₘ))
h₃ :
  Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (f.comp (algebraMap R Rₘ)))
    (g.comp (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Sₘ) (algebraMap R Rₘ)))
h₄ : Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (f.comp (algebraMap R Rₘ))) (g.comp (algebraMap R Sₘ))
⊢ 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ₘ))
have h₅ : Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (f.comp (algebraMap R Rₘ)))
  (g.comp (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₘ) (algebraMap R S)))
Tactic: 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]
-- 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 : IsScalarTower S Sₘ L
⊢ 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))
have this₁ : 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]
-- 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 := ⋯
⊢ 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))
have 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)))
Tactic: rw [map_spanIntNorm]
-- 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 := ⋯
⊢ 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)))
have 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ₘ)
Tactic: refine span_eq_span (Set.image_subset_iff.mpr ?_) (Set.image_subset_iff.mpr ?_)
-- 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 := ⋯
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ₘ)
⊢ 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)))
have 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ₘ)
Tactic: refine span_eq_span (Set.image_subset_iff.mpr ?_) (Set.image_subset_iff.mpr ?_)
-- 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' ∈ (↑(map (F := S →+* Sₘ) (algebraMap S Sₘ) I) : Set Sₘ)
⊢ 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'
have 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)
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' ⊢
Cleared hypotheses: ha'
-- 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) (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)
have 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) sorry) :
                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: obtain ⟨⟨a, ha⟩, ⟨_, ⟨s, hs, rfl⟩⟩, has⟩ := ha'
Cleared hypotheses: ha'
-- 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 (β := 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)
have 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) sorry) : 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) sorry) :
        R) :
      R)
Tactic: refine ⟨⟨Algebra.intNorm R S a, intNorm_mem_spanNorm _ ha⟩,
      ⟨s ^ Module.finrank K L, pow_mem hs _⟩, ?_⟩
-- 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 (β := 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)
⊢ 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)
have 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)
Tactic: simp only [map_pow] at 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 (β := Sₘ) a' ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) s : S) : Sₘ) =
    (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₁ : 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
Cleared hypotheses: has