awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
y : A
h_Iy : y ∈ I
hy₀ :
  Membership.mem.{u_3, u_3} (α := K) (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
⊢ y * b ∈ I * (Multiset.map PrimeSpectrum.asIdeal Z).prod

Tactic:
exact Submodule.smul_mem_smul h_Iy hbZ

Premises used: Submodule.smul_mem_smul
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
y : A
h_Iy : y ∈ I
hy₀ :
  Membership.mem.{u_3, u_3} (α := K) (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
⊢ y * b ∈ J

Tactic:
have h_yb : y * b ∈ J := by
      apply hle
      rw [Multiset.prod_cons]
      exact Submodule.smul_mem_smul h_Iy hbZ
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
y : A
h_Iy : y ∈ I
hy₀ :
  Membership.mem.{u_3, u_3} (α := K) (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
h_yb : y * b ∈ J
⊢ ∃ (a_1 : A), a_1 * a = y * b

Tactic:
rw [Ideal.mem_span_singleton'] at h_yb

Premises used: Ideal.mem_span_singleton'
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
y : A
h_Iy : y ∈ I
hy₀ :
  Membership.mem.{u_3, u_3} (α := K) (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
h_yb : ∃ (a_1 : A), a_1 * a = y * b
refine_2 :
  ∀ (c : A) (hc : c * a = y * b),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (y * b) : K)
        (((algebraMap A K : (a : A) → K) a)⁻¹ : K))
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1
    (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (y * b) : K)
      (((algebraMap A K : (a : A) → K) a)⁻¹ : K))

Tactic:
rcases h_yb with ⟨c, hc⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
y : A
h_Iy : y ∈ I
hy₀ :
  Membership.mem.{u_3, u_3} (α := K) (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
c : A
hc : c * a = y * b
refine_2 :
  Membership.mem.{u_3, u_3} (α := K) (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1
    ((algebraMap A K : (a : A) → K) c : K)
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1
    (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (y * b) : K)
      (((algebraMap A K : (a : A) → K) a)⁻¹ : K))

Tactic:
rw [← hc, map_mul, mul_assoc, mul_inv_cancel₀ hnz_fa, mul_one]

Premises used: mul_inv_cancel₀, mul_assoc, map_mul, mul_one
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
y : A
h_Iy : y ∈ I
hy₀ :
  Membership.mem.{u_3, u_3} (α := K) (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
c : A
hc : c * a = y * b
⊢ Membership.mem.{u_3, u_3} (α := K) (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1
    ((algebraMap A K : (a : A) → K) c : K)

Tactic:
apply coe_mem_one

Premises used: FractionalIdeal.coe_mem_one
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
⊢ HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) (((algebraMap A K : (a : A) → K) a)⁻¹ : K) ∉
    (↑1 : Set K)

Tactic:
mt (mem_one_iff _).mp ?_

Premises used: FractionalIdeal.mem_one_iff, mt, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
refine_3 :
  ¬∃ (x' : A),
      (algebraMap A K : (a : A) → K) x' =
        HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) (((algebraMap A K : (a : A) → K) a)⁻¹ : K)
⊢ HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) (((algebraMap A K : (a : A) → K) a)⁻¹ : K) ∉
    (↑1 : Set K)

Tactic:
refine mt (mem_one_iff _).mp ?_

Premises used: FractionalIdeal.mem_one_iff, mt, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
x' : A
h₂_abs :
  (algebraMap A K : (a : A) → K) x' =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) (((algebraMap A K : (a : A) → K) a)⁻¹ : K)
⊢ Eq.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) (x' * a) : K) ((algebraMap A K : (a : A) → K) b : K)

Tactic:
rw [← div_eq_mul_inv, eq_div_iff_mul_eq hnz_fa, ← map_mul] at h₂_abs

Premises used: div_eq_mul_inv, map_mul, eq_div_iff_mul_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
x' : A
h₂_abs : Eq.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) (x' * a) : K) ((algebraMap A K : (a : A) → K) b : K)
⊢ Membership.mem (γ := Ideal A) (span {a}) b

Tactic:
have := Ideal.mem_span_singleton'.mpr ⟨x', IsFractionRing.injective A K h₂_abs⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
x' : A
h₂_abs : Eq.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) (x' * a) : K) ((algebraMap A K : (a : A) → K) b : K)
this : Membership.mem (γ := Ideal A) (span {a}) b
⊢ False

Tactic:
contradiction
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI :
  (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1
⊢ ∃ (J : Ideal A),
    (↑J : FractionalIdeal A⁰ K) =
      HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹

Tactic:
le_one_iff_exists_coeIdeal.mp mul_one_div_le_one

Premises used: FractionalIdeal.le_one_iff_exists_coeIdeal, FractionalIdeal.mul_one_div_le_one, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI :
  (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1
obtain :
  ∀ (J : Ideal A)
    (hJ :
      (↑J : FractionalIdeal A⁰ K) =
        HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
          (↑I : FractionalIdeal A⁰ K)⁻¹),
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹ =
      1
⊢ HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
    1

Tactic:
obtain ⟨J, hJ⟩ : ∃ J : Ideal A, (J : FractionalIdeal A⁰ K) = I * (I : FractionalIdeal A⁰ K)⁻¹ :=
    le_one_iff_exists_coeIdeal.mp mul_one_div_le_one

Premises used: FractionalIdeal.le_one_iff_exists_coeIdeal, Ideal, FractionalIdeal.mul_one_div_le_one, Iff.mp, FractionalIdeal.coeIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI :
  (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1
J : Ideal A
hJ :
  (↑J : FractionalIdeal A⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹
pos :
  ∀ (hJ0 : J = ⊥),
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹ =
      1
neg :
  ∀ (hJ0 : ¬J = ⊥),
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹ =
      1
⊢ HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
    1

Tactic:
by_cases hJ0 : J = ⊥
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI :
  (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1
J : Ideal A
hJ :
  (↑J : FractionalIdeal A⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹
hJ0 : J = ⊥
⊢ (↑⊥ : FractionalIdeal A⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹

Tactic:
subst hJ0
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI :
  (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1
hJ :
  (↑⊥ : FractionalIdeal A⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹
⊢ HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
    1

Tactic:
absurd ?_ hI0

Premises used: absurd
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI :
  (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1
hJ :
  (↑⊥ : FractionalIdeal A⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹
pos : I = ⊥
⊢ HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
    1

Tactic:
refine absurd ?_ hI0

Premises used: absurd
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI :
  (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1
hJ :
  (↑⊥ : FractionalIdeal A⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹
pos :
  (↑I : FractionalIdeal A⁰ K) ≤
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹
⊢ I = ⊥

Tactic:
rw [eq_bot_iff, ← coeIdeal_le_coeIdeal K, hJ]

Premises used: eq_bot_iff, FractionalIdeal.coeIdeal_le_coeIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI :
  (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1
hJ :
  (↑⊥ : FractionalIdeal A⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹
⊢ (↑I : FractionalIdeal A⁰ K) ≤
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹

Tactic:
coe_ideal_le_self_mul_inv K I

Premises used: FractionalIdeal.coe_ideal_le_self_mul_inv
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI :
  (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1
hJ :
  (↑⊥ : FractionalIdeal A⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹
⊢ (↑I : FractionalIdeal A⁰ K) ≤
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹

Tactic:
exact coe_ideal_le_self_mul_inv K I

Premises used: FractionalIdeal.coe_ideal_le_self_mul_inv
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI :
  (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1
J : Ideal A
hJ :
  (↑J : FractionalIdeal A⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹
hJ0 : ¬J = ⊥
pos :
  ∀ (hJ1 : J = ⊤),
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹ =
      1
neg :
  ∀ (hJ1 : ¬J = ⊤),
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹ =
      1
⊢ HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
    1

Tactic:
by_cases hJ1 : J = ⊤
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI :
  (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1
J : Ideal A
hJ :
  (↑J : FractionalIdeal A⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹
hJ0 : ¬J = ⊥
hJ1 : J = ⊤
pos : Eq.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) 1
pos₁ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑⊤ : FractionalIdeal A⁰ K) 1
pos₂ pos₃ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 1
⊢ HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
    1

Tactic:
rw [← hJ, hJ1, coeIdeal_top]

Premises used: FractionalIdeal.coeIdeal_top
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI :
  (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1
J : Ideal A
hJ :
  (↑J : FractionalIdeal A⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹
hJ0 : ¬J = ⊥
hJ1 : ¬J = ⊤
⊢ HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
    1

Tactic:
(not_inv_le_one_of_ne_bot (K := K) hJ0 hJ1 (hJ ▸ hI)).elim

Premises used: False.elim, FractionalIdeal.not_inv_le_one_of_ne_bot
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI :
  (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1
J : Ideal A
hJ :
  (↑J : FractionalIdeal A⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹
hJ0 : ¬J = ⊥
hJ1 : ¬J = ⊤
⊢ HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
    1

Tactic:
exact (not_inv_le_one_of_ne_bot (K := K) hJ0 hJ1 (hJ ▸ hI)).elim

Premises used: False.elim, FractionalIdeal.not_inv_le_one_of_ne_bot
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
apply :
  (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1
⊢ HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
    1

Tactic:
apply mul_inv_cancel_of_le_one hI0

Premises used: FractionalIdeal.mul_inv_cancel_of_le_one
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
pos :
  ∀
    (hJ0 :
      HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
          (↑I : FractionalIdeal A⁰ K)⁻¹ =
        0),
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
          (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
      1
neg :
  ∀
    (hJ0 :
      ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
            (↑I : FractionalIdeal A⁰ K)⁻¹ =
          0),
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
          (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
      1
⊢ (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1

Tactic:
by_cases hJ0 : I * (I : FractionalIdeal A⁰ K)⁻¹ = 0

Premises used: FractionalIdeal.coeIdeal