awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ (↑n.properDivisors : Set ℕ)
hdvd : k ∣ n
hlt : k < n
hk : k ≠ 0
neg : k.factorization ≠ n.factorization
⊢ k.factorization < n.factorization

Tactic:
apply lt_of_le_of_ne <| factorization_le_iff_dvd hk hn |>.mpr hdvd

Premises used: Iff.mpr, Nat.factorization_le_iff_dvd, lt_of_le_of_ne
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ (↑n.properDivisors : Set ℕ)
hdvd : k ∣ n
hlt : k < n
hk : k ≠ 0
⊢ k.factorization ≠ n.factorization

Tactic:
mt (Nat.eq_of_factorization_eq' hk hn) hlt.ne

Premises used: Nat.eq_of_factorization_eq', mt, LT.lt.ne
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ (↑n.properDivisors : Set ℕ)
hdvd : k ∣ n
hlt : k < n
hk : k ≠ 0
⊢ k.factorization ≠ n.factorization

Tactic:
exact mt (Nat.eq_of_factorization_eq' hk hn) hlt.ne

Premises used: Nat.eq_of_factorization_eq', mt, LT.lt.ne
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h_1 : Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
rw : Dvd.dvd (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
⊢ k ∣ n

Tactic:
rw [← h, ← prod_factorization_pow_eq_self hn]

Premises used: Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h_1 : Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
apply :
  ∀ a ∈ f.support,
    HPow.hPow (β := ℕ) a ((f : (a : ℕ) → ℕ) a : ℕ) ∣ HPow.hPow (β := ℕ) a ((n.factorization : (a : ℕ) → ℕ) a : ℕ)
⊢ Dvd.dvd (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)

Tactic:
apply prod_dvd_prod_of_subset_of_dvd <| support_mono hlt.le

Premises used: LT.lt.le, Finsupp.support_mono, Finsupp.prod_dvd_prod_of_subset_of_dvd
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h_1 : Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
⊢ ∀ a ∈ f.support,
    HPow.hPow (β := ℕ) a ((f : (a : ℕ) → ℕ) a : ℕ) ∣ HPow.hPow (β := ℕ) a ((n.factorization : (a : ℕ) → ℕ) a : ℕ)

Tactic:
fun p _ ↦ Nat.pow_dvd_pow p <| hlt.le p

Premises used: LT.lt.le, Nat.pow_dvd_pow
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h_1 : Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
⊢ ∀ a ∈ f.support,
    HPow.hPow (β := ℕ) a ((f : (a : ℕ) → ℕ) a : ℕ) ∣ HPow.hPow (β := ℕ) a ((n.factorization : (a : ℕ) → ℕ) a : ℕ)

Tactic:
exact fun p _ ↦ Nat.pow_dvd_pow p <| hlt.le p

Premises used: LT.lt.le, Nat.pow_dvd_pow
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h_1 : Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
⊢ k ∣ n

Tactic:
have : k ∣ n := by
      rw [← h, ← prod_factorization_pow_eq_self hn]
      apply prod_dvd_prod_of_subset_of_dvd <| support_mono hlt.le
      exact fun p _ ↦ Nat.pow_dvd_pow p <| hlt.le p
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h_1 : Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
this : k ∣ n
⊢ k ∈ (↑n.properDivisors : Set ℕ)

Tactic:
mem_properDivisors.mpr ⟨this, lt_of_le_of_ne (le_of_dvd (Nat.pos_of_ne_zero hn) this) ?_⟩

Premises used: Iff.mpr, Nat.pos_of_ne_zero, And.intro, Nat.mem_properDivisors, Nat.le_of_dvd, lt_of_le_of_ne
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h_1 : Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
this : k ∣ n
neg : k ≠ n
⊢ k ∈ (↑n.properDivisors : Set ℕ)

Tactic:
refine mem_properDivisors.mpr ⟨this, lt_of_le_of_ne (le_of_dvd (Nat.pos_of_ne_zero hn) this) ?_⟩

Premises used: Iff.mpr, Nat.pos_of_ne_zero, And.intro, Nat.mem_properDivisors, Nat.le_of_dvd, lt_of_le_of_ne
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h_1 : Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
this : k ∣ n
neg : k.factorization = f
⊢ k ≠ n

Tactic:
suffices k.factorization = f from (this ▸ hlt.ne <| congrArg _ ·)
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h_1 : Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
this : k ∣ n
⊢ k.factorization = f

Tactic:
h ▸ factorization_prod_pow_eq_self_of_le_factorization hlt.le

Premises used: Nat.factorization_prod_pow_eq_self_of_le_factorization, Eq.rec, LT.lt.le
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h_1 : Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
this : k ∣ n
⊢ k.factorization = f

Tactic:
exact h ▸ factorization_prod_pow_eq_self_of_le_factorization hlt.le
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
apply :
  (↑n.properDivisors : Set ℕ) =
    (↑(Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iio n.factorization)) : Set ℕ)
⊢ n.properDivisors = Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iio n.factorization)

Tactic:
apply Finset.coe_inj.mp

Premises used: Finset.coe_inj, Iff.mp
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
⊢ (↑n.properDivisors : Set ℕ) =
    (↑(Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iio n.factorization)) : Set ℕ)

