case mp
m n : ℕ
a✝ : n ! = 1
⊢ n ≤ 1

case mpr
m n : ℕ
a✝ : n ≤ 1
⊢ n ! = 1
m n : ℕ
⊢ n ! = 1 ↔ n ≤ 1
apply Iff.intro <;> intro
case mp
m n : ℕ
a✝ : n ! = 1
⊢ ¬1 < 1
case mp
m n : ℕ
a✝ : n ! = 1
⊢ n ≤ 1
rw [← not_lt, ← one_lt_factorial, ‹n ! = 1›]
no goals
case mp
m n : ℕ
a✝ : n ! = 1
⊢ ¬1 < 1
apply lt_irrefl
case mpr.refl
m : ℕ
⊢ 1! = 1

case mpr.step
m n : ℕ
a✝ : Nat.le n 0
⊢ n ! = 1
case mpr
m n : ℕ
a✝ : n ≤ 1
⊢ n ! = 1
cases ‹n ≤ 1›
no goals
case mpr.refl
m : ℕ
⊢ 1! = 1
rfl
case mpr.step.refl
m : ℕ
⊢ 0! = 1
case mpr.step
m n : ℕ
a✝ : Nat.le n 0
⊢ n ! = 1
cases ‹n ≤ 0›
no goals
case mpr.step.refl
m : ℕ
⊢ 0! = 1
rfl