awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
a : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
⊢ P ^ (e - 1) ∣ differentIdeal A B
have suffices : ∀ x ∈ a, Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)
Tactic: suffices ∀ x ∈ a, intTrace A B x ∈ p by
    have hP : ((P ^ (e - 1) :)⁻¹ : FractionalIdeal B⁰ L) = a / p.map (algebraMap A B) := by
      apply inv_involutive.injective
      simp only [inv_inv, ha, FractionalIdeal.coeIdeal_mul, inv_div,
          mul_div_assoc]
      rw [div_self (by simpa), mul_one]
    rw [Ideal.dvd_iff_le, differentialIdeal_le_iff (K := K) (L := L) (pow_ne_zero _ hPbot), hP,
      Submodule.map_le_iff_le_comap]
    intro x hx
    rw [Submodule.restrictScalars_mem, FractionalIdeal.mem_coe,
      FractionalIdeal.mem_div_iff_of_ne_zero (by simpa using hp')] at hx
    rw [Submodule.mem_comap, LinearMap.coe_restrictScalars, ← FractionalIdeal.coe_one,
      ← div_self (G₀ := FractionalIdeal A⁰ K) (a := p) (by simpa using hp),
      FractionalIdeal.mem_coe, FractionalIdeal.mem_div_iff_of_ne_zero (by simpa using hp)]
    simp only [FractionalIdeal.mem_coeIdeal, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂] at hx
    intro y hy'
    obtain ⟨y, hy, rfl : algebraMap A K _ = _⟩ := (FractionalIdeal.mem_coeIdeal _).mp hy'
    obtain ⟨z, hz, hz'⟩ := hx _ (Ideal.mem_map_of_mem _ hy)
    have : trace K L (algebraMap B L z) ∈ (p : FractionalIdeal A⁰ K) := by
      rw [← algebraMap_intTrace (A := A)]
      exact ⟨intTrace A B z, this z hz, rfl⟩
    rwa [mul_comm, ← smul_eq_mul, ← map_smul, Algebra.smul_def, mul_comm,
      ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B L, ← hz']
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
a : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
x : B
hx : x ∈ a
⊢ Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)
have rw : IsNilpotent.{u_1} (R := A ⧸ p)
  ((Algebra.trace (A ⧸ p) (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)) :
        (a : B ⧸ Ideal.map (algebraMap A B) p) → A ⧸ p)
      ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p) : (a : B) → B ⧸ Ideal.map (algebraMap A B) p)
        x) :
    A ⧸ p)
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, ← trace_quotient_eq_of_isDedekindDomain,
    ← isNilpotent_iff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
a : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
x : B
hx : x ∈ a
⊢ IsNilpotent.{u_1} (R := A ⧸ p)
    ((Algebra.trace (A ⧸ p) (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)) :
          (a : B ⧸ Ideal.map (algebraMap A B) p) → A ⧸ p)
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p) : (a : B) → B ⧸ Ideal.map (algebraMap A B) p)
          x) :
      A ⧸ p)
have refine : HPow.hPow (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
    ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p) : (a : B) → B ⧸ Ideal.map (algebraMap A B) p) x :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
    e =
  0
Tactic: refine isNilpotent_trace_of_isNilpotent ⟨e, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
a : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
x : B
hx : x ∈ a
⊢ HPow.hPow (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
      ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p) : (a : B) → B ⧸ Ideal.map (algebraMap A B) p)
          x :
        HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
      e =
    0
have rw : Membership.mem (γ := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (x ^ e)
Tactic: rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem]
-- 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
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
⊢ P ^ (e - 1) ∣ differentIdeal A B
have this : IsLocalization (algebraMapSubmonoid.{u_1, u_3} (R := A) B A⁰) (FractionRing B)
Tactic: have : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
    IsIntegralClosure.isLocalization _ (FractionRing A) _ _
