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_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 : 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
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
a : L
ha : a ∈ I
w : L
⊢ IsIntegral A w ↔ IsInteger B w

Tactic:
IsIntegralClosure.isIntegral_iff (A := B)

Premises used: IsLocalization.IsInteger, Set.Mem, setOf, IsIntegralClosure.isIntegral_iff, Set.range
-- 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 : 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
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
a : L
ha : a ∈ I
w : L
⊢ IsIntegral A w ↔ IsInteger B w

Tactic:
exact IsIntegralClosure.isIntegral_iff (A := B)

Premises used: IsIntegralClosure.isIntegral_iff
-- 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 : 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
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
a : L
ha : a ∈ I
⊢ HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) b : L) a = b • a

Tactic:
(Algebra.smul_def _ _).symm

Premises used: Algebra.smul_def, Eq.symm
-- 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 : 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
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
a : L
ha : a ∈ I
⊢ HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) b : L) a = b • a

Tactic:
exact (Algebra.smul_def _ _).symm

Premises used: Algebra.smul_def, Eq.symm
-- 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 : 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
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
⊢ dual A K I = 0 ↔ I = 0

Tactic:
⟨not_imp_not.mp (dual_ne_zero A K), fun e ↦ e.symm ▸ dual_zero A K L B⟩

Premises used: Eq.rec, FractionalIdeal.dual_zero, FractionalIdeal.dual_ne_zero, Iff.intro, Iff.mp, Eq.symm, not_imp_not
-- 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 : 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
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
⊢ dual A K I ≠ 0 ↔ I ≠ 0

Tactic:
dual_eq_zero_iff.not

Premises used: Iff.not, FractionalIdeal.dual_eq_zero_iff
-- 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 : 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
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
rw : J ≤ Subtype.mk (p := fun (I : Submodule B L) ↦ IsFractional B⁰ I) (↑I : Submodule B L)ᵛ ⋯
⊢ J ≤ dual A K I

Tactic:
rw [dual, dif_neg hI]

Premises used: FractionalIdeal.dual, dif_neg
-- 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 : 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
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : Membership.mem (γ := Submodule A L) (Submodule.restrictScalars A (↑I : Submodule B L)) y
rw :
  ∃ (y_1 : A),
    Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y_1 : K)
      ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
⊢ 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) y : K)

Tactic:
rw [mem_one]

Premises used: Submodule.mem_one
-- 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 : 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
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : Membership.mem (γ := Submodule A L) (Submodule.restrictScalars A (↑I : Submodule B L)) y
apply : IsIntegral.{u_1, u_2} A (A := K) ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
⊢ ∃ (y_1 : A),
    Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y_1 : K)
      ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)

Tactic:
apply IsIntegrallyClosed.isIntegral_iff.mp

Premises used: IsIntegrallyClosed.isIntegral_iff, Iff.mp
-- 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 : 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
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : Membership.mem (γ := Submodule A L) (Submodule.restrictScalars A (↑I : Submodule B L)) y
hx₁ :
  IsIntegral A (A := L) ((((AlgHom.toLinearMap (lmul K L) : (a : L) → L →ₗ[K] L) x : L →ₗ[K] L) : (a : L) → L) y : L)
⊢ IsIntegral.{u_1, u_2} A (A := K) ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)

Tactic:
apply isIntegral_trace

Premises used: Algebra.isIntegral_trace
-- 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 : 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
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : Membership.mem (γ := Submodule A L) (Submodule.restrictScalars A (↑I : Submodule B L)) y
hx₁ :
  ∃ (y_1 : B),
    Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y_1 : L)
      ((((AlgHom.toLinearMap (lmul K L) : (a : L) → L →ₗ[K] L) x : L →ₗ[K] L) : (a : L) → L) y : L)
⊢ IsIntegral A (A := L) ((((AlgHom.toLinearMap (lmul K L) : (a : L) → L →ₗ[K] L) x : L →ₗ[K] L) : (a : L) → L) y : L)

Tactic:
rw [IsIntegralClosure.isIntegral_iff (A := B)]

Premises used: IsIntegralClosure.isIntegral_iff
-- 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 : 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
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : Membership.mem (γ := Submodule A L) (Submodule.restrictScalars A (↑I : Submodule B L)) y
hx₁ :
  ∀ z ∈ (↑⊤ : Set B),
    ∀ (hz : (Algebra.linearMap B L : (a : B) → L) z = y * x),
      ∃ (y_1 : B),
        Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y_1 : L)
          ((((AlgHom.toLinearMap (lmul K L) : (a : L) → L →ₗ[K] L) x : L →ₗ[K] L) : (a : L) → L) y : L)
⊢ ∃ (y_1 : B),
    Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y_1 : L)
      ((((AlgHom.toLinearMap (lmul K L) : (a : L) → L →ₗ[K] L) x : L →ₗ[K] L) : (a : L) → L) y : L)

Tactic:
have ⟨z, _, hz⟩ := hIJ (FractionalIdeal.mul_mem_mul hy hx)
-- 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 : 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
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : Membership.mem (γ := Submodule A L) (Submodule.restrictScalars A (↑I : Submodule B L)) y
z : B
left : z ∈ (↑⊤ : Set B)
hz : (Algebra.linearMap B L : (a : B) → L) z = y * x
⊢ (Algebra.linearMap B L : (a : B) → L) z = x * y

