awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R_1 : Type u_1
inst : CommRing R_1
K_1 : Type u_2
inst_1 : Field K_1
inst_2 : Algebra R_1 K_1
inst_3 : IsFractionRing R_1 K_1
R : Type u_1
inst_4 : CommRing R
K : Type u_2
inst_5 : Field K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : IsDedekindDomain R
a c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 0
⊢ HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑c.den : R)) :
          FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑a.den : R)) :
          FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) *
      a ≤
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑c.den : R)) :
          FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑a.den : R)) :
          FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) *
      c

Tactic:
gcongr
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R_1 : Type u_1
inst : CommRing R_1
K_1 : Type u_2
inst_1 : Field K_1
inst_2 : Algebra R_1 K_1
inst_3 : IsFractionRing R_1 K_1
R : Type u_1
inst_4 : CommRing R
K : Type u_2
inst_5 : Field K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : IsDedekindDomain R
a c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 0
⊢ Ideal.span {(↑c.den : R)} * a.num ≤ c.num * Ideal.span {(↑a.den : R)}

Tactic:
have H : Ideal.span {c.den.1} * a.num ≤ c.num * Ideal.span {a.den.1} := by
    rw [← FractionalIdeal.coeIdeal_le_coeIdeal K]
    simp only [FractionalIdeal.coeIdeal_mul, FractionalIdeal.coeIdeal_span_singleton, ←
      FractionalIdeal.den_mul_self_eq_num']
    ring_nf
    gcongr
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R_1 : Type u_1
inst : CommRing R_1
K_1 : Type u_2
inst_1 : Field K_1
inst_2 : Algebra R_1 K_1
inst_3 : IsFractionRing R_1 K_1
R : Type u_1
inst_4 : CommRing R
K : Type u_2
inst_5 : Field K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : IsDedekindDomain R
a c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 0
H : Ideal.span {(↑c.den : R)} * a.num ≤ c.num * Ideal.span {(↑a.den : R)}
⊢ Ideal.span {(↑c.den : R)} * a.num ≠ 0

Tactic:
simpa using FractionalIdeal.num_eq_zero_iff.not.mpr ha

Premises used: Iff.mpr, Iff.not, FractionalIdeal.num_eq_zero_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R_1 : Type u_1
inst : CommRing R_1
K_1 : Type u_2
inst_1 : Field K_1
inst_2 : Algebra R_1 K_1
inst_3 : IsFractionRing R_1 K_1
R : Type u_1
inst_4 : CommRing R
K : Type u_2
inst_5 : Field K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : IsDedekindDomain R
a c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 0
H : Ideal.span {(↑c.den : R)} * a.num ≤ c.num * Ideal.span {(↑a.den : R)}
x : R
hx : Ideal.span {(↑c.den : R)} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {(↑a.den : R)}
⊢ ∃ (x : K), a + HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (FractionalIdeal.spanSingleton R⁰ x) 1 = c

Tactic:
⟨algebraMap R K x / algebraMap R K (a.den.1 * c.den.1), ?_⟩

Premises used: HMul.hMul, Algebra.algebraMap, HDiv.hDiv, FractionalIdeal.den, Exists.intro, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R_1 : Type u_1
inst : CommRing R_1
K_1 : Type u_2
inst_1 : Field K_1
inst_2 : Algebra R_1 K_1
inst_3 : IsFractionRing R_1 K_1
R : Type u_1
inst_4 : CommRing R
K : Type u_2
inst_5 : Field K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : IsDedekindDomain R
a c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 0
H : Ideal.span {(↑c.den : R)} * a.num ≤ c.num * Ideal.span {(↑a.den : R)}
x : R
hx : Ideal.span {(↑c.den : R)} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {(↑a.den : R)}
refine :
  a +
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰
          (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
            ((algebraMap R K : (a : R) → K) ((↑a.den : R) * (↑c.den : R)) : K)))
        1 =
    c
⊢ ∃ (x : K), a + HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (FractionalIdeal.spanSingleton R⁰ x) 1 = c

Tactic:
refine ⟨algebraMap R K x / algebraMap R K (a.den.1 * c.den.1), ?_⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R_1 : Type u_1
inst : CommRing R_1
K_1 : Type u_2
inst_1 : Field K_1
inst_2 : Algebra R_1 K_1
inst_3 : IsFractionRing R_1 K_1
R : Type u_1
inst_4 : CommRing R
K : Type u_2
inst_5 : Field K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : IsDedekindDomain R
a c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 0
H : Ideal.span {(↑c.den : R)} * a.num ≤ c.num * Ideal.span {(↑a.den : R)}
x : R
hx : Ideal.span {(↑c.den : R)} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {(↑a.den : R)}
⊢ a +
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰
          (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
            ((algebraMap R K : (a : R) → K) ((↑a.den : R) * (↑c.den : R)) : K)))
        1 =
    c

