awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
P : Ideal B
inst_9 : P.IsPrime
hPbot : P ≠ ⊥
hp : Ne (α := Ideal A) (Ideal.under A P) ⊥
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P)) ⊥
this_1 : P.IsMaximal
this : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H :
  Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.comap (F := A →+* B) (algebraMap A B) P) ≤ P ^ HAdd.hAdd (α := ℕ) 1 1
⊢ P ^ HSub.hSub (α := ℕ) 2 1 ∣ differentIdeal A B
have inr : HPow.hPow (β := ℕ) P 2 ∣ Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P)
Tactic: apply pow_sub_one_dvd_differentIdeal _ _ _ hp
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
P : Ideal B
inst_9 : P.IsPrime
hPbot : P ≠ ⊥
hp : Ne (α := Ideal A) (Ideal.under A P) ⊥
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P)) ⊥
this_1 : P.IsMaximal
this : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : IsUnramifiedAt A P
⊢ ¬P ∣ differentIdeal A B
have inr : ∀ (Q : Ideal B) (h₁ : P ⊔ Q = ⊤)
  (h₂ :
    Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P) =
      P ^
          Multiset.count P
            (UniqueFactorizationMonoid.normalizedFactors
              (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P))) *
        Q),
  ¬P ∣ differentIdeal A B
Tactic: obtain ⟨Q, h₁, h₂⟩ := Ideal.eq_prime_pow_mul_coprime hp' P
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
P : Ideal B
inst_9 : P.IsPrime
hPbot : P ≠ ⊥
hp : Ne (α := Ideal A) (Ideal.under A P) ⊥
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P)) ⊥
this_1 : P.IsMaximal
this : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : IsUnramifiedAt A P
Q : Ideal B
h₁ : P ⊔ Q = ⊤
h₂ :
  Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P) =
    P ^
        Multiset.count P
          (UniqueFactorizationMonoid.normalizedFactors (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P))) *
      Q
⊢ ¬P ∣ differentIdeal A B
have h₃ : Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P) = P * Q
Tactic: rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp' ‹_› hPbot,
      Ideal.ramificationIdx_eq_one_of_isUnramifiedAt hPbot, pow_one] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
P : Ideal B
inst_9 : P.IsPrime
hPbot : P ≠ ⊥
hp : Ne (α := Ideal A) (Ideal.under A P) ⊥
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P)) ⊥
this_1 : P.IsMaximal
this : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : IsUnramifiedAt A P
Q : Ideal B
h₁ : P ⊔ Q = ⊤
h₂ : Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P) = P * Q
⊢ ¬P ∣ differentIdeal A B
have h₃ : Algebra.IsSeparable.{u_1, u_3} (Ideal.ResidueField (Ideal.under A P)) P.ResidueField
Tactic: obtain ⟨h₃, h₄⟩ := (Algebra.isUnramifiedAt_iff_map_eq (p := P.under A) _ _).mp H
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
P : Ideal B
inst_9 : P.IsPrime
hPbot : P ≠ ⊥
hp : Ne (α := Ideal A) (Ideal.under A P) ⊥
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P)) ⊥
this_1 : P.IsMaximal
this : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : IsUnramifiedAt A P
Q : Ideal B
h₁ : P ⊔ Q = ⊤
h₂ : Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P) = P * Q
h₃ : Algebra.IsSeparable.{u_1, u_3} (Ideal.ResidueField (Ideal.under A P)) P.ResidueField
⊢ ¬P ∣ differentIdeal A B
have h₄ : Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
  (Ideal.map (F := RingHom.{u_1, u_3} A (Localization.AtPrime P)) (algebraMap A (Localization.AtPrime P))
    (Ideal.under A P))
  (IsLocalRing.maximalIdeal (Localization.AtPrime P))
Tactic: obtain ⟨h₃, h₄⟩ := (Algebra.isUnramifiedAt_iff_map_eq (p := P.under A) _ _).mp H
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
P : Ideal B
inst_9 : P.IsPrime
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
have inl : ∀ [inst_10 : Ideal.IsPrime.{u_3} (α := B) ⊥],
  ¬Dvd.dvd (α := Ideal B) ⊥ (differentIdeal A B) ↔ IsUnramifiedAt.{u_1, u_3} A (A := B) ⊥