Tactic:
rw [mul_comm] at hz

Premises used: mul_comm
-- 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 : 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
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : Membership.mem (γ := Submodule A L) (Submodule.restrictScalars A (↑I : Submodule B L)) y
z : B
left : z ∈ (↑⊤ : Set B)
hz : (Algebra.linearMap B L : (a : B) → L) z = x * y
⊢ ∃ (y_1 : B),
    Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y_1 : L)
      ((((AlgHom.toLinearMap (lmul K L) : (a : L) → L →ₗ[K] L) x : L →ₗ[K] L) : (a : L) → L) y : L)

Tactic:
⟨z, hz⟩

Premises used: Exists.intro
-- 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 : 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
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : Membership.mem (γ := Submodule A L) (Submodule.restrictScalars A (↑I : Submodule B L)) y
z : B
left : z ∈ (↑⊤ : Set B)
hz : (Algebra.linearMap B L : (a : B) → L) z = x * y
⊢ ∃ (y_1 : B),
    Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y_1 : L)
      ((((AlgHom.toLinearMap (lmul K L) : (a : L) → L →ₗ[K] L) x : L →ₗ[K] L) : (a : L) → L) y : L)

Tactic:
exact ⟨z, hz⟩
-- 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 : 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
rw rw₁ : LE.le.{u} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 1
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 1 ≤ 1

Tactic:
rw [one_mul]

Premises used: one_mul
-- 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 : 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
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hJ : J ≠ 0
pos : ∀ (hI : I = 0), I ≤ dual A K J ↔ I * J ≤ dual A K 1
neg : ∀ (hI : ¬I = 0), I ≤ dual A K J ↔ I * J ≤ dual A K 1
⊢ I ≤ dual A K J ↔ I * J ≤ dual A K 1

Tactic:
by_cases hI : I = 0
-- 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 : 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
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hJ : J ≠ 0
hI : I = 0
⊢ I ≤ dual A K J ↔ I * J ≤ dual A K 1

Tactic:
simp [hI]
-- 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 : 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
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hJ : J ≠ 0
hI : ¬I = 0
neg : (↑I : Submodule B L) ≤ (↑(dual A K J) : Submodule B L) ↔ I * J ≤ dual A K 1
neg₁ :
  (↑I : Submodule B L) ≤ (↑(dual A K J) : Submodule B L) ↔ (↑(I * J) : Submodule B L) ≤ (↑(dual A K 1) : Submodule B L)
neg₂ :
  (↑I : Submodule B L) ≤ (↑(dual A K J) : Submodule B L) ↔
    (↑I : Submodule B L) * (↑J : Submodule B L) ≤ (↑(dual A K 1) : Submodule B L)
neg₃ :
  (↑I : Submodule B L) ≤ (↑J : Submodule B L)ᵛ ↔
    (↑I : Submodule B L) * (↑J : Submodule B L) ≤ (↑(dual A K 1) : Submodule B L)
neg₄ : (↑I : Submodule B L) ≤ (↑J : Submodule B L)ᵛ ↔ (↑I : Submodule B L) * (↑J : Submodule B L) ≤ 1ᵛ
neg₅ neg₆ : (↑I : Submodule B L) * (↑J : Submodule B L) ≤ 1ᵛ ↔ (↑I : Submodule B L) * (↑J : Submodule B L) ≤ 1ᵛ
⊢ I ≤ dual A K J ↔ I * J ≤ dual A K 1

Tactic:
rw [← coe_le_coe, ← coe_le_coe, coe_mul, coe_dual A K hJ, coe_dual_one, le_traceDual]

Premises used: FractionalIdeal.coe_le_coe, FractionalIdeal.coe_dual, FractionalIdeal.coe_dual_one, FractionalIdeal.coe_mul, Submodule.le_traceDual
-- 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 : 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
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I = 0
⊢ I⁻¹ ≤ dual A K I

Tactic:
simp [hI]
-- 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 : 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
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
⊢ I⁻¹ ≤ dual A K I

Tactic:
exact if hI : I = 0 then by simp [hI] else le_dual_inv_aux A K hI (le_of_eq (mul_inv_cancel₀ hI))
-- 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 : 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
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
⊢ I⁻¹ ≤ dual A K I

Tactic:
classical
  exact if hI : I = 0 then by simp [hI] else le_dual_inv_aux A K hI (le_of_eq (mul_inv_cancel₀ hI))
-- 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 : 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
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
pos : ∀ (hI : I = 0), (dual A K I)⁻¹ ≤ I
neg : ∀ (hI : ¬I = 0), (dual A K I)⁻¹ ≤ I
⊢ (dual A K I)⁻¹ ≤ I

Tactic:
by_cases hI : I = 0
-- 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 : 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
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I = 0
⊢ (dual A K I)⁻¹ ≤ I

Tactic:
simp [hI]
-- 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 : 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
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : ¬I = 0
⊢ 0 < dual A K I

Tactic:
simpa [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- 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 : 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
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : ¬I = 0
⊢ 0 < I

Tactic:
simpa [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero