case mp
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b → ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b

case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b) → a = b
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b ↔ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
constructor
case mp
a : ℕ
ha hb : a ≠ 0
⊢ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p a
case mp
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b → ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
rintro rfl
no goals
case mp
a : ℕ
ha hb : a ≠ 0
⊢ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p a
simp
case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
⊢ a = b
case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b) → a = b
intro h
case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
⊢ ↑(factorization a) p = ↑(factorization b) p
case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
⊢ a = b
refine' eq_of_factorization_eq ha hb fun p => _
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : Prime p
⊢ ↑(factorization a) p = ↑(factorization b) p

case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : ¬Prime p
⊢ ↑(factorization a) p = ↑(factorization b) p
case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
⊢ ↑(factorization a) p = ↑(factorization b) p
by_cases pp : p.Prime
no goals
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : Prime p
⊢ ↑(factorization a) p = ↑(factorization b) p
simp [factorization_def, pp, h p pp]
no goals
case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : ¬Prime p
⊢ ↑(factorization a) p = ↑(factorization b) p
simp [factorization_eq_zero_of_non_prime, pp]