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
neg : I⁻¹ ≤ dual A K I
⊢ (dual A K I)⁻¹ ≤ I

Tactic:
rw [inv_le_comm₀ (by simpa [pos_iff_ne_zero]) (by simpa [pos_iff_ne_zero])]

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

Tactic:
inv_le_dual ..

Premises used: Set.Mem, FractionalIdeal.inv_le_dual
-- 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:
exact inv_le_dual ..

Premises used: FractionalIdeal.inv_le_dual
-- 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 = dual A K 1 * I⁻¹
neg : ∀ (hI : ¬I = 0), dual A K I = dual A K 1 * I⁻¹
⊢ dual A K I = dual A K 1 * 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 = dual A K 1 * 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
neg : dual A K I ≤ dual A K 1 * I⁻¹
neg₁ : dual A K 1 * I⁻¹ ≤ dual A K I
⊢ dual A K I = dual A K 1 * I⁻¹

Tactic:
apply 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_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
neg : dual A K I * I ≤ dual A K 1
neg₁ neg₂ : dual A K I ≤ dual A K I
⊢ dual A K I ≤ dual A K 1 * I⁻¹

Tactic:
rw [le_mul_inv_iff₀ (pos_iff_ne_zero.2 hI), ← le_dual_iff A K hI]

Premises used: Iff.mpr, FractionalIdeal.le_dual_iff, le_mul_inv_iff₀, 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
neg : dual A K 1 * I⁻¹ * I ≤ dual A K 1
neg₁ : dual A K 1 * (I⁻¹ * I) ≤ dual A K 1
neg₂ : HMul.hMul (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) 1 ≤ dual A K 1
neg₃ neg₄ : LE.le.{u} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) (dual A K 1)
⊢ dual A K 1 * I⁻¹ ≤ dual A K I

Tactic:
rw [le_dual_iff A K hI, mul_assoc, inv_mul_cancel₀ hI, mul_one]

Premises used: FractionalIdeal.le_dual_iff, mul_assoc, mul_one, inv_mul_cancel₀
-- 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
rw : J⁻¹ / I⁻¹ = I / J
rw₁ : Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) 0
⊢ dual A K J / dual A K I = I / J

Tactic:
rw [dual_eq_mul_inv A K J, dual_eq_mul_inv A K I, mul_div_mul_comm, div_self, one_mul]

Premises used: FractionalIdeal.dual_eq_mul_inv, mul_div_mul_comm, one_mul, div_self
-- 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
⊢ J⁻¹ / I⁻¹ = I / J

Tactic:
inv_div_inv J I

Premises used: Set.Mem, setOf, inv_div_inv
-- 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
⊢ J⁻¹ / I⁻¹ = I / J

Tactic:
exact inv_div_inv J I

Premises used: inv_div_inv
-- 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
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) 0

Tactic:
simp only [ne_eq, dual_eq_zero_iff, one_ne_zero, not_false_eq_true]

Premises used: ne_eq, FractionalIdeal.dual_eq_zero_iff, one_ne_zero, not_false_eq_true
-- 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
rw : dual A K 1 * I⁻¹ * I = dual A K 1
rw₁ : dual A K 1 * (I⁻¹ * I) = dual A K 1
rw₂ : HMul.hMul (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) 1 = dual A K 1
rw₃ rw₄ : Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) (dual A K 1)
⊢ dual A K I * I = dual A K 1

Tactic:
rw [dual_eq_mul_inv, mul_assoc, inv_mul_cancel₀ hI, mul_one]

Premises used: mul_assoc, FractionalIdeal.dual_eq_mul_inv, mul_one, inv_mul_cancel₀
-- 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
rw : dual A K I * I = dual A K 1
rw₁ rw₂ : Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) (dual A K 1)
⊢ I * dual A K I = dual A K 1

Tactic:
rw [mul_comm, dual_mul_self A K hI]

Premises used: FractionalIdeal.dual_mul_self, 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 : FractionalIdeal.{u_3, u} (R := B) B⁰ L
rw : dual A K 1 * I⁻¹⁻¹ = dual A K 1 * I
rw₁ rw₂ : dual A K 1 * I = dual A K 1 * I
⊢ dual A K I⁻¹ = dual A K 1 * I

Tactic:
rw [dual_eq_mul_inv, inv_inv]

Premises used: FractionalIdeal.dual_eq_mul_inv, inv_inv
-- 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
rw : Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) 0
⊢ dual A K (dual A K I) = I

Tactic:
rw [dual_eq_mul_inv, dual_eq_mul_inv A K (I := I), mul_inv, inv_inv, ← mul_assoc, mul_inv_cancel₀,
    one_mul]

Premises used: mul_inv_cancel₀, mul_inv, mul_assoc, FractionalIdeal.dual_eq_mul_inv, inv_inv, 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 : FractionalIdeal.{u_3, u} (R := B) B⁰ L
rw : Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 0
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) 0

Tactic:
rw [dual_ne_zero_iff]

Premises used: FractionalIdeal.dual_ne_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 : FractionalIdeal.{u_3, u} (R := B) B⁰ L
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 0

Tactic:
one_ne_zero

Premises used: one_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
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 0

Tactic:
exact one_ne_zero

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

Tactic:
nth_rewrite 2 [← dual_dual A K I]

Premises used: FractionalIdeal.dual_dual
-- 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
hJ : J ≠ 0
rwa rwa₁ rwa₂ rwa₃ : I ≠ 0
⊢ dual A K I ≠ 0

Tactic:
rwa [dual_ne_zero_iff]

Premises used: FractionalIdeal.dual_ne_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
hJ : J ≠ 0
rw : dual A K I * J ≤ dual A K 1 ↔ J ≤ dual A K (dual A K I)
rw₁ : dual A K I * J ≤ dual A K 1 ↔ J * dual A K I ≤ dual A K 1
rw₂ rw₃ : J * dual A K I ≤ dual A K 1 ↔ J * dual A K I ≤ dual A K 1
⊢ dual A K I ≤ dual A K J ↔ J ≤ dual A K (dual A K I)

Tactic:
rw [le_dual_iff A K hJ, le_dual_iff A K (I := J) (by rwa [dual_ne_zero_iff]), mul_comm]

Premises used: FractionalIdeal.le_dual_iff, 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
⊢ Function.Involutive.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K)

Tactic:
dual_dual A K

Premises used: Function.Involutive, FractionalIdeal.dual_dual
-- 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
⊢ Function.Injective.{u + 1, u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K)

Tactic:
dual_involutive.injective

Premises used: FractionalIdeal.dual_involutive, Function.Involutive.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
x : M
hx : Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual A K 1) x
simp :
  ∀
    (hx :
      ∀ (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) : K))
    (a : B),
    ∃ (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) : K)
⊢ Membership.mem.{u, u} (α := L) (γ := FractionalIdeal.{u_5, u} (R := B) B⁰ L) (dual A K 1)
    ((Algebra.trace L M : (a : M) → L) x : L)

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, ← LinearMap.map_smul_of_tower,
    Algebra.trace_trace] at hx ⊢

Premises used: Algebra.algebraMap, RingHom.mem_range, Algebra.traceForm_apply, FractionalIdeal.mem_one_iff, forall_exists_index, FractionalIdeal.mem_dual, ne_eq, Algebra.trace_trace, mul_comm, Algebra.smul_def, LinearMap.map_smul_of_tower, 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
x : M
hx :
  ∀ (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) : K)
⊢ ∀ (a : B),
    ∃ (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) : K)

Tactic:
simpa using fun b ↦ hx (algebraMap B C b)

Premises used: Algebra.algebraMap, DFunLike.coe