m n : ℕ
hn : 1 < n !
h : n ! = m !
⊢ n = m
m n : ℕ
hn : 1 < n !
⊢ n ! = m ! ↔ n = m
refine' ⟨fun h => _, congr_arg _⟩
case inl
m n : ℕ
hn : 1 < n !
h : n ! = m !
hnm : n < m
⊢ n = m

case inr.inl
n : ℕ
hn : 1 < n !
h : n ! = n !
⊢ n = n

case inr.inr
m n : ℕ
hn : 1 < n !
h : n ! = m !
hnm : m < n
⊢ n = m
m n : ℕ
hn : 1 < n !
h : n ! = m !
⊢ n = m
obtain hnm | rfl | hnm := lt_trichotomy n m
case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m < n
⊢ n = m
case inr.inr
m n : ℕ
hn : 1 < n !
h : n ! = m !
hnm : m < n
⊢ n = m
rw [h, one_lt_factorial] at hn
case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m ! < m !
⊢ n = m
case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m < n
⊢ n = m
rw [← factorial_lt (lt_trans one_pos hn), h] at hnm
no goals
case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m ! < m !
⊢ n = m
cases lt_irrefl _ hnm
case inl
m n : ℕ
hn : 1 < n !
h : n ! = m !
hnm : m ! < m !
⊢ n = m
case inl
m n : ℕ
hn : 1 < n !
h : n ! = m !
hnm : n < m
⊢ n = m
rw [← factorial_lt <| pos_of_gt <| one_lt_factorial.mp hn, h] at hnm
no goals
case inl
m n : ℕ
hn : 1 < n !
h : n ! = m !
hnm : m ! < m !
⊢ n = m
cases lt_irrefl _ hnm
no goals
case inr.inl
n : ℕ
hn : 1 < n !
h : n ! = n !
⊢ n = n
rfl