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 : IsScalarTower R Rₘ K
h : IsFractionRing Rₘ K := ⋯
rw : Eq (α := S →+* L) (algebraMap S L) (g.comp (algebraMap S Sₘ))
⊢ Eq (α := S →+* L) (algebraMap S L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₘ L) (algebraMap S Sₘ))
have rw₁ : Eq (α := S →+* L) (algebraMap S L) (RingHom.comp (algebraMap S L) (RingHom.id S))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_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 : IsScalarTower R Rₘ K
h : IsFractionRing Rₘ K := ⋯
rw : Eq (α := S →+* L) (algebraMap S L) (g.comp (algebraMap S Sₘ))
rw₁ : Eq (α := S →+* L) (algebraMap S L) (RingHom.comp (algebraMap S L) (RingHom.id S))
⊢ Eq (α := S →+* L) (algebraMap S L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₘ L) (algebraMap S Sₘ))
have rw₂ : Eq (α := S →+* L) (algebraMap S L) (algebraMap S L)
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_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 : IsScalarTower R Rₘ K
h : IsFractionRing Rₘ K := ⋯
⊢ 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 S Sₘ L
Tactic: have : IsScalarTower S Sₘ L := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_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 : IsScalarTower S Sₘ L
⊢ IsScalarTower Rₘ Sₘ L
have h : Eq (α := Rₘ →+* L) (algebraMap Rₘ L)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₘ L) (algebraMap Rₘ Sₘ))
Tactic: apply IsScalarTower.of_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 : IsScalarTower S Sₘ L
⊢ Eq (α := Rₘ →+* L) (algebraMap Rₘ L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₘ L) (algebraMap Rₘ Sₘ))
have 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ₘ))
Tactic: apply IsLocalization.ringHom_ext M
-- 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 : IsScalarTower S Sₘ L
⊢ 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 (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ₘ))
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 (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ₘ))
⊢ 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 (RingHom.comp (algebraMap K L) f) (algebraMap R Rₘ))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (g.comp (algebraMap Rₘ Sₘ)) (algebraMap R Rₘ))
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 (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ₘ))
⊢ 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ₘ)))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (g.comp (algebraMap Rₘ Sₘ)) (algebraMap R Rₘ))
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 (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ₘ))
⊢ 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 Rₘ Sₘ) (algebraMap R Rₘ)))
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 (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ₘ)))
⊢ 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 (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]