-- Module: Mathlib.RingTheory.DedekindDomain.Different
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 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
h :
  ∀ (a : FractionRing B),
    (a ∈ I →
        ∃ (y : A),
          Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y : FractionRing A)
            ((Algebra.trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
                (HMul.hMul (α := FractionRing B)
                  (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B) x :
                    FractionRing B)
                  a) :
              FractionRing A)) ↔
      a ∈ I →
        ∃ (y : A),
          Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y : K)
            ((Algebra.trace K L : (a : L) → K)
                (HMul.hMul (β := L) x ((FractionRing.algEquiv B L : (a : FractionRing B) → L) a : L)) :
              K)
⊢ ∀ (a : FractionRing B),
    Membership.mem (γ := Submodule A (FractionRing B)) (Submodule.restrictScalars A I) a →
        Membership.mem.{u_1, u_1} (α := FractionRing A) (γ := Submodule A (FractionRing A)) 1
          ((((traceForm (FractionRing A) (FractionRing B) :
                      (a : FractionRing B) → FractionRing B →ₗ[FractionRing A] FractionRing A)
                    ((((↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) :
                            L →ₗ[B] FractionRing B) :
                          L →ₗ[B] FractionRing B) :
                        (a : L) → FractionRing B)
                      x) :
                  LinearMap.{u_1, u_1, u_3, u_1} (R := FractionRing A) (RingHom.id (FractionRing A)) (FractionRing B)
                    (FractionRing A)) :
                (a : FractionRing B) → FractionRing A)
              a :
            FractionRing A) ↔
      Membership.mem (α := L) (γ := Submodule A L)
          (Submodule.restrictScalars A
            (comap
              (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B) I))
          ((AlgEquiv.toEquiv (FractionRing.algEquiv B L) : (a : FractionRing B) → L) a : L) →
        Membership.mem.{u_2, u_2} (α := K) (γ := Submodule A K) 1
          ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K)
              ((AlgEquiv.toEquiv (FractionRing.algEquiv B L) : (a : FractionRing B) → L) a : L) :
            K)

Tactic:
simp only [restrictScalars_mem, LinearEquiv.coe_coe, AlgEquiv.coe_symm_toLinearEquiv,
    traceForm_apply, mem_one, AlgEquiv.toEquiv_eq_coe, EquivLike.coe_coe, mem_comap,
    AlgEquiv.symm_apply_apply]

Premises used: Algebra.traceForm_apply, Submodule.mem_comap, AlgEquiv.coe_symm_toLinearEquiv, AlgEquiv.symm_apply_apply, Submodule.mem_one, Submodule.restrictScalars_mem, AlgEquiv.toEquiv_eq_coe, EquivLike.coe_coe, LinearEquiv.coe_coe