awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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⁰)
⊢ 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)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
have 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)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
⊢ 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)
have 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
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
⊢ 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)
have refine_1 : HMul.hMul (α := Set M) {x} ((⇑(IsLocalization.map M (algebraMap B C) sorry) : (a : L) → M) '' (↑(dual A K 1)⁻¹ : Set L)) ⊆
  (↑(traceDual B L 1) : Set 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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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.{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)
have 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))
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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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 (γ := 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))
have 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))
Tactic: rw [← FractionalIdeal.coe_one (S := B⁰)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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 (γ := 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))
have 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)
Tactic: refine (mem_inv_iff (by simp)).mp ha _ (trace_mem_dual_one A K L B C M _ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
⊢ 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
have refine_2 : (↑(↑(dual B L 1) : Submodule C M) : Set M) *
    (⇑(IsLocalization.map M (algebraMap B C) sorry) : (a : L) → M) '' (↑(dual A K 1) : Set L) ⊆
  (↑(↑(dual A K 1) : Submodule C M) : Set M)
Tactic: rw [← FractionalIdeal.coe_le_coe, coe_mul, extendedHom'_apply,
      coe_extended_eq_span, ← span_eq (coeToSubmodule _), span_mul_span, span_le]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
⊢ (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)
have 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)
Tactic: simp only [SetLike.mem_coe, mem_coe, ← h_alg, mul_comm a, ← Algebra.smul_def] at ha hb ⊢
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Algebra.IsIntegral A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
inst_9 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
⊢ coeSubmodule (FractionRing B) (differentIdeal A B) =
    HDiv.hDiv (α := Submodule B (FractionRing B)) 1 (traceDual A (FractionRing A) 1)
have rw : HDiv.hDiv (α := Submodule B (FractionRing B)) 1 (traceDual A (FractionRing A) 1) ≤
  LinearMap.range (Algebra.linearMap B (FractionRing B))
Tactic: rw [coeSubmodule, differentIdeal, Submodule.map_comap_eq, inf_eq_right]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Algebra.IsIntegral A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
inst_9 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
⊢ HDiv.hDiv (α := Submodule B (FractionRing B)) 1 (traceDual A (FractionRing A) 1) ≤
    LinearMap.range (Algebra.linearMap B (FractionRing B))
have this : LE.le.{u_3} (α := FractionalIdeal (R := B) B⁰ (FractionRing B)) (FractionalIdeal.dual A (FractionRing A) 1)⁻¹ 1
Tactic: have := FractionalIdeal.dual_inv_le (A := A) (K := FractionRing A)
    (1 : FractionalIdeal B⁰ (FractionRing B))
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Algebra.IsIntegral A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
inst_9 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
this : LE.le.{u_3} (α := FractionalIdeal (R := B) B⁰ (FractionRing B)) (FractionalIdeal.dual A (FractionRing A) 1)⁻¹ 1
⊢ HDiv.hDiv (α := Submodule B (FractionRing B)) 1 (traceDual A (FractionRing A) 1) ≤
    LinearMap.range (Algebra.linearMap B (FractionRing B))
have this₁ : LE.le.{u_3} (α := Submodule B (FractionRing B))
  ((↑(FractionalIdeal.dual A (FractionRing A) 1)⁻¹ : Submodule B (FractionRing B)) : Submodule B (FractionRing B))
  (↑1 : Submodule B (FractionRing B))
Tactic: have : _ ≤ ((1 : FractionalIdeal B⁰ (FractionRing B)) : Submodule B (FractionRing B)) := this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Algebra.IsIntegral A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
inst_9 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
this_1 : LE.le.{u_3} (α := FractionalIdeal (R := B) B⁰ (FractionRing B)) (FractionalIdeal.dual A (FractionRing A) 1)⁻¹ 1
this :
  LE.le.{u_3} (α := Submodule B (FractionRing B))
    ((↑(FractionalIdeal.dual A (FractionRing A) 1)⁻¹ : Submodule B (FractionRing B)) : Submodule B (FractionRing B))
    (↑1 : Submodule B (FractionRing B))
⊢ HDiv.hDiv (α := Submodule B (FractionRing B)) 1 (traceDual A (FractionRing A) 1) ≤
    LinearMap.range (Algebra.linearMap B (FractionRing B))
have rw : ∀
  (this :
    HDiv.hDiv (α := Submodule B (FractionRing B)) (↑1 : Submodule B (FractionRing B))
        (traceDual A (FractionRing A) (↑1 : Submodule B (FractionRing B))) ≤
      (↑1 : Submodule B (FractionRing B))),
  HDiv.hDiv (α := Submodule B (FractionRing B)) 1 (traceDual A (FractionRing A) 1) ≤
    LinearMap.range (Algebra.linearMap B (FractionRing B))
Tactic: rw [← one_div, FractionalIdeal.coe_div (FractionalIdeal.dual_ne_zero _ _ _),
    FractionalIdeal.coe_dual] at this
Cleared hypotheses: this