awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
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)
⊢ (↑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 [← this, inf_comm, coe_inf]

Premises used: FractionalIdeal.coe_inf, inf_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 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)

Tactic:
inf_le_inf ?_ le_rfl

Premises used: le_rfl, inf_le_inf, Set.Mem
-- 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 : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
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)
⊢ 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:
refine inf_le_inf ?_ le_rfl

Premises used: le_rfl, inf_le_inf
-- 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 : (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
neg : x ∈ (↑(spanSingleton R⁰ (I'.divMod I J')⁻¹ * J') : Submodule R K)
⊢ x ∈ (↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J') : Submodule R K)

Tactic:
rw [spanSingleton_inv]

Premises used: FractionalIdeal.spanSingleton_inv
-- 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 : (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
⊢ 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) ∈
    spanSingleton R⁰ (I'.divMod I J')⁻¹ * J'

Tactic:
mul_mem_mul (mem_spanSingleton_self _ _) hx

Premises used: FractionalIdeal.mem_spanSingleton_self, FractionalIdeal.mul_mem_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
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
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)
⊢ x ∈ (↑(spanSingleton R⁰ (I'.divMod I J')⁻¹ * J') : Submodule R K)

Tactic:
convert! mul_mem_mul (mem_spanSingleton_self _ _) hx

Premises used: FractionalIdeal.mem_spanSingleton_self, FractionalIdeal.mul_mem_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
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 =
    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:
simp [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
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
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)
⊢ 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:
ext x
-- 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 = spanSingleton R⁰ (I'.divMod I J') * J
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:
simp [Submodule.mem_span_singleton_mul]

Premises used: Submodule.mem_span_singleton_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
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)

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]
-- 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_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)
refine_4₁ : (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K) ≤ (↑I' : Submodule R K)
refine_4₂ : (↑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))

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]

Premises used: Iff.mpr, Submodule.map_comap_eq, Submodule.map_top, Submodule.map_le_map_iff_of_injective, Submodule.map_sup, LinearMap.range_comp, LinearMap.restrict, LinearMap.range_eq_top, Submodule.injective_subtype, Submodule.mapQ, FractionalIdeal.coeToSubmodule, sup_comm, top_le_iff, LinearMap.range_domRestrict, Submodule.ker_mkQ, Submodule.mkQ_surjective, Submodule.map_le_iff_le_comap, inf_eq_right, LinearMap.range_codRestrict, Submodule.range_subtype, Submodule.range_liftQ, Submodule.comap_map_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
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)
⊢ (↑(J' + spanSingleton R⁰ (I'.divMod I J') * I) : Submodule R K) ≤
    (↑J' : Submodule R K) ⊔ (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K)

Tactic:
simp
-- 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_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)
⊢ (↑I' : Submodule R K) ≤
    (↑J' : Submodule R K) ⊔ (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K)

Tactic:
exact le_trans (divMod_spec h' hJ' hI).ge (by simp)

Premises used: Eq.ge, FractionalIdeal.divMod_spec, le_trans
-- 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_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)
⊢ (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K) ≤
    (↑(J' + spanSingleton R⁰ (I'.divMod I J') * I) : Submodule R K)

Tactic:
simp
-- 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_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)
⊢ (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K) ≤ (↑I' : Submodule R K)

Tactic:
exact le_trans (by simp) (divMod_spec h' hJ' hI).le

Premises used: Eq.le, FractionalIdeal.divMod_spec, le_trans
-- 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_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)
⊢ (↑J' : Submodule R K) ≤ (↑I' : Submodule R K)

Tactic:
h'

Premises used: Set.Mem
-- 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_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)
⊢ (↑J' : Submodule R K) ≤ (↑I' : Submodule R K)

Tactic:
exact h'
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : Algebra S R
inst_4 : Algebra.IsIntegral S R
inst_5 : IsDomain S
inst_6 : Module.IsTorsionFree S R
p : Ideal S
inst_7 : p.IsMaximal
hp : p ≠ 0
⊢ Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0

Tactic:
have h : map (algebraMap S R) p ≠ 0 := map_ne_bot_of_ne_bot hp
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : Algebra S R
inst_4 : Algebra.IsIntegral S R
inst_5 : IsDomain S
inst_6 : Module.IsTorsionFree S R
p : Ideal S
inst_7 : p.IsMaximal
hp : p ≠ 0
h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0
rw :
  Eq (α := Ideal R) (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
    (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
⊢ Eq (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)

Tactic:
rw [← finprod_heightOneSpectrum_factorization (I := p.map (algebraMap S R)) h]

Premises used: Ideal.finprod_heightOneSpectrum_factorization
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : Algebra S R
inst_4 : Algebra.IsIntegral S R
inst_5 : IsDomain S
inst_6 : Module.IsTorsionFree S R
p : Ideal S
inst_7 : p.IsMaximal
hp : p ≠ 0
h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0
hF : Fintype (↑{v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p} : Type u_1) :=
  ⋯.fintype (s := {v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p})
rw :
  Eq.{u_1 + 1} (α := Ideal R)
    (∏ i : (↑{v : HeightOneSpectrum R | v.asIdeal ∣ map (algebraMap S R) p} : Type u_1),
      (↑i : HeightOneSpectrum R).maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
    (∏ i : (↑(p.primesOver R) : Type u_1), (↑i : Ideal R) ^ p.ramificationIdx (↑i : Ideal R))
h₁ :
  (mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing (map (F := S →+* R) (algebraMap S R) p)) ⊆
    (↑(toFinset {v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p}) :
      Set (HeightOneSpectrum R))
⊢ Eq (α := Ideal R) (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
    (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)

Tactic:
rw [finprod_eq_finsetProd_of_mulSupport_subset
    (s := {v | v.asIdeal ∣ p.map (algebraMap S R)}.toFinset), ← Finset.prod_set_coe,
    ← Finset.prod_set_coe]

Premises used: Finset.prod_set_coe, finprod_eq_finsetProd_of_mulSupport_subset
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : Algebra S R
inst_4 : Algebra.IsIntegral S R
inst_5 : IsDomain S
inst_6 : Module.IsTorsionFree S R
p : Ideal S
inst_7 : p.IsMaximal
hp : p ≠ 0
h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0
hF : Fintype (↑{v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p} : Type u_1) :=
  ⋯.fintype (s := {v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p})
x : Fintype { v : HeightOneSpectrum R // v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p } := hF
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (∏ i : (↑{v : HeightOneSpectrum R | v.asIdeal ∣ map (algebraMap S R) p} : Type u_1),
      (↑i : HeightOneSpectrum R).maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
    (∏ i : (↑(p.primesOver R) : Type u_1), (↑i : Ideal R) ^ p.ramificationIdx (↑i : Ideal R))

Tactic:
Fintype.prod_equiv (equivPrimesOver _ hp) _ _ fun ⟨v, _⟩ ↦ ?_

Premises used: Fintype.prod_equiv, Algebra.algebraMap, _private.0.Ideal.map_algebraMap_eq_finsetProd_pow.match_1, Set.Mem, setOf, Ideal.map, HPow.hPow, IsDedekindDomain.HeightOneSpectrum.equivPrimesOver, Subtype.val, IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Eq, DFunLike.coe, Ideal.ramificationIdx
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : Algebra S R
inst_4 : Algebra.IsIntegral S R
inst_5 : IsDomain S
inst_6 : Module.IsTorsionFree S R
p : Ideal S
inst_7 : p.IsMaximal
hp : p ≠ 0
h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0
hF : Fintype (↑{v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p} : Type u_1) :=
  ⋯.fintype (s := {v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p})
x : Fintype { v : HeightOneSpectrum R // v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p } := hF
refine :
  ∀ (x : { v : HeightOneSpectrum R // v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p }) (v : HeightOneSpectrum R)
    (property : v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p),
    (↑(Subtype.mk (p := fun (v : HeightOneSpectrum R) ↦ v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p) v property) :
            HeightOneSpectrum R).maxPowDividing
        (map (F := S →+* R) (algebraMap S R) p) =
      HPow.hPow (α := Ideal R)
        (↑((equivPrimesOver R hp :
                (a : { v : HeightOneSpectrum R // v.asIdeal ∣ map (algebraMap S R) p }) →
                  (↑(p.primesOver R) : Type u_1))
              (Subtype.mk (p := fun (v : HeightOneSpectrum R) ↦ v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p) v
                property)) :
          Ideal R)
        (ramificationIdx.{u_3, u_1} (S := R) p
          (↑((equivPrimesOver R hp :
                  (a : { v : HeightOneSpectrum R // v.asIdeal ∣ map (algebraMap S R) p }) →
                    (↑(p.primesOver R) : Type u_1))
                (Subtype.mk (p := fun (v : HeightOneSpectrum R) ↦ v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p) v
                  property)) :
            Ideal R))
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (∏ i : (↑{v : HeightOneSpectrum R | v.asIdeal ∣ map (algebraMap S R) p} : Type u_1),
      (↑i : HeightOneSpectrum R).maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
    (∏ i : (↑(p.primesOver R) : Type u_1), (↑i : Ideal R) ^ p.ramificationIdx (↑i : Ideal R))

Tactic:
refine Fintype.prod_equiv (equivPrimesOver _ hp) _ _ fun ⟨v, _⟩ ↦ ?_

Premises used: Fintype.prod_equiv, IsDedekindDomain.HeightOneSpectrum.equivPrimesOver