awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Function.onFun Coprime
    (fun (p : ↥n.primeFactors) ↦ HPow.hPow (β := ℕ) (↑p : ℕ) ((n.factorization : (a : ℕ) → ℕ) (↑p : ℕ) : ℕ)) p1 p2

Tactic:
Nat.Coprime.pow (n.factorization p1) (n.factorization p2) ?_

Premises used: Nat.Coprime.pow, Subtype.val, DFunLike.coe, Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
refine : (↑p1 : ℕ).Coprime (↑p2 : ℕ)
⊢ Function.onFun Coprime
    (fun (p : ↥n.primeFactors) ↦ HPow.hPow (β := ℕ) (↑p : ℕ) ((n.factorization : (a : ℕ) → ℕ) (↑p : ℕ) : ℕ)) p1 p2

Tactic:
refine Nat.Coprime.pow (n.factorization p1) (n.factorization p2) ?_

Premises used: Nat.Coprime.pow, Subtype.val, DFunLike.coe, Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ (↑p1 : ℕ).Coprime (↑p2 : ℕ)

Tactic:
(Nat.coprime_primes ?_ ?_).mpr <| Subtype.coe_ne_coe.mpr hp

Premises used: Iff.mpr, Subtype.coe_ne_coe, Nat.coprime_primes
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
refine_1 : Prime (↑p1 : ℕ)
refine_2 : Prime (↑p2 : ℕ)
⊢ (↑p1 : ℕ).Coprime (↑p2 : ℕ)

Tactic:
refine (Nat.coprime_primes ?_ ?_).mpr <| Subtype.coe_ne_coe.mpr hp

Premises used: Iff.mpr, Subtype.coe_ne_coe, Nat.coprime_primes
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Prime (↑p1 : ℕ)

Tactic:
Nat.prime_of_mem_primeFactors p1.2

Premises used: Nat.prime_of_mem_primeFactors, Subtype.property
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Prime (↑p1 : ℕ)

Tactic:
exact Nat.prime_of_mem_primeFactors p1.2

Premises used: Nat.prime_of_mem_primeFactors, Subtype.property
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Prime (↑p2 : ℕ)

Tactic:
Nat.prime_of_mem_primeFactors p2.2

Premises used: Nat.prime_of_mem_primeFactors, Subtype.property
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Prime (↑p2 : ℕ)

Tactic:
exact Nat.prime_of_mem_primeFactors p2.2

Premises used: Nat.prime_of_mem_primeFactors, Subtype.property
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p : ℕ
⊢ #({e ∈ Finset.range 0 | p ∣ e + 1}) = 0 / p

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p n : ℕ
hn : #({e ∈ Finset.range n | p ∣ e + 1}) = n / p
⊢ #({e ∈ Finset.range (n + 1) | p ∣ e + 1}) = (n + 1) / p

Tactic:
simp [Nat.succ_div, add_ite, add_zero, Finset.range_add_one, filter_insert, apply_ite card,
      card_insert_of_notMem, hn]

