case h₁
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n : ℕ
⊢ P 0

case h₂
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n : ℕ
⊢ ∀ (x : ℕ), IsUnit x → P x

case h₃
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n : ℕ
⊢ ∀ (a p : ℕ), a ≠ 0 → Prime p → P a → P (p * a)
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n : ℕ
⊢ P n
apply UniqueFactorizationMonoid.induction_on_prime
no goals
case h₁
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n : ℕ
⊢ P 0
exact h₀
case h₂
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h✝ : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n✝ n : ℕ
h : IsUnit n
⊢ P n
case h₂
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n : ℕ
⊢ ∀ (x : ℕ), IsUnit x → P x
intro n h
case h₂
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h✝ : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n✝ n : ℕ
h : IsUnit n
⊢ P 1
case h₂
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h✝ : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n✝ n : ℕ
h : IsUnit n
⊢ P n
rw [Nat.isUnit_iff.1 h]
no goals
case h₂
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h✝ : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n✝ n : ℕ
h : IsUnit n
⊢ P 1
exact h₁
case h₃
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n a p : ℕ
a✝ : a ≠ 0
hp : Prime p
ha : P a
⊢ P (p * a)
case h₃
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n : ℕ
⊢ ∀ (a p : ℕ), a ≠ 0 → Prime p → P a → P (p * a)
intro a p _ hp ha
no goals
case h₃
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n a p : ℕ
a✝ : a ≠ 0
hp : Prime p
ha : P a
⊢ P (p * a)
exact h p a hp.nat_prime ha