Tactic:
grind [coe_properDivisors_eq_prod_pow_lt_factorization]

Premises used: Nat.coe_properDivisors_eq_prod_pow_lt_factorization
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
⊢ Function.Injective (β := ℕ) fun (x : ↥(Finset.Iio n.factorization)) ↦ (↑x : ℕ →₀ ℕ).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2

Tactic:
grind [Function.Injective, factorization_prod_pow_eq_self_of_le_factorization]

Premises used: Nat.factorization_prod_pow_eq_self_of_le_factorization, Function.Injective
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
rw :
  n.properDivisors =
    Finset.image
      (⇑{ toFun := fun (x : ↥(Finset.Iio n.factorization)) ↦ (↑x : ℕ →₀ ℕ).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2, inj' := ⋯ :
            ↥(Finset.Iio n.factorization) ↪ ℕ } :
        (a : ↥(Finset.Iio n.factorization)) → ℕ)
      (Finset.Iio n.factorization).attach
⊢ n.properDivisors =
    Finset.map
      { toFun := fun (x : ↥(Finset.Iio n.factorization)) ↦ (↑x : ℕ →₀ ℕ).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2, inj' := ⋯ :
        ↥(Finset.Iio n.factorization) ↪ ℕ }
      (Finset.Iio n.factorization).attach

Tactic:
rw [Finset.map_eq_image]

Premises used: Finset.map_eq_image
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
rw : n.properDivisors = Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iio n.factorization)
⊢ n.properDivisors =
    Finset.image
      ((fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∘
        Subtype.val (p := fun (x : ℕ →₀ ℕ) ↦ x ∈ Finset.Iio n.factorization))
      (Finset.Iio n.factorization).attach

Tactic:
rw [← Finset.image_image, Finset.attach_image_val]

Premises used: Finset.image_image, Finset.attach_image_val
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
⊢ n.properDivisors = Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iio n.factorization)

Tactic:
properDivisors_eq_image_Iio_factorization_prod_pow

Premises used: Nat.properDivisors_eq_image_Iio_factorization_prod_pow
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
⊢ n.properDivisors = Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iio n.factorization)

Tactic:
exact properDivisors_eq_image_Iio_factorization_prod_pow

Premises used: Nat.properDivisors_eq_image_Iio_factorization_prod_pow
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
letI : motive (k + 2)
⊢ motive (k + 2)

Tactic:
letI p := (k + 2).minFac
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
⊢ Prime p

Tactic:
haveI hp : Prime p := minFac_prime (succ_succ_ne_one k)
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := ((k + 2).factorization : (a : ℕ) → ℕ) p
⊢ p ^ t ∣ k + 2

Tactic:
haveI hpt : p ^ t ∣ k + 2 := ordProj_dvd _ _
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := ((k + 2).factorization : (a : ℕ) → ℕ) p
hpt : p ^ t ∣ k + 2
⊢ 0 < t

Tactic:
haveI htp : 0 < t := hp.factorization_pos_of_dvd (k + 1).succ_ne_zero (k + 2).minFac_dvd
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := ((k + 2).factorization : (a : ℕ) → ℕ) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
h : k + 2 = p ^ t * ((k + 2) / p ^ t)
convert_1 : ¬p ∣ (k + 2) / p ^ t
convert_2 : k + 2 < p ^ t * (k + 2)
⊢ motive (k + 2)

