-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma map_equiv_traceDual [IsDomain A] [IsFractionRing B L] [IsDomain B]
    [FaithfulSMul A B] (I : Submodule B (FractionRing B)) :
    (traceDual A (FractionRing A) I).map (FractionRing.algEquiv B L) =
      traceDual A K (I.map (FractionRing.algEquiv B L))

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsFractionRing A K
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
⊢ Submodule.map (↑(FractionRing.algEquiv B L).toLinearEquiv) (traceDual A (FractionRing A) I) =
    (Submodule.map (↑(FractionRing.algEquiv B L).toLinearEquiv) I)ᵛ

Tactic:
rw [Submodule.map_equiv_eq_comap_symm, Submodule.map_equiv_eq_comap_symm]

Result:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsFractionRing A K
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
⊢ comap (↑(FractionRing.algEquiv B L).toLinearEquiv.symm) (traceDual A (FractionRing A) I) =
    (comap (↑(FractionRing.algEquiv B L).toLinearEquiv.symm) I)ᵛ

Proof state:
case h.he.h.a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsFractionRing A K
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
x✝ : A
⊢ (((algebraMap K L).comp ↑(FractionRing.algEquiv A K).toRingEquiv).comp (algebraMap A (FractionRing A))) x✝ =
    (((↑(FractionRing.algEquiv B L).toRingEquiv).comp (algebraMap (FractionRing A) (FractionRing B))).comp
        (algebraMap A (FractionRing A)))
      x✝

Tactic:
simp only [AlgEquiv.toRingEquiv_eq_coe, AlgEquiv.toRingEquiv_toRingHom, RingHom.coe_comp,
  RingHom.coe_coe, Function.comp_apply, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]

Result:
case h.he.h.a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsFractionRing A K
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
x✝ : A
⊢ (algebraMap A L) x✝ = (FractionRing.algEquiv B L) ((algebraMap A (FractionRing B)) x✝)

Proof state:
case h
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsFractionRing A K
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
⊢ ∀ (a : FractionRing B),
    a ∈ I → (Algebra.trace (FractionRing A) (FractionRing B)) ((FractionRing.algEquiv B L).symm x * a) ∈ 1 ↔
      a ∈ I → (Algebra.trace K L) (x * (FractionRing.algEquiv B L) a) ∈ 1

Tactic:
refine fun {y} ↦ (forall_congr' fun hy ↦ ?_)

Result:
case h
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsFractionRing A K
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
⊢ (Algebra.trace (FractionRing A) (FractionRing B)) ((FractionRing.algEquiv B L).symm x * y) ∈ 1 ↔
    (Algebra.trace K L) (x * (FractionRing.algEquiv B L) y) ∈ 1

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsFractionRing A K
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
⊢ comap (↑(FractionRing.algEquiv B L).toLinearEquiv.symm) (traceDual A (FractionRing A) I) =
    (comap (↑(FractionRing.algEquiv B L).toLinearEquiv.symm) I)ᵛ

Tactic:
ext x

Result:
case h
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsFractionRing A K
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
⊢ x ∈ comap (↑(FractionRing.algEquiv B L).toLinearEquiv.symm) (traceDual A (FractionRing A) I) ↔
    x ∈ (comap (↑(FractionRing.algEquiv B L).toLinearEquiv.symm) I)ᵛ

Proof state:
case h
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsFractionRing A K
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
⊢ (FractionRing.algEquiv B L).symm x ∈
      ((traceForm (FractionRing A) (FractionRing B)).dualSubmodule (restrictScalars A I)).toAddSubmonoid ↔
    x ∈
      ((traceForm K L).dualSubmodule
          (restrictScalars A (comap (FractionRing.algEquiv B L).symm.toLinearMap I))).toAddSubmonoid

Tactic:
apply (FractionRing.algEquiv B L).forall_congr

Result:
case h
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsFractionRing A K
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
⊢ ∀ (a : FractionRing B),
    a ∈ restrictScalars A I →
        ((traceForm (FractionRing A) (FractionRing B)) ((FractionRing.algEquiv B L).symm x)) a ∈ 1 ↔
      (FractionRing.algEquiv B L).toEquiv a ∈ restrictScalars A (comap (FractionRing.algEquiv B L).symm.toLinearMap I) →
        ((traceForm K L) x) ((FractionRing.algEquiv B L).toEquiv a) ∈ 1