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
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)
⊢ FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)

Tactic:
have : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
-- 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
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
neg : ∀ (he : ¬e = 0), P ^ (e - 1) ∣ differentIdeal A B
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
by_cases he : e = 0
-- 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
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
pos : Dvd.dvd (α := Ideal B) 1 (differentIdeal A B)
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
rw [he, pow_zero]

Premises used: pow_zero
-- 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
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
⊢ Dvd.dvd (α := Ideal B) 1 (differentIdeal A B)

Tactic:
one_dvd _

Premises used: Set.Mem, one_dvd
-- 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
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
⊢ Dvd.dvd (α := Ideal B) 1 (differentIdeal A B)

Tactic:
exact one_dvd _

Premises used: one_dvd
-- 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
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

Tactic:
pow_sub_one_dvd_differentIdeal_aux A (FractionRing A) (FractionRing B) _ he hp hP

Premises used: FractionRing, pow_sub_one_dvd_differentIdeal_aux
-- 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
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

Tactic:
exact pow_sub_one_dvd_differentIdeal_aux A (FractionRing A) (FractionRing B) _ he hp hP

Premises used: FractionRing, pow_sub_one_dvd_differentIdeal_aux
-- 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
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
neg : ∀ (hp : ¬p = ⊥), ¬P ∣ differentIdeal A B
⊢ ¬P ∣ differentIdeal A B

Tactic:
by_cases hp : p = ⊥
-- 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
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 * Q = Ideal.map (R := A) (F := A →+* B) (algebraMap A B) ⊥

Tactic:
subst 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 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) ⊥
⊢ ((intTrace A B : (a : B) → A) x : A) ∉ ⊥

Tactic:
subst 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 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 = ⊥ ∨ Q = ⊥

Tactic:
simp only [Ideal.map_bot, Ideal.mul_eq_bot] at hP

Premises used: Ideal.map_bot, Ideal.mul_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)
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)
pos₁ : ∀ (hxQ : Membership.mem (γ := Ideal B) ⊥ x), ¬P ∣ differentIdeal A B
⊢ ¬P ∣ differentIdeal A B

Tactic:
obtain (rfl | rfl) := hP

Premises used: 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)
Q : Ideal B
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ ⊥
pos : ¬Eq (α := Ideal B) (differentIdeal A B) 0
⊢ ¬Dvd.dvd (α := Ideal B) ⊥ (differentIdeal A B)

Tactic:
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)
Q : Ideal B
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ ⊥
⊢ ¬Eq (α := Ideal B) (differentIdeal A B) 0

Tactic:
differentIdeal_ne_bot

Premises used: differentIdeal_ne_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)
Q : Ideal B
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ ⊥
⊢ ¬Eq (α := Ideal B) (differentIdeal A B) 0

Tactic:
exact differentIdeal_ne_bot

Premises used: differentIdeal_ne_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)
P : Ideal B
x : B
hx : ((intTrace A B : (a : B) → A) x : A) ∉ ⊥
hxQ : Membership.mem (γ := Ideal B) ⊥ x
⊢ ((intTrace A B : (a : B) → A) 0 : A) ∉ ⊥

Tactic:
obtain rfl := hxQ

Premises used: 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)
P : Ideal B
hx : ((intTrace A B : (a : B) → A) 0 : A) ∉ ⊥
⊢ ¬P ∣ differentIdeal A B

Tactic:
simp at hx
-- 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
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 = ⊥
rw : P * Q ≤ Q
⊢ p ≤ Ideal.comap (F := A →+* B) (algebraMap A B) Q

Tactic:
rw [← Ideal.map_le_iff_le_comap, ← hP]

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 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 * Q ≤ Q

Tactic:
Ideal.mul_le_left

Premises used: Set.Mem, Ideal.mul_le_left
-- 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
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 * Q ≤ Q

Tactic:
exact Ideal.mul_le_left

Premises used: Ideal.mul_le_left
-- 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
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
⊢ IsLocalization (algebraMapSubmonoid.{u_1, u_3} (R := A) B A⁰) L

Tactic:
have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L :=
    IsIntegralClosure.isLocalization _ K _ _
-- 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
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
⊢ FiniteDimensional K L

Tactic:
have : FiniteDimensional K L := .of_isLocalization A B A⁰
-- 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
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
neg : ¬differentIdeal A B ≤ P
⊢ ¬P ∣ differentIdeal A B

Tactic:
rw [Ideal.dvd_iff_le]

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 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
⊢ 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
-- 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
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)
⊢ 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

Premises used: coeIdeal_differentIdeal, FractionalIdeal.coeIdeal_mul
-- 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
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 :
  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)
⊢ HMul.hMul (α := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1 : FractionalIdeal (R := B) B⁰ L)
      (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)) ≤
    HMul.hMul (α := FractionalIdeal (R := B) B⁰ L) (β := FractionalIdeal (R := B) B⁰ L)
      (FractionalIdeal.dual A K 1 : FractionalIdeal (R := B) B⁰ L)
      (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)

Tactic:
replace H := mul_le_mul_right H (FractionalIdeal.dual A K 1)
-- 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
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 :
  HMul.hMul (α := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1 : FractionalIdeal (R := B) B⁰ L)
      (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)) ≤
    HMul.hMul (α := FractionalIdeal (R := B) B⁰ L) (β := FractionalIdeal (R := B) B⁰ L)
      (FractionalIdeal.dual A K 1 : FractionalIdeal (R := B) B⁰ L)
      (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)
⊢ Ne.{u_3 + 1} (α := FractionalIdeal (R := B) B⁰ L) 1 0

Tactic:
have hne : (1 : FractionalIdeal B⁰ L) ≠ 0 := one_ne_zero
-- 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
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 :
  HMul.hMul (α := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1 : FractionalIdeal (R := B) B⁰ L)
      (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)) ≤
    HMul.hMul (α := FractionalIdeal (R := B) B⁰ L) (β := FractionalIdeal (R := B) B⁰ L)
      (FractionalIdeal.dual A K 1 : FractionalIdeal (R := B) B⁰ L)
      (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)
hne : Ne.{u_3 + 1} (α := FractionalIdeal (R := B) B⁰ L) 1 0
⊢ (↑Q : FractionalIdeal B⁰ L) ≤
    HMul.hMul (α := FractionalIdeal (R := B) B⁰ L) (β := FractionalIdeal (R := B) B⁰ L)
      (FractionalIdeal.dual A K 1 : FractionalIdeal (R := B) B⁰ L)
      (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)

Tactic:
rw [mul_inv_cancel_left₀ (FractionalIdeal.dual_ne_zero A K hne)] at H

Premises used: mul_inv_cancel_left₀, FractionalIdeal.dual_ne_zero