Tactic: classical
  rcases eq_or_ne P ⊥ with rfl | hPbot
  · simp_rw [← Ideal.zero_eq_bot, zero_dvd_iff]
    simp only [Submodule.zero_eq_bot, differentIdeal_ne_bot, not_false_eq_true, true_iff]
    let K := FractionRing A
    let L := FractionRing B
    have : IsLocalization B⁰ (Localization.AtPrime (⊥ : Ideal B)) := by
      convert!
        (inferInstance :
          IsLocalization (⊥ : Ideal B).primeCompl (Localization.AtPrime (⊥ : Ideal B)))
      ext; simp [Ideal.primeCompl]
    refine (Algebra.FormallyUnramified.iff_of_equiv (A := L)
      ((IsLocalization.algEquiv B⁰ _ _).restrictScalars A)).mp ?_
    have : Algebra.FormallyUnramified K L := by
      rwa [Algebra.FormallyUnramified.iff_isSeparable]
    refine .comp A K L
  have hp : P.under A ≠ ⊥ := mt Ideal.eq_bot_of_comap_eq_bot hPbot
  have hp' := (Ideal.map_eq_bot_iff_of_injective
    (FaithfulSMul.algebraMap_injective A B)).not.mpr hp
  have := Ideal.IsPrime.isMaximal inferInstance hPbot
  let := Localization.AtPrime.algebraOfLiesOver (P.under A) P
  constructor
  · intro H
    · rw [Algebra.isUnramifiedAt_iff_map_eq (p := P.under A)]
      constructor
      · suffices Algebra.IsSeparable (A ⧸ P.under A) (B ⧸ P) by infer_instance
        contrapose H
        exact dvd_differentIdeal_of_not_isSeparable A hp P H
      · rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hPbot Ideal.map_comap_le]
        apply Ideal.ramificationIdx_spec
        · simp [Ideal.map_le_iff_le_comap]
        · contrapose H
          rw [← pow_one P, show 1 = 2 - 1 by simp]
          apply pow_sub_one_dvd_differentIdeal _ _ _ hp
          simpa [Ideal.dvd_iff_le] using H
  · intro H
    obtain ⟨Q, h₁, h₂⟩ := Ideal.eq_prime_pow_mul_coprime hp' P
    rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp' ‹_› hPbot,
      Ideal.ramificationIdx_eq_one_of_isUnramifiedAt hPbot, pow_one] at h₂
    obtain ⟨h₃, h₄⟩ := (Algebra.isUnramifiedAt_iff_map_eq (p := P.under A) _ _).mp H
    exact not_dvd_differentIdeal_of_isCoprime_of_isSeparable
      A P Q (Ideal.isCoprime_iff_sup_eq.mpr h₁) h₂.symm
Cleared hypotheses: P, inst_9
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
P : Ideal B
inst_9 : P.IsPrime
inl :
  ∀ [inst_10 : Ideal.IsPrime.{u_3} (α := B) ⊥],
    ¬Dvd.dvd (α := Ideal B) ⊥ (differentIdeal A B) ↔ IsUnramifiedAt.{u_1, u_3} A (A := B) ⊥
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
have inr : ∀ (hPbot : P ≠ ⊥), ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
Tactic: classical
  rcases eq_or_ne P ⊥ with rfl | hPbot
  · simp_rw [← Ideal.zero_eq_bot, zero_dvd_iff]
    simp only [Submodule.zero_eq_bot, differentIdeal_ne_bot, not_false_eq_true, true_iff]
    let K := FractionRing A
    let L := FractionRing B
    have : IsLocalization B⁰ (Localization.AtPrime (⊥ : Ideal B)) := by
      convert!
        (inferInstance :
          IsLocalization (⊥ : Ideal B).primeCompl (Localization.AtPrime (⊥ : Ideal B)))
      ext; simp [Ideal.primeCompl]
    refine (Algebra.FormallyUnramified.iff_of_equiv (A := L)
      ((IsLocalization.algEquiv B⁰ _ _).restrictScalars A)).mp ?_
    have : Algebra.FormallyUnramified K L := by
      rwa [Algebra.FormallyUnramified.iff_isSeparable]
    refine .comp A K L
  have hp : P.under A ≠ ⊥ := mt Ideal.eq_bot_of_comap_eq_bot hPbot
  have hp' := (Ideal.map_eq_bot_iff_of_injective
    (FaithfulSMul.algebraMap_injective A B)).not.mpr hp
  have := Ideal.IsPrime.isMaximal inferInstance hPbot
  let := Localization.AtPrime.algebraOfLiesOver (P.under A) P
  constructor
  · intro H
    · rw [Algebra.isUnramifiedAt_iff_map_eq (p := P.under A)]
      constructor
      · suffices Algebra.IsSeparable (A ⧸ P.under A) (B ⧸ P) by infer_instance
        contrapose H
        exact dvd_differentIdeal_of_not_isSeparable A hp P H
      · rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hPbot Ideal.map_comap_le]
        apply Ideal.ramificationIdx_spec
        · simp [Ideal.map_le_iff_le_comap]
        · contrapose H
          rw [← pow_one P, show 1 = 2 - 1 by simp]
          apply pow_sub_one_dvd_differentIdeal _ _ _ hp
          simpa [Ideal.dvd_iff_le] using H
  · intro H
    obtain ⟨Q, h₁, h₂⟩ := Ideal.eq_prime_pow_mul_coprime hp' P
    rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp' ‹_› hPbot,
      Ideal.ramificationIdx_eq_one_of_isUnramifiedAt hPbot, pow_one] at h₂
    obtain ⟨h₃, h₄⟩ := (Algebra.isUnramifiedAt_iff_map_eq (p := P.under A) _ _).mp H
    exact not_dvd_differentIdeal_of_isCoprime_of_isSeparable
      A P Q (Ideal.isCoprime_iff_sup_eq.mpr h₁) h₂.symm
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
P : Ideal B
inst_9 : P.IsPrime
inl :
  ∀ [inst_10 : Ideal.IsPrime.{u_3} (α := B) ⊥],
    ¬Dvd.dvd (α := Ideal B) ⊥ (differentIdeal A B) ↔ IsUnramifiedAt.{u_1, u_3} A (A := B) ⊥
