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
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
H₁ :
  (↑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:
rw [mul_inv_cancel_left₀ (FractionalIdeal.dual_ne_zero A K hne)] at H

Premises used: mul_inv_cancel_left₀, FractionalIdeal.dual_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 :
  (↑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
neg : Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)
⊢ False

Tactic:
apply 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 = ⊥
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_3 : FiniteDimensional K L
H :
  (↑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
this :
  Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) ((algebraMap B L : (a : B) → L) x) : K)
obtain :
  ∀ (y : A) (hy : y ∈ (↑p : Set A))
    (e :
      Eq (α := K) ((Algebra.linearMap A K : (a : A) → K) y : K)
        (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) ((algebraMap B L : (a : B) → L) x) : K)),
    Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)
⊢ Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)

Tactic:
obtain ⟨y, hy, e⟩ := this
-- 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 :
  (↑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
y : A
hy : y ∈ (↑p : Set A)
e :
  Eq (α := K) ((Algebra.linearMap A K : (a : A) → K) y : K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) ((algebraMap B L : (a : B) → L) x) : K)
⊢ y = (intTrace A B : (a : B) → A) x

Tactic:
rw [← Algebra.algebraMap_intTrace (A := A), Algebra.linearMap_apply,
      (IsLocalization.injective _ le_rfl).eq_iff] at e

Premises used: le_rfl, Function.Injective.eq_iff, IsLocalization.injective, Algebra.linearMap_apply, Algebra.algebraMap_intTrace
-- 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 :
  (↑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
y : A
hy : y ∈ (↑p : Set A)
e : y = (intTrace A B : (a : B) → A) x
⊢ Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)

Tactic:
e ▸ hy

Premises used: Eq.rec
-- 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 :
  (↑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
y : A
hy : y ∈ (↑p : Set A)
e : y = (intTrace A B : (a : B) → A) x
⊢ Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)

Tactic:
exact e ▸ hy
-- 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 :
  (↑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
neg :
  Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) ((algebraMap B L : (a : B) → L) x) : K)
⊢ Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)

Tactic:
suffices Algebra.trace K L (algebraMap B L x) ∈ (p : FractionalIdeal A⁰ K) by
    obtain ⟨y, hy, e⟩ := this
    rw [← Algebra.algebraMap_intTrace (A := A), Algebra.linearMap_apply,
      (IsLocalization.injective _ le_rfl).eq_iff] at e
    exact e ▸ hy
-- 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 :
  (↑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
⊢ Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) ((algebraMap B L : (a : B) → L) x) : K)

Tactic:
FractionalIdeal.mul_induction_on (H ⟨_, hxQ, rfl⟩) ?_ ?_

Premises used: Set.Mem, Quotient.mk', And.intro, Exists.intro, OreLocalization.oreDiv, rfl, FractionalIdeal.mul_induction_on
-- 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 :
  (↑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
neg :
  ∀ (i : L),
    Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) i →
      ∀ (j : L),
        Membership.mem (γ := FractionalIdeal (R := B) B⁰ L)
            (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L) j →
          Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
            (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) (i * j) : K)
neg₁ :
  ∀ (x y : L),
    Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
        (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) x : K) →
      Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
          (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) y : K) →
        Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
          (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) (x + y) : K)
⊢ Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) ((algebraMap B L : (a : B) → L) x) : K)

Tactic:
refine FractionalIdeal.mul_induction_on (H ⟨_, hxQ, 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 A
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x_1 : B
hxQ : x_1 ∈ Q
hx_1 : ((intTrace A B : (a : B) → A) x_1 : 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 :
  (↑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
y_1 y : B
h : Membership.mem (γ := Set B) ((⇑(algebraMap A B) : (a : A) → B) '' (↑p : Set A)) y
x : L
hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x
neg :
  ∀ (y : A) (hy : y ∈ (↑p : Set A)),
    Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
      (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K)
          (HMul.hMul (β := L) x ((Algebra.linearMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) y) : L)) :
        K)
⊢ Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K)
        (HMul.hMul (β := L) x ((Algebra.linearMap B L : (a : B) → L) y : L)) :
      K)

Tactic:
obtain ⟨y, hy, rfl⟩ := h

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 A
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x_1 : B
hxQ : x_1 ∈ Q
hx_1 : ((intTrace A B : (a : B) → A) x_1 : 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 :
  (↑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
y_1 : B
x : L
hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x
y : A
hy : y ∈ (↑p : Set A)
⊢ Ne.{u_3 + 1} (α := FractionalIdeal (R := B) B⁰ L) 1 0

Tactic:
simp
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
p : Ideal A
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x_1 : B
hxQ : x_1 ∈ Q
hx_1 : ((intTrace A B : (a : B) → A) x_1 : 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 :
  (↑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
y_1 : B
x : L
hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x
y : A
hy : y ∈ (↑p : Set A)
neg :
  ∀ (z : A)
    (hz :
      Eq (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) z : K)
        ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) 1 : K)),
    Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
      (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K)
          (HMul.hMul (β := L) x ((Algebra.linearMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) y) : L)) :
        K)
⊢ Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K)
        (HMul.hMul (β := L) x ((Algebra.linearMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) y) : L)) :
      K)

Tactic:
obtain ⟨z, hz⟩ :=
        (FractionalIdeal.mem_dual (by simp)).mp hx 1 ⟨1, trivial, (algebraMap B L).map_one⟩

Premises used: trivial, Algebra.algebraMap, RingHom.map_one, FractionalIdeal.mem_dual, And.intro, Exists.intro, Iff.mp, OfNat.ofNat
-- 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_1 : B
hxQ : x_1 ∈ Q
hx_1 : ((intTrace A B : (a : B) → A) x_1 : 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 :
  (↑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
y_1 : B
x : L
hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x
y : A
hy : y ∈ (↑p : Set A)
z : A
hz :
  Eq (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) z : K)
    ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) 1 : K)
⊢ Eq (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) z : K) (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) x : K)

Tactic:
simp only [Algebra.traceForm_apply, mul_one] at hz

Premises used: Algebra.traceForm_apply, mul_one
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
p : Ideal A
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x_1 : B
hxQ : x_1 ∈ Q
hx_1 : ((intTrace A B : (a : B) → A) x_1 : 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 :
  (↑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
y_1 : B
x : L
hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x
y : A
hy : y ∈ (↑p : Set A)
z : A
hz :
  Eq (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) z : K) (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) x : K)
⊢ Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K)
        (HMul.hMul (β := L) x ((Algebra.linearMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) y) : L)) :
      K)

Tactic:
⟨z * y, Ideal.mul_mem_left _ _ hy, ?_⟩

Premises used: HMul.hMul, Set.Mem, setOf, And.intro, Exists.intro, Set.image, Ideal.mul_mem_left