Theorem: factorial_isUnit (DividedPowers/ForMathlib/AlgebraLemmas.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
⊢ IsUnit ↑m !
Tactic:
apply isUnit_of_dvd_unit _ hn_fac
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
⊢ ↑m ! ∣ ↑(n - 1)!

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
⊢ ↑m ! ∣ ↑(n - 1)!
Tactic:
apply Nat.cast_dvd_cast
State after:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
⊢ m ! ∣ (n - 1)!

State before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
⊢ m ! ∣ (n - 1)!
Tactic:
apply Nat.factorial_dvd_factorial
State after:
case h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
⊢ m ≤ n - 1

State before:
case h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
⊢ m ≤ n - 1
Tactic:
exact Nat.le_sub_one_of_lt hmn
State after:
no goals