-- Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicative.lean
theorem induction_on_prime_power {P : α → Prop} (s : Finset α) (i : α → ℕ)
    (is_prime : ∀ p ∈ s, Prime p) (is_coprime : ∀ᵉ (p ∈ s) (q ∈ s), p ∣ q → p = q)
    (h1 : ∀ {x}, IsUnit x → P x) (hpr : ∀ {p} (i : ℕ), Prime p → P (p ^ i))
    (hcp : ∀ {x y}, IsRelPrime x y → P x → P y → P (x * y)) :
    P (∏ p ∈ s, p ^ i p)

Proof state:
case insert
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
i : α → ℕ
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
p : α
f' : Finset α
hpf' : p ∉ f'
ih : (∀ p ∈ f', Prime p) → (∀ p ∈ f', ∀ q ∈ f', p ∣ q → p = q) → P (∏ p ∈ f', p ^ i p)
is_prime : ∀ p_1 ∈ insert p f', Prime p_1
is_coprime : ∀ p_1 ∈ insert p f', ∀ q ∈ insert p f', p_1 ∣ q → p_1 = q
⊢ P (p ^ i p * ∏ x ∈ f', x ^ i x)

Tactic:
exact
  hcp (prime_pow_coprime_prod_of_coprime_insert i p hpf' is_prime is_coprime)
    (hpr (i p) (is_prime _ (Finset.mem_insert_self _ _)))
    (ih (fun q hq => is_prime _ (Finset.mem_insert_of_mem hq)) fun q hq q' hq' =>
      is_coprime _ (Finset.mem_insert_of_mem hq) _ (Finset.mem_insert_of_mem hq'))

Result:
no goals

Proof state:
case insert
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
i : α → ℕ
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
p : α
f' : Finset α
hpf' : p ∉ f'
ih : (∀ p ∈ f', Prime p) → (∀ p ∈ f', ∀ q ∈ f', p ∣ q → p = q) → P (∏ p ∈ f', p ^ i p)
is_prime : ∀ p_1 ∈ insert p f', Prime p_1
is_coprime : ∀ p_1 ∈ insert p f', ∀ q ∈ insert p f', p_1 ∣ q → p_1 = q
⊢ P (∏ p ∈ insert p f', p ^ i p)

Tactic:
rw [Finset.prod_insert hpf']

Result:
case insert
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
i : α → ℕ
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
p : α
f' : Finset α
hpf' : p ∉ f'
ih : (∀ p ∈ f', Prime p) → (∀ p ∈ f', ∀ q ∈ f', p ∣ q → p = q) → P (∏ p ∈ f', p ^ i p)
is_prime : ∀ p_1 ∈ insert p f', Prime p_1
is_coprime : ∀ p_1 ∈ insert p f', ∀ q ∈ insert p f', p_1 ∣ q → p_1 = q
⊢ P (p ^ i p * ∏ x ∈ f', x ^ i x)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
s : Finset α
i : α → ℕ
is_prime : ∀ p ∈ s, Prime p
is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
⊢ P (∏ p ∈ s, p ^ i p)

Tactic:
induction' s using Finset.induction_on with p f' hpf' ih

Result:
case empty
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
i : α → ℕ
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
is_prime : ∀ p ∈ ∅, Prime p
is_coprime : ∀ p ∈ ∅, ∀ q ∈ ∅, p ∣ q → p = q
⊢ P (∏ p ∈ ∅, p ^ i p)

case insert
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
i : α → ℕ
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
p : α
f' : Finset α
hpf' : p ∉ f'
ih : (∀ p ∈ f', Prime p) → (∀ p ∈ f', ∀ q ∈ f', p ∣ q → p = q) → P (∏ p ∈ f', p ^ i p)
is_prime : ∀ p_1 ∈ insert p f', Prime p_1
is_coprime : ∀ p_1 ∈ insert p f', ∀ q ∈ insert p f', p_1 ∣ q → p_1 = q
⊢ P (∏ p ∈ insert p f', p ^ i p)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
s : Finset α
i : α → ℕ
is_prime : ∀ p ∈ s, Prime p
is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
⊢ P (∏ p ∈ s, p ^ i p)

Tactic:
letI := Classical.decEq α

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
s : Finset α
i : α → ℕ
is_prime : ∀ p ∈ s, Prime p
is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
⊢ P (∏ p ∈ s, p ^ i p)

Proof state:
case empty
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
i : α → ℕ
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
is_prime : ∀ p ∈ ∅, Prime p
is_coprime : ∀ p ∈ ∅, ∀ q ∈ ∅, p ∣ q → p = q
⊢ P (∏ p ∈ ∅, p ^ i p)

Tactic:
simpa using h1 isUnit_one

Result:
no goals