awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
inst_7 : Algebra R Rₘ
inst_8 : IsTorsionFree R S
inst_9 : Algebra.IsSeparable.{u_1, u_2} K L
M : Submonoid R
inst_10 : IsLocalization M Rₘ
inst_11 : Algebra Rₘ Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra R Sₘ
inst_14 : IsScalarTower R Rₘ Sₘ
inst_15 : IsScalarTower R S Sₘ
inst_16 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_17 : Algebra.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
inst_18 : IsScalarTower.{u_4, u_4, u_5} Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := algebraMapSubmonoid S M
hM' : LE.le (α := Submonoid S) (algebraMapSubmonoid S M) S⁰
f₁ : RingHom.{u_4, u_1} Rₘ K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
f₂ : RingHom.{u_5, u_2} Sₘ L := IsLocalization.map (M := algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) hM'
algInst : Algebra.{u_4, u_1} Rₘ K := f₁.toAlgebra
algInst_1 : Algebra.{u_5, u_2} Sₘ L := f₂.toAlgebra
this_1 : IsScalarTower R Rₘ K
this_2 : IsScalarTower S Sₘ L
this_3 : IsFractionRing.{u_4, u_1} Rₘ K
this_4 : IsFractionRing.{u_5, u_2} Sₘ L
this : IsDomain Rₘ
x : R
⊢ Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing Rₘ) (FractionRing Sₘ))
              (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Rₘ K))) : K →+* FractionRing Rₘ))
            (algebraMap R K) :
          (a : R) → FractionRing Sₘ)
        x :
      FractionRing Sₘ)
    (((@RingHom.comp _ K _ _ Semiring.toNonAssocSemiring _
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Sₘ L))) : L →+* FractionRing Sₘ) (algebraMap K L))
              (algebraMap R K) :
            RingHom.{u_1, u_5} R (FractionRing Sₘ)) :
          (a : R) → FractionRing Sₘ)
        x :
      FractionRing Sₘ)
have he : Eq.{u_5 + 1} (α := FractionRing Sₘ)
  ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
      ((AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Rₘ K)) : (a : K) → FractionRing Rₘ)
        ((algebraMap R K : (a : R) → K) x)) :
    FractionRing Sₘ)
  ((AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Sₘ L)) : (a : L) → FractionRing Sₘ)
      ((algebraMap R L : (a : R) → L) x) :
    FractionRing Sₘ)
Tactic: simp only [RingHom.coe_comp,
      RingHom.coe_coe, Function.comp_apply, ← algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
inst_7 : Algebra R Rₘ
inst_8 : IsTorsionFree R S
inst_9 : Algebra.IsSeparable.{u_1, u_2} K L
M : Submonoid R
inst_10 : IsLocalization M Rₘ
inst_11 : Algebra Rₘ Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra R Sₘ
inst_14 : IsScalarTower R Rₘ Sₘ
inst_15 : IsScalarTower R S Sₘ
inst_16 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_17 : Algebra.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
inst_18 : IsScalarTower.{u_4, u_4, u_5} Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := algebraMapSubmonoid S M
hM' : LE.le (α := Submonoid S) (algebraMapSubmonoid S M) S⁰
f₁ : RingHom.{u_4, u_1} Rₘ K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
f₂ : RingHom.{u_5, u_2} Sₘ L := IsLocalization.map (M := algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) hM'
algInst : Algebra.{u_4, u_1} Rₘ K := f₁.toAlgebra
algInst_1 : Algebra.{u_5, u_2} Sₘ L := f₂.toAlgebra
this_1 : IsScalarTower R Rₘ K
this_2 : IsScalarTower S Sₘ L
this_3 : IsFractionRing.{u_4, u_1} Rₘ K
this_4 : IsFractionRing.{u_5, u_2} Sₘ L
this : IsDomain Rₘ
x : R
⊢ Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
        ((AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Rₘ K)) : (a : K) → FractionRing Rₘ)
          ((algebraMap R K : (a : R) → K) x)) :
      FractionRing Sₘ)
    ((AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Sₘ L)) : (a : L) → FractionRing Sₘ)
        ((algebraMap R L : (a : R) → L) x) :
      FractionRing Sₘ)