Premises used: apply_ite, Finset.range_add_one, Finset.card_insert_of_notMem, add_ite, Nat.succ_div, Finset.filter_insert, Finset.card, add_zero
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
zero : #({e ∈ Finset.range 0 | p ∣ e + 1}) = 0 / p
succ :
  ∀ (n : ℕ) (hn : #({e ∈ Finset.range n | p ∣ e + 1}) = n / p), #({e ∈ Finset.range (n + 1) | p ∣ e + 1}) = (n + 1) / p
⊢ #({e ∈ Finset.range n | p ∣ e + 1}) = n / p

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    simp [Nat.succ_div, add_ite, add_zero, Finset.range_add_one, filter_insert, apply_ite card,
      card_insert_of_notMem, hn]

Premises used: apply_ite, Finset.range_add_one, Finset.card_insert_of_notMem, add_ite, Nat.succ_div, Finset.filter_insert, Finset.card, Nat.zero, add_zero, Nat.succ
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
zero : card (α := ℕ) ({x ∈ Ioc 0 0 | p ∣ x}) = 0 / p
succ : ∀ (n : ℕ), #({x ∈ Ioc 0 n | p ∣ x}) = n / p → #({x ∈ Ioc 0 (n + 1) | p ∣ x}) = (n + 1) / p
⊢ #({x ∈ Ioc 0 n | p ∣ x}) = n / p

Tactic:
induction n
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p : ℕ
⊢ card (α := ℕ) ({x ∈ Ioc 0 0 | p ∣ x}) = 0 / p

Tactic:
simp [Nat.succ_div, add_ite, ← insert_Ioc_right_eq_Ioc_add_one, filter_insert,
    apply_ite card, *]

Premises used: Finset.insert_Ioc_right_eq_Ioc_add_one, apply_ite, add_ite, Nat.succ_div, Finset.filter_insert, Finset.card
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p n : ℕ
h : #({x ∈ Ioc 0 n | p ∣ x}) = n / p
⊢ #({x ∈ Ioc 0 (n + 1) | p ∣ x}) = (n + 1) / p

Tactic:
simp [Nat.succ_div, add_ite, ← insert_Ioc_right_eq_Ioc_add_one, filter_insert,
    apply_ite card, *]

Premises used: Finset.insert_Ioc_right_eq_Ioc_add_one, apply_ite, add_ite, Nat.succ_div, Finset.filter_insert, Finset.card
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
⊢ #({k ∈ Finset.range (succ 0) | k ≠ 0 ∧ n ∣ k}) = 0 / n

Tactic:
simp [Finset.filter_false_of_mem]

Premises used: Finset.filter_false_of_mem
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
succ :
  #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n
⊢ #({k ∈ Finset.range (N + 1).succ | k ≠ 0 ∧ n ∣ k}) = (N + 1) / n

Tactic:
rw [Finset.range_add_one, Finset.filter_insert]

Premises used: Finset.range_add_one, Finset.filter_insert
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
pos :
  ∀ (h : n ∣ N.succ),
    #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
        else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
      (N + 1) / n
neg :
  ∀ (h : ¬n ∣ N.succ),
    #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
        else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
      (N + 1) / n
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n

Tactic:
by_cases h : n ∣ N.succ

Premises used: Nat.succ
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
h : n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n

Tactic:
simp [h, succ_div_of_dvd, ih]

Premises used: Nat.succ_div_of_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
h : ¬n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n

Tactic:
simp [h, succ_div_of_not_dvd, ih]

Premises used: Nat.succ_div_of_not_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
N n : ℕ
zero : #({k ∈ Finset.range (Nat.succ 0) | k ≠ 0 ∧ n ∣ k}) = 0 / n
succ :
  ∀ (N : ℕ) (ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n),
    #({k ∈ Finset.range (N + 1).succ | k ≠ 0 ∧ n ∣ k}) = (N + 1) / n
⊢ #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n

Tactic:
induction N with
  | zero => simp [Finset.filter_false_of_mem]
  | succ N ih =>
    rw [Finset.range_add_one, Finset.filter_insert]
    by_cases h : n ∣ N.succ
    · simp [h, succ_div_of_dvd, ih]
    · simp [h, succ_div_of_not_dvd, ih]

Premises used: Finset.filter_false_of_mem, Finset.range_add_one, Finset.filter_insert, Nat.succ_div_of_not_dvd, Nat.succ_div_of_dvd, Nat.zero, Nat.succ
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
pos : ∀ (ha0 : a = 0), ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
neg : ∀ (ha0 : ¬a = 0), ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m

Tactic:
by_cases ha0 : a = 0
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : a = 0
⊢ b ^ n = a ^ m

Tactic:
symm at h
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : a = 0
h₁ : b ^ n = a ^ m
⊢ a = 0

Tactic:
symm at h
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
pos : ∀ (hm0 : m = 0), ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
neg : ∀ (hm0 : ¬m = 0), ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m

Tactic:
by_cases hm0 : m = 0
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
hm0 : m = 0
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
hm0 : ¬m = 0
h₁ : a = HPow.hPow (α := ℕ) 0 n ∧ b = HPow.hPow (α := ℕ) 0 m
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m

Tactic:
use 0
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
hm0 : ¬m = 0
⊢ a = HPow.hPow (α := ℕ) 0 n ∧ b = HPow.hPow (α := ℕ) 0 m

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
pos : ∀ (hn0 : n = 0), ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
neg : ∀ (hn0 : ¬n = 0), ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m

Tactic:
by_cases hn0 : n = 0
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : n = 0
h₁ : a = b ^ n ∧ b = b ^ m
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m

Tactic:
use b
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : n = 0
⊢ a = b ^ n ∧ b = b ^ m

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
⊢ let c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2;
  c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2

Tactic:
set c := factors.prod (· ^ ·) with hc

Premises used: HPow.hPow, Finsupp.prod
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
h₁ : a = c ^ n ∧ b = c ^ m
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m

Tactic:
use c
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
ha : a = c ^ n
⊢ a = c ^ n ∧ b = c ^ m

Tactic:
⟨ha, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
ha : a = c ^ n
refine : b = c ^ m
⊢ a = c ^ n ∧ b = c ^ m

Tactic:
refine ⟨ha, ?_⟩
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
ha : a = c ^ n
a₁ : Eq (α := ℕ) ((fun (a : ℕ) ↦ a ^ n) b) ((fun (a : ℕ) ↦ a ^ n) (c ^ m))
⊢ b = c ^ m

Tactic:
apply Nat.pow_left_injective hn0

Premises used: Nat.pow_left_injective
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
ha : a = c ^ n
⊢ Eq (α := ℕ) ((fun (a : ℕ) ↦ a ^ n) b) ((fun (a : ℕ) ↦ a ^ n) (c ^ m))

Tactic:
simp [← h, ha, Nat.pow_right_comm]

Premises used: Nat.pow_right_comm
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
h₁ : a = c ^ n
⊢ a = c ^ n ∧ b = c ^ m

Tactic:
suffices ha : a = c ^ n by
    refine ⟨ha, ?_⟩
    apply Nat.pow_left_injective hn0
    simp [← h, ha, Nat.pow_right_comm]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
⊢ c ^ n ≠ 0

Tactic:
simp [c, factors]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
h₁ : ∀ (p : ℕ), Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (((c ^ n).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ a = c ^ n

Tactic:
apply eq_of_factorization_eq ha0 (by simp [c, factors])

Premises used: Nat.eq_of_factorization_eq
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
p : ℕ
⊢ ∀ (p : ℕ) (hp : p ∈ factors.support), Prime p

Tactic:
have foo (p) (hp : p ∈ factors.support) : Prime p :=
    prime_of_mem_primeFactors (Finsupp.support_mapRange hp)
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
p : ℕ
foo : ∀ (p : ℕ) (hp : p ∈ factors.support), Prime p
h₁ : Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((n • factors : (a : ℕ) → ℕ) p : ℕ)
⊢ Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (((c ^ n).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [factorization_pow, hc, prod_pow_factorization_eq_self foo]

Premises used: Nat.prod_pow_factorization_eq_self, Nat.factorization_pow
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
p : ℕ
foo : ∀ (p : ℕ) (hp : p ∈ factors.support), Prime p
this : n ∣ (a.factorization : (a : ℕ) → ℕ) p
⊢ Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((n • factors : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp [factors, Nat.mul_div_cancel' this]

Premises used: Nat.mul_div_cancel'
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
p : ℕ
foo : ∀ (p : ℕ) (hp : p ∈ factors.support), Prime p
h₁ : n ∣ (a.factorization : (a : ℕ) → ℕ) p
⊢ Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((n • factors : (a : ℕ) → ℕ) p : ℕ)

Tactic:
suffices n ∣ a.factorization p by
    simp [factors, Nat.mul_div_cancel' this]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
p : ℕ
foo : ∀ (p : ℕ) (hp : p ∈ factors.support), Prime p
⊢ n ∣ (a.factorization : (a : ℕ) → ℕ) p

Tactic:
hmn.symm.dvd_of_dvd_mul_left ⟨b.factorization p, ?_⟩

Premises used: Nat.Coprime.symm, Exists.intro, Nat.Coprime.dvd_of_dvd_mul_left, DFunLike.coe, Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
p : ℕ
foo : ∀ (p : ℕ) (hp : p ∈ factors.support), Prime p
h₁ :
  HMul.hMul (β := ℕ) m ((a.factorization : (a : ℕ) → ℕ) p : ℕ) =
    HMul.hMul (β := ℕ) n ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ n ∣ (a.factorization : (a : ℕ) → ℕ) p

Tactic:
refine hmn.symm.dvd_of_dvd_mul_left ⟨b.factorization p, ?_⟩

Premises used: Nat.Coprime.symm, Exists.intro, Nat.Coprime.dvd_of_dvd_mul_left, DFunLike.coe, Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
p : ℕ
foo : ∀ (p : ℕ) (hp : p ∈ factors.support), Prime p
⊢ HMul.hMul (β := ℕ) m ((a.factorization : (a : ℕ) → ℕ) p : ℕ) =
    HMul.hMul (β := ℕ) n ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simpa using congr(factorization $h p)
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
set :
  let g := m.gcd n;
  ∃ (c : ℕ), a = c ^ (n / g) ∧ b = c ^ (m / g)
⊢ ∃ (c : ℕ), a = c ^ (n / m.gcd n) ∧ b = c ^ (m / m.gcd n)

Tactic:
set g := gcd m n

Premises used: Nat.gcd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
inl : ∀ (hm : m ≠ 0), m'.Coprime n'
inr : ∀ (hn : n ≠ 0), m'.Coprime n'
⊢ m'.Coprime n'

Tactic:
rcases hmn with hm | hn
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
hm : m ≠ 0
⊢ m'.Coprime n'

Tactic:
gcd_div_gcd_div_gcd_of_pos_left (zero_lt_of_ne_zero hm)

Premises used: Nat.zero_lt_of_ne_zero, Nat.gcd_div_gcd_div_gcd_of_pos_left
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
hm : m ≠ 0
⊢ m'.Coprime n'

Tactic:
exact gcd_div_gcd_div_gcd_of_pos_left (zero_lt_of_ne_zero hm)

Premises used: Nat.zero_lt_of_ne_zero, Nat.gcd_div_gcd_div_gcd_of_pos_left
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
hn : n ≠ 0
⊢ m'.Coprime n'

Tactic:
gcd_div_gcd_div_gcd_of_pos_right (zero_lt_of_ne_zero hn)

Premises used: Nat.zero_lt_of_ne_zero, Nat.gcd_div_gcd_div_gcd_of_pos_right
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
hn : n ≠ 0
⊢ m'.Coprime n'

Tactic:
exact gcd_div_gcd_div_gcd_of_pos_right (zero_lt_of_ne_zero hn)

Premises used: Nat.zero_lt_of_ne_zero, Nat.gcd_div_gcd_div_gcd_of_pos_right
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
⊢ m'.Coprime n'

Tactic:
have coprime : m'.Coprime n' := by
    rcases hmn with hm | hn
    · exact gcd_div_gcd_div_gcd_of_pos_left (zero_lt_of_ne_zero hm)
    · exact gcd_div_gcd_div_gcd_of_pos_right (zero_lt_of_ne_zero hn)
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
rw : a ^ (m' * g)
| a ^ m

Tactic:
rw [show m = m' * g from (Nat.div_mul_cancel (gcd_dvd_left m n)).symm]

Premises used: Nat.gcd_dvd_left, Nat.div_mul_cancel, Eq.symm
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
conv_lhs :
  ∀ (h : a ^ (m' * g) = b ^ n),
    let n' := n / m.gcd n;
    ∀ (coprime : m'.Coprime n'), a ^ m' = b ^ n'
⊢ a ^ m' = b ^ n'

Tactic:
conv_lhs at h => rw [show m = m' * g from (Nat.div_mul_cancel (gcd_dvd_left m n)).symm]

Premises used: Nat.gcd_dvd_left, Nat.div_mul_cancel, Eq.symm
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
h : a ^ (m' * g) = b ^ n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
rw : b ^ (n' * g)
| b ^ n

Tactic:
rw [show n = n' * g from (Nat.div_mul_cancel (gcd_dvd_right m n)).symm]

Premises used: Nat.div_mul_cancel, Nat.gcd_dvd_right, Eq.symm
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
h : a ^ (m' * g) = b ^ n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
⊢ a ^ (m' * g) = b ^ (n' * g)

Tactic:
conv_rhs at h => rw [show n = n' * g from (Nat.div_mul_cancel (gcd_dvd_right m n)).symm]

Premises used: Nat.div_mul_cancel, Nat.gcd_dvd_right, Eq.symm
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
h : a ^ (m' * g) = b ^ n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
h₁ : a ^ (m' * g) = b ^ (n' * g)
⊢ m'.Coprime n'

Tactic:
conv_rhs at h => rw [show n = n' * g from (Nat.div_mul_cancel (gcd_dvd_right m n)).symm]

Premises used: Nat.div_mul_cancel, Nat.gcd_dvd_right, Eq.symm
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : a ^ (m' * g) = b ^ (n' * g)
coprime : m'.Coprime n'
⊢ (a ^ m') ^ g = (b ^ n') ^ g

Tactic:
rw [pow_mul, pow_mul] at h

Premises used: pow_mul
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : a ^ (m' * g) = b ^ (n' * g)
coprime : m'.Coprime n'
h₁ : (a ^ m') ^ g = (b ^ n') ^ g
⊢ m'.Coprime n'

Tactic:
rw [pow_mul, pow_mul] at h

Premises used: pow_mul
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : (a ^ m') ^ g = (b ^ n') ^ g
coprime : m'.Coprime n'
inl : ∀ (hm : m ≠ 0), g ≠ 0
inr : ∀ (hn : n ≠ 0), g ≠ 0
⊢ g ≠ 0

Tactic:
rcases hmn with hm | hn
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : (a ^ m') ^ g = (b ^ n') ^ g
coprime : m'.Coprime n'
hm : m ≠ 0
⊢ g ≠ 0

Tactic:
gcd_ne_zero_left hm

Premises used: Nat.gcd_ne_zero_left
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : (a ^ m') ^ g = (b ^ n') ^ g
coprime : m'.Coprime n'
hm : m ≠ 0
⊢ g ≠ 0

Tactic:
exact gcd_ne_zero_left hm

Premises used: Nat.gcd_ne_zero_left
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : (a ^ m') ^ g = (b ^ n') ^ g
coprime : m'.Coprime n'
hn : n ≠ 0
⊢ g ≠ 0

Tactic:
gcd_ne_zero_right hn

Premises used: Nat.gcd_ne_zero_right
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : (a ^ m') ^ g = (b ^ n') ^ g
coprime : m'.Coprime n'
hn : n ≠ 0
⊢ g ≠ 0

Tactic:
exact gcd_ne_zero_right hn

Premises used: Nat.gcd_ne_zero_right
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : (a ^ m') ^ g = (b ^ n') ^ g
coprime : m'.Coprime n'
⊢ g ≠ 0

Tactic:
have : g ≠ 0 := by
      rcases hmn with hm | hn
      · exact gcd_ne_zero_left hm
      · exact gcd_ne_zero_right hn
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : (a ^ m') ^ g = (b ^ n') ^ g
coprime : m'.Coprime n'
this : g ≠ 0
⊢ a ^ m' = b ^ n'

Tactic:
Nat.pow_left_injective this h

Premises used: Nat.pow_left_injective