Tactic:
mul_left_injective₀ (b := .spanSingleton _
    (algebraMap R K (a.den.1 * c.den.1))) ?_ ?_

Premises used: mul_left_injective₀
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R_1 : Type u_1
inst : CommRing R_1
K_1 : Type u_2
inst_1 : Field K_1
inst_2 : Algebra R_1 K_1
inst_3 : IsFractionRing R_1 K_1
R : Type u_1
inst_4 : CommRing R
K : Type u_2
inst_5 : Field K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : IsDedekindDomain R
a c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 0
H : Ideal.span {(↑c.den : R)} * a.num ≤ c.num * Ideal.span {(↑a.den : R)}
x : R
hx : Ideal.span {(↑c.den : R)} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {(↑a.den : R)}
refine_1 :
  Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) ((↑a.den : R) * (↑c.den : R))) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (0 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
refine_2 :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    ((fun (a_1 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) ↦
        HMul.hMul (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) a_1
          (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) ((↑a.den : R) * (↑c.den : R))) :
            FractionalIdeal.{u_1, u_2} (R := R) R⁰ K))
      (a +
        HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
          (FractionalIdeal.spanSingleton R⁰
            (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
              ((algebraMap R K : (a : R) → K) ((↑a.den : R) * (↑c.den : R)) : K)))
          1))
    ((fun (a_1 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) ↦
        HMul.hMul (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) a_1
          (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) ((↑a.den : R) * (↑c.den : R))) :
            FractionalIdeal.{u_1, u_2} (R := R) R⁰ K))
      c)
⊢ a +
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰
          (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
            ((algebraMap R K : (a : R) → K) ((↑a.den : R) * (↑c.den : R)) : K)))
        1 =
    c

Tactic:
refine mul_left_injective₀ (b := .spanSingleton _
    (algebraMap R K (a.den.1 * c.den.1))) ?_ ?_

Premises used: mul_left_injective₀
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R_1 : Type u_1
inst : CommRing R_1
K_1 : Type u_2
inst_1 : Field K_1
inst_2 : Algebra R_1 K_1
inst_3 : IsFractionRing R_1 K_1
R : Type u_1
inst_4 : CommRing R
K : Type u_2
inst_5 : Field K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : IsDedekindDomain R
a c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 0
H : Ideal.span {(↑c.den : R)} * a.num ≤ c.num * Ideal.span {(↑a.den : R)}
x : R
hx : Ideal.span {(↑c.den : R)} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {(↑a.den : R)}
⊢ Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) ((↑a.den : R) * (↑c.den : R))) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (0 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)

Tactic:
simp [FractionalIdeal.spanSingleton_eq_zero_iff]

Premises used: FractionalIdeal.spanSingleton_eq_zero_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R_1 : Type u_1
inst : CommRing R_1
K_1 : Type u_2
inst_1 : Field K_1
inst_2 : Algebra R_1 K_1
inst_3 : IsFractionRing R_1 K_1
R : Type u_1
inst_4 : CommRing R
K : Type u_2
inst_5 : Field K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : IsDedekindDomain R
a c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 0
H : Ideal.span {(↑c.den : R)} * a.num ≤ c.num * Ideal.span {(↑a.den : R)}
x : R
hx : Ideal.span {(↑c.den : R)} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {(↑a.den : R)}
refine_2 :
  HAdd.hAdd (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (a *
        FractionalIdeal.spanSingleton R⁰
          (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) (↑a.den : R) : K)
            ((algebraMap R K : (a : R) → K) (↑c.den : R) : K)))
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) x) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) =
    c *
      FractionalIdeal.spanSingleton R⁰
        (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) (↑a.den : R) : K)
          ((algebraMap R K : (a : R) → K) (↑c.den : R) : K))
⊢ Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    ((fun (a_1 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) ↦
        HMul.hMul (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) a_1
          (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) ((↑a.den : R) * (↑c.den : R))) :
            FractionalIdeal.{u_1, u_2} (R := R) R⁰ K))
      (a +
        HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
          (FractionalIdeal.spanSingleton R⁰
            (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
              ((algebraMap R K : (a : R) → K) ((↑a.den : R) * (↑c.den : R)) : K)))
          1))
    ((fun (a_1 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) ↦
        HMul.hMul (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) a_1
          (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) ((↑a.den : R) * (↑c.den : R))) :
            FractionalIdeal.{u_1, u_2} (R := R) R⁰ K))
      c)