have he : Eq.{u_5 + 1} (α := FractionRing Sₘ)
  ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
      ((algebraMap Rₘ (FractionRing Rₘ) : (a : Rₘ) → FractionRing Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x)) :
    FractionRing Sₘ)
  ((algebraMap Sₘ (FractionRing Sₘ) : (a : Sₘ) → FractionRing Sₘ)
      ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) x : S)) :
    FractionRing Sₘ)
Tactic: rw [algebraMap_apply R Rₘ (FractionRing R), AlgEquiv.coe_ringEquiv, AlgEquiv.commutes,
    algebraMap_apply R S L, algebraMap_apply S Sₘ L, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
inst_7 : Algebra R Rₘ
inst_8 : IsTorsionFree R S
inst_9 : Algebra.IsSeparable.{u_1, u_2} K L
M : Submonoid R
inst_10 : IsLocalization M Rₘ
inst_11 : Algebra Rₘ Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra R Sₘ
inst_14 : IsScalarTower R Rₘ Sₘ
inst_15 : IsScalarTower R S Sₘ
inst_16 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_17 : Algebra.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
inst_18 : IsScalarTower.{u_4, u_4, u_5} Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := algebraMapSubmonoid S M
hM' : LE.le (α := Submonoid S) (algebraMapSubmonoid S M) S⁰
f₁ : RingHom.{u_4, u_1} Rₘ K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
f₂ : RingHom.{u_5, u_2} Sₘ L := IsLocalization.map (M := algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) hM'
algInst : Algebra.{u_4, u_1} Rₘ K := f₁.toAlgebra
algInst_1 : Algebra.{u_5, u_2} Sₘ L := f₂.toAlgebra
this_1 : IsScalarTower R Rₘ K
this_2 : IsScalarTower S Sₘ L
this_3 : IsFractionRing.{u_4, u_1} Rₘ K
this_4 : IsFractionRing.{u_5, u_2} Sₘ L
this : IsDomain Rₘ
x : R
⊢ Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
        ((algebraMap Rₘ (FractionRing Rₘ) : (a : Rₘ) → FractionRing Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x)) :
      FractionRing Sₘ)
    ((algebraMap Sₘ (FractionRing Sₘ) : (a : Sₘ) → FractionRing Sₘ)
        ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) x : S)) :
      FractionRing Sₘ)
have he : Eq.{u_5 + 1} (α := FractionRing Sₘ)
  ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
      ((algebraMap R (FractionRing Rₘ) : (a : R) → FractionRing Rₘ) x) :
    FractionRing Sₘ)
  ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
Tactic: simp only [← algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
inst_7 : Algebra R Rₘ
inst_8 : IsTorsionFree R S
inst_9 : Algebra.IsSeparable.{u_1, u_2} K L
M : Submonoid R
inst_10 : IsLocalization M Rₘ
inst_11 : Algebra Rₘ Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra R Sₘ
inst_14 : IsScalarTower R Rₘ Sₘ
inst_15 : IsScalarTower R S Sₘ
inst_16 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_17 : Algebra.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
inst_18 : IsScalarTower.{u_4, u_4, u_5} Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := algebraMapSubmonoid S M
hM' : LE.le (α := Submonoid S) (algebraMapSubmonoid S M) S⁰
f₁ : RingHom.{u_4, u_1} Rₘ K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
f₂ : RingHom.{u_5, u_2} Sₘ L := IsLocalization.map (M := algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) hM'
algInst : Algebra.{u_4, u_1} Rₘ K := f₁.toAlgebra
algInst_1 : Algebra.{u_5, u_2} Sₘ L := f₂.toAlgebra
this_1 : IsScalarTower R Rₘ K
this_2 : IsScalarTower S Sₘ L
this_3 : IsFractionRing.{u_4, u_1} Rₘ K
this_4 : IsFractionRing.{u_5, u_2} Sₘ L
this : IsDomain Rₘ
x : R
⊢ Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
        ((algebraMap R (FractionRing Rₘ) : (a : R) → FractionRing Rₘ) x) :
      FractionRing Sₘ)
    ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
