-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem emultiplicity_eq_emultiplicity_span {a b : R} :
    emultiplicity (Ideal.span {a}) (Ideal.span ({b} : Set R)) = emultiplicity a b

Proof state:
case pos.hsucc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ ¬a ^ (multiplicity a b + 1) ∣ b

Tactic:
apply h.not_pow_dvd_of_multiplicity_lt

Result:
case pos.hsucc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ multiplicity a b < multiplicity a b + 1

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ a ^ n ∣ b

Tactic:
exact FiniteMultiplicity.not_iff_forall.mp h n

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : ¬FiniteMultiplicity a b
⊢ emultiplicity (span {a}) (span {b}) = emultiplicity a b

Tactic:
suffices ¬FiniteMultiplicity (Ideal.span ({a} : Set R)) (Ideal.span ({b} : Set R)) by
  rw [emultiplicity_eq_top.2 h, emultiplicity_eq_top.2 this]

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : ¬FiniteMultiplicity a b
⊢ ¬FiniteMultiplicity (span {a}) (span {b})

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ emultiplicity (span {a}) (span {b}) = emultiplicity a b

Tactic:
rw [h.emultiplicity_eq_multiplicity]

Result:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ emultiplicity (span {a}) (span {b}) = ↑(multiplicity a b)

Proof state:
case pos.hk
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ a ^ multiplicity a b ∣ b

Tactic:
exact pow_multiplicity_dvd a b

Result:
no goals

Proof state:
case pos.hsucc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ multiplicity a b < multiplicity a b + 1

Tactic:
apply lt_add_one

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : ¬FiniteMultiplicity a b
⊢ ¬FiniteMultiplicity (span {a}) (span {b})

Tactic:
exact FiniteMultiplicity.not_iff_forall.mpr fun n => by
  rw [Ideal.span_singleton_pow, span_singleton_dvd_span_singleton_iff_dvd]
  exact FiniteMultiplicity.not_iff_forall.mp h n

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : ¬FiniteMultiplicity a b
this : ¬FiniteMultiplicity (span {a}) (span {b})
⊢ emultiplicity (span {a}) (span {b}) = emultiplicity a b

Tactic:
rw [emultiplicity_eq_top.2 h, emultiplicity_eq_top.2 this]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ span {a} ^ n ∣ span {b}

Tactic:
rw [Ideal.span_singleton_pow, span_singleton_dvd_span_singleton_iff_dvd]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ a ^ n ∣ b

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
⊢ emultiplicity (span {a}) (span {b}) = emultiplicity a b

Tactic:
by_cases h : FiniteMultiplicity a b

Result:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ emultiplicity (span {a}) (span {b}) = emultiplicity a b

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : ¬FiniteMultiplicity a b
⊢ emultiplicity (span {a}) (span {b}) = emultiplicity a b

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ emultiplicity (span {a}) (span {b}) = ↑(multiplicity a b)

Tactic:
apply emultiplicity_eq_of_dvd_of_not_dvd <;>
  rw [Ideal.span_singleton_pow, span_singleton_dvd_span_singleton_iff_dvd]

Result:
case pos.hk
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ a ^ multiplicity a b ∣ b

case pos.hsucc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ ¬a ^ (multiplicity a b + 1) ∣ b