Tactic:
convert! prime_pow_mul ((k + 2) / p ^ t) p t hp _ htp (hk _ (Nat.div_lt_of_lt_mul _)) using 1

Premises used: HDiv.hDiv, Nat.div_lt_of_lt_mul, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := ((k + 2).factorization : (a : ℕ) → ℕ) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
h h₁ : k + 2 = k + 2
⊢ k + 2 = p ^ t * ((k + 2) / p ^ t)

Tactic:
rw [Nat.mul_div_cancel' hpt]

Premises used: Nat.mul_div_cancel'
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := ((k + 2).factorization : (a : ℕ) → ℕ) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
convert_1 : ¬p ^ t.succ ∣ k + 2
⊢ ¬p ∣ (k + 2) / p ^ t

Tactic:
rw [Nat.dvd_div_iff_mul_dvd hpt, ← Nat.pow_succ]

Premises used: Nat.pow_succ, Nat.dvd_div_iff_mul_dvd
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := ((k + 2).factorization : (a : ℕ) → ℕ) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ ¬p ^ t.succ ∣ k + 2

Tactic:
pow_succ_factorization_not_dvd (k + 1).succ_ne_zero hp

Premises used: Nat.pow_succ_factorization_not_dvd, Nat.succ_ne_zero, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := ((k + 2).factorization : (a : ℕ) → ℕ) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ ¬p ^ t.succ ∣ k + 2

Tactic:
exact pow_succ_factorization_not_dvd (k + 1).succ_ne_zero hp

Premises used: Nat.pow_succ_factorization_not_dvd, Nat.succ_ne_zero, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := ((k + 2).factorization : (a : ℕ) → ℕ) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ k + 2 < p ^ t * (k + 2)

Tactic:
simp [htp.ne', hp.one_lt]

Premises used: Nat.Prime.one_lt, LT.lt.ne'
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
pos : (ha1 : a = 1) → motive (p ^ n * a)
neg : (ha1 : ¬a = 1) → motive (p ^ n * a)
⊢ motive (p ^ n * a)

Tactic:
by_cases ha1 : a = 1
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : a = 1
pos : motive (p ^ n)
⊢ motive (p ^ n * a)

Tactic:
rw [ha1, mul_one]

Premises used: mul_one
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : a = 1
⊢ motive (p ^ n)

Tactic:
exact prime_pow p n hp' hn
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
neg : 1 < a
neg₁ : (p ^ n).Coprime a
⊢ motive (p ^ n * a)

Tactic:
refine coprime (p ^ n) a (hp'.one_lt.trans_le (le_self_pow hn.ne' _)) ?_ ?_
      (prime_pow _ _ hp' hn) hPa

Premises used: Nat.le_self_pow, Nat.Prime.one_lt, LT.lt.ne', HPow.hPow, LT.lt.trans_le
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
neg : ∀ (hpa : a ≤ 1), p ∣ a
⊢ 1 < a

Tactic:
contrapose! hpa
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
hpa : a ≤ 1
⊢ p ∣ a

Tactic:
simp [lt_one_iff.1 (lt_of_le_of_ne hpa ha1)]

Premises used: Nat.lt_one_iff, Iff.mp, lt_of_le_of_ne
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
⊢ (p ^ n).Coprime a

Tactic:
simpa [hn, Prime.coprime_iff_not_dvd hp']

Premises used: Nat.Prime.coprime_iff_not_dvd
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
⊢ ∀ (n : ℕ), motive n

Tactic:
recOnPrimePow zero one ?_

Premises used: Nat.recOnPrimePow
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
refine : ∀ (a p n : ℕ), Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
⊢ ∀ (n : ℕ), motive n

Tactic:
refine recOnPrimePow zero one ?_
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p : ℕ
hp : Prime p
ha : motive a
⊢ motive (HPow.hPow (β := ℕ) p 0 * a)

Tactic:
simpa using ha
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p : ℕ
hp : Prime p
ha : motive a
n : ℕ
ih : motive (p ^ n * a)
succ : motive (p * (p ^ n * a))
⊢ motive (p ^ (n + 1) * a)

Tactic:
rw [pow_succ', mul_assoc]

Premises used: Nat.pow_succ', mul_assoc
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p : ℕ
hp : Prime p
ha : motive a
n : ℕ
ih : motive (p ^ n * a)
⊢ motive (p * (p ^ n * a))

Tactic:
prime_mul _ _ hp ih
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p : ℕ
hp : Prime p
ha : motive a
n : ℕ
ih : motive (p ^ n * a)
⊢ motive (p * (p ^ n * a))

Tactic:
exact prime_mul _ _ hp ih
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p n : ℕ
hp : Prime p
ha : motive a
zero₁ : motive (HPow.hPow (β := ℕ) p 0 * a)
succ : ∀ (n : ℕ) (ih : motive (p ^ n * a)), motive (p ^ (n + 1) * a)
⊢ motive (p ^ n * a)

Tactic:
induction n with
  | zero => simpa using ha
  | succ n ih =>
    rw [pow_succ', mul_assoc]
    exact prime_mul _ _ hp ih

Premises used: Nat.pow_succ', mul_assoc, Nat.succ
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime : ∀ (p : ℕ), Prime p → motive p
composite : ∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)
n : ℕ
⊢ motive n

Tactic:
induction_on_primes zero one ?_ _

Premises used: induction_on_primes
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime : ∀ (p : ℕ), Prime p → motive p
composite : ∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)
n : ℕ
refine : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
⊢ motive n

Tactic:
refine induction_on_primes zero one ?_ _

Premises used: induction_on_primes
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime : ∀ (p : ℕ), Prime p → motive p
composite : ∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)
n p : ℕ
hp : Prime p
ha : motive 0
⊢ motive (p * 0)

Tactic:
simpa
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime : ∀ (p : ℕ), Prime p → motive p
composite : ∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)
n p : ℕ
hp : Prime p
ha : motive (HAdd.hAdd (α := ℕ) 0 1)
⊢ motive (p * HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simpa using prime _ hp
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime : ∀ (p : ℕ), Prime p → motive p
composite : ∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)
n p a : ℕ
hp : Prime p
ha : motive (a + 1 + 1)
⊢ motive (p * (a + 1 + 1))

Tactic:
composite _ hp.two_le (prime _ hp) _ a.one_lt_succ_succ ha

Premises used: Nat.one_lt_succ_succ, Nat.Prime.two_le
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime : ∀ (p : ℕ), Prime p → motive p
composite : ∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)
n p a : ℕ
hp : Prime p
ha : motive (a + 1 + 1)
⊢ motive (p * (a + 1 + 1))

