fix: remove references to Nat.pow outside of tactic code (#9008)

leanprover-community · Dec 12, 2023 · 416fba9 · 416fba9
1 parent a6c8a98
commit 416fba9
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 3 deletions.
diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean
@@ -630,7 +630,7 @@ theorem prod_primeFactors_dvd (n : ℕ) : ∏ p in n.primeFactors, p ∣ n := by
 theorem factorization_gcd {a b : ℕ} (ha_pos : a ≠ 0) (hb_pos : b ≠ 0) :
     (gcd a b).factorization = a.factorization ⊓ b.factorization := by
   let dfac := a.factorization ⊓ b.factorization
-  let d := dfac.prod Nat.pow
+  let d := dfac.prod (· ^ ·)
   have dfac_prime : ∀ p : ℕ, p ∈ dfac.support → Prime p := by
     intro p hp
     have : p ∈ a.factors ∧ p ∈ b.factors := by simpa using hp

diff --git a/Mathlib/NumberTheory/Divisors.lean b/Mathlib/NumberTheory/Divisors.lean
@@ -445,9 +445,8 @@ theorem mem_properDivisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) {x : ℕ
     simp [h_left, le_of_lt]
 #align nat.mem_proper_divisors_prime_pow Nat.mem_properDivisors_prime_pow
 
--- Porting note: Specified pow to Nat.pow
 theorem properDivisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) :
-    properDivisors (p ^ k) = (Finset.range k).map ⟨Nat.pow p, pow_right_injective pp.two_le⟩ := by
+    properDivisors (p ^ k) = (Finset.range k).map ⟨HPow.hPow p, pow_right_injective pp.two_le⟩ := by
   ext a
   simp only [mem_properDivisors, Nat.isUnit_iff, mem_map, mem_range, Function.Embedding.coeFn_mk,
     pow_eq]