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 : 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))
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')) ⋯) ⋯) :
      (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)

Tactic:
refine .ofBijective (Submodule.mapQ _ _ (LinearMap.restrict
    (Algebra.lsmul R _ _ (I'.divMod I J')) ?_) ?_) ⟨?_, ?_⟩
-- 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
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)

Tactic:
(divMod_spec h' hJ' hI).le ?_

Premises used: Set.Mem, Eq.le, FractionalIdeal.divMod_spec
-- 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
hx : x ∈ (↑I : Submodule R K)
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)
⊢ 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 (divMod_spec h' hJ' hI).le ?_

Premises used: Eq.le, FractionalIdeal.divMod_spec
-- 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
hx : x ∈ (↑I : Submodule R K)
⊢ 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:
Submodule.mem_sup_right (mul_mem_mul (mem_spanSingleton_self _ _) hx)

Premises used: Set.Mem, setOf, FractionalIdeal.mem_spanSingleton_self, FractionalIdeal.mul_mem_mul, Submodule.mem_sup_right
-- 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
hx : x ∈ (↑I : Submodule R K)
⊢ 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:
exact Submodule.mem_sup_right (mul_mem_mul (mem_spanSingleton_self _ _) hx)

Premises used: FractionalIdeal.mem_spanSingleton_self, FractionalIdeal.mul_mem_mul, Submodule.mem_sup_right
-- 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
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))
⊢ 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))

Tactic:
rw [← Submodule.comap_comp, LinearMap.subtype_comp_restrict, LinearMap.domRestrict,
      Submodule.comap_comp]

Premises used: LinearMap.subtype_comp_restrict, LinearMap.domRestrict, Submodule.comap_comp
-- 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.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:
Submodule.comap_mono ?_

Premises used: Submodule.comap_mono, 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 : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
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)
⊢ 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:
refine Submodule.comap_mono ?_

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

Tactic:
(Submodule.mem_inf.mp (this.ge ?_)).1

Premises used: Eq.ge, Set.Mem, setOf, Submodule.mem_inf, Set.preimage, And.left, Iff.mp
-- 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
hx : x ∈ (↑J : Submodule R K)
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)
⊢ 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

Tactic:
refine (Submodule.mem_inf.mp (this.ge ?_)).1

Premises used: Eq.ge, Submodule.mem_inf, And.left, Iff.mp
-- 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
hx : x ∈ (↑J : Submodule R K)
refine_2 : I'.divMod I J' * x ∈ spanSingleton R⁰ (I'.divMod I J') * J
⊢ 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:
simp only [Algebra.lsmul_coe, smul_eq_mul]

Premises used: smul_eq_mul, Algebra.lsmul_coe
-- 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
hx : x ∈ (↑J : Submodule R K)
⊢ I'.divMod I J' * x ∈ spanSingleton R⁰ (I'.divMod I J') * J

Tactic:
mul_mem_mul (mem_spanSingleton_self _ _) hx

Premises used: Set.Mem, 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 : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
x : K
hx : x ∈ (↑J : Submodule R K)
⊢ I'.divMod I J' * x ∈ spanSingleton R⁰ (I'.divMod I J') * J

Tactic:
exact 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 : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
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)
⊢ 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))

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]

Premises used: le_bot_iff, LinearMap.subtype_comp_restrict, Submodule.map_comap_eq, LinearMap.ker_eq_bot, LinearMap.ker_comp, LinearMap.domRestrict, Submodule.mapQ, Submodule.comap_comp, Submodule.ker_mkQ, Submodule.map_le_iff_le_comap, Submodule.range_subtype, Submodule.ker_liftQ, Submodule.comap_bot
-- 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
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)
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)
⊢ (↑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

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
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H' : I'.divMod I J' = 0
⊢ J' = I'

Tactic:
simpa [H'] using divMod_spec h' hJ' hI

Premises used: FractionalIdeal.divMod_spec
-- 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' : I'.divMod I J' = 0
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)
⊢ (↑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:
obtain rfl : J' = I' := by simpa [H'] using divMod_spec h' hJ' hI

Premises used: rfl
-- 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' = 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 = J

Tactic:
mul_left_injective₀ hJ' (H.trans (mul_comm _ _))

Premises used: mul_left_injective₀, mul_comm, Eq.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 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
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)
⊢ (↑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 : I = J := mul_left_injective₀ hJ' (H.trans (mul_comm _ _))

Premises used: mul_left_injective₀, mul_comm, rfl, Eq.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' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hJ' : J' ≠ 0
hI : I ≠ 0
h' : J' ≤ J'
H' : J'.divMod I J' = 0
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:
inf_le_left

Premises used: Set.Mem, inf_le_left
-- 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' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hJ' : J' ≠ 0
hI : I ≠ 0
h' : J' ≤ J'
H' : J'.divMod I J' = 0
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:
exact inf_le_left

Premises used: inf_le_left
-- 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' : ¬I'.divMod I J' = 0
⊢ Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (I'.divMod I J')) 0

Tactic:
simpa [spanSingleton_eq_zero_iff] using H'

Premises used: FractionalIdeal.spanSingleton_eq_zero_iff
-- 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' ⊓
      (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * (spanSingleton R⁰ (I'.divMod I J') * I) =
    J
H' : ¬I'.divMod I J' = 0
⊢ Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (I'.divMod I J')) 0

Tactic:
simpa [spanSingleton_eq_zero_iff] using H'

Premises used: FractionalIdeal.spanSingleton_eq_zero_iff
-- 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' : ¬I'.divMod I J' = 0
⊢ (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

Premises used: mul_inf₀, inv_mul_eq_iff_eq_mul₀, inv_mul_cancel_left₀
-- 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' : ¬I'.divMod I J' = 0
this₁ : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
⊢ ¬I'.divMod I J' = 0

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

Premises used: mul_inf₀, inv_mul_eq_iff_eq_mul₀, inv_mul_cancel_left₀