awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
x : L
hx : Membership.mem (γ := FractionalIdeal.{u_5, u} (R := B) B⁰ L) (dual A K 1) x
y : M
hy : Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual B L 1) y
simp :
  ∀
    (hx :
      ∀ (a : B),
        ∃ (x_1 : A),
          Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
            ((Algebra.trace K L : (a : L) → K) (a • x) : K))
    (hy :
      ∀ (a : C),
        ∃ (x : B),
          Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) x : L)
            ((Algebra.trace L M : (a : M) → L) (a • y) : L))
    (a : C),
    ∃ (x_1 : A),
      Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
        ((Algebra.trace K M : (a : M) → K) (a • x • y) : K)
⊢ Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual A K 1) (x • y)

Tactic:
simp only [ne_eq, one_ne_zero, not_false_eq_true, mem_dual, mem_one_iff, traceForm_apply,
    RingHom.mem_range, forall_exists_index, forall_apply_eq_imp_iff, mul_comm _ (algebraMap _ _ _),
    ← Algebra.smul_def] at hx hy ⊢

Premises used: Algebra.algebraMap, RingHom.mem_range, Algebra.traceForm_apply, FractionalIdeal.mem_one_iff, forall_exists_index, FractionalIdeal.mem_dual, ne_eq, mul_comm, Algebra.smul_def, one_ne_zero, not_false_eq_true, forall_apply_eq_imp_iff, DFunLike.coe
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
x : L
y : M
hx :
  ∀ (a : B),
    ∃ (x_1 : A),
      Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
        ((Algebra.trace K L : (a : L) → K) (a • x) : K)
hy :
  ∀ (a : C),
    ∃ (x : B),
      Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) x : L)
        ((Algebra.trace L M : (a : M) → L) (a • y) : L)
c : C
obtain :
  ∀ (b : B)
    (hb :
      Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) b : L)
        ((Algebra.trace L M : (a : M) → L) (c • y) : L)),
    ∃ (x_1 : A),
      Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
        ((Algebra.trace K M : (a : M) → K) (c • x • y) : K)
⊢ ∃ (x_1 : A),
    Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
      ((Algebra.trace K M : (a : M) → K) (c • x • y) : K)

Tactic:
obtain ⟨b, hb⟩ := hy c
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
x : L
y : M
hx :
  ∀ (a : B),
    ∃ (x_1 : A),
      Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
        ((Algebra.trace K L : (a : L) → K) (a • x) : K)
hy :
  ∀ (a : C),
    ∃ (x : B),
      Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) x : L)
        ((Algebra.trace L M : (a : M) → L) (a • y) : L)
c : C
b : B
hb :
  Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) b : L) ((Algebra.trace L M : (a : M) → L) (c • y) : L)
obtain :
  ∀ (a : A)
    (ha :
      Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) a : K)
        ((Algebra.trace K L : (a : L) → K) (b • x) : K)),
    ∃ (x_1 : A),
      Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
        ((Algebra.trace K M : (a : M) → K) (c • x • y) : K)
⊢ ∃ (x_1 : A),
    Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
      ((Algebra.trace K M : (a : M) → K) (c • x • y) : K)

Tactic:
obtain ⟨a, ha⟩ := hx b
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
x : L
y : M
hx :
  ∀ (a : B),
    ∃ (x_1 : A),
      Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
        ((Algebra.trace K L : (a : L) → K) (a • x) : K)
hy :
  ∀ (a : C),
    ∃ (x : B),
      Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) x : L)
        ((Algebra.trace L M : (a : M) → L) (a • y) : L)
c : C
b : B
hb :
  Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) b : L) ((Algebra.trace L M : (a : M) → L) (c • y) : L)
a : A
ha :
  Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) a : K)
    ((Algebra.trace K L : (a : L) → K) (b • x) : K)
h :
  Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) a : K)
    ((Algebra.trace K M : (a : M) → K) (c • x • y) : K)
⊢ ∃ (x_1 : A),
    Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
      ((Algebra.trace K M : (a : M) → K) (c • x • y) : K)

Tactic:
use a
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
x : L
y : M
hx :
  ∀ (a : B),
    ∃ (x_1 : A),
      Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
        ((Algebra.trace K L : (a : L) → K) (a • x) : K)
hy :
  ∀ (a : C),
    ∃ (x : B),
      Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) x : L)
        ((Algebra.trace L M : (a : M) → L) (a • y) : L)
c : C
b : B
hb :
  Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) b : L) ((Algebra.trace L M : (a : M) → L) (c • y) : L)
a : A
ha :
  Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) a : K)
    ((Algebra.trace K L : (a : L) → K) (b • x) : K)
⊢ Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) a : K)
    ((Algebra.trace K M : (a : M) → K) (c • x • y) : K)

Tactic:
simpa [Algebra.smul_def b, hb, mul_comm _ x, ← smul_eq_mul, ← (Algebra.trace L M).map_smul,
    Algebra.trace_trace, smul_comm x c y] using ha

