awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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)
⊢ 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
have 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)
Tactic: refine mul_left_injective₀ (b := .spanSingleton _
    (algebraMap R K (a.den.1 * c.den.1))) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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)}
⊢ 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)
have 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))
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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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)}
⊢ 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))
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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)}
⊢ 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)
have 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)
Tactic: simp_rw [← FractionalIdeal.coeIdeal_span_singleton, ← FractionalIdeal.coeIdeal_mul,
      ← hx, ← FractionalIdeal.coeIdeal_sup]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [← FractionalIdeal.coeIdeal_span_singleton, ← FractionalIdeal.coeIdeal_mul,
      ← hx, ← FractionalIdeal.coeIdeal_sup]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [← FractionalIdeal.coeIdeal_span_singleton, ← FractionalIdeal.coeIdeal_mul,
      ← hx, ← FractionalIdeal.coeIdeal_sup]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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⁰ (c.divMod b a) * b = c
have rw : a + spanSingleton R⁰ (Exists.choose (p := fun (x : K) ↦ a + spanSingleton R⁰ x * b = c) sorry) * b = c
Tactic: rw [divMod, dif_pos ⟨hac, ha, hb⟩]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
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
have 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)
Tactic: have := FractionalIdeal.sup_mul_inf J' (spanSingleton R⁰ (I'.divMod I J') * I)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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)
⊢ J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
have rwa : ∀ (this : (J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I) * I' = spanSingleton R⁰ (I'.divMod I J') * J * I'), I' ≠ 0
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
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
⊢ (↥(↑I : Submodule R K) ⧸ Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)) ≃ₗ[R]
    ↥(↑I' : Submodule R K) ⧸ Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K)
have this : 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')
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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 = spanSingleton R⁰ (I'.divMod I J') * J
⊢ (↥(↑I : Submodule R K) ⧸ Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)) ≃ₗ[R]
    ↥(↑I' : Submodule R K) ⧸ Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K)
have refine_1 : ∀ x ∈ (↑I : Submodule R K),
  Membership.mem (α := K) (↑I' : Submodule R K)
    ((((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J') : Module.End R K) : (a : K) → K) x : K)
Tactic: refine .ofBijective (Submodule.mapQ _ _ (LinearMap.restrict
    (Algebra.lsmul R _ _ (I'.divMod I J')) ?_) ?_) ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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 = spanSingleton R⁰ (I'.divMod I J') * J
refine_1 :
  ∀ x ∈ (↑I : Submodule R K),
    Membership.mem (α := K) (↑I' : Submodule R K)
      ((((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J') : Module.End R K) : (a : K) → K) x : K)
⊢ (↥(↑I : Submodule R K) ⧸ Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)) ≃ₗ[R]
    ↥(↑I' : Submodule R K) ⧸ Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K)
have refine_2 : Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K) ≤
  Submodule.comap (σ₁₂ := RingHom.id R)
    (LinearMap.restrict ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J')) sorry)
    (Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K))
Tactic: refine .ofBijective (Submodule.mapQ _ _ (LinearMap.restrict
    (Algebra.lsmul R _ _ (I'.divMod I J')) ?_) ?_) ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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 = spanSingleton R⁰ (I'.divMod I J') * J
refine_1 :
  ∀ x ∈ (↑I : Submodule R K),
    Membership.mem (α := K) (↑I' : Submodule R K)
      ((((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J') : Module.End R K) : (a : K) → K) x : K)
refine_2 :
  Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K) ≤
    Submodule.comap (σ₁₂ := RingHom.id R)
      (LinearMap.restrict ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J')) ⋯)
      (Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K))
⊢ (↥(↑I : Submodule R K) ⧸ Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)) ≃ₗ[R]
    ↥(↑I' : Submodule R K) ⧸ Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K)
have refine_3 : Injective.{u_2 + 1, u_2 + 1} (α :=
  ↥(↑I : Submodule R K) ⧸ Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)) (β :=
  ↥(↑I' : Submodule R K) ⧸ Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K))
  (⇑((Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)).mapQ
        (Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K))
        (LinearMap.restrict ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J')) sorry) sorry) :
    (a : ↥(↑I : Submodule R K) ⧸ Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)) →
      ↥(↑I' : Submodule R K) ⧸ Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K))
Tactic: refine .ofBijective (Submodule.mapQ _ _ (LinearMap.restrict
    (Algebra.lsmul R _ _ (I'.divMod I J')) ?_) ?_) ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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 = spanSingleton R⁰ (I'.divMod I J') * J
refine_1 :
  ∀ x ∈ (↑I : Submodule R K),
    Membership.mem (α := K) (↑I' : Submodule R K)
      ((((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J') : Module.End R K) : (a : K) → K) x : K)
refine_2 :
  Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K) ≤
    Submodule.comap (σ₁₂ := RingHom.id R)
      (LinearMap.restrict ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J')) ⋯)
      (Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K))
refine_3 :
  Injective.{u_2 + 1, u_2 + 1} (α :=
    ↥(↑I : Submodule R K) ⧸ Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)) (β :=
    ↥(↑I' : Submodule R K) ⧸ Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K))
    (⇑((Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)).mapQ
          (Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K))
          (LinearMap.restrict ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J')) ⋯) ⋯) :
      (a : ↥(↑I : Submodule R K) ⧸ Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)) →
        ↥(↑I' : Submodule R K) ⧸ Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K))
⊢ (↥(↑I : Submodule R K) ⧸ Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)) ≃ₗ[R]
    ↥(↑I' : Submodule R K) ⧸ Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K)
have refine_4 : Surjective.{u_2 + 1, u_2 + 1} (α :=
  ↥(↑I : Submodule R K) ⧸ Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)) (β :=
  ↥(↑I' : Submodule R K) ⧸ Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K))
  (⇑((Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)).mapQ
        (Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K))
        (LinearMap.restrict ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J')) sorry) sorry) :
    (a : ↥(↑I : Submodule R K) ⧸ Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)) →
      ↥(↑I' : Submodule R K) ⧸ Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K))
Tactic: refine .ofBijective (Submodule.mapQ _ _ (LinearMap.restrict
    (Algebra.lsmul R _ _ (I'.divMod I J')) ?_) ?_) ⟨?_, ?_⟩