have he : Eq.{u_5 + 1} (α := FractionRing Sₘ)
  ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
      ((algebraMap Rₘ (FractionRing Rₘ) : (a : Rₘ) → FractionRing Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x)) :
    FractionRing Sₘ)
  ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
Tactic: rw [algebraMap_apply R Rₘ (FractionRing Rₘ), ← algebraMap_apply Rₘ, ← algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
inst_7 : Algebra R Rₘ
inst_8 : IsTorsionFree R S
inst_9 : Algebra.IsSeparable.{u_1, u_2} K L
M : Submonoid R
inst_10 : IsLocalization M Rₘ
inst_11 : Algebra Rₘ Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra R Sₘ
inst_14 : IsScalarTower R Rₘ Sₘ
inst_15 : IsScalarTower R S Sₘ
inst_16 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_17 : Algebra.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
inst_18 : IsScalarTower.{u_4, u_4, u_5} Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := algebraMapSubmonoid S M
hM' : LE.le (α := Submonoid S) (algebraMapSubmonoid S M) S⁰
f₁ : RingHom.{u_4, u_1} Rₘ K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
f₂ : RingHom.{u_5, u_2} Sₘ L := IsLocalization.map (M := algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) hM'
algInst : Algebra.{u_4, u_1} Rₘ K := f₁.toAlgebra
algInst_1 : Algebra.{u_5, u_2} Sₘ L := f₂.toAlgebra
this_1 : IsScalarTower R Rₘ K
this_2 : IsScalarTower S Sₘ L
this_3 : IsFractionRing.{u_4, u_1} Rₘ K
this_4 : IsFractionRing.{u_5, u_2} Sₘ L
this : IsDomain Rₘ
x : R
he :
  Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
        ((algebraMap Rₘ (FractionRing Rₘ) : (a : Rₘ) → FractionRing Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x)) :
      FractionRing Sₘ)
    ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
⊢ Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
        ((algebraMap R (FractionRing Rₘ) : (a : R) → FractionRing Rₘ) x) :
      FractionRing Sₘ)
    ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
have he₁ : Eq.{u_5 + 1} (α := FractionRing Sₘ)
  ((algebraMap Rₘ (FractionRing Sₘ) : (a : Rₘ) → FractionRing Sₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x) :
    FractionRing Sₘ)
  ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
Tactic: rw [algebraMap_apply R Rₘ (FractionRing Rₘ), ← algebraMap_apply Rₘ, ← algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
inst_7 : Algebra R Rₘ
inst_8 : IsTorsionFree R S
inst_9 : Algebra.IsSeparable.{u_1, u_2} K L
M : Submonoid R
inst_10 : IsLocalization M Rₘ
inst_11 : Algebra Rₘ Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra R Sₘ
inst_14 : IsScalarTower R Rₘ Sₘ
inst_15 : IsScalarTower R S Sₘ
inst_16 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_17 : Algebra.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
inst_18 : IsScalarTower.{u_4, u_4, u_5} Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := algebraMapSubmonoid S M
hM' : LE.le (α := Submonoid S) (algebraMapSubmonoid S M) S⁰
f₁ : RingHom.{u_4, u_1} Rₘ K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
f₂ : RingHom.{u_5, u_2} Sₘ L := IsLocalization.map (M := algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) hM'
algInst : Algebra.{u_4, u_1} Rₘ K := f₁.toAlgebra
algInst_1 : Algebra.{u_5, u_2} Sₘ L := f₂.toAlgebra
this_1 : IsScalarTower R Rₘ K
this_2 : IsScalarTower S Sₘ L
this_3 : IsFractionRing.{u_4, u_1} Rₘ K
this_4 : IsFractionRing.{u_5, u_2} Sₘ L
this : IsDomain Rₘ
x : R
he :
  Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
        ((algebraMap Rₘ (FractionRing Rₘ) : (a : Rₘ) → FractionRing Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x)) :
      FractionRing Sₘ)
    ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