Tactic:
simp only [map_mul, mul_one, add_mul, FractionalIdeal.spanSingleton_mul_spanSingleton,
      isUnit_iff_ne_zero, ne_eq, mul_eq_zero, FaithfulSMul.algebraMap_eq_zero_iff,
      nonZeroDivisors.coe_ne_zero, or_self, not_false_eq_true, IsUnit.div_mul_cancel]

Premises used: add_mul, FractionalIdeal.spanSingleton_mul_spanSingleton, isUnit_iff_ne_zero, mul_eq_zero, ne_eq, map_mul, nonZeroDivisors.coe_ne_zero, or_self, mul_one, IsUnit.div_mul_cancel, not_false_eq_true, FaithfulSMul.algebraMap_eq_zero_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R_1 : Type u_1
inst : CommRing R_1
K_1 : Type u_2
inst_1 : Field K_1
inst_2 : Algebra R_1 K_1
inst_3 : IsFractionRing R_1 K_1
R : Type u_1
inst_4 : CommRing R
K : Type u_2
inst_5 : Field K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : IsDedekindDomain R
a c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 0
H : Ideal.span {(↑c.den : R)} * a.num ≤ c.num * Ideal.span {(↑a.den : R)}
x : R
hx : Ideal.span {(↑c.den : R)} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {(↑a.den : R)}
refine_2 :
  HAdd.hAdd (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑c.den : R)) :
          FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        ((↑a.num : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K))
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) x) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑c.num : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑a.den : R)) :
        FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
⊢ HAdd.hAdd (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (a *
        FractionalIdeal.spanSingleton R⁰
          (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) (↑a.den : R) : K)
            ((algebraMap R K : (a : R) → K) (↑c.den : R) : K)))
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) x) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) =
    c *
      FractionalIdeal.spanSingleton R⁰
        (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) (↑a.den : R) : K)
          ((algebraMap R K : (a : R) → K) (↑c.den : R) : K))

Tactic:
rw [← FractionalIdeal.spanSingleton_mul_spanSingleton, ← mul_assoc, mul_comm a,
      FractionalIdeal.den_mul_self_eq_num', ← mul_assoc, mul_right_comm,
      mul_comm c, FractionalIdeal.den_mul_self_eq_num', mul_comm]

Premises used: FractionalIdeal.spanSingleton_mul_spanSingleton, mul_assoc, mul_right_comm, mul_comm, FractionalIdeal.den_mul_self_eq_num'
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R_1 : Type u_1
inst : CommRing R_1
K_1 : Type u_2
inst_1 : Field K_1
inst_2 : Algebra R_1 K_1
inst_3 : IsFractionRing R_1 K_1
R : Type u_1
inst_4 : CommRing R
K : Type u_2
inst_5 : Field K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : IsDedekindDomain R
a c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 0
H : Ideal.span {(↑c.den : R)} * a.num ≤ c.num * Ideal.span {(↑a.den : R)}
x : R
hx : Ideal.span {(↑c.den : R)} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {(↑a.den : R)}
refine_2 :
  HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑(Ideal.span {(↑c.den : R)}) : FractionalIdeal R⁰ K)
        (↑a.num : FractionalIdeal R⁰ K) +
      (↑(Ideal.span {x}) : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑c.num : FractionalIdeal R⁰ K)
      (↑(Ideal.span {(↑a.den : R)}) : FractionalIdeal R⁰ K)
refine_2₁ :
  HAdd.hAdd (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (↑(Ideal.span {(↑c.den : R)} * a.num) : FractionalIdeal R⁰ K) (↑(Ideal.span {x}) : FractionalIdeal R⁰ K) =
    (↑(c.num * Ideal.span {(↑a.den : R)}) : FractionalIdeal R⁰ K)
refine_2₂ :
  HAdd.hAdd (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (↑(Ideal.span {(↑c.den : R)} * a.num) : FractionalIdeal R⁰ K) (↑(Ideal.span {x}) : FractionalIdeal R⁰ K) =
    (↑(Ideal.span {(↑c.den : R)} * a.num ⊔ Ideal.span {x}) : FractionalIdeal R⁰ K)
⊢ HAdd.hAdd (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑c.den : R)) :
          FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        ((↑a.num : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K))
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) x) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑c.num : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑a.den : R)) :
        FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)

Tactic:
simp_rw [← FractionalIdeal.coeIdeal_span_singleton, ← FractionalIdeal.coeIdeal_mul,
      ← hx, ← FractionalIdeal.coeIdeal_sup]

