α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this : DecidableEq R := Classical.decEq R
⊢ Function.Injective ((fun x x_1 => x ^ x_1) a)
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
⊢ Function.Injective ((fun x x_1 => x ^ x_1) a)
letI := Classical.decEq R
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this : DecidableEq R := Classical.decEq R
i j : ℕ
hij : (fun x x_1 => x ^ x_1) a i = (fun x x_1 => x ^ x_1) a j
⊢ i = j
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this : DecidableEq R := Classical.decEq R
⊢ Function.Injective ((fun x x_1 => x ^ x_1) a)
intro i j hij
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this✝ : DecidableEq R := Classical.decEq R
i j : ℕ
hij : (fun x x_1 => x ^ x_1) a i = (fun x x_1 => x ^ x_1) a j
this : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }
⊢ i = j
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this : DecidableEq R := Classical.decEq R
i j : ℕ
hij : (fun x x_1 => x ^ x_1) a i = (fun x x_1 => x ^ x_1) a j
⊢ i = j
letI : Nontrivial R := ⟨⟨a, 0, ha0⟩⟩
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this✝¹ : DecidableEq R := Classical.decEq R
i j : ℕ
hij : (fun x x_1 => x ^ x_1) a i = (fun x x_1 => x ^ x_1) a j
this✝ : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }
this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
⊢ i = j
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this✝ : DecidableEq R := Classical.decEq R
i j : ℕ
hij : (fun x x_1 => x ^ x_1) a i = (fun x x_1 => x ^ x_1) a j
this : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }
⊢ i = j
letI : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
case intro.intro
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this✝¹ : DecidableEq R := Classical.decEq R
i j : ℕ
hij : (fun x x_1 => x ^ x_1) a i = (fun x x_1 => x ^ x_1) a j
this✝ : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }
this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
p' : R
hp' : Irreducible p'
dvd' : p' ∣ a
⊢ i = j
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this✝¹ : DecidableEq R := Classical.decEq R
i j : ℕ
hij : (fun x x_1 => x ^ x_1) a i = (fun x x_1 => x ^ x_1) a j
this✝ : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }
this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
⊢ i = j
obtain ⟨p', hp', dvd'⟩ := WfDvdMonoid.exists_irreducible_factor ha1 ha0
case intro.intro.intro.intro
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this✝¹ : DecidableEq R := Classical.decEq R
i j : ℕ
hij : (fun x x_1 => x ^ x_1) a i = (fun x x_1 => x ^ x_1) a j
this✝ : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }
this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
p' : R
hp' : Irreducible p'
dvd' : p' ∣ a
p : R
mem : p ∈ normalizedFactors a
right✝ : p' ~ᵤ p
⊢ i = j
case intro.intro
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this✝¹ : DecidableEq R := Classical.decEq R
i j : ℕ
hij : (fun x x_1 => x ^ x_1) a i = (fun x x_1 => x ^ x_1) a j
this✝ : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }
this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
p' : R
hp' : Irreducible p'
dvd' : p' ∣ a
⊢ i = j
obtain ⟨p, mem, _⟩ := exists_mem_normalizedFactors_of_dvd ha0 hp' dvd'
case intro.intro.intro.intro
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this✝² : DecidableEq R := Classical.decEq R
i j : ℕ
hij : (fun x x_1 => x ^ x_1) a i = (fun x x_1 => x ^ x_1) a j
this✝¹ : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }
this✝ : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
p' : R
hp' : Irreducible p'
dvd' : p' ∣ a
p : R
mem : p ∈ normalizedFactors a
right✝ : p' ~ᵤ p
this :
  (fun x => Multiset.count p (normalizedFactors x)) ((fun x x_1 => x ^ x_1) a i) =
    (fun x => Multiset.count p (normalizedFactors x)) ((fun x x_1 => x ^ x_1) a j)
⊢ i = j
case intro.intro.intro.intro
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this✝¹ : DecidableEq R := Classical.decEq R
i j : ℕ
hij : (fun x x_1 => x ^ x_1) a i = (fun x x_1 => x ^ x_1) a j
this✝ : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }
this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
p' : R
hp' : Irreducible p'
dvd' : p' ∣ a
p : R
mem : p ∈ normalizedFactors a
right✝ : p' ~ᵤ p
⊢ i = j
have := congr_arg (fun x => Multiset.count p (normalizedFactors x)) hij
case intro.intro.intro.intro
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this✝² : DecidableEq R := Classical.decEq R
i j : ℕ
hij : (fun x x_1 => x ^ x_1) a i = (fun x x_1 => x ^ x_1) a j
this✝¹ : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }
this✝ : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
p' : R
hp' : Irreducible p'
dvd' : p' ∣ a
p : R
mem : p ∈ normalizedFactors a
right✝ : p' ~ᵤ p
this : i * Multiset.count p (normalizedFactors a) = j * Multiset.count p (normalizedFactors a)
⊢ i = j
case intro.intro.intro.intro
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this✝² : DecidableEq R := Classical.decEq R
i j : ℕ
hij : (fun x x_1 => x ^ x_1) a i = (fun x x_1 => x ^ x_1) a j
this✝¹ : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }
this✝ : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
p' : R
hp' : Irreducible p'
dvd' : p' ∣ a
p : R
mem : p ∈ normalizedFactors a
right✝ : p' ~ᵤ p
this :
  (fun x => Multiset.count p (normalizedFactors x)) ((fun x x_1 => x ^ x_1) a i) =
    (fun x => Multiset.count p (normalizedFactors x)) ((fun x x_1 => x ^ x_1) a j)
⊢ i = j
simp only [normalizedFactors_pow, Multiset.count_nsmul] at this
no goals
case intro.intro.intro.intro
α : Type ?u.956127
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
ha0 : a ≠ 0
ha1 : ¬IsUnit a
this✝² : DecidableEq R := Classical.decEq R
i j : ℕ
hij : (fun x x_1 => x ^ x_1) a i = (fun x x_1 => x ^ x_1) a j
this✝¹ : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }
this✝ : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
p' : R
hp' : Irreducible p'
dvd' : p' ∣ a
p : R
mem : p ∈ normalizedFactors a
right✝ : p' ~ᵤ p
this : i * Multiset.count p (normalizedFactors a) = j * Multiset.count p (normalizedFactors a)
⊢ i = j
exact mul_right_cancel₀ (Multiset.count_ne_zero.mpr mem) this