Premises used: Algebra.trace_trace, LinearMap.map_smul, mul_comm, Algebra.smul_def, smul_eq_mul, SMulCommClass.smul_comm, Algebra.trace
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
inst_41 : IsTorsionFree B C
⊢ IsLocalization (algebraMapSubmonoid.{u_5, u_3} (R := B) C B⁰) M

Tactic:
have := IsIntegralClosure.isLocalization B L M C
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
inst_41 : IsTorsionFree B C
this : IsLocalization (algebraMapSubmonoid.{u_5, u_3} (R := B) C B⁰) M
⊢ LE.le (α := Submonoid B) B⁰ (Submonoid.comap (F := B →+* C) (algebraMap B C) C⁰)

Tactic:
have h : B⁰ ≤ Submonoid.comap (algebraMap B C) C⁰ :=
    nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _ <| FaithfulSMul.algebraMap_injective _ _
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
inst_41 : IsTorsionFree B C
this : IsLocalization (algebraMapSubmonoid.{u_5, u_3} (R := B) C B⁰) M
h : LE.le (α := Submonoid B) B⁰ (Submonoid.comap (F := B →+* C) (algebraMap B C) C⁰)
⊢ ∀ {x : L},
    Eq.{u_4 + 1} (α := M) ((algebraMap L M : (a : L) → M) x : M)
      ((IsLocalization.map M (algebraMap B C) h : (a : L) → M) x : M)

Tactic:
have h_alg {x : L} : algebraMap L M x = IsLocalization.map M (algebraMap B C) h x :=
    IsLocalization.algebraMap_apply_eq_map_map_submonoid B⁰ C L M x
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
inst_41 : IsTorsionFree B C
this : IsLocalization (algebraMapSubmonoid.{u_5, u_3} (R := B) C B⁰) M
h : LE.le (α := Submonoid B) B⁰ (Submonoid.comap (F := B →+* C) (algebraMap B C) C⁰)
h_alg :
  ∀ {x : L},
    Eq.{u_4 + 1} (α := M) ((algebraMap L M : (a : L) → M) x : M)
      ((IsLocalization.map M (algebraMap B C) h : (a : L) → M) x : M)
⊢ dual A K 1 =
    HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (β := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M)
      (dual B L 1)
      ((extendedHom M C : (a : FractionalIdeal B⁰ L) → FractionalIdeal C⁰ M) (dual A K 1) :
        FractionalIdeal.{u_3, u_4} (R := C) C⁰ M)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
inst_41 : IsTorsionFree B C
this : IsLocalization (algebraMapSubmonoid.{u_5, u_3} (R := B) C B⁰) M
h : LE.le (α := Submonoid B) B⁰ (Submonoid.comap (F := B →+* C) (algebraMap B C) C⁰)
h_alg :
  ∀ {x : L},
    Eq.{u_4 + 1} (α := M) ((algebraMap L M : (a : L) → M) x : M)
      ((IsLocalization.map M (algebraMap B C) h : (a : L) → M) x : M)
refine_1 :
  dual A K 1 ≤
    HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (β := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M)
      (dual B L 1)
      ((extendedHom M C : (a : FractionalIdeal B⁰ L) → FractionalIdeal C⁰ M) (dual A K 1) :
        FractionalIdeal.{u_3, u_4} (R := C) C⁰ M)
refine_2 :
  HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (β := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual B L 1)
      ((extendedHom M C : (a : FractionalIdeal B⁰ L) → FractionalIdeal C⁰ M) (dual A K 1) :
        FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) ≤
    dual A K 1
⊢ dual A K 1 =
    HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (β := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M)
      (dual B L 1)
      ((extendedHom M C : (a : FractionalIdeal B⁰ L) → FractionalIdeal C⁰ M) (dual A K 1) :
        FractionalIdeal.{u_3, u_4} (R := C) C⁰ M)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
inst_41 : IsTorsionFree B C
this : IsLocalization (algebraMapSubmonoid.{u_5, u_3} (R := B) C B⁰) M
h : LE.le (α := Submonoid B) B⁰ (Submonoid.comap (F := B →+* C) (algebraMap B C) C⁰)
h_alg :
  ∀ {x : L},
    Eq.{u_4 + 1} (α := M) ((algebraMap L M : (a : L) → M) x : M)
      ((IsLocalization.map M (algebraMap B C) h : (a : L) → M) x : M)
x : M
hx : Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual A K 1) x
⊢ Ne.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M)
    ((extendedHom M C : (a : FractionalIdeal B⁰ L) → FractionalIdeal C⁰ M) (dual A K 1) :
      FractionalIdeal.{u_3, u_4} (R := C) C⁰ M)
    (⊥ : FractionalIdeal.{u_3, u_4} (R := C) C⁰ M)

Tactic:
simp [-extendedHom'_apply]

Premises used: FractionalIdeal.extendedHom'_apply