awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : IsLocalRing A
inst_4 : IsDedekindDomain A
inst_5 : Algebra R A
inst_6 : FaithfulSMul R A
inst_7 : Module.Finite R A
p : Ideal R
inst_8 : p.IsMaximal
hp0 : p ≠ ⊥
this : IsDomain R
rw : (↑(IsDedekindDomain.primesOverFinset p A) : Set (Ideal A)) = {maximalIdeal A}
⊢ Eq (α := Finset (Ideal A)) (IsDedekindDomain.primesOverFinset p A) {maximalIdeal A}
have rw₁ : Eq (α := Set (Ideal A)) (p.primesOver A) {maximalIdeal A}
Tactic: rw [← Finset.coe_eq_singleton, IsDedekindDomain.coe_primesOverFinset hp0,
    IsLocalRing.primesOver_eq A hp0]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : IsLocalRing A
inst_4 : IsDedekindDomain A
inst_5 : Algebra R A
inst_6 : FaithfulSMul R A
inst_7 : Module.Finite R A
p : Ideal R
inst_8 : p.IsMaximal
hp0 : p ≠ ⊥
this : IsDomain R
rw : (↑(IsDedekindDomain.primesOverFinset p A) : Set (Ideal A)) = {maximalIdeal A}
rw₁ : Eq (α := Set (Ideal A)) (p.primesOver A) {maximalIdeal A}
⊢ Eq (α := Finset (Ideal A)) (IsDedekindDomain.primesOverFinset p A) {maximalIdeal A}
have rw₂ : Eq (α := Set (Ideal A)) {maximalIdeal A} {maximalIdeal A}
Tactic: rw [← Finset.coe_eq_singleton, IsDedekindDomain.coe_primesOverFinset hp0,
    IsLocalRing.primesOver_eq A hp0]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
A_1 : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A_1
inst_2 : Field K
A : Type u_4
inst_3 : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst_4 : CommRing B
inst_5 : IsDedekindDomain B
inst_6 : Algebra A B
inst_7 : IsDomain A
inst_8 : IsTorsionFree A B
hp : p ≠ 0
v : HeightOneSpectrum B
hv :
  Membership.mem (γ := Set (HeightOneSpectrum B))
    (fun (v : HeightOneSpectrum B) ↦ ∃ (c : Ideal B), map (F := A →+* B) (algebraMap A B) p = v.asIdeal * c) v
⊢ v.asIdeal.LiesOver p
have rwa : v.asIdeal ∣ map (F := A →+* B) (algebraMap A B) p
Tactic: rwa [liesOver_iff_dvd_map v.isPrime.ne_top]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
inst_6 : Algebra.IsIntegral A B
⊢ Set.Finite (α := Ideal B) (p.primesOver B)
have pos : ∀ (hpb : p = ⊥), Set.Finite (α := Ideal B) (p.primesOver B)
Tactic: by_cases hpb : p = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
inst_6 : Algebra.IsIntegral A B
pos : ∀ (hpb : p = ⊥), Set.Finite (α := Ideal B) (p.primesOver B)
⊢ Set.Finite (α := Ideal B) (p.primesOver B)
have neg : ∀ (hpb : ¬p = ⊥), Set.Finite (α := Ideal B) (p.primesOver B)
Tactic: by_cases hpb : p = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
inst_6 : Algebra.IsIntegral A B
hpb : p = ⊥
⊢ Set.Finite (α := Ideal B) (p.primesOver B)
have pos : ∀ (hpm : IsMaximal.{u_4} (α := A) ⊥) (B : Type u_5) [inst_7 : CommRing B] [IsDedekindDomain B] [inst_9 : Algebra A B]
  [IsDomain A] [IsTorsionFree A B] [Algebra.IsIntegral A B] (hpb : p = ⊥),
  Set.Finite (α := Ideal B) (primesOver.{u_4, u_5} (A := A) ⊥ B)
