awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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
⊢ I ≤ dual A K J ↔ I * J ≤ dual A K 1
have pos : ∀ (hI : I = 0), I ≤ dual A K J ↔ I * J ≤ dual A K 1
Tactic: by_cases hI : I = 0
-- 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_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
⊢ I ≤ dual A K J ↔ I * J ≤ dual A K 1
have neg : ∀ (hI : ¬I = 0), I ≤ dual A K J ↔ I * J ≤ dual A K 1
Tactic: by_cases hI : I = 0
-- 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_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
have neg : (↑I : Submodule B L) ≤ (↑(dual A K J) : Submodule B L) ↔ 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]
-- 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_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
⊢ I ≤ dual A K J ↔ I * J ≤ dual A K 1
have neg₁ : (↑I : Submodule B L) ≤ (↑(dual A K J) : Submodule B L) ↔ (↑(I * J) : Submodule B L) ≤ (↑(dual A K 1) : Submodule B L)
Tactic: rw [← coe_le_coe, ← coe_le_coe, coe_mul, coe_dual A K hJ, coe_dual_one, le_traceDual]
-- 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_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)
⊢ I ≤ dual A K J ↔ I * J ≤ dual A K 1
have 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)
Tactic: rw [← coe_le_coe, ← coe_le_coe, coe_mul, coe_dual A K hJ, coe_dual_one, le_traceDual]
-- 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_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)
⊢ I ≤ dual A K J ↔ I * J ≤ dual A K 1
have neg₃ : (↑I : Submodule B L) ≤ (↑J : Submodule B L)ᵛ ↔
  (↑I : Submodule B L) * (↑J : Submodule B L) ≤ (↑(dual A K 1) : Submodule B L)
Tactic: rw [← coe_le_coe, ← coe_le_coe, coe_mul, coe_dual A K hJ, coe_dual_one, le_traceDual]
-- 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_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)
⊢ I ≤ dual A K J ↔ I * J ≤ dual A K 1
have neg₄ : (↑I : Submodule B L) ≤ (↑J : Submodule B L)ᵛ ↔ (↑I : Submodule B L) * (↑J : Submodule B L) ≤ 1ᵛ
Tactic: rw [← coe_le_coe, ← coe_le_coe, coe_mul, coe_dual A K hJ, coe_dual_one, le_traceDual]
-- 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_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ᵛ
⊢ I ≤ dual A K J ↔ I * J ≤ dual A K 1
have neg₅ : (↑I : Submodule B L) * (↑J : Submodule B L) ≤ 1ᵛ ↔ (↑I : Submodule B L) * (↑J : Submodule B L) ≤ 1ᵛ
Tactic: rw [← coe_le_coe, ← coe_le_coe, coe_mul, coe_dual A K hJ, coe_dual_one, le_traceDual]
-- 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_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)⁻¹ ≤ I
have pos : ∀ (hI : I = 0), (dual A K I)⁻¹ ≤ I
Tactic: by_cases hI : I = 0
-- 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_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
⊢ (dual A K I)⁻¹ ≤ I
have neg : ∀ (hI : ¬I = 0), (dual A K I)⁻¹ ≤ I
Tactic: by_cases hI : I = 0
-- 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_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
have neg : I⁻¹ ≤ dual A K I
Tactic: rw [inv_le_comm₀ (by simpa [pos_iff_ne_zero]) (by simpa [pos_iff_ne_zero])]
-- 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_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 = dual A K 1 * I⁻¹
have pos : ∀ (hI : I = 0), dual A K I = dual A K 1 * I⁻¹
Tactic: by_cases hI : I = 0
-- 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_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⁻¹
⊢ dual A K I = dual A K 1 * I⁻¹
have neg : ∀ (hI : ¬I = 0), dual A K I = dual A K 1 * I⁻¹
Tactic: by_cases hI : I = 0
-- 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_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⁻¹
have neg : dual A K I ≤ dual A K 1 * I⁻¹
Tactic: apply 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_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⁻¹
⊢ dual A K I = dual A K 1 * I⁻¹
have neg₁ : dual A K 1 * I⁻¹ ≤ dual A K I
Tactic: apply 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_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⁻¹
have neg : dual A K I * I ≤ dual A K 1
Tactic: rw [le_mul_inv_iff₀ (pos_iff_ne_zero.2 hI), ← le_dual_iff A K hI]
-- 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_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
⊢ dual A K I ≤ dual A K 1 * I⁻¹
have neg₁ : dual A K I ≤ dual A K I
Tactic: rw [le_mul_inv_iff₀ (pos_iff_ne_zero.2 hI), ← le_dual_iff A K hI]
-- 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_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 1 * I⁻¹ ≤ dual A K I
have neg : dual A K 1 * I⁻¹ * I ≤ dual A K 1
Tactic: rw [le_dual_iff A K hI, mul_assoc, inv_mul_cancel₀ hI, mul_one]
-- 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_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
⊢ dual A K 1 * I⁻¹ ≤ dual A K I
have neg₁ : dual A K 1 * (I⁻¹ * I) ≤ dual A K 1
Tactic: rw [le_dual_iff A K hI, mul_assoc, inv_mul_cancel₀ hI, mul_one]
-- 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_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
⊢ dual A K 1 * I⁻¹ ≤ dual A K I
have neg₂ : HMul.hMul (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) 1 ≤ dual A K 1
Tactic: rw [le_dual_iff A K hI, mul_assoc, inv_mul_cancel₀ hI, mul_one]
-- 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_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
⊢ dual A K 1 * I⁻¹ ≤ dual A K I
have neg₃ : LE.le.{u} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) (dual A K 1)
Tactic: rw [le_dual_iff A K hI, mul_assoc, inv_mul_cancel₀ hI, mul_one]
-- 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_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
⊢ dual A K J / dual A K I = I / J
have rw : J⁻¹ / 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]
-- 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_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
⊢ dual A K J / dual A K I = I / J
have rw₁ : Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) 0
Tactic: rw [dual_eq_mul_inv A K J, dual_eq_mul_inv A K I, mul_div_mul_comm, div_self, one_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_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 = dual A K 1
have rw : dual A K 1 * I⁻¹ * I = dual A K 1
Tactic: rw [dual_eq_mul_inv, mul_assoc, inv_mul_cancel₀ hI, mul_one]
-- 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_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
⊢ dual A K I * I = dual A K 1
have rw₁ : dual A K 1 * (I⁻¹ * I) = dual A K 1
Tactic: rw [dual_eq_mul_inv, mul_assoc, inv_mul_cancel₀ hI, mul_one]
-- 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_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
⊢ dual A K I * I = dual A K 1
have rw₂ : HMul.hMul (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) 1 = dual A K 1
Tactic: rw [dual_eq_mul_inv, mul_assoc, inv_mul_cancel₀ hI, mul_one]