-- 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
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
this : IsLocalization (algebraMapSubmonoid.{u_1, u_3} (R := A) B A⁰) (FractionRing B)
⊢ P ^ (e - 1) ∣ differentIdeal A B
have this₁ : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
Tactic: have : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B 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 A
inst_9 : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
this_1 : IsLocalization (algebraMapSubmonoid.{u_1, u_3} (R := A) B A⁰) (FractionRing B)
this : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
⊢ P ^ (e - 1) ∣ differentIdeal A B
have pos : ∀ (he : e = 0), P ^ (e - 1) ∣ differentIdeal A B
Tactic: by_cases he : e = 0
-- 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
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
this_1 : IsLocalization (algebraMapSubmonoid.{u_1, u_3} (R := A) B A⁰) (FractionRing B)
this : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
pos : ∀ (he : e = 0), P ^ (e - 1) ∣ differentIdeal A B
⊢ P ^ (e - 1) ∣ differentIdeal A B
have neg : ∀ (he : ¬e = 0), P ^ (e - 1) ∣ differentIdeal A B
Tactic: by_cases he : e = 0
-- 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
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
this_1 : IsLocalization (algebraMapSubmonoid.{u_1, u_3} (R := A) B A⁰) (FractionRing B)
this : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
he : e = 0
⊢ P ^ (e - 1) ∣ differentIdeal A B
have pos : Dvd.dvd (α := Ideal B) 1 (differentIdeal A B)
Tactic: rw [he, pow_zero]
-- 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
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ p
⊢ ¬P ∣ differentIdeal A B
have pos : ∀ (hp : p = ⊥), ¬P ∣ differentIdeal A B
Tactic: by_cases hp : p = ⊥
-- 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
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ p
pos : ∀ (hp : p = ⊥), ¬P ∣ differentIdeal A B
⊢ ¬P ∣ differentIdeal A B
have neg : ∀ (hp : ¬p = ⊥), ¬P ∣ differentIdeal A B
Tactic: by_cases 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 A
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ p
hp : p = ⊥
⊢ ¬P ∣ differentIdeal A B
have hP₁ : P * Q = Ideal.map (R := A) (F := A →+* B) (algebraMap A B) ⊥
Tactic: subst hp
Cleared hypotheses: p, hP, hx, 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
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ p
hp : p = ⊥
hP₁ : P * Q = Ideal.map (R := A) (F := A →+* B) (algebraMap A B) ⊥
⊢ ¬P ∣ differentIdeal A B
have hx₁ : ((intTrace A B : (a : B) → A) x : A) ∉ ⊥
Tactic: subst hp
Cleared hypotheses: p, hP, hx, 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 Q : Ideal B
x : B
hxQ : x ∈ Q
hP : P * Q = Ideal.map (R := A) (F := A →+* B) (algebraMap A B) ⊥
hx : ((intTrace A B : (a : B) → A) x : A) ∉ ⊥
⊢ ¬P ∣ differentIdeal A B
have hP₁ : P = ⊥ ∨ Q = ⊥
Tactic: simp only [Ideal.map_bot, Ideal.mul_eq_bot] at hP
Cleared hypotheses: 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 Q : Ideal B
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ ⊥
hP : P = ⊥ ∨ Q = ⊥
⊢ ¬P ∣ differentIdeal A B
have pos : ¬Dvd.dvd (α := Ideal B) ⊥ (differentIdeal A B)
Tactic: obtain (rfl | rfl) := hP
Cleared hypotheses: P, 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 Q : Ideal B
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ ⊥
hP : P = ⊥ ∨ Q = ⊥
pos : ¬Dvd.dvd (α := Ideal B) ⊥ (differentIdeal A B)
⊢ ¬P ∣ differentIdeal A B
have pos₁ : ∀ (hxQ : Membership.mem (γ := Ideal B) ⊥ x), ¬P ∣ differentIdeal A B
Tactic: obtain (rfl | rfl) := hP
Cleared hypotheses: Q, hxQ, 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)
Q : Ideal B
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ ⊥
⊢ ¬Dvd.dvd (α := Ideal B) ⊥ (differentIdeal A B)
have pos : ¬Eq (α := Ideal B) (differentIdeal A B) 0
Tactic: rw [← Ideal.zero_eq_bot, zero_dvd_iff]
-- 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
x : B
hx : ((intTrace A B : (a : B) → A) x : A) ∉ ⊥
hxQ : Membership.mem (γ := Ideal B) ⊥ x
⊢ ¬P ∣ differentIdeal A B
have hx₁ : ((intTrace A B : (a : B) → A) 0 : A) ∉ ⊥
Tactic: obtain rfl := hxQ
Cleared hypotheses: x, hx, hxQ
-- 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
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ p
hp : ¬p = ⊥
⊢ p ≤ Ideal.comap (F := A →+* B) (algebraMap A B) Q
have rw : P * Q ≤ Q
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
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ p
hp : ¬p = ⊥
this : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
⊢ ¬P ∣ differentIdeal A B
have this₁ : IsLocalization (algebraMapSubmonoid.{u_1, u_3} (R := A) B A⁰) L
Tactic: have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L :=
    IsIntegralClosure.isLocalization _ K _ _
-- 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
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ p
hp : ¬p = ⊥
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this : IsLocalization (algebraMapSubmonoid.{u_1, u_3} (R := A) B A⁰) L
⊢ ¬P ∣ differentIdeal A B
have this₁ : FiniteDimensional K L
Tactic: have : FiniteDimensional K L := .of_isLocalization A B 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 A
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ p
hp : ¬p = ⊥
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this_2 : IsLocalization (algebraMapSubmonoid.{u_1, u_3} (R := A) B A⁰) L
this : FiniteDimensional K L
⊢ ¬P ∣ differentIdeal A B
have neg : ¬differentIdeal A B ≤ P
Tactic: rw [Ideal.dvd_iff_le]
-- 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
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ p
hp : ¬p = ⊥
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this_2 : IsLocalization (algebraMapSubmonoid.{u_1, u_3} (R := A) B A⁰) L
this : FiniteDimensional K L
H : differentIdeal A B ≤ P
⊢ False
have H₁ : differentIdeal A B * Q ≤ Ideal.map (F := A →+* B) (algebraMap A B) p
Tactic: replace H := (mul_le_mul_left H Q).trans_eq hP
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 A
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ p
hp : ¬p = ⊥
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this_2 : IsLocalization (algebraMapSubmonoid.{u_1, u_3} (R := A) B A⁰) L
this : FiniteDimensional K L
H :
  LE.le (α := FractionalIdeal (R := B) B⁰ L) (↑(differentIdeal A B * Q) : FractionalIdeal B⁰ L)
    (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)
⊢ False
have H₁ : HMul.hMul (α := FractionalIdeal (R := B) B⁰ L) (β := FractionalIdeal (R := B) B⁰ L)
    ((FractionalIdeal.dual A K 1)⁻¹ : FractionalIdeal (R := B) B⁰ L) (↑Q : FractionalIdeal B⁰ L) ≤
  (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)
Tactic: rw [FractionalIdeal.coeIdeal_mul, coeIdeal_differentIdeal A K] at H
Cleared hypotheses: H