inr inr₁ : ∀ (hPbot : P ≠ ⊥), ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
have inr₂ : ∀ (hPbot : P ≠ ⊥) (hp : Ne (α := Ideal A) (Ideal.under A P) ⊥), ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
Tactic: classical
  rcases eq_or_ne P ⊥ with rfl | hPbot
  · simp_rw [← Ideal.zero_eq_bot, zero_dvd_iff]
    simp only [Submodule.zero_eq_bot, differentIdeal_ne_bot, not_false_eq_true, true_iff]
    let K := FractionRing A
    let L := FractionRing B
    have : IsLocalization B⁰ (Localization.AtPrime (⊥ : Ideal B)) := by
      convert!
        (inferInstance :
          IsLocalization (⊥ : Ideal B).primeCompl (Localization.AtPrime (⊥ : Ideal B)))
      ext; simp [Ideal.primeCompl]
    refine (Algebra.FormallyUnramified.iff_of_equiv (A := L)
      ((IsLocalization.algEquiv B⁰ _ _).restrictScalars A)).mp ?_
    have : Algebra.FormallyUnramified K L := by
      rwa [Algebra.FormallyUnramified.iff_isSeparable]
    refine .comp A K L
  have hp : P.under A ≠ ⊥ := mt Ideal.eq_bot_of_comap_eq_bot hPbot
  have hp' := (Ideal.map_eq_bot_iff_of_injective
    (FaithfulSMul.algebraMap_injective A B)).not.mpr hp
  have := Ideal.IsPrime.isMaximal inferInstance hPbot
  let := Localization.AtPrime.algebraOfLiesOver (P.under A) P
  constructor
  · intro H
    · rw [Algebra.isUnramifiedAt_iff_map_eq (p := P.under A)]
      constructor
      · suffices Algebra.IsSeparable (A ⧸ P.under A) (B ⧸ P) by infer_instance
        contrapose H
        exact dvd_differentIdeal_of_not_isSeparable A hp P H
      · rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hPbot Ideal.map_comap_le]
        apply Ideal.ramificationIdx_spec
        · simp [Ideal.map_le_iff_le_comap]
        · contrapose H
          rw [← pow_one P, show 1 = 2 - 1 by simp]
          apply pow_sub_one_dvd_differentIdeal _ _ _ hp
          simpa [Ideal.dvd_iff_le] using H
  · intro H
    obtain ⟨Q, h₁, h₂⟩ := Ideal.eq_prime_pow_mul_coprime hp' P
    rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp' ‹_› hPbot,
      Ideal.ramificationIdx_eq_one_of_isUnramifiedAt hPbot, pow_one] at h₂
    obtain ⟨h₃, h₄⟩ := (Algebra.isUnramifiedAt_iff_map_eq (p := P.under A) _ _).mp H
    exact not_dvd_differentIdeal_of_isCoprime_of_isSeparable
      A P Q (Ideal.isCoprime_iff_sup_eq.mpr h₁) h₂.symm
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
P : Ideal B
inst_9 : P.IsPrime
inl :
  ∀ [inst_10 : Ideal.IsPrime.{u_3} (α := B) ⊥],
    ¬Dvd.dvd (α := Ideal B) ⊥ (differentIdeal A B) ↔ IsUnramifiedAt.{u_1, u_3} A (A := B) ⊥
