-- 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
x : L
hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x
y : B
hy : y ∈ (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : Set B)
neg :
  ∀ (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),
    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)
neg₁ :
  ∀ (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)
neg₂ :
  ∀ (y z : B),
    Membership.mem (γ := Submodule B B) (span B ((⇑(algebraMap A B) : (a : A) → B) '' (↑p : Set A))) y →
      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 (α := 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)
neg₃ :
  ∀ (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)
⊢ 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:
induction hy using Submodule.span_induction generalizing x with
    | mem y h =>
      obtain ⟨y, hy, rfl⟩ := h
      obtain ⟨z, hz⟩ :=
        (FractionalIdeal.mem_dual (by simp)).mp hx 1 ⟨1, trivial, (algebraMap B L).map_one⟩
      simp only [Algebra.traceForm_apply, mul_one] at hz
      refine ⟨z * y, Ideal.mul_mem_left _ _ hy, ?_⟩
      rw [Algebra.linearMap_apply, Algebra.linearMap_apply, mul_comm x,
        ← IsScalarTower.algebraMap_apply,
        ← Algebra.smul_def, LinearMap.map_smul_of_tower, ← hz,
        Algebra.smul_def, map_mul, mul_comm]
    | zero => simp
    | add y z _ _ hy hz =>
      simp only [map_add, mul_add]
      exact Submodule.add_mem _ (hy x hx) (hz x hx)
    | smul y z hz IH =>
      simpa [Algebra.smul_def, mul_assoc, -FractionalIdeal.mem_coeIdeal, mul_left_comm x] using
        IH _ (Submodule.smul_mem _ y hx)

Premises used: trivial, Algebra.algebraMap, Algebra.traceForm_apply, mul_assoc, RingHom.map_one, Algebra.linearMap_apply, map_add, FractionalIdeal.mem_coeIdeal, mul_left_comm, FractionalIdeal.mem_dual, map_mul, And.intro, Exists.intro, Iff.mp, mul_comm, Algebra.smul_def, mul_add, LinearMap.map_smul_of_tower, mul_one, OfNat.ofNat, IsScalarTower.algebraMap_apply, rfl