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
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
refine_1 :
  HMul.hMul (α := Set M) {x} ((⇑(IsLocalization.map M (algebraMap B C) ⋯) : (a : L) → M) '' (↑(dual A K 1)⁻¹ : Set L)) ⊆
    (↑(traceDual B L 1) : Set M)
⊢ x ∈
    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:
rw [← spanSingleton_le_iff_mem, ← mul_inv_le_iff₀ (bot_lt_iff_ne_bot.mpr
      (by simp [-extendedHom'_apply])), ← map_inv₀, ← FractionalIdeal.coe_le_coe,
        extendedHom'_apply, coe_mul, coe_spanSingleton, coe_extended_eq_span, coe_dual_one,
        span_mul_span, span_le]

Premises used: FractionalIdeal.coe_le_coe, FractionalIdeal.extendedHom'_apply, FractionalIdeal.spanSingleton_le_iff_mem, Submodule.span_mul_span, map_inv₀, FractionalIdeal.coe_dual_one, mul_inv_le_iff₀, FractionalIdeal.coe_mul, FractionalIdeal.coe_spanSingleton, Submodule.span_le, FractionalIdeal.coe_extended_eq_span
-- 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
a : L
ha : a ∈ (↑(dual A K 1)⁻¹ : Set L)
m : C
refine_1 :
  Membership.mem (γ := Submodule B L) 1
    (HMul.hMul (β := L) a
      ((Algebra.trace L M : (a : M) → L) (HMul.hMul (α := M) ((algebraMap C M : (a : C) → M) m : M) x) : L))
⊢ Membership.mem.{u, u} (α := L) (γ := Submodule B L) 1
    (((traceForm L M : (a : M) → M →ₗ[L] L)
            ((fun (x1 x2 : M) ↦ x1 * x2) x ((IsLocalization.map M (algebraMap B C) ⋯ : (a : L) → M) a)) :
          (a : M) → L)
        ((LinearMap.toSpanSingleton C M 1 : (a : C) → M) m : M) :
      L)

Tactic:
simp only [← h_alg, mul_comm _ (algebraMap _ _ _), ← Algebra.smul_def a, map_smul,
      LinearMap.toSpanSingleton_apply, Algebra.smul_def m, mul_one,
      LinearMap.smul_apply, traceForm_apply, smul_eq_mul]

Premises used: Algebra.algebraMap, LinearMap.smul_apply, Algebra.traceForm_apply, LinearMap.toSpanSingleton_apply, mul_comm, Algebra.smul_def, smul_eq_mul, mul_one, DFunLike.coe, map_smul
-- 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
a : L
ha : a ∈ (↑(dual A K 1)⁻¹ : Set L)
m : C
refine_1 :
  Membership.mem (γ := Submodule B L) (↑1 : Submodule B L)
    (HMul.hMul (β := L) a
      ((Algebra.trace L M : (a : M) → L) (HMul.hMul (α := M) ((algebraMap C M : (a : C) → M) m : M) x) : L))
⊢ Membership.mem (γ := Submodule B L) 1
    (HMul.hMul (β := L) a
      ((Algebra.trace L M : (a : M) → L) (HMul.hMul (α := M) ((algebraMap C M : (a : C) → M) m : M) x) : L))

Tactic:
rw [← FractionalIdeal.coe_one (S := B⁰)]

Premises used: FractionalIdeal.coe_one
-- 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
a : L
ha : a ∈ (↑(dual A K 1)⁻¹ : Set L)
m : C
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_5, u} (R := B) B⁰ L) (dual A K 1) 0

Tactic:
simp
-- 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
a : L
ha : a ∈ (↑(dual A K 1)⁻¹ : Set L)
m : C
refine_1 :
  Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual A K 1)
    (HMul.hMul (α := M) ((algebraMap C M : (a : C) → M) m : M) x)
⊢ Membership.mem (γ := Submodule B L) (↑1 : Submodule B L)
    (HMul.hMul (β := L) a
      ((Algebra.trace L M : (a : M) → L) (HMul.hMul (α := M) ((algebraMap C M : (a : C) → M) m : M) x) : L))

Tactic:
refine (mem_inv_iff (by simp)).mp ha _ (trace_mem_dual_one A K L B C M _ ?_)

Premises used: Iff.mp, FractionalIdeal.trace_mem_dual_one, FractionalIdeal.mem_inv_iff
-- 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
a : L
ha : a ∈ (↑(dual A K 1)⁻¹ : Set L)
m : C
⊢ Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual A K 1)
    (HMul.hMul (α := M) ((algebraMap C M : (a : C) → M) m : M) x)

Tactic:
Algebra.smul_def m x ▸ smul_mem _ _ hx

Premises used: Set.Mem, Eq.rec, Algebra.smul_def, Submodule.smul_mem
-- 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
a : L
ha : a ∈ (↑(dual A K 1)⁻¹ : Set L)
m : C
⊢ Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual A K 1)
    (HMul.hMul (α := M) ((algebraMap C M : (a : C) → M) m : M) x)

Tactic:
exact Algebra.smul_def m x ▸ smul_mem _ _ hx
-- 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_2 :
  (↑(↑(dual B L 1) : Submodule C M) : Set M) *
      (⇑(IsLocalization.map M (algebraMap B C) ⋯) : (a : L) → M) '' (↑(dual A K 1) : Set L) ⊆
    (↑(↑(dual A K 1) : Submodule C M) : Set M)
⊢ 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

Tactic:
rw [← FractionalIdeal.coe_le_coe, coe_mul, extendedHom'_apply,
      coe_extended_eq_span, ← span_eq (coeToSubmodule _), span_mul_span, span_le]

Premises used: FractionalIdeal.coe_le_coe, FractionalIdeal.extendedHom'_apply, Submodule.span_mul_span, Submodule.span_eq, FractionalIdeal.coe_mul, FractionalIdeal.coeToSubmodule, Submodule.span_le, FractionalIdeal.coe_extended_eq_span
-- 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)
a : M
ha : a ∈ (↑(↑(dual B L 1) : Submodule C M) : Set M)
b : L
hb : b ∈ (↑(dual A K 1) : Set L)
refine_2 :
  ∀ (ha : Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual B L 1) a)
    (hb : Membership.mem (γ := FractionalIdeal.{u_5, u} (R := B) B⁰ L) (dual A K 1) b),
    Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual A K 1) (b • a)
⊢ (fun (x1 x2 : M) ↦ x1 * x2) a ((IsLocalization.map M (algebraMap B C) ⋯ : (a : L) → M) b) ∈
    (↑(↑(dual A K 1) : Submodule C M) : Set M)

Tactic:
simp only [SetLike.mem_coe, mem_coe, ← h_alg, mul_comm a, ← Algebra.smul_def] at ha hb ⊢

Premises used: SetLike.mem_coe, mul_comm, FractionalIdeal.mem_coe, Algebra.smul_def
-- 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)
a : M
b : L
ha : Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual B L 1) a
hb : Membership.mem (γ := FractionalIdeal.{u_5, u} (R := B) B⁰ L) (dual A K 1) b
⊢ Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual A K 1) (b • a)

Tactic:
smul_mem_dual_one A K L B C M hb ha

Premises used: FractionalIdeal.smul_mem_dual_one
-- 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)
a : M
b : L
ha : Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual B L 1) a
hb : Membership.mem (γ := FractionalIdeal.{u_5, u} (R := B) B⁰ L) (dual A K 1) b
⊢ Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual A K 1) (b • a)

Tactic:
exact smul_mem_dual_one A K L B C M hb ha

Premises used: FractionalIdeal.smul_mem_dual_one