inr inr₁ : ∀ (hPbot : P ≠ ⊥), ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
inr₂ : ∀ (hPbot : P ≠ ⊥) (hp : Ne (α := Ideal A) (Ideal.under A P) ⊥), ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
have inr₃ : ∀ (hPbot : P ≠ ⊥) (hp : Ne (α := Ideal A) (Ideal.under A P) ⊥)
  (hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P)) ⊥),
  ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
Tactic: classical
  rcases eq_or_ne P ⊥ with rfl | hPbot
  · simp_rw [← Ideal.zero_eq_bot, zero_dvd_iff]
    simp only [Submodule.zero_eq_bot, differentIdeal_ne_bot, not_false_eq_true, true_iff]
    let K := FractionRing A
    let L := FractionRing B
    have : IsLocalization B⁰ (Localization.AtPrime (⊥ : Ideal B)) := by
      convert!
        (inferInstance :
          IsLocalization (⊥ : Ideal B).primeCompl (Localization.AtPrime (⊥ : Ideal B)))
      ext; simp [Ideal.primeCompl]
    refine (Algebra.FormallyUnramified.iff_of_equiv (A := L)
      ((IsLocalization.algEquiv B⁰ _ _).restrictScalars A)).mp ?_
    have : Algebra.FormallyUnramified K L := by
      rwa [Algebra.FormallyUnramified.iff_isSeparable]
    refine .comp A K L
  have hp : P.under A ≠ ⊥ := mt Ideal.eq_bot_of_comap_eq_bot hPbot
  have hp' := (Ideal.map_eq_bot_iff_of_injective
    (FaithfulSMul.algebraMap_injective A B)).not.mpr hp
  have := Ideal.IsPrime.isMaximal inferInstance hPbot
  let := Localization.AtPrime.algebraOfLiesOver (P.under A) P
  constructor
  · intro H
    · rw [Algebra.isUnramifiedAt_iff_map_eq (p := P.under A)]
      constructor
      · suffices Algebra.IsSeparable (A ⧸ P.under A) (B ⧸ P) by infer_instance
        contrapose H
        exact dvd_differentIdeal_of_not_isSeparable A hp P H
      · rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hPbot Ideal.map_comap_le]
        apply Ideal.ramificationIdx_spec
        · simp [Ideal.map_le_iff_le_comap]
        · contrapose H
          rw [← pow_one P, show 1 = 2 - 1 by simp]
          apply pow_sub_one_dvd_differentIdeal _ _ _ hp
          simpa [Ideal.dvd_iff_le] using H
  · intro H
    obtain ⟨Q, h₁, h₂⟩ := Ideal.eq_prime_pow_mul_coprime hp' P
    rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp' ‹_› hPbot,
      Ideal.ramificationIdx_eq_one_of_isUnramifiedAt hPbot, pow_one] at h₂
    obtain ⟨h₃, h₄⟩ := (Algebra.isUnramifiedAt_iff_map_eq (p := P.under A) _ _).mp H
    exact not_dvd_differentIdeal_of_isCoprime_of_isSeparable
      A P Q (Ideal.isCoprime_iff_sup_eq.mpr h₁) h₂.symm
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Dvr (goal)
Goal:
R : Type u_2
Rₘ : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing Rₘ
inst_3 : Algebra R Rₘ
M : Submonoid R
inst_4 : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
⊢ p.IsMaximal
have refine : ∀ (P : Ideal Rₘ) (hpP : p < P) (hPm : P.IsMaximal), False
Tactic: refine Ideal.isMaximal_def.mpr ⟨hpp.ne_top, Ideal.maximal_of_no_maximal fun P hpP hPm => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Dvr (hypothesis)
Goal:
R : Type u_2
Rₘ : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing Rₘ
inst_3 : Algebra R Rₘ
M : Submonoid R
inst_4 : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
⊢ False
have hpP' : Subtype.mk (p := fun (p : Ideal Rₘ) ↦ p.IsPrime) p hpp < Subtype.mk (p := fun (p : Ideal Rₘ) ↦ p.IsPrime) P sorry
Tactic: have hpP' : (⟨p, hpp⟩ : { p : Ideal Rₘ // p.IsPrime }) < ⟨P, hPm.isPrime⟩ := hpP
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Dvr (hypothesis)
Goal:
R : Type u_2
Rₘ : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing Rₘ
inst_3 : Algebra R Rₘ
M : Submonoid R
inst_4 : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : Subtype.mk (p := fun (p : Ideal Rₘ) ↦ p.IsPrime) p hpp < Subtype.mk (p := fun (p : Ideal Rₘ) ↦ p.IsPrime) P ⋯
⊢ False
have hpP'₁ : LT.lt.{u_2} (α := { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
  (((IsLocalization.orderIsoOfPrime M Rₘ :
          OrderIso.{u_3, u_2} { p : Ideal Rₘ // p.IsPrime }
            { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) :
        (a : { p : Ideal Rₘ // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
      (Subtype.mk (p := fun (p : Ideal Rₘ) ↦ p.IsPrime) p hpp) :
    { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
  (((IsLocalization.orderIsoOfPrime M Rₘ :
          OrderIso.{u_3, u_2} { p : Ideal Rₘ // p.IsPrime }
            { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) :
        (a : { p : Ideal Rₘ // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
      (Subtype.mk (p := fun (p : Ideal Rₘ) ↦ p.IsPrime) P sorry) :
    { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
Tactic: rw [← (IsLocalization.orderIsoOfPrime M Rₘ).lt_iff_lt] at hpP'
Cleared hypotheses: hpP'
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Dvr (goal)
Goal:
R : Type u_2
Rₘ : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing Rₘ
inst_3 : Algebra R Rₘ
M : Submonoid R
inst_4 : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' :
  LT.lt.{u_2} (α := { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
    (((IsLocalization.orderIsoOfPrime M Rₘ :
            OrderIso.{u_3, u_2} { p : Ideal Rₘ // p.IsPrime }
              { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) :
          (a : { p : Ideal Rₘ // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
        (Subtype.mk (p := fun (p : Ideal Rₘ) ↦ p.IsPrime) p hpp) :
      { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
    (((IsLocalization.orderIsoOfPrime M Rₘ :
            OrderIso.{u_3, u_2} { p : Ideal Rₘ // p.IsPrime }
              { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) :
          (a : { p : Ideal Rₘ // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
        (Subtype.mk (p := fun (p : Ideal Rₘ) ↦ p.IsPrime) P ⋯) :
      { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
⊢ False
have refine : LT.lt (α := Ideal R) ⊥ (Ideal.under R p)
Tactic: refine h.not_lt_lt ⊥ (p.under R) (P.under R) ⟨?_, hpP'⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Dvr (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
⊢ IsDedekindDomain Aₘ
have h : ∀ (y : ↥M),
  IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
Tactic: have h : ∀ y : M, IsUnit (algebraMap A (FractionRing A) y) := by
    rintro ⟨y, hy⟩
    exact IsUnit.mk0 _ (mt IsFractionRing.to_map_eq_zero_iff.mp (nonZeroDivisors.ne_zero (hM hy)))
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Dvr (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
⊢ IsDedekindDomain Aₘ
have this₁ : IsScalarTower A Aₘ (FractionRing A)
Tactic: haveI : IsScalarTower A Aₘ (FractionRing A) :=
    IsScalarTower.of_algebraMap_eq fun x => (IsLocalization.lift_eq h x).symm
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Dvr (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this : IsScalarTower A Aₘ (FractionRing A)
⊢ IsDedekindDomain Aₘ
have this₁ : IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)
Tactic: haveI : IsFractionRing Aₘ (FractionRing A) :=
    IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M _ _
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Dvr (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this_2 : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)
refine_1 : IsDomain Aₘ
⊢ IsDedekindDomain Aₘ
have refine_2 : IsNoetherianRing Aₘ
Tactic: refine (isDedekindDomain_iff _ (FractionRing A)).mpr ⟨?_, ?_, ?_, ?_⟩