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

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑n !
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 !
m : ℕ
hmn : m ≤ n
⊢ ↑m ! ∣ ↑n !

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑n !
m : ℕ
hmn : m ≤ n
⊢ ↑m ! ∣ ↑n !
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 !
m : ℕ
hmn : m ≤ n
⊢ m ! ∣ n !

State before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑n !
m : ℕ
hmn : m ≤ n
⊢ m ! ∣ n !
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 !
m : ℕ
hmn : m ≤ n
⊢ m ≤ n

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