case pos
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : multiplicity.Finite a b
⊢ multiplicity (span {a}) (span {b}) = multiplicity a b

case neg
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : ¬multiplicity.Finite a b
⊢ multiplicity (span {a}) (span {b}) = multiplicity a b
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
⊢ multiplicity (span {a}) (span {b}) = multiplicity a b
by_cases h : Finite a b
case pos
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : multiplicity.Finite a b
⊢ multiplicity (span {a}) (span {b}) = ↑(Part.get (multiplicity a b) (_ : (multiplicity a b).Dom))
case pos
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : multiplicity.Finite a b
⊢ multiplicity (span {a}) (span {b}) = multiplicity a b
rw [← PartENat.natCast_get (finite_iff_dom.mp h)]
case pos.refine_1
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : multiplicity.Finite a b
⊢ a ^ Part.get (multiplicity a b) h ∣ b

case pos.refine_2
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : multiplicity.Finite a b
⊢ ¬a ^ (Part.get (multiplicity a b) h + 1) ∣ b
case pos
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : multiplicity.Finite a b
⊢ multiplicity (span {a}) (span {b}) = ↑(Part.get (multiplicity a b) (_ : (multiplicity a b).Dom))
refine (multiplicity.unique
  (show Ideal.span {a} ^ (multiplicity a b).get h ∣ Ideal.span {b} from ?_) ?_).symm <;>
  rw [Ideal.span_singleton_pow, span_singleton_dvd_span_singleton_iff_dvd]
case pos.refine_2
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : multiplicity.Finite a b
⊢ ¬a ^ (Part.get (multiplicity a b) h + 1) ∣ b
case pos.refine_1
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : multiplicity.Finite a b
⊢ a ^ Part.get (multiplicity a b) h ∣ b

case pos.refine_2
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : multiplicity.Finite a b
⊢ ¬a ^ (Part.get (multiplicity a b) h + 1) ∣ b
exact pow_multiplicity_dvd h
no goals
case pos.refine_2
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : multiplicity.Finite a b
⊢ ¬a ^ (Part.get (multiplicity a b) h + 1) ∣ b
exact multiplicity.is_greatest
  ((PartENat.lt_coe_iff _ _).mpr (Exists.intro (finite_iff_dom.mp h) (Nat.lt_succ_self _)))
case neg
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : ¬multiplicity.Finite a b
⊢ ¬multiplicity.Finite (span {a}) (span {b})
case neg
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : ¬multiplicity.Finite a b
⊢ multiplicity (span {a}) (span {b}) = multiplicity a b
suffices ¬Finite (Ideal.span ({a} : Set R)) (Ideal.span ({b} : Set R)) by
  rw [finite_iff_dom, PartENat.not_dom_iff_eq_top] at h this
  rw [h, this]
no goals
case neg
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : ¬multiplicity.Finite a b
⊢ ¬multiplicity.Finite (span {a}) (span {b})
exact not_finite_iff_forall.mpr fun n => by
  rw [Ideal.span_singleton_pow, span_singleton_dvd_span_singleton_iff_dvd]
  exact not_finite_iff_forall.mp h n
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h✝ : ¬multiplicity.Finite a b
h : multiplicity a b = ⊤
this✝ : ¬multiplicity.Finite (span {a}) (span {b})
this : multiplicity (span {a}) (span {b}) = ⊤
⊢ multiplicity (span {a}) (span {b}) = multiplicity a b
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : ¬multiplicity.Finite a b
this : ¬multiplicity.Finite (span {a}) (span {b})
⊢ multiplicity (span {a}) (span {b}) = multiplicity a b
rw [finite_iff_dom, PartENat.not_dom_iff_eq_top] at h this
no goals
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h✝ : ¬multiplicity.Finite a b
h : multiplicity a b = ⊤
this✝ : ¬multiplicity.Finite (span {a}) (span {b})
this : multiplicity (span {a}) (span {b}) = ⊤
⊢ multiplicity (span {a}) (span {b}) = multiplicity a b
rw [h, this]
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : ¬multiplicity.Finite a b
n : ℕ
⊢ a ^ n ∣ b
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : ¬multiplicity.Finite a b
n : ℕ
⊢ span {a} ^ n ∣ span {b}
rw [Ideal.span_singleton_pow, span_singleton_dvd_span_singleton_iff_dvd]
no goals
R : Type u_1
A : Type ?u.1353425
K : Type ?u.1353428
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : R
h : ¬multiplicity.Finite a b
n : ℕ
⊢ a ^ n ∣ b
exact not_finite_iff_forall.mp h n