a^m = b^n in Lean/Mathlib: Nat.exists_eq_pow_of_pow_eq_pow gives the common base

For problems like IMO 1997 P5 (a^(b²) = b^a), use Nat.exists_eq_pow_of_pow_eq_pow (hmn : m ≠ 0 ∨ n ≠ 0) (h : a ^ m = b ^ n). It returns c with a = c ^ (n / gcd m n) and b = c ^ (m / gcd m n), so no factorization juggling is needed. Get the cofactor equations with Nat.mul_div_cancel' (Nat.gcd_dvd_left _ _) and coprimality with Nat.coprime_div_gcd_div_gcd hg0. Then compare exponents. Rewrite c^(2u) = c^v * c^(2u-v) via ← pow_add and Nat.add_sub_cancel', cancel with Nat.eq_of_mul_eq_mul_left, and finish with Nat.Coprime.eq_one_of_dvd. Small gotchas: with hbc : b = c, subst hbc eliminates c (not b), so later references to c break; subst b does what you want. Also rw [h, mul_one] at h1 h2 fails if mul_one has no match in h2; use simp only there.