no goals
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
⊢ ∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a
classical
  let n := (normalizedFactors a₀).count (normalize x)
  obtain ⟨a, ha1, ha2⟩ :=
    @exists_eq_pow_mul_and_not_dvd R _ _ x a₀ (ne_top_iff_finite.mp (PartENat.ne_top_iff.mpr _))
  simp_rw [← (multiplicity_eq_count_normalizedFactors hx h).symm] at ha1
  use n
  use a
  use ha2
  rw [ha1]
  congr
  use n
  exact multiplicity_eq_count_normalizedFactors hx h
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
⊢ ∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
⊢ ∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a
let n := (normalizedFactors a₀).count (normalize x)
case intro.intro
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
a : R
ha1 : a₀ = x ^ Part.get (multiplicity x a₀) (_ : multiplicity.Finite x a₀) * a
ha2 : ¬x ∣ a
⊢ ∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
⊢ ∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a
obtain ⟨a, ha1, ha2⟩ :=
  @exists_eq_pow_mul_and_not_dvd R _ _ x a₀ (ne_top_iff_finite.mp (PartENat.ne_top_iff.mpr _))
case intro.intro
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
a : R
ha2 : ¬x ∣ a
ha1 :
  a₀ =
    x ^
        Part.get ↑(count (↑normalize x) (normalizedFactors a₀))
          (_ : (↑(count (↑normalize x) (normalizedFactors a₀))).Dom) *
      a
⊢ ∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a
case intro.intro
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
a : R
ha1 : a₀ = x ^ Part.get (multiplicity x a₀) (_ : multiplicity.Finite x a₀) * a
ha2 : ¬x ∣ a
⊢ ∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a
simp_rw [← (multiplicity_eq_count_normalizedFactors hx h).symm] at ha1
case intro.intro
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
a : R
ha2 : ¬x ∣ a
ha1 :
  a₀ =
    x ^
        Part.get ↑(count (↑normalize x) (normalizedFactors a₀))
          (_ : (↑(count (↑normalize x) (normalizedFactors a₀))).Dom) *
      a
⊢ ∃ a, ¬x ∣ a ∧ a₀ = x ^ n * a
case intro.intro
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
a : R
ha2 : ¬x ∣ a
ha1 :
  a₀ =
    x ^
        Part.get ↑(count (↑normalize x) (normalizedFactors a₀))
          (_ : (↑(count (↑normalize x) (normalizedFactors a₀))).Dom) *
      a
⊢ ∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a
use n
case intro.intro
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
a : R
ha2 : ¬x ∣ a
ha1 :
  a₀ =
    x ^
        Part.get ↑(count (↑normalize x) (normalizedFactors a₀))
          (_ : (↑(count (↑normalize x) (normalizedFactors a₀))).Dom) *
      a
⊢ ¬x ∣ a ∧ a₀ = x ^ n * a
case intro.intro
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
a : R
ha2 : ¬x ∣ a
ha1 :
  a₀ =
    x ^
        Part.get ↑(count (↑normalize x) (normalizedFactors a₀))
          (_ : (↑(count (↑normalize x) (normalizedFactors a₀))).Dom) *
      a
⊢ ∃ a, ¬x ∣ a ∧ a₀ = x ^ n * a
use a
case intro.intro
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
a : R
ha2 : ¬x ∣ a
ha1 :
  a₀ =
    x ^
        Part.get ↑(count (↑normalize x) (normalizedFactors a₀))
          (_ : (↑(count (↑normalize x) (normalizedFactors a₀))).Dom) *
      a
⊢ a₀ = x ^ n * a
case intro.intro
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
a : R
ha2 : ¬x ∣ a
ha1 :
  a₀ =
    x ^
        Part.get ↑(count (↑normalize x) (normalizedFactors a₀))
          (_ : (↑(count (↑normalize x) (normalizedFactors a₀))).Dom) *
      a
⊢ ¬x ∣ a ∧ a₀ = x ^ n * a
use ha2
case intro.intro
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
a : R
ha2 : ¬x ∣ a
ha1 :
  a₀ =
    x ^
        Part.get ↑(count (↑normalize x) (normalizedFactors a₀))
          (_ : (↑(count (↑normalize x) (normalizedFactors a₀))).Dom) *
      a
⊢ x ^
        Part.get ↑(count (↑normalize x) (normalizedFactors a₀))
          (_ : (↑(count (↑normalize x) (normalizedFactors a₀))).Dom) *
      a =
    x ^ n * a

α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
⊢ ∃ n, multiplicity x a₀ = ↑n
case intro.intro
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
a : R
ha2 : ¬x ∣ a
ha1 :
  a₀ =
    x ^
        Part.get ↑(count (↑normalize x) (normalizedFactors a₀))
          (_ : (↑(count (↑normalize x) (normalizedFactors a₀))).Dom) *
      a
⊢ a₀ = x ^ n * a
rw [ha1]
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
⊢ ∃ n, multiplicity x a₀ = ↑n
case intro.intro
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
a : R
ha2 : ¬x ∣ a
ha1 :
  a₀ =
    x ^
        Part.get ↑(count (↑normalize x) (normalizedFactors a₀))
          (_ : (↑(count (↑normalize x) (normalizedFactors a₀))).Dom) *
      a
⊢ x ^
        Part.get ↑(count (↑normalize x) (normalizedFactors a₀))
          (_ : (↑(count (↑normalize x) (normalizedFactors a₀))).Dom) *
      a =
    x ^ n * a

α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
⊢ ∃ n, multiplicity x a₀ = ↑n
congr
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
⊢ multiplicity x a₀ = ↑n
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
⊢ ∃ n, multiplicity x a₀ = ↑n
use n
no goals
α : Type ?u.1300334
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : Nontrivial R
inst✝ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
a₀ x : R
h : a₀ ≠ 0
hx : Irreducible x
n : ℕ := count (↑normalize x) (normalizedFactors a₀)
⊢ multiplicity x a₀ = ↑n
exact multiplicity_eq_count_normalizedFactors hx h