he₁ :
  Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap Rₘ (FractionRing Sₘ) : (a : Rₘ) → FractionRing Sₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x) :
      FractionRing Sₘ)
    ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
⊢ Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
        ((algebraMap R (FractionRing Rₘ) : (a : R) → FractionRing Rₘ) x) :
      FractionRing Sₘ)
    ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
have he₂ : Eq.{u_5 + 1} (α := FractionRing Sₘ) ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
  ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
Tactic: rw [algebraMap_apply R Rₘ (FractionRing Rₘ), ← algebraMap_apply Rₘ, ← algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
⊢ IsTorsionFree S Sₚ
have rw : ∀ (c : ↥P'), IsRegular (↑c : S)
Tactic: rw [isTorsionFree_iff_algebraMap_injective,
    injective_iff_isRegular (algebraMapSubmonoid S P.primeCompl)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
⊢ IsTorsionFree.{u_1, u_2} R Sₚ
have this : FaithfulSMul R Rₚ
Tactic: have := IsLocalization.AtPrime.faithfulSMul Rₚ R P
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
⊢ IsScalarTower.{u_1, u_2, u_2} Rₚ Sₚ L
have refine : Eq (α := RingHom.{u_1, u_2} R L)
  (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
  (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L) (algebraMap Rₚ Sₚ)) (algebraMap R Rₚ))
Tactic: refine IsScalarTower.of_algebraMap_eq' <| IsLocalization.ringHom_ext P.primeCompl ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
⊢ Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L) (algebraMap Rₚ Sₚ)) (algebraMap R Rₚ))
have rw : Eq (α := RingHom.{u_1, u_2} R L)
  (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
  (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ Sₚ) (algebraMap R Rₚ)))
Tactic: rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq R Rₚ Sₚ, IsScalarTower.algebraMap_eq R S Sₚ,
    ← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq S Sₚ L, IsScalarTower.algebraMap_eq Rₚ K L,
    RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
    ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
rw :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L)
      (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ Sₚ) (algebraMap R Rₚ)))
⊢ Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L) (algebraMap Rₚ Sₚ)) (algebraMap R Rₚ))
have rw₁ : Eq (α := RingHom.{u_1, u_2} R L)
  (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
  (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L) (algebraMap R Sₚ))
Tactic: rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq R Rₚ Sₚ, IsScalarTower.algebraMap_eq R S Sₚ,
    ← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq S Sₚ L, IsScalarTower.algebraMap_eq Rₚ K L,
    RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
    ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
rw :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L)
      (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ Sₚ) (algebraMap R Rₚ)))
rw₁ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L) (algebraMap R Sₚ))
⊢ Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L) (algebraMap Rₚ Sₚ)) (algebraMap R Rₚ))
have rw₂ : Eq (α := RingHom.{u_1, u_2} R L)
  (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
  (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S)))
Tactic: rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq R Rₚ Sₚ, IsScalarTower.algebraMap_eq R S Sₚ,
    ← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq S Sₚ L, IsScalarTower.algebraMap_eq Rₚ K L,
    RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
    ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
rw :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L)
      (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ Sₚ) (algebraMap R Rₚ)))
rw₁ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L) (algebraMap R Sₚ))
rw₂ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S)))
⊢ Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L) (algebraMap Rₚ Sₚ)) (algebraMap R Rₚ))
have rw₃ : Eq (α := RingHom.{u_1, u_2} R L)
  (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L) (algebraMap S Sₚ)) (algebraMap R S))
Tactic: rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq R Rₚ Sₚ, IsScalarTower.algebraMap_eq R S Sₚ,
    ← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq S Sₚ L, IsScalarTower.algebraMap_eq Rₚ K L,
    RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
    ← IsScalarTower.algebraMap_eq]