awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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 : ¬P ∣ differentIdeal A B
inr : Ideal.ramificationIdx (Ideal.comap (F := A →+* B) (algebraMap A B) P) P = 1
⊢ 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:
rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hPbot Ideal.map_comap_le]

Premises used: Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff, Ideal.map_comap_le
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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 : ¬P ∣ differentIdeal A B
inr : Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.comap (F := A →+* B) (algebraMap A B) P) ≤ HPow.hPow (β := ℕ) P 1
inr₁ :
  ¬Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.comap (F := A →+* B) (algebraMap A B) P) ≤
      P ^ HAdd.hAdd (α := ℕ) 1 1
⊢ Ideal.ramificationIdx (Ideal.comap (F := A →+* B) (algebraMap A B) P) P = 1

Tactic:
apply Ideal.ramificationIdx_spec

Premises used: Ideal.ramificationIdx_spec
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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 : ¬P ∣ differentIdeal A B
⊢ Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.comap (F := A →+* B) (algebraMap A B) P) ≤ HPow.hPow (β := ℕ) P 1

Tactic:
simp [Ideal.map_le_iff_le_comap]

Premises used: Ideal.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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 : ¬P ∣ differentIdeal A B
inr :
  ∀
    (H :
      Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.comap (F := A →+* B) (algebraMap A B) P) ≤
        P ^ HAdd.hAdd (α := ℕ) 1 1),
    P ∣ differentIdeal A B
⊢ ¬Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.comap (F := A →+* B) (algebraMap A B) P) ≤
      P ^ HAdd.hAdd (α := ℕ) 1 1

Tactic:
contrapose H
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
⊢ 1 = HSub.hSub (α := ℕ) 2 1

Tactic:
simp
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
inr : P ^ HSub.hSub (α := ℕ) 2 1 ∣ differentIdeal A B
⊢ P ∣ differentIdeal A B

Tactic:
rw [← pow_one P, show 1 = 2 - 1 by simp]

Premises used: pow_one
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
inr : HPow.hPow (β := ℕ) P 2 ∣ Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P)
⊢ P ^ HSub.hSub (α := ℕ) 2 1 ∣ differentIdeal A B

Tactic:
apply pow_sub_one_dvd_differentIdeal _ _ _ hp

Premises used: pow_sub_one_dvd_differentIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
⊢ HPow.hPow (β := ℕ) P 2 ∣ Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P)

Tactic:
simpa [Ideal.dvd_iff_le] using H

Premises used: Ideal.dvd_iff_le
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
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
⊢ ¬P ∣ differentIdeal A B

Tactic:
obtain ⟨Q, h₁, h₂⟩ := Ideal.eq_prime_pow_mul_coprime hp' P

Premises used: Ideal.eq_prime_pow_mul_coprime
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
⊢ 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₂

Premises used: Ideal.ramificationIdx_eq_one_of_isUnramifiedAt, Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count, pow_one
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
⊢ 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

Premises used: Algebra.isUnramifiedAt_iff_map_eq, Iff.mp, Ideal.under
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
⊢ 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

Premises used: Algebra.isUnramifiedAt_iff_map_eq, Iff.mp, Ideal.under
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
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))
⊢ ¬P ∣ differentIdeal A B

Tactic:
not_dvd_differentIdeal_of_isCoprime_of_isSeparable
      A P Q (Ideal.isCoprime_iff_sup_eq.mpr h₁) h₂.symm

Premises used: Iff.mpr, not_dvd_differentIdeal_of_isCoprime_of_isSeparable, Eq.symm, Ideal.isCoprime_iff_sup_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
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))
⊢ ¬P ∣ differentIdeal A B

Tactic:
exact not_dvd_differentIdeal_of_isCoprime_of_isSeparable
      A P Q (Ideal.isCoprime_iff_sup_eq.mpr h₁) h₂.symm

Premises used: Iff.mpr, not_dvd_differentIdeal_of_isCoprime_of_isSeparable, Eq.symm, Ideal.isCoprime_iff_sup_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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

Tactic:
iff_not_comm.mp not_dvd_differentIdeal_iff.symm

Premises used: iff_not_comm, not_dvd_differentIdeal_iff, Iff.mp, Iff.symm
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
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

Tactic:
Ideal.isMaximal_def.mpr ⟨hpp.ne_top, Ideal.maximal_of_no_maximal fun P hpP hPm => ?_⟩

Premises used: Ideal.maximal_of_no_maximal, Iff.mpr, And.intro, Ideal.IsPrime.ne_top, Ideal.isMaximal_def
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
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
refine : ∀ (P : Ideal Rₘ) (hpP : p < P) (hPm : P.IsMaximal), False
⊢ p.IsMaximal

Tactic:
refine Ideal.isMaximal_def.mpr ⟨hpp.ne_top, Ideal.maximal_of_no_maximal fun P hpP hPm => ?_⟩

Premises used: Ideal.maximal_of_no_maximal, Iff.mpr, And.intro, Ideal.IsPrime.ne_top, Ideal.isMaximal_def
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
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
⊢ Subtype.mk (p := fun (p : Ideal Rₘ) ↦ p.IsPrime) p hpp < Subtype.mk (p := fun (p : Ideal Rₘ) ↦ p.IsPrime) P ⋯

Tactic:
have hpP' : (⟨p, hpp⟩ : { p : Ideal Rₘ // p.IsPrime }) < ⟨P, hPm.isPrime⟩ := hpP
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
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 ⋯
⊢ 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) })

Tactic:
rw [← (IsLocalization.orderIsoOfPrime M Rₘ).lt_iff_lt] at hpP'

Premises used: OrderIso.lt_iff_lt, IsLocalization.orderIsoOfPrime
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
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

Tactic:
h.not_lt_lt ⊥ (p.under R) (P.under R) ⟨?_, hpP'⟩

Premises used: Ring.DimensionLEOne.not_lt_lt, Bot.bot, And.intro, Ideal.under
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
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) })
refine : LT.lt (α := Ideal R) ⊥ (Ideal.under R p)
⊢ False

Tactic:
refine h.not_lt_lt ⊥ (p.under R) (P.under R) ⟨?_, hpP'⟩

Premises used: Ring.DimensionLEOne.not_lt_lt, Bot.bot, And.intro, Ideal.under
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
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) })
⊢ LT.lt (α := Ideal R) ⊥ (Ideal.under R p)

Tactic:
IsLocalization.bot_lt_under_prime _ _ hM _ hp0

Premises used: IsLocalization.bot_lt_under_prime