Premises used: FractionalIdeal.coeIdeal_span_singleton, FractionalIdeal.coeIdeal_sup, FractionalIdeal.coeIdeal_mul
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
a b c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
rw : a + spanSingleton R⁰ (Exists.choose (p := fun (x : K) ↦ a + spanSingleton R⁰ x * b = c) ⋯) * b = c
⊢ a + spanSingleton R⁰ (c.divMod b a) * b = c

Tactic:
rw [divMod, dif_pos ⟨hac, ha, hb⟩]

Premises used: FractionalIdeal.divMod, dif_pos
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
a b c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
⊢ a + spanSingleton R⁰ (Exists.choose (p := fun (x : K) ↦ a + spanSingleton R⁰ x * b = c) ⋯) * b = c

Tactic:
(IsDedekindDomain.exists_add_spanSingleton_mul_eq hac ha hb).choose_spec

Premises used: Exists.choose_spec, Set.Mem, setOf, IsDedekindDomain.exists_add_spanSingleton_mul_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
a b c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
⊢ a + spanSingleton R⁰ (Exists.choose (p := fun (x : K) ↦ a + spanSingleton R⁰ x * b = c) ⋯) * b = c

Tactic:
exact (IsDedekindDomain.exists_add_spanSingleton_mul_eq hac ha hb).choose_spec

Premises used: Exists.choose_spec, IsDedekindDomain.exists_add_spanSingleton_mul_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
I J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
⊢ I.divMod 0 J = 0

Tactic:
simp [divMod]

Premises used: FractionalIdeal.divMod
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
I J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
⊢ I.divMod J 0 = 0

Tactic:
simp [divMod]

Premises used: FractionalIdeal.divMod
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
I J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
⊢ divMod 0 I J = 0

Tactic:
simp [divMod, ← and_assoc]

Premises used: FractionalIdeal.divMod, and_assoc
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
a b c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : ¬a ≤ c
⊢ c.divMod b a = 0

Tactic:
simp [divMod, hac]

Premises used: FractionalIdeal.divMod
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
⊢ (J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I) * (J' ⊔ spanSingleton R⁰ (I'.divMod I J') * I) =
    J' * (spanSingleton R⁰ (I'.divMod I J') * I)

Tactic:
have := FractionalIdeal.sup_mul_inf J' (spanSingleton R⁰ (I'.divMod I J') * I)
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this :
  (J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I) * (J' ⊔ spanSingleton R⁰ (I'.divMod I J') * I) =
    J' * (spanSingleton R⁰ (I'.divMod I J') * I)
rwa : ∀ (this : (J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I) * I' = spanSingleton R⁰ (I'.divMod I J') * J * I'), I' ≠ 0
⊢ J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J

Tactic:
rwa [FractionalIdeal.sup_eq_add, divMod_spec h' hJ' hI, mul_left_comm, mul_comm J' I, H,
      mul_comm I' J, ← mul_assoc, (mul_left_injective₀ _).eq_iff] at this

Premises used: FractionalIdeal.sup_eq_add, mul_left_injective₀, mul_assoc, Function.Injective.eq_iff, mul_left_comm, FractionalIdeal.divMod_spec, mul_comm
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
I J J' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
h : J ≤ I
hJ' : J' ≠ 0
hI : I ≠ 0
H : I * J' = 0 * J
h' : J' ≤ 0
this : (J' ⊓ spanSingleton R⁰ (divMod 0 I J') * I) * 0 = spanSingleton R⁰ (divMod 0 I J') * J * 0
⊢ J' = 0

Tactic:
simpa using h'
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
I J J' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
h : J ≤ I
hJ' : J' ≠ 0
hI : I ≠ 0
H : I * J' = 0 * J
h' : J' ≤ 0
this : (J' ⊓ spanSingleton R⁰ (divMod 0 I J') * I) * 0 = spanSingleton R⁰ (divMod 0 I J') * J * 0
⊢ False

Tactic:
exact hJ' (by simpa using h')
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
⊢ J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J

Tactic:
haveI : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J := by
    have := FractionalIdeal.sup_mul_inf J' (spanSingleton R⁰ (I'.divMod I J') * I)
    rwa [FractionalIdeal.sup_eq_add, divMod_spec h' hJ' hI, mul_left_comm, mul_comm J' I, H,
      mul_comm I' J, ← mul_assoc, (mul_left_injective₀ _).eq_iff] at this
    rintro rfl
    exact hJ' (by simpa using h')