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 A
inst_9 : p.IsMaximal
inst_10 : Finite.{u_1 + 1} (A ⧸ p)
P Q : Ideal B
inst_11 : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
⊢ P * Q ≤ P

Tactic:
Ideal.mul_le_right

Premises used: Ideal.mul_le_right, Set.Mem
-- 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 A
inst_9 : p.IsMaximal
inst_10 : Finite.{u_1 + 1} (A ⧸ p)
P Q : Ideal B
inst_11 : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
⊢ P * Q ≤ P

Tactic:
exact Ideal.mul_le_right

Premises used: Ideal.mul_le_right
-- 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 A
inst_9 : p.IsMaximal
inst_10 : Finite.{u_1 + 1} (A ⧸ p)
P Q : Ideal B
inst_11 : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
⊢ P.LiesOver p

Tactic:
have : P.LiesOver p := by
    constructor
    refine ‹p.IsMaximal›.eq_of_le ?_ ?_
    · simpa using ‹P.IsMaximal›.ne_top
    · rw [← Ideal.map_le_iff_le_comap, ← hP]
      exact Ideal.mul_le_right
-- 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 A
inst_9 : p.IsMaximal
inst_10 : Finite.{u_1 + 1} (A ⧸ p)
P Q : Ideal B
inst_11 : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
this : P.LiesOver p
⊢ ¬P ∣ differentIdeal A B

Tactic:
not_dvd_differentIdeal_of_isCoprime_of_isSeparable A P Q hPQ hP

Premises used: not_dvd_differentIdeal_of_isCoprime_of_isSeparable
-- 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 A
inst_9 : p.IsMaximal
inst_10 : Finite.{u_1 + 1} (A ⧸ p)
P Q : Ideal B
inst_11 : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
this : P.LiesOver p
⊢ ¬P ∣ differentIdeal A B

Tactic:
exact not_dvd_differentIdeal_of_isCoprime_of_isSeparable A P Q hPQ hP

Premises used: not_dvd_differentIdeal_of_isCoprime_of_isSeparable
-- 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
inl :
  ∀ [inst_10 : Ideal.IsPrime.{u_3} (α := B) ⊥],
    ¬Dvd.dvd (α := Ideal B) ⊥ (differentIdeal A B) ↔ IsUnramifiedAt.{u_1, u_3} A (A := B) ⊥
inr : ∀ (hPbot : P ≠ ⊥), ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P

Tactic:
rcases eq_or_ne P ⊥ with rfl | hPbot

Premises used: Bot.bot, eq_or_ne, rfl
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
inl : ¬Eq (α := Ideal B) (differentIdeal A B) 0 ↔ IsUnramifiedAt.{u_1, u_3} A (A := B) 0
⊢ ¬Dvd.dvd (α := Ideal B) ⊥ (differentIdeal A B) ↔ IsUnramifiedAt.{u_1, u_3} A (A := B) ⊥

Tactic:
simp_rw [← Ideal.zero_eq_bot, zero_dvd_iff]

Premises used: zero_dvd_iff, Ideal.zero_eq_bot
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
inl : IsUnramifiedAt.{u_1, u_3} A (A := B) ⊥
⊢ ¬Eq (α := Ideal B) (differentIdeal A B) 0 ↔ IsUnramifiedAt.{u_1, u_3} A (A := B) 0

Tactic:
simp only [Submodule.zero_eq_bot, differentIdeal_ne_bot, not_false_eq_true, true_iff]

Premises used: differentIdeal_ne_bot, true_iff, Submodule.zero_eq_bot, not_false_eq_true
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
⊢ IsLocalization.{u_3, u_3} (R := B) (Ideal.primeCompl ⊥) (Localization.AtPrime (R := B) ⊥)

Tactic:
(inferInstance :
          IsLocalization (⊥ : Ideal B).primeCompl (Localization.AtPrime (⊥ : Ideal B)))

Premises used: inferInstance
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
h : Eq (α := Submonoid B) (B⁰ : Submonoid B) (Ideal.primeCompl ⊥)
⊢ IsLocalization.{u_3, u_3} (R := B) B⁰ (Localization.AtPrime (R := B) ⊥)

Tactic:
convert!
        (inferInstance :
          IsLocalization (⊥ : Ideal B).primeCompl (Localization.AtPrime (⊥ : Ideal B)))

Premises used: inferInstance
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
h : ∀ (x : B), Membership.mem (γ := Submonoid B) B⁰ x ↔ Membership.mem (γ := Submonoid B) (Ideal.primeCompl ⊥) x
⊢ Eq (α := Submonoid B) (B⁰ : Submonoid B) (Ideal.primeCompl ⊥)

Tactic:
ext
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
x : B
⊢ Membership.mem (γ := Submonoid B) B⁰ x ↔ Membership.mem (γ := Submonoid B) (Ideal.primeCompl ⊥) x

Tactic:
simp [Ideal.primeCompl]

Premises used: Ideal.primeCompl
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
⊢ IsLocalization.{u_3, u_3} (R := B) B⁰ (Localization.AtPrime (R := B) ⊥)