Tactic:
exact composite _ hp.two_le (prime _ hp) _ a.one_lt_succ_succ ha

Premises used: Nat.one_lt_succ_succ, Nat.Prime.two_le
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
β : Type u_1
inst : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
prime_pow : ∀ (p n : ℕ), Prime p → 0 < n → p ^ n ≠ 0 → f (p ^ n) = (p ^ n).factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
zero : Ne (α := ℕ) 0 0 → f 0 = (factorization 0).prod fun (p k : ℕ) ↦ f (p ^ k)
one : Ne (α := ℕ) 1 0 → f 1 = (factorization 1).prod fun (p k : ℕ) ↦ f (p ^ k)
coprime :
  ∀ (a b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          (a ≠ 0 → f a = a.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)) →
            (b ≠ 0 → f b = b.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)) →
              a * b ≠ 0 → f (a * b) = (a * b).factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
⊢ ∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)

Tactic:
apply Nat.recOnPosPrimePosCoprime
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
β : Type u_1
inst : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ k) = (p ^ k).factorization.prod fun (p k : ℕ) ↦ f (p ^ k)

Tactic:
simp [Prime.factorization_pow hp, Finsupp.prod_single_index _, hf]

Premises used: Nat.Prime.factorization_pow, Finsupp.prod_single_index
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
β : Type u_1
inst : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ Ne (α := ℕ) 0 0 → f 0 = (factorization 0).prod fun (p k : ℕ) ↦ f (p ^ k)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
β : Type u_1
inst : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
one : Eq.{u_1 + 1} (α := β) 1 (Finsupp.prod 0 fun (p k : ℕ) ↦ f (p ^ k))
⊢ f 1 = (factorization 1).prod fun (p k : ℕ) ↦ f (p ^ k)

Tactic:
rw [factorization_one, hf]

Premises used: Nat.factorization_one
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
β : Type u_1
inst : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ Eq.{u_1 + 1} (α := β) 1 (Finsupp.prod 0 fun (p k : ℕ) ↦ f (p ^ k))

Tactic:
simp