awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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
rcases : ∀ (P : Ideal B) (hPm : P.IsMaximal) (hp : P.LiesOver p), Set.ncard (α := Ideal B) (p.primesOver B) ≠ 0
⊢ Set.ncard (α := Ideal B) (p.primesOver B) ≠ 0

Tactic:
rcases exists_maximal_ideal_liesOver_of_isIntegral (S := B) p with ⟨P, hPm, hp⟩

Premises used: Ideal.exists_maximal_ideal_liesOver_of_isIntegral
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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
P : Ideal B
hPm : P.IsMaximal
hp : P.LiesOver p
⊢ Set.ncard (α := Ideal B) (p.primesOver B) ≠ 0

Tactic:
Set.ncard_ne_zero_of_mem ⟨hPm.isPrime, hp⟩ (primesOver_finite p B)

Premises used: Ideal.IsMaximal.isPrime, And.intro, IsDedekindDomain.primesOver_finite, Set.ncard_ne_zero_of_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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
P : Ideal B
hPm : P.IsMaximal
hp : P.LiesOver p
⊢ Set.ncard (α := Ideal B) (p.primesOver B) ≠ 0

Tactic:
exact Set.ncard_ne_zero_of_mem ⟨hPm.isPrime, hp⟩ (primesOver_finite p B)
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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
⊢ 1 ≤ Set.ncard (α := Ideal B) (p.primesOver B)

Tactic:
Nat.one_le_iff_ne_zero.mpr (primesOver_ncard_ne_zero p B)

Premises used: Iff.mpr, IsDedekindDomain.primesOver_ncard_ne_zero, Nat.one_le_iff_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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)
⊢ IsDomain R

Tactic:
have := (FaithfulSMul.algebraMap_injective R A).isDomain
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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 ≠ ⊥
⊢ RingHom.ker (F := R →+* A) (algebraMap R A) ≤ p

Tactic:
simp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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 ≠ ⊥
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 }
⊢ ∃ (a : HeightOneSpectrum A), f a = { asIdeal := p, isPrime := isPrime, ne_bot := hp }

Tactic:
obtain ⟨P, hP, rfl⟩ := p.exists_ideal_over_prime_of_isIntegral_of_isDomain (S := A) (by simp)

Premises used: Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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 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) ⊥
⊢ P ≠ ⊥

Tactic:
aesop
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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 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:
exact ⟨⟨P, hP, by aesop⟩, rfl⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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
⊢ 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⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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_1 : IsDomain R
f : (p : HeightOneSpectrum A) → HeightOneSpectrum R := fun (p : HeightOneSpectrum A) ↦ HeightOneSpectrum.under R p
this : Function.Surjective f
⊢ Nontrivial.{u_2} (HeightOneSpectrum A)

Tactic:
this.nontrivial

Premises used: Function.Surjective.nontrivial
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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_1 : IsDomain R
f : (p : HeightOneSpectrum A) → HeightOneSpectrum R := fun (p : HeightOneSpectrum A) ↦ HeightOneSpectrum.under R p
this : Function.Surjective f
⊢ Nontrivial.{u_2} (HeightOneSpectrum A)

Tactic:
exact this.nontrivial

Premises used: Function.Surjective.nontrivial
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
A : Type u_4
B : Type u_5
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Algebra A B
inst_3 : NoZeroDivisors B
inst_4 : FaithfulSMul A B
S : Submonoid A
hS : S ≤ A⁰
⊢ LE.le (α := Submonoid B) (algebraMapSubmonoid B S) B⁰

Tactic:
map_le_nonZeroDivisors_of_injective _ (FaithfulSMul.algebraMap_injective A B) hS

Premises used: Set.Mem, map_le_nonZeroDivisors_of_injective, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
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
⊢ LE.le (α := Submonoid S) (algebraMapSubmonoid S M) S⁰

Tactic:
have hM' : algebraMapSubmonoid S M ≤ S⁰ := algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul
    _ hM
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
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
⊢ IsScalarTower R Rₘ K

Tactic:
have := localization_isScalarTower_of_submonoid_le Rₘ K _ _ hM
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
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
⊢ IsScalarTower S Sₘ L

Tactic:
have := localization_isScalarTower_of_submonoid_le Sₘ L _ _ hM'
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
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
⊢ IsFractionRing.{u_4, u_1} Rₘ K

Tactic:
have := isFractionRing_of_isDomain_of_isLocalization M Rₘ K
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
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
⊢ IsFractionRing.{u_5, u_2} Sₘ L

Tactic:
have := isFractionRing_of_isDomain_of_isLocalization M' Sₘ L
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
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
⊢ IsDomain Rₘ

Tactic:
have : IsDomain Rₘ := isDomain_of_le_nonZeroDivisors _ hM
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
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ₘ
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))
⊢ Algebra.IsSeparable.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)

Tactic:
apply Algebra.IsSeparable.of_equiv_equiv (FractionRing.algEquiv Rₘ K).symm.toRingEquiv
    (FractionRing.algEquiv Sₘ L).symm.toRingEquiv
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
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ₘ
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))
⊢ 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 ringHom_ext R⁰

Premises used: nonZeroDivisors, IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
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ₘ
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ₘ)
⊢ 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:
ext