awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : K
hx : 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)
have refine_1 : Membership.mem (α := K) (J' + spanSingleton R⁰ (I'.divMod I J') * I)
  ((((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 (divMod_spec h' hJ' hI).le ?_
-- 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
⊢ 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))
have refine_2 : Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K) ≤
  Submodule.comap (↑I : Submodule R K).subtype
    (Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
      (↑J' : Submodule R K))
Tactic: rw [← Submodule.comap_comp, LinearMap.subtype_comp_restrict, LinearMap.domRestrict,
      Submodule.comap_comp]
-- 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
⊢ Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K) ≤
    Submodule.comap (↑I : Submodule R K).subtype
      (Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
        (↑J' : Submodule R K))
have refine_2 : (↑J : Submodule R K) ≤
  Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
    (↑J' : Submodule R K)
Tactic: refine Submodule.comap_mono ?_
-- 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
x : K
hx : x ∈ (↑J : Submodule R K)
⊢ Membership.mem (γ := Submodule R K)
    (Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
      (↑J' : Submodule R K))
    x
have refine_2 : Membership.mem (α := K) (spanSingleton R⁰ (I'.divMod I J') * J)
  ((((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 (Submodule.mem_inf.mp (this.ge ?_)).1
-- 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
x : K
hx : x ∈ (↑J : Submodule R K)
⊢ Membership.mem (α := K) (spanSingleton R⁰ (I'.divMod I J') * J)
    ((((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J') : Module.End R K) : (a : K) → K) x : K)
have refine_2 : I'.divMod I J' * x ∈ spanSingleton R⁰ (I'.divMod I J') * J
Tactic: simp only [Algebra.lsmul_coe, smul_eq_mul]
-- 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
⊢ 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))
have refine_3 : (↑I : Submodule R K) ⊓
    Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
      (↑J' : Submodule R K) ≤
  (↑J : Submodule R K)
Tactic: rw [← LinearMap.ker_eq_bot, Submodule.mapQ, Submodule.ker_liftQ,
      LinearMap.ker_comp, Submodule.ker_mkQ, ← Submodule.comap_comp,
      LinearMap.subtype_comp_restrict, ← le_bot_iff, Submodule.map_le_iff_le_comap,
      Submodule.comap_bot, Submodule.ker_mkQ, LinearMap.domRestrict,
      Submodule.comap_comp, ← Submodule.map_le_iff_le_comap,
      Submodule.map_comap_eq, Submodule.range_subtype]
-- 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 (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
        (↑J' : Submodule R K) ≤
    (↑J : Submodule R K)
have pos : ∀ (H' : I'.divMod I J' = 0),
  (↑I : Submodule R K) ⊓
      Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
        (↑J' : Submodule R K) ≤
    (↑J : Submodule R K)
Tactic: by_cases H' : I'.divMod I J' = 0
-- 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
pos :
  ∀ (H' : I'.divMod I J' = 0),
    (↑I : Submodule R K) ⊓
        Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
          (↑J' : Submodule R K) ≤
      (↑J : Submodule R K)
⊢ (↑I : Submodule R K) ⊓
      Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
        (↑J' : Submodule R K) ≤
    (↑J : Submodule R K)
have neg : ∀ (H' : ¬I'.divMod I J' = 0),
  (↑I : Submodule R K) ⊓
      Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
        (↑J' : Submodule R K) ≤
    (↑J : Submodule R K)
Tactic: by_cases H' : I'.divMod I J' = 0
-- 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
H' : I'.divMod I J' = 0
⊢ (↑I : Submodule R K) ⊓
      Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
        (↑J' : Submodule R K) ≤
    (↑J : Submodule R K)
have pos : ∀ (H : I * J' = J' * J) (h' : J' ≤ J')
  (this : J' ⊓ spanSingleton R⁰ (J'.divMod I J') * I = spanSingleton R⁰ (J'.divMod I J') * J) (H' : J'.divMod I J' = 0),
  (↑I : Submodule R K) ⊓
      Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (J'.divMod I J'))
        (↑J' : Submodule R K) ≤
    (↑J : Submodule R K)
Tactic: obtain rfl : J' = I' := by simpa [H'] using divMod_spec h' hJ' hI
Cleared hypotheses: I', H, h', this, 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 J' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
h : J ≤ I
hJ' : J' ≠ 0
hI : I ≠ 0
H : I * J' = J' * J
h' : J' ≤ J'
this : J' ⊓ spanSingleton R⁰ (J'.divMod I J') * I = spanSingleton R⁰ (J'.divMod I J') * J
H' : J'.divMod I J' = 0
⊢ (↑I : Submodule R K) ⊓
      Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (J'.divMod I J'))
        (↑J' : Submodule R K) ≤
    (↑J : Submodule R K)
have pos : ∀ (h : I ≤ I) (H : I * J' = J' * I)
  (this : J' ⊓ spanSingleton R⁰ (J'.divMod I J') * I = spanSingleton R⁰ (J'.divMod I J') * I),
  (↑I : Submodule R K) ⊓
      Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (J'.divMod I J'))
        (↑J' : Submodule R K) ≤
    (↑I : Submodule R K)
Tactic: obtain rfl : I = J := mul_left_injective₀ hJ' (H.trans (mul_comm _ _))
Cleared hypotheses: J, h, H, 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
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H' : ¬I'.divMod I J' = 0
⊢ (↑I : Submodule R K) ⊓
      Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
        (↑J' : Submodule R K) ≤
    (↑J : Submodule R K)
have this₁ : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
Tactic: rw [← inv_mul_eq_iff_eq_mul₀ (by simpa [spanSingleton_eq_zero_iff] using H'), mul_inf₀
      (zero_le _), inv_mul_cancel_left₀ (by simpa [spanSingleton_eq_zero_iff] using H')] at this
Cleared hypotheses: this, 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 : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
⊢ (↑I : Submodule R K) ⊓
      Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
        (↑J' : Submodule R K) ≤
    (↑J : Submodule R K)
have neg : Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
      (↑J' : Submodule R K) ⊓
    (↑I : Submodule R K) ≤
  (↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J') : Submodule R K) ⊓ (↑I : Submodule R K)
Tactic: rw [← this, inf_comm, coe_inf]
-- 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 : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
⊢ Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
        (↑J' : Submodule R K) ⊓
      (↑I : Submodule R K) ≤
    (↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J') : Submodule R K) ⊓ (↑I : Submodule R K)
have neg : Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
    (↑J' : Submodule R K) ≤
  (↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J') : Submodule R K)
Tactic: refine inf_le_inf ?_ le_rfl
-- 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 : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
x : K
hx :
  Membership.mem (γ := Submodule R K)
    (Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
      (↑J' : Submodule R K))
    x
⊢ x ∈ (↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J') : Submodule R K)
have neg : x ∈ (↑(spanSingleton R⁰ (I'.divMod I J')⁻¹ * J') : Submodule R K)
Tactic: rw [spanSingleton_inv]
-- 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 : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
x : K
hx :
  Membership.mem (γ := Submodule R K)
    (Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
      (↑J' : Submodule R K))
    x
⊢ x ∈ (↑(spanSingleton R⁰ (I'.divMod I J')⁻¹ * J') : Submodule R K)
have h₁ : x =
  HMul.hMul (β := K) (I'.divMod I J')⁻¹
    ((((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: convert! mul_mem_mul (mem_spanSingleton_self _ _) hx
-- 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
⊢ Submodule.map (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
      (↑I : Submodule R K) =
    (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K)
have h₁ : ∀ (x : K),
  Membership.mem (γ := Submodule R K)
      (Submodule.map (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
        (↑I : Submodule R K))
      x ↔
    x ∈ (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K)
Tactic: ext x
-- 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
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ 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')) ⋯) ⋯) :
      (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))
have H₁ : Submodule.map (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
    (↑I : Submodule R K) =
  (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K)
Tactic: have H : Submodule.map (Algebra.lsmul R R K (I'.divMod I J')) ↑I =
        (spanSingleton R⁰ (I'.divMod I J') * I) := by
      ext x
      simp [Submodule.mem_span_singleton_mul]
-- 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_1 : 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
H :
  Submodule.map (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
      (↑I : Submodule R K) =
    (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K)
⊢ 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')) ⋯) ⋯) :
      (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))
have refine_4 : (↑I' : Submodule R K) ≤
  (↑J' : Submodule R K) ⊔ (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K)
Tactic: rw [← LinearMap.range_eq_top, Submodule.mapQ, Submodule.range_liftQ,
      LinearMap.range_comp, LinearMap.restrict, LinearMap.range_codRestrict,
      LinearMap.range_domRestrict, ← top_le_iff, H,
      ← LinearMap.range_eq_top.mpr (Submodule.mkQ_surjective _),
      ← Submodule.map_top, Submodule.map_le_iff_le_comap, Submodule.comap_map_eq, Submodule.ker_mkQ,
      ← Submodule.map_le_map_iff_of_injective I'.coeToSubmodule.injective_subtype,
      Submodule.map_top, Submodule.map_sup,
      Submodule.map_comap_eq, Submodule.map_comap_eq, Submodule.range_subtype, sup_comm,
      inf_eq_right.mpr, inf_eq_right.mpr]
-- 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_1 : 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
H :
  Submodule.map (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
      (↑I : Submodule R K) =
    (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K)
refine_4 :
  (↑I' : Submodule R K) ≤
    (↑J' : Submodule R K) ⊔ (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K)
⊢ 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')) ⋯) ⋯) :
      (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))
have refine_4₁ : (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K) ≤ (↑I' : Submodule R K)
Tactic: rw [← LinearMap.range_eq_top, Submodule.mapQ, Submodule.range_liftQ,
      LinearMap.range_comp, LinearMap.restrict, LinearMap.range_codRestrict,
      LinearMap.range_domRestrict, ← top_le_iff, H,
      ← LinearMap.range_eq_top.mpr (Submodule.mkQ_surjective _),
      ← Submodule.map_top, Submodule.map_le_iff_le_comap, Submodule.comap_map_eq, Submodule.ker_mkQ,
      ← Submodule.map_le_map_iff_of_injective I'.coeToSubmodule.injective_subtype,
      Submodule.map_top, Submodule.map_sup,
      Submodule.map_comap_eq, Submodule.map_comap_eq, Submodule.range_subtype, sup_comm,
      inf_eq_right.mpr, inf_eq_right.mpr]