Tactic: rw [hpb] at hpm ⊢
Cleared hypotheses: hpm, B, inst_1, inst_2, inst_3, inst_4, inst_5, inst_6, hpb
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : IsMaximal.{u_4} (α := A) ⊥
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
inst_6 : Algebra.IsIntegral A B
hpb : p = ⊥
this : IsDomain A
⊢ Set.Finite (α := Ideal B) (primesOver.{u_4, u_5} (A := A) ⊥ B)
have pos : Set.Finite (α := Ideal B) {⊥}
Tactic: rw [primesOver_bot A B]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
inst_6 : Algebra.IsIntegral A B
hpb : ¬p = ⊥
⊢ Set.Finite (α := Ideal B) (p.primesOver B)
have neg : (↑(primesOverFinset p B) : Set (Ideal B)).Finite
Tactic: rw [← coe_primesOverFinset hpb B]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
inst_6 : Algebra.IsIntegral A B
⊢ Set.ncard (α := Ideal B) (p.primesOver B) ≠ 0
have rcases : ∀ (P : Ideal B) (hPm : P.IsMaximal) (hp : P.LiesOver p), Set.ncard (α := Ideal B) (p.primesOver B) ≠ 0
Tactic: rcases exists_maximal_ideal_liesOver_of_isIntegral (S := B) p with ⟨P, hPm, hp⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : Algebra R A
inst_4 : FaithfulSMul R A
inst_5 : Algebra.IsIntegral R A
inst_6 : Nontrivial.{u_1} (HeightOneSpectrum R)
⊢ Nontrivial.{u_2} (HeightOneSpectrum A)
have this : IsDomain R
Tactic: have := (FaithfulSMul.algebraMap_injective R A).isDomain
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : Algebra R A
inst_4 : FaithfulSMul R A
inst_5 : Algebra.IsIntegral R A
inst_6 : Nontrivial.{u_1} (HeightOneSpectrum R)
this : IsDomain R
f : (p : HeightOneSpectrum A) → HeightOneSpectrum R := fun (p : HeightOneSpectrum A) ↦ HeightOneSpectrum.under R p
x : HeightOneSpectrum R
p : Ideal R
isPrime : p.IsPrime
hp : p ≠ ⊥
⊢ ∃ (a : HeightOneSpectrum A), f a = { asIdeal := p, isPrime := isPrime, ne_bot := hp }
have obtain : ∀ (P : Ideal A) (hP : P.IsPrime) (isPrime : Ideal.IsPrime (Ideal.comap (F := R →+* A) (algebraMap R A) P))
  (hp : Ne (α := Ideal R) (Ideal.comap (F := R →+* A) (algebraMap R A) P) ⊥),
  ∃ (a : HeightOneSpectrum A),
    f a = { asIdeal := Ideal.comap (F := R →+* A) (algebraMap R A) P, isPrime := isPrime, ne_bot := hp }
Tactic: obtain ⟨P, hP, rfl⟩ := p.exists_ideal_over_prime_of_isIntegral_of_isDomain (S := A) (by simp)
Cleared hypotheses: p, isPrime, hp
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : Algebra R A
inst_4 : FaithfulSMul R A
inst_5 : Algebra.IsIntegral R A
inst_6 : Nontrivial.{u_1} (HeightOneSpectrum R)
this : IsDomain R
f : (p : HeightOneSpectrum A) → HeightOneSpectrum R := fun (p : HeightOneSpectrum A) ↦ HeightOneSpectrum.under R p
⊢ Nontrivial.{u_2} (HeightOneSpectrum A)
have this₁ : Function.Surjective f
Tactic: have : Function.Surjective f := fun ⟨p, _, hp⟩ ↦ by
    obtain ⟨P, hP, rfl⟩ := p.exists_ideal_over_prime_of_isIntegral_of_isDomain (S := A) (by simp)
    exact ⟨⟨P, hP, by aesop⟩, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (hypothesis)
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
⊢ Algebra.IsSeparable.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
have hM' : LE.le (α := Submonoid S) (algebraMapSubmonoid S M) S⁰
Tactic: have hM' : algebraMapSubmonoid S M ≤ S⁰ := algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul
    _ hM
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (hypothesis)
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
⊢ Algebra.IsSeparable.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
have this : IsScalarTower R Rₘ K
Tactic: have := localization_isScalarTower_of_submonoid_le Rₘ K _ _ hM
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (hypothesis)
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 : IsScalarTower R Rₘ K
⊢ Algebra.IsSeparable.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
have this₁ : IsScalarTower S Sₘ L
Tactic: have := localization_isScalarTower_of_submonoid_le Sₘ L _ _ hM'
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (hypothesis)
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 : IsScalarTower S Sₘ L
⊢ Algebra.IsSeparable.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
have this₁ : IsFractionRing.{u_4, u_1} Rₘ K
Tactic: have := isFractionRing_of_isDomain_of_isLocalization M Rₘ K
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (hypothesis)
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 : IsFractionRing.{u_4, u_1} Rₘ K
⊢ Algebra.IsSeparable.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
have this₁ : IsFractionRing.{u_5, u_2} Sₘ L
Tactic: have := isFractionRing_of_isDomain_of_isLocalization M' Sₘ L
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Instances (hypothesis)
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 : IsFractionRing.{u_5, u_2} Sₘ L
⊢ Algebra.IsSeparable.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
have this₁ : IsDomain Rₘ
Tactic: have : IsDomain Rₘ := isDomain_of_le_nonZeroDivisors _ hM
-- 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ₘ
⊢ Algebra.IsSeparable.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
have he : Eq (α := RingHom.{u_1, u_5} K (FractionRing Sₘ))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing Rₘ) (FractionRing Sₘ))
    (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Rₘ K))) : K →+* FractionRing Rₘ))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Sₘ L))) : L →+* FractionRing Sₘ) (algebraMap K L))
Tactic: apply Algebra.IsSeparable.of_equiv_equiv (FractionRing.algEquiv Rₘ K).symm.toRingEquiv
    (FractionRing.algEquiv Sₘ L).symm.toRingEquiv
-- 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ₘ
⊢ Eq (α := RingHom.{u_1, u_5} K (FractionRing Sₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing Rₘ) (FractionRing Sₘ))
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Rₘ K))) : K →+* FractionRing Rₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Sₘ L))) : L →+* FractionRing Sₘ) (algebraMap K L))
have he : Eq (α := RingHom.{u_1, u_5} R (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))
  (@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))
Tactic: apply ringHom_ext R⁰
-- 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ₘ
⊢ Eq (α := RingHom.{u_1, u_5} R (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))
    (@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))
have he : ∀ (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ₘ)
Tactic: ext