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 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
over : Ne (α := Ideal A) (Ideal.under A P) ⊤
⊢ p = Ideal.under A P
have over₁ : p ≤ Ideal.under A P
Tactic: refine ‹p.IsMaximal›.eq_of_le ?_ ?_
-- 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 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 ≤ Ideal.under A P
have over : P * Q ≤ P
Tactic: rw [← Ideal.map_le_iff_le_comap, ← hP]
-- 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 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 ∣ differentIdeal A B
have this : 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
-- 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: rcases eq_or_ne P ⊥ with rfl | hPbot
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: rcases eq_or_ne P ⊥ with rfl | hPbot
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
⊢ ¬Dvd.dvd (α := Ideal B) ⊥ (differentIdeal A B) ↔ IsUnramifiedAt.{u_1, u_3} A (A := B) ⊥
have inl : ¬Eq (α := Ideal B) (differentIdeal A B) 0 ↔ IsUnramifiedAt.{u_1, u_3} A (A := B) 0
Tactic: simp_rw [← Ideal.zero_eq_bot, zero_dvd_iff]
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
⊢ ¬Eq (α := Ideal B) (differentIdeal A B) 0 ↔ IsUnramifiedAt.{u_1, u_3} A (A := B) 0
have inl : IsUnramifiedAt.{u_1, u_3} A (A := B) ⊥
Tactic: simp only [Submodule.zero_eq_bot, differentIdeal_ne_bot, not_false_eq_true, true_iff]
-- 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)
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) ⊥)
have h : Eq (α := Submonoid B) (B⁰ : Submonoid B) (Ideal.primeCompl ⊥)
Tactic: convert!
        (inferInstance :
          IsLocalization (⊥ : Ideal B).primeCompl (Localization.AtPrime (⊥ : Ideal B)))
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
⊢ Eq (α := Submonoid B) (B⁰ : Submonoid B) (Ideal.primeCompl ⊥)
have h : ∀ (x : B), Membership.mem (γ := Submonoid B) B⁰ x ↔ Membership.mem (γ := Submonoid B) (Ideal.primeCompl ⊥) x
Tactic: ext
-- 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)
inst_9 : Ideal.IsPrime.{u_3} (α := B) ⊥
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
⊢ IsUnramifiedAt.{u_1, u_3} A (A := B) ⊥
have this : 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]
-- 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)
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) ⊥
have inl : FormallyUnramified A L
Tactic: refine (Algebra.FormallyUnramified.iff_of_equiv (A := L)
      ((IsLocalization.algEquiv B⁰ _ _).restrictScalars A)).mp ?_
-- 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)
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 A L
have this₁ : FormallyUnramified K L
Tactic: have : Algebra.FormallyUnramified K L := by
      rwa [Algebra.FormallyUnramified.iff_isSeparable]
-- 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 ≠ ⊥
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
have hp : Ne (α := Ideal A) (Ideal.under A P) ⊥
Tactic: have hp : P.under A ≠ ⊥ := mt Ideal.eq_bot_of_comap_eq_bot hPbot
-- 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) ⊥
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
have hp' : ¬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
-- 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)) ⊥
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
have this : P.IsMaximal
Tactic: have := Ideal.IsPrime.isMaximal inferInstance hPbot
-- 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
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
have inr : ¬P ∣ differentIdeal A B → IsUnramifiedAt A P
Tactic: constructor
-- 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
inr : ¬P ∣ differentIdeal A B → IsUnramifiedAt A P
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
have inr₁ : IsUnramifiedAt A P → ¬P ∣ differentIdeal A B
Tactic: constructor
-- 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 : ¬P ∣ differentIdeal A B
⊢ IsUnramifiedAt A P
have 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))
Tactic: rw [Algebra.isUnramifiedAt_iff_map_eq (p := P.under A)]
-- 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 : ¬P ∣ differentIdeal A B
⊢ 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))
have inr : Algebra.IsSeparable.{u_1, u_3} (Ideal.ResidueField (Ideal.under A P)) P.ResidueField
Tactic: constructor
-- 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 : ¬P ∣ differentIdeal A B
inr : Algebra.IsSeparable.{u_1, u_3} (Ideal.ResidueField (Ideal.under A P)) P.ResidueField
⊢ 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))
have 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))
Tactic: constructor
-- 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 : ¬P ∣ differentIdeal A B
⊢ Algebra.IsSeparable.{u_1, u_3} (Ideal.ResidueField (Ideal.under A P)) P.ResidueField
have inr : Algebra.IsSeparable.{u_1, u_3} (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A P)) (B ⧸ P)
Tactic: suffices Algebra.IsSeparable (A ⧸ P.under A) (B ⧸ P) by infer_instance
-- 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 : ¬P ∣ differentIdeal A B
⊢ Algebra.IsSeparable.{u_1, u_3} (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A P)) (B ⧸ P)
have inr : ∀ (H : ¬Algebra.IsSeparable.{u_1, u_3} (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A P)) (B ⧸ P)),
  P ∣ differentIdeal A B
Tactic: contrapose H
Cleared hypotheses: 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
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
⊢ 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))
have inr : Ideal.ramificationIdx (Ideal.comap (F := A →+* B) (algebraMap A B) P) P = 1
Tactic: rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hPbot Ideal.map_comap_le]
-- 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 : ¬P ∣ differentIdeal A B
⊢ Ideal.ramificationIdx (Ideal.comap (F := A →+* B) (algebraMap A B) P) P = 1
have inr : Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.comap (F := A →+* B) (algebraMap A B) P) ≤ HPow.hPow (β := ℕ) P 1
Tactic: apply Ideal.ramificationIdx_spec
-- 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 : ¬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
⊢ Ideal.ramificationIdx (Ideal.comap (F := A →+* B) (algebraMap A B) P) P = 1
have inr₁ : ¬Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.comap (F := A →+* B) (algebraMap A B) P) ≤ P ^ HAdd.hAdd (α := ℕ) 1 1
Tactic: apply Ideal.ramificationIdx_spec
-- 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 : ¬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
have 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
Tactic: contrapose H
Cleared hypotheses: 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
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 ∣ differentIdeal A B
have inr : P ^ HSub.hSub (α := ℕ) 2 1 ∣ differentIdeal A B
Tactic: rw [← pow_one P, show 1 = 2 - 1 by simp]