-- Mathlib/Data/Nat/Factors.lean
theorem replicate_subperm_primeFactorsList_iff {a b n : ℕ} (ha : Prime a) (hb : b ≠ 0) :
    replicate n a <+~ primeFactorsList b ↔ a ^ n ∣ b

Proof state:
case succ.mp.intro.intro
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
⊢ a ^ (n + 1) ∣ b

Tactic:
rw [← Nat.prod_primeFactorsList hb, ← hu1.prod_eq, ← prod_replicate]

Result:
case succ.mp.intro.intro
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
⊢ (replicate (n + 1) a).prod ∣ u.prod

Proof state:
case zero
a : ℕ
ha : Prime a
b : ℕ
hb : b ≠ 0
⊢ replicate 0 a <+~ b.primeFactorsList ↔ a ^ 0 ∣ b

Tactic:
simp

Result:
no goals

Proof state:
case succ.mpr.intro
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList

Tactic:
rw [pow_succ', mul_assoc, replicate_succ,
  (Nat.perm_primeFactorsList_mul hb.1 hb.2).subperm_left, primeFactorsList_prime ha,
  singleton_append, subperm_cons, ih hb.2]

Result:
case succ.mpr.intro
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ a ^ n ∣ a ^ n * c

Proof state:
case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ (∃ l, l ~ b.primeFactorsList ∧ replicate (n + 1) a <+ l) → a ^ (n + 1) ∣ b

Tactic:
rintro ⟨u, hu1, hu2⟩

Result:
case succ.mp.intro.intro
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
⊢ a ^ (n + 1) ∣ b

Proof state:
case succ.mpr.intro
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : a ^ (n + 1) * c ≠ 0
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList

Tactic:
rw [Ne, pow_succ', mul_assoc, mul_eq_zero, _root_.not_or] at hb

Result:
case succ.mpr.intro
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList

Proof state:
case succ.mp.intro.intro
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
⊢ (replicate (n + 1) a).prod ∣ u.prod

Tactic:
exact hu2.prod_dvd_prod

Result:
no goals

Proof state:
case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b → replicate (n + 1) a <+~ b.primeFactorsList

Tactic:
rintro ⟨c, rfl⟩

Result:
case succ.mpr.intro
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : a ^ (n + 1) * c ≠ 0
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList

Proof state:
case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ replicate (n + 1) a <+~ b.primeFactorsList → a ^ (n + 1) ∣ b

Tactic:
rw [List.subperm_iff]

Result:
case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ (∃ l, l ~ b.primeFactorsList ∧ replicate (n + 1) a <+ l) → a ^ (n + 1) ∣ b

Proof state:
case succ.mpr.intro
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ a ^ n ∣ a ^ n * c

Tactic:
exact dvd_mul_right _ _

Result:
no goals

Proof state:
case succ
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ replicate (n + 1) a <+~ b.primeFactorsList ↔ a ^ (n + 1) ∣ b

Tactic:
constructor

Result:
case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ replicate (n + 1) a <+~ b.primeFactorsList → a ^ (n + 1) ∣ b

case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b → replicate (n + 1) a <+~ b.primeFactorsList