Theorem: coprime_add_self_pow (Flt/Primes.lean)

State before:
R : Type u_1
inst✝ : CommRing R
x y z : R
n : ℕ
hn : 0 < n
hsoln : x ^ n + y ^ n = z ^ n
hxx : IsCoprime x y
⊢ IsCoprime x z
Tactic:
have := IsCoprime.mul_add_left_right (hxx.pow (n := n) (m := n)) 1
State after:
R : Type u_1
inst✝ : CommRing R
x y z : R
n : ℕ
hn : 0 < n
hsoln : x ^ n + y ^ n = z ^ n
hxx : IsCoprime x y
this : IsCoprime (x ^ n) (x ^ n * 1 + y ^ n)
⊢ IsCoprime x z

State before:
R : Type u_1
inst✝ : CommRing R
x y z : R
n : ℕ
hn : 0 < n
hsoln : x ^ n + y ^ n = z ^ n
hxx : IsCoprime x y
this : IsCoprime (x ^ n) (x ^ n * 1 + y ^ n)
⊢ IsCoprime x z
Tactic:
rwa [mul_one, hsoln, IsCoprime.pow_iff hn hn] at this
State after:
no goals