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
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)))
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))
⊢ 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 _ (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ₚ))
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)))
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))
rw₄ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ _ _ _ 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 _
    (@RingHom.comp _ K _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap Rₚ K)) (algebraMap R Rₚ))
  (@RingHom.comp _ _ _ _ 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ₚ))
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)))
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))
rw₄ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
rw₅ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ K _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap Rₚ K)) (algebraMap R Rₚ))
    (@RingHom.comp _ _ _ _ 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 _ K _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ K) (algebraMap R Rₚ)))
  (@RingHom.comp _ _ _ _ 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ₚ))
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)))
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))
rw₄ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
rw₅ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ K _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap Rₚ K)) (algebraMap R Rₚ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
rw₆ :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ K _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
      (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ K) (algebraMap R Rₚ)))
    (@RingHom.comp _ _ _ _ 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 _ K _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K))
  (@RingHom.comp _ _ _ _ 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
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
⊢ IsLocalization (algebraMapSubmonoid T P') Tₚ
have rw : IsLocalization P'' Tₚ
Tactic: rw [show algebraMapSubmonoid T P' = P'' by simp]
-- 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
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
⊢ Eq (α := RingHom.{u_2, u_3} S Tₚ) (algebraMap S Tₚ)
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ) (algebraMap S Sₚ))
have rw : Eq (α := RingHom.{u_2, u_3} S Tₚ) (algebraMap S Tₚ)
  (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _
    (IsLocalization.map (M := P') (T := algebraMapSubmonoid T P') Tₚ (algebraMap S T) sorry) (algebraMap S Sₚ))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← 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
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
rw :
  Eq (α := RingHom.{u_2, u_3} S Tₚ) (algebraMap S Tₚ)
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map (M := P') (T := algebraMapSubmonoid T P') Tₚ (algebraMap S T) ⋯) (algebraMap S Sₚ))
⊢ Eq (α := RingHom.{u_2, u_3} S Tₚ) (algebraMap S Tₚ)
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ) (algebraMap S Sₚ))
have rw₁ : Eq (α := RingHom.{u_2, u_3} S Tₚ) (algebraMap S Tₚ)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap T Tₚ) (algebraMap S T))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← 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
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
rw :
  Eq (α := RingHom.{u_2, u_3} S Tₚ) (algebraMap S Tₚ)
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map (M := P') (T := algebraMapSubmonoid T P') Tₚ (algebraMap S T) ⋯) (algebraMap S Sₚ))
rw₁ :
  Eq (α := RingHom.{u_2, u_3} S Tₚ) (algebraMap S Tₚ)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap T Tₚ) (algebraMap S T))
⊢ Eq (α := RingHom.{u_2, u_3} S Tₚ) (algebraMap S Tₚ)
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ) (algebraMap S Sₚ))
have rw₂ : Eq (α := RingHom.{u_2, u_3} S Tₚ) (algebraMap S Tₚ) (algebraMap S Tₚ)
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← 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
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
⊢ Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
    (@RingHom.comp.{u_1, u_2, u_3} _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ) (algebraMap R Sₚ))
have rw : Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
  (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S)))
Tactic: rw [IsScalarTower.algebraMap_eq R S Sₚ, ← RingHom.comp_assoc,
      ← IsScalarTower.algebraMap_eq S, ← 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
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
rw :
  Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S)))
⊢ Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
    (@RingHom.comp.{u_1, u_2, u_3} _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ) (algebraMap R Sₚ))
have rw₁ : Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ) (algebraMap S Sₚ)) (algebraMap R S))
Tactic: rw [IsScalarTower.algebraMap_eq R S Sₚ, ← RingHom.comp_assoc,
      ← IsScalarTower.algebraMap_eq S, ← 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
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
rw :
  Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S)))
rw₁ :
  Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ) (algebraMap S Sₚ)) (algebraMap R S))
⊢ Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
    (@RingHom.comp.{u_1, u_2, u_3} _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ) (algebraMap R Sₚ))
have rw₂ : Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Tₚ) (algebraMap R S))
Tactic: rw [IsScalarTower.algebraMap_eq R S Sₚ, ← RingHom.comp_assoc,
      ← IsScalarTower.algebraMap_eq S, ← 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
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
rw :
  Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S)))
rw₁ :
  Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ) (algebraMap S Sₚ)) (algebraMap R S))
rw₂ :
  Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Tₚ) (algebraMap R S))
⊢ Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
    (@RingHom.comp.{u_1, u_2, u_3} _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ) (algebraMap R Sₚ))
have rw₃ : Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ) (algebraMap R Tₚ)
Tactic: rw [IsScalarTower.algebraMap_eq R S Sₚ, ← RingHom.comp_assoc,
      ← IsScalarTower.algebraMap_eq S, ← 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
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
inst_12 : IsTorsionFree R T
⊢ IsScalarTower.{u_1, u_2, u_3} Rₚ Sₚ Tₚ
have refine : ∀ (a : Rₚ) (b : Sₚ) (c : Tₚ) (x : R × ↥P.primeCompl) (a₁ : R) (a₂ : ↥P.primeCompl),
  HSMul.hSMul (α := Rₚ) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) b • c =
    HSMul.hSMul (α := Rₚ) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) (b • c)
Tactic: refine ⟨fun a b c ↦ a.ind fun ⟨a₁, a₂⟩ ↦ ?_⟩
-- 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
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
inst_12 : IsTorsionFree R T
a : Rₚ
b : Sₚ
c : Tₚ
x : R × ↥P.primeCompl
a₁ : R
a₂ : ↥P.primeCompl
⊢ HSMul.hSMul (α := Rₚ) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) b • c =
    HSMul.hSMul (α := Rₚ) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) (b • c)
have this : (↑a₂ : R) ≠ 0
Tactic: have : a₂.val ≠ 0 := nonZeroDivisors.ne_zero <| Ideal.primeCompl_le_nonZeroDivisors P <| a₂.prop
-- 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
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
inst_12 : IsTorsionFree R T
inst_13 : IsTorsionFree S T
inst_14 : Algebra.IsSeparable.{u_2, u_3} L F
⊢ Algebra.IsSeparable.{u_2, u_3} (FractionRing Sₚ) (FractionRing Tₚ)
have refine : LE.le (α := Submonoid S) P' S⁰
Tactic: refine FractionRing.isSeparable_of_isLocalization T Sₚ Tₚ (M := 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
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
inst_12 : IsTorsionFree R T
inst_13 : IsTorsionFree S T
inst_14 : Algebra.IsSeparable.{u_2, u_3} L F
⊢ LE.le (α := Submonoid S) P' S⁰
have hS : P.primeCompl ≤ R⁰
Tactic: apply algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (hypothesis)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
⊢ IsLocalization (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) L
have this : IsDomain C
Tactic: haveI : IsDomain C :=
    (IsIntegralClosure.equiv A C L (integralClosure A L)).toMulEquiv.isDomain (integralClosure A L)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (hypothesis)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this : IsDomain C
⊢ IsLocalization (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) L
have this₁ : IsTorsionFree A L
Tactic: haveI : IsTorsionFree A L := .trans_faithfulSMul A K L
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (hypothesis)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this : IsTorsionFree A L
⊢ IsLocalization (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) L
have this₁ : IsTorsionFree A C
Tactic: haveI : IsTorsionFree A C := IsIntegralClosure.isTorsionFree A L