Tactic:
have : IsLocalization B⁰ (Localization.AtPrime (⊥ : Ideal B)) := by
      convert!
        (inferInstance :
          IsLocalization (⊥ : Ideal B).primeCompl (Localization.AtPrime (⊥ : Ideal B)))
      ext; simp [Ideal.primeCompl]
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this : IsLocalization.{u_3, u_3} (R := B) B⁰ (Localization.AtPrime (R := B) ⊥)
⊢ IsUnramifiedAt.{u_1, u_3} A (A := B) ⊥

Tactic:
(Algebra.FormallyUnramified.iff_of_equiv (A := L)
      ((IsLocalization.algEquiv B⁰ _ _).restrictScalars A)).mp ?_

Premises used: nonZeroDivisors, AlgEquiv.restrictScalars, IsLocalization.algEquiv, Iff.mp, Algebra.FormallyUnramified.iff_of_equiv
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this : IsLocalization.{u_3, u_3} (R := B) B⁰ (Localization.AtPrime (R := B) ⊥)
inl : FormallyUnramified A L
⊢ IsUnramifiedAt.{u_1, u_3} A (A := B) ⊥

Tactic:
refine (Algebra.FormallyUnramified.iff_of_equiv (A := L)
      ((IsLocalization.algEquiv B⁰ _ _).restrictScalars A)).mp ?_

Premises used: nonZeroDivisors, AlgEquiv.restrictScalars, IsLocalization.algEquiv, Iff.mp, Algebra.FormallyUnramified.iff_of_equiv
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this : IsLocalization.{u_3, u_3} (R := B) B⁰ (Localization.AtPrime (R := B) ⊥)
rwa rwa₁ rwa₂ rwa₃ : Algebra.IsSeparable K L
⊢ FormallyUnramified K L

Tactic:
rwa [Algebra.FormallyUnramified.iff_isSeparable]

Premises used: Algebra.FormallyUnramified.iff_isSeparable
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this : IsLocalization.{u_3, u_3} (R := B) B⁰ (Localization.AtPrime (R := B) ⊥)
⊢ FormallyUnramified K L

Tactic:
have : Algebra.FormallyUnramified K L := by
      rwa [Algebra.FormallyUnramified.iff_isSeparable]
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this_1 : IsLocalization.{u_3, u_3} (R := B) B⁰ (Localization.AtPrime (R := B) ⊥)
this : FormallyUnramified K L
⊢ FormallyUnramified A L

Tactic:
.comp A K L

Premises used: Algebra.FormallyUnramified.comp
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this_1 : IsLocalization.{u_3, u_3} (R := B) B⁰ (Localization.AtPrime (R := B) ⊥)
this : FormallyUnramified K L
⊢ FormallyUnramified A L

Tactic:
refine .comp A K L
-- 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 ≠ ⊥
⊢ Ne (α := Ideal A) (Ideal.under A P) ⊥

Tactic:
have hp : P.under A ≠ ⊥ := mt Ideal.eq_bot_of_comap_eq_bot hPbot
-- 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) ⊥
⊢ ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P)) ⊥

Tactic:
have hp' := (Ideal.map_eq_bot_iff_of_injective
    (FaithfulSMul.algebraMap_injective A B)).not.mpr hp
-- 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)) ⊥
⊢ P.IsMaximal

Tactic:
have := Ideal.IsPrime.isMaximal inferInstance hPbot
-- 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
inr : ¬P ∣ differentIdeal A B → IsUnramifiedAt A P
inr₁ : IsUnramifiedAt A P → ¬P ∣ differentIdeal A B
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P

Tactic:
constructor
-- 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 :
  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))
⊢ IsUnramifiedAt A P

Tactic:
rw [Algebra.isUnramifiedAt_iff_map_eq (p := P.under A)]

Premises used: Algebra.isUnramifiedAt_iff_map_eq, 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 : ¬P ∣ differentIdeal A B
inr : Algebra.IsSeparable.{u_1, u_3} (Ideal.ResidueField (Ideal.under A P)) P.ResidueField
inr₁ :
  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))
⊢ 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:
constructor
-- 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_2 : 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
this : Algebra.IsSeparable.{u_1, u_3} (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A P)) (B ⧸ P)
⊢ Algebra.IsSeparable.{u_1, u_3} (Ideal.ResidueField (Ideal.under A P)) P.ResidueField

Tactic:
infer_instance
-- 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 : Algebra.IsSeparable.{u_1, u_3} (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A P)) (B ⧸ P)
⊢ Algebra.IsSeparable.{u_1, u_3} (Ideal.ResidueField (Ideal.under A P)) P.ResidueField

Tactic:
suffices Algebra.IsSeparable (A ⧸ P.under A) (B ⧸ P) by infer_instance
-- 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 : ¬Algebra.IsSeparable.{u_1, u_3} (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A P)) (B ⧸ P)),
    P ∣ differentIdeal A B
⊢ Algebra.IsSeparable.{u_1, u_3} (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A P)) (B ⧸ P)

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 : ¬Algebra.IsSeparable.{u_1, u_3} (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A P)) (B ⧸ P)
⊢ P ∣ differentIdeal A B

Tactic:
dvd_differentIdeal_of_not_isSeparable A hp P H

Premises used: dvd_differentIdeal_of_not_isSeparable
-- 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 : ¬Algebra.IsSeparable.{u_1, u_3} (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A P)) (B ⧸ P)
⊢ P ∣ differentIdeal A B

Tactic:
exact dvd_differentIdeal_of_not_isSeparable A hp P H

Premises used: dvd_differentIdeal_of_not_isSeparable