case mp
n : ℕ
⊢ minFac n = 1 → n = 1

case mpr
n : ℕ
⊢ n = 1 → minFac n = 1
n : ℕ
⊢ minFac n = 1 ↔ n = 1
constructor
case mp
n : ℕ
h : minFac n = 1
⊢ n = 1
case mp
n : ℕ
⊢ minFac n = 1 → n = 1
intro h
case mp
n : ℕ
h : minFac n = 1
hn : ¬n = 1
⊢ False
case mp
n : ℕ
h : minFac n = 1
⊢ n = 1
by_contra hn
case mp
n : ℕ
h : minFac n = 1
hn : ¬n = 1
this : Prime (minFac n)
⊢ False
case mp
n : ℕ
h : minFac n = 1
hn : ¬n = 1
⊢ False
have := minFac_prime hn
case mp
n : ℕ
h : minFac n = 1
hn : ¬n = 1
this : Prime 1
⊢ False
case mp
n : ℕ
h : minFac n = 1
hn : ¬n = 1
this : Prime (minFac n)
⊢ False
rw [h] at this
no goals
case mp
n : ℕ
h : minFac n = 1
hn : ¬n = 1
this : Prime 1
⊢ False
exact not_prime_one this
case mpr

⊢ minFac 1 = 1
case mpr
n : ℕ
⊢ n = 1 → minFac n = 1
rintro rfl
no goals
case mpr

⊢ minFac 1 = 1
rfl