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_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)
neg :
  Eq (α := K) ((Algebra.linearMap A K : (a : A) → K) (z * y) : 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:
refine ⟨z * y, Ideal.mul_mem_left _ _ 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_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 : B
x : L
hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x
⊢ Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) (x * (Algebra.linearMap B L : (a : B) → L) 0) : K)

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 y z : B
hx_2 : Membership.mem (γ := Submodule B B) (span B ((⇑(algebraMap A B) : (a : A) → B) '' (↑p : Set A))) y
hy_1 : Membership.mem (γ := Submodule B B) (span B ((⇑(algebraMap A B) : (a : A) → B) '' (↑p : Set A))) z
hy :
  ∀ (x : L) (hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x),
    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)
hz :
  ∀ (x : L) (hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x),
    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) z : L)) :
        K)
x : L
hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x
neg :
  Membership.mem (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (HAdd.hAdd (α := K) (β := 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)
      (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K)
          (HMul.hMul (β := L) x ((Algebra.linearMap B L : (a : B) → L) z : 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 + z) : L)) :
      K)

Tactic:
simp only [map_add, mul_add]

Premises used: map_add, mul_add
-- 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 z : B
hx_2 : Membership.mem (γ := Submodule B B) (span B ((⇑(algebraMap A B) : (a : A) → B) '' (↑p : Set A))) y
hy_1 : Membership.mem (γ := Submodule B B) (span B ((⇑(algebraMap A B) : (a : A) → B) '' (↑p : Set A))) z
hy :
  ∀ (x : L) (hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x),
    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)
hz :
  ∀ (x : L) (hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x),
    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) z : L)) :
        K)
x : L
hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x
⊢ Membership.mem (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (HAdd.hAdd (α := K) (β := 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)
      (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K)
          (HMul.hMul (β := L) x ((Algebra.linearMap B L : (a : B) → L) z : L)) :
        K))

Tactic:
Submodule.add_mem _ (hy x hx) (hz x hx)

Premises used: Set.Mem, Submodule.add_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
p : Ideal A
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 z : B
hx_2 : Membership.mem (γ := Submodule B B) (span B ((⇑(algebraMap A B) : (a : A) → B) '' (↑p : Set A))) y
hy_1 : Membership.mem (γ := Submodule B B) (span B ((⇑(algebraMap A B) : (a : A) → B) '' (↑p : Set A))) z
hy :
  ∀ (x : L) (hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x),
    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)
hz :
  ∀ (x : L) (hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x),
    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) z : L)) :
        K)
x : L
hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x
⊢ Membership.mem (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (HAdd.hAdd (α := K) (β := 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)
      (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K)
          (HMul.hMul (β := L) x ((Algebra.linearMap B L : (a : B) → L) z : L)) :
        K))

Tactic:
exact Submodule.add_mem _ (hy x hx) (hz x hx)

Premises used: Submodule.add_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
p : Ideal A
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 z : B
hz : Membership.mem (γ := Submodule B B) (span B ((⇑(algebraMap A B) : (a : A) → B) '' (↑p : Set A))) z
IH :
  ∀ (x : L) (hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x),
    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) z : L)) :
        K)
x : L
hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x
⊢ 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 • z) : L)) :
      K)

Tactic:
simpa [Algebra.smul_def, mul_assoc, -FractionalIdeal.mem_coeIdeal, mul_left_comm x] using
        IH _ (Submodule.smul_mem _ y hx)

Premises used: mul_assoc, FractionalIdeal.mem_coeIdeal, mul_left_comm, Algebra.smul_def, Submodule.smul_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
p : Ideal A
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 :
  ∀ (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 (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
          (HAdd.hAdd (α := K) (β := K) (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) x : K)
            (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) y : K))
⊢ ∀ (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)

Tactic:
simp only [map_add]

Premises used: map_add
-- 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
⊢ ∀ (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 (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
          (HAdd.hAdd (α := K) (β := K) (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) x : K)
            (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) y : K))

Tactic:
fun _ _ h₁ h₂ ↦ Submodule.add_mem _ h₁ h₂

Premises used: Set.Mem, FractionalIdeal.coeToSubmodule, FractionalIdeal.coeIdeal, Submodule.add_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
p : Ideal A
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
⊢ ∀ (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 (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
          (HAdd.hAdd (α := K) (β := K) (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) x : K)
            (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) y : K))

Tactic:
exact fun _ _ h₁ h₂ ↦ Submodule.add_mem _ h₁ h₂

Premises used: Submodule.add_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
p : Ideal A
inst_9 : p.IsMaximal
P Q : Ideal B
inst_10 : P.IsMaximal
inst_11 : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
inst_12 : Algebra.IsSeparable.{u_1, u_3} (A ⧸ p) (B ⧸ 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
inst_9 : p.IsMaximal
P Q : Ideal B
inst_10 : P.IsMaximal
inst_11 : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
inst_12 : Algebra.IsSeparable.{u_1, u_3} (A ⧸ p) (B ⧸ 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
inst_9 : p.IsMaximal
P Q : Ideal B
inst_10 : P.IsMaximal
inst_11 : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
inst_12 : Algebra.IsSeparable.{u_1, u_3} (A ⧸ p) (B ⧸ 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
inst_9 : p.IsMaximal
P Q : Ideal B
inst_10 : P.IsMaximal
inst_11 : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
inst_12 : Algebra.IsSeparable.{u_1, u_3} (A ⧸ p) (B ⧸ P)
this : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
⊢ IsScalarTower.{u_1, u_1, u_3} A (A ⧸ p) (B ⧸ Q)

Tactic:
have : IsScalarTower A (A ⧸ p) (B ⧸ Q) := .of_algebraMap_eq' 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
inst_9 : p.IsMaximal
P Q : Ideal B
inst_10 : P.IsMaximal
inst_11 : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
inst_12 : Algebra.IsSeparable.{u_1, u_3} (A ⧸ p) (B ⧸ P)
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this : IsScalarTower.{u_1, u_1, u_3} A (A ⧸ p) (B ⧸ Q)
⊢ Module.Finite.{u_1, u_3} (A ⧸ p) (B ⧸ Q)

Tactic:
have : Module.Finite (A ⧸ p) (B ⧸ Q) :=
    Module.Finite.of_restrictScalars_finite A (A ⧸